Proving the Correctness of GNAT Light Runtime Library
This is a modal window.
The media could not be loaded, either because the server or network failed or because the format is not supported.
Formal Metadata
| Title |
| |
| Title of Series | ||
| Number of Parts | 287 | |
| Author | ||
| License | CC Attribution 2.0 Belgium: You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor. | |
| Identifiers | 10.5446/57030 (DOI) | |
| Publisher | ||
| Release Date | ||
| Language |
Content Metadata
| Subject Area | ||
| Genre | ||
| Abstract |
|
FOSDEM 2022163 / 287
2
4
6
8
12
17
21
23
31
35
37
41
44
45
46
47
50
62
65
66
67
68
71
73
81
84
85
86
90
92
94
100
102
105
111
114
115
116
117
118
121
122
124
127
131
133
135
137
139
140
141
142
145
149
150
156
164
165
167
169
170
171
172
174
176
178
180
183
184
189
190
192
194
198
205
206
207
208
210
218
220
224
225
229
230
232
235
236
238
239
240
242
243
244
245
246
249
250
253
260
262
264
267
273
274
277
282
283
287
00:00
ArmComputing platformSource codeRepository (publishing)Power (physics)Scripting languageCore dumpString (computer science)Numeral (linguistics)Interface (computing)Attribute grammarPotenz <Mathematik>Point (geometry)Revision controlRun time (program lifecycle phase)Formal languageProof theoryInformation securitySoftwareImplementationDataflowMachine codeSubsetLevel (video gaming)GodRun time (program lifecycle phase)Projective planeWeightSubject indexingPoint (geometry)DataflowFormal languageExecution unitDepictionBitRevision controlConstraint (mathematics)Level (video gaming)Variety (linguistics)Computer architectureScaling (geometry)SubsetMathematical analysisSource codeProof theoryInformation securityVector spaceNumbering schemeInformationIntegerPublic key certificatePropagatorEntropiecodierungGreatest elementFormal verificationRepository (publishing)Intermediate languageCodeDifferent (Kate Ryan album)INTEGRALLatent heatComputing platformString (computer science)Computer fileDegree (graph theory)Task (computing)MereologyInterface (computing)Symbol tableKey (cryptography)Computing platformProper mapGeneric programmingWell-formed formulaSoftware testingSuite (music)Validity (statistics)Library (computing)Attribute grammarMultiplication signMedical imagingFerry CorstenException handlingMilitary baseBuildingBeat (acoustics)Group actionForm (programming)Computer programmingExplosionMachine visionWhiteboardGoodness of fitCategory of beingDirection (geometry)MiniDiscArithmetic meanObservational studyCausalityPower (physics)DiagramEngineering drawingXMLUMLComputer animation
06:27
Buffer overflowAlgorithmSoftware developerDivision (mathematics)Sheaf (mathematics)Core dumpWeb pagePoint (geometry)CompilerMaß <Mathematik>ImplementationPairwise comparisonSoftwareFrequencyException handlingComputer iconBoolean algebraQuotientGeneric programmingProof theoryProjective planeWeightCompilerSoftware testingMultiplication signIntegerResultantRun time (program lifecycle phase)ImplementationScaling (geometry)NeuroinformatikQuotientMultiplicationDifferent (Kate Ryan album)Latent heatMathematicsBuffer overflowVolume (thermodynamics)Goodness of fitCASE <Informatik>outputAlgorithmFrequencyAreaCompilerVirtual machineExecution unitFunktionalanalysisCodeDivisorConstraint (mathematics)Regular expressionCondition numberData conversionEqualiser (mathematics)Descriptive statisticsPoint (geometry)Software bugEntropiecodierungPrisoner's dilemmaProof theory2 (number)Exception handlingPhysical systemSpacetimeComputerDataflowNumbering schemeDivision (mathematics)Level (video gaming)Computer fileMereologyLocal ringWordData managementLattice (order)Game theoryMatching (graph theory)DemonGroup actionBit rateDialectDecision theoryArithmetic meanComplete metric spaceTwitterWave packetAdditionInternetworkingClosed setBitMedical imagingComputer animation
13:18
String (computer science)Semiconductor memoryPairwise comparisonAddress spacePointer (computer programming)Physical systemPoint (geometry)TrigonometryAttribute grammarLevel (video gaming)Data modelDeterminantMoment (mathematics)Multiplication signWebsiteState of matterWhiteboardIntelligent NetworkFood energyObject (grammar)Data storage deviceClosed setUsabilityPairwise comparisonData conversionReal-time operating systemNumbering schemeSemiconductor memoryAddress spaceComplex analysisLevel (video gaming)Doubling the cubeType theoryFormal languageRepresentation (politics)Floating pointGoodness of fitDynamical systemInfinityPointer (computer programming)DampingFunktionalanalysisRun time (program lifecycle phase)Physical systemTrigonometryComputer animation
15:07
Interface (computing)Function (mathematics)IterationVariable (mathematics)Core dumpLoop (music)Invariant (mathematics)Junction (traffic)String (computer science)Arithmetic meanStress (mechanics)Boolean algebraInclusion mapNetwork topologyComputer multitaskingIntrusion detection systemNatural numberCountingLogical constantMathematicsBeta functionMachine codePhysical systemPoint (geometry)Buffer overflowIntegerInterior (topology)Internet service providerSoftware developerRaw image formatMaxima and minimaProcess (computing)Division (mathematics)RoundingNumerical digitScaling (geometry)Scale (map)Divisor (algebraic geometry)Musical ensembleFrame problemControl flowMaß <Mathematik>MereologyCuboidSubsetArithmetic meanGroup actionGrand Unified TheoryBinary fileRight angle1 (number)ResultantRange (statistics)Order (biology)Condition numberParameter (computer programming)Level (video gaming)Slide ruleMultiplication signMassGreatest elementState of matterOcean currentVideo gameAdditionRegular expressionError messageEntropiecodierungExecution unitRule of inferenceGoodness of fitCASE <Informatik>GoogolString (computer science)IterationFunktionalanalysisData structurePosition operatorSubject indexingContrast (vision)Row (database)CircleLevel of measurementImplementationNumbering schemeCore dumpServer (computing)Point (geometry)BitProcedural programmingLoop (music)ProgrammschleifeGeneric programmingLemma (mathematics)Category of beingLengthBound stateDifferent (Kate Ryan album)Sign (mathematics)DivisorScaling (geometry)Proof theoryVariable (mathematics)IntegerModul <Datentyp>Invariant (mathematics)Price indexCodeInterface (computing)PreconditionerBuffer overflowComputer fileComputer animation
21:44
Control flowString (computer science)Maß <Mathematik>Boolean algebraFunction (mathematics)Core dumpPrice indexComputer multitaskingRankingBefehlsprozessorPattern languageSource codeJunction (traffic)Natural numberSign (mathematics)MoistureSoftware testingMechatronicsDiscrete element methodGamma functionFreewareData Encryption StandardCNNTexture mappingPhysical systemRight angleExponentiationPotenz <Mathematik>Modul <Datentyp>Binary fileSoftwareLemma (mathematics)Computer wormRevision controlOpen sourceComputer fileIntegerMathematical analysisMixed realityFactory (trading post)Variable (mathematics)Constraint (mathematics)Interior (topology)Parameter (computer programming)Expandierender GraphLine (geometry)Exponential functionDivisorSynchronizationProgrammable read-only memoryComputer-generated imageryReverse engineeringSystem programmingMenu (computing)Logical constantFloating pointAxiomEmailCoroutineMaxima and minimaResultantType theoryRange (statistics)CASE <Informatik>Descriptive statisticsNumbering schemeIntegerLatent heatSign (mathematics)Lemma (mathematics)Medical imagingImplementationModule (mathematics)Design by contractEntropiecodierungModulo (jargon)Potenz <Mathematik>FunktionalanalysisString (computer science)Endliche ModelltheoriePreconditionerBellman equationLetterpress printingBitExponentiationModul <Datentyp>Greatest elementProcess (computing)Loop (music)Game controllerExecution unitParameter (computer programming)Source codePattern languageWordVirtual machineCondition numberInvariant (mathematics)Position operatoroutputBoolean algebraRevision controlSystem callObject-oriented programmingCodeRun time (program lifecycle phase)Proof theoryForm (programming)Thermal expansionPhase transitionState of matterReading (process)Extension (kinesiology)Level (video gaming)Moment (mathematics)Observational studyFormal grammarData storage deviceCore dumpWave packetPattern recognitionDecision theoryOrder (biology)Subject indexingMetreSelf-organizationGroup actionConnected spaceUtility softwareMultiplication signReverse engineeringComputer animation
28:11
Boolean algebraString (computer science)Core dumpPhysical systemReverse engineeringFunction (mathematics)Computer-generated imageryPrice indexoutputMaß <Mathematik>Partial derivativeProof theoryServer (computing)CodeAdditionProjective planeGroup actionDecision theoryData storage deviceCondition numberState of matterPosition operatorExecution unitArithmetic meanRevision controlMultiplication signOpen sourceLevel (video gaming)AgreeablenessMedical imagingServer (computing)Wave packetContext awarenessSubject indexingExpected valueGoodness of fitFault-tolerant systemReading (process)Run time (program lifecycle phase)Software testingCompileroutputConstraint (mathematics)WeightCategory of beingCodeBuffer overflowDataflowProof theoryData conversionError messageFigurate numberLatent heatAddress spaceField (computer science)String (computer science)Natural numberPrice indexTotal S.A.Numbering schemeCore dumpMaxima and minimaLoop (music)ArmConfiguration spacePointer (computer programming)Computer animation
32:09
Video gameDeclarative programmingLine (geometry)Design by contractPhysical systemFunktionalanalysisLatent heatTerm (mathematics)String (computer science)CASE <Informatik>Subject indexingLevel (video gaming)Complex analysisVisualization (computer graphics)CodeBitWorkstation <Musikinstrument>Electronic mailing listSoftware maintenanceSpeciesSpacetimeHand fanForm (programming)Open setEntropiecodierungGroup actionGraph (mathematics)Order (biology)Computer animationMeeting/Interview
34:52
Term (mathematics)Medical imagingMultiplication signState of matterProof theoryTypprüfungDefault (computer science)Design by contractCombinational logicSoftware developerINTEGRALMetropolitan area networkVideo gameWordComplex analysisGroup actionComputer animationMeeting/Interview
36:19
Run time (program lifecycle phase)Design by contractPreconditionerCodeCost curveGroup actionExecution unitMultiplication signContext awarenessCondition numberCASE <Informatik>Order (biology)Meeting/Interview
37:39
Proof theoryFunktionalanalysisTerm (mathematics)Latent heatContext awarenessRun time (program lifecycle phase)Software testingPublic key certificate2 (number)Group actionDivision (mathematics)Medical imagingMeeting/Interview
38:27
Raw image formatNumbering schemeComputer animation
Transcript: English(auto-generated)
00:13
Hello, I'm going to talk about the project I've been working on for the past six months with my colleague, Claire Ross, and an intern the last summer, Pierre-Alexandre Bazin,
00:24
about proving the correctness of the Gnat light runtime library. So what is this Gnat runtime library? That's what we call previously at Edicor the zero footprint ZFP or revenge score SFP or search runtime. So now it's divided between the light runtime
00:41
and a more encompassing embedded runtime. And this light runtime is targeted at embedded platforms. So we have 77 platforms supported right now. Most of them are bare metal with a variety of chips, ARM, Leon, PowerPC, RISC-V, x86, and x86 64-bits.
01:03
And sometimes with an S on top, so like PyCOS or vectors. And the units of that runtime are ready for certification. So a subset of these have been already certified for use in various projects in Avionics, in Space, in Railway and Automotive, subject to the suitable certification documents.
01:24
So like DO-178 for Avionics, CSCSS for Space, EN-50128 for Railway, and ISO-26262 for Automotive. So you can say that the units in that runtime have been subject to a high degree of scrutiny with proper specifications put in place,
01:42
and test suites and reviews, et cetera. So you can build this runtime based on the project that you have available freely on GitHub, in VB runtimes, where it takes the sources from the GCC repository under the gnat-sources sub-director. So just to give you a tour quickly
02:01
of these units in the gnat-light runtime, if I take the x86 64-bits version, because of course for each version you have different number of units. And here it has 182 spec files. And I'm only counting the spec files here because some of them are just spec files,
02:22
but some of them are bodies, and some of them are instantiations of generics. So they have spec plus bodies, but declared just as a spec file. So between all of these 182 files, you have of course support for the ada-standard library.
02:42
So that's the a-something files, and the i-something files for interfaces. So you have here carton string handling, you have some Nurex library, you have support for assertions and exceptions, but in this runtime there's no propagation of exceptions,
03:00
it's only local, or calling the last chance handler. And there's interfaces with C. You have also a little bit of the gnat user library, so we have a few g-something files, it's mostly for IO. And you have many files that deal with the support for features of the language,
03:21
so the gnat runtime library. So you have 140 s-something files. And so here you have support for various attributes like tick image, tick value, tick width, attributes of floating point numbers. You have support for arithmetic operations, especially on fixed points and floats, and explanations including integers and some Nurex.
03:43
And support for tasking. So all of that. Now I'm going to talk about proof. So proof using the Spark tool. It's a formal verification tool doing two kinds of analysis, one called flow analysis and one called proof. And proof is the most involved, whether it asks provers about the validity
04:03
of some formulas which entail the correction of the code. And so here you can see very briefly a depiction of the architecture of the Spark tool, where it starts from the complete left inside an editor, where you can see the codes. And at the bottom you can see here some Spark codes,
04:22
say assigning a value 42 in index one of array A. And through some codes, part of it, which is shared with the compiler, what I call the GNAB here, we transform that code into a YML intermediate form.
04:41
So that's this code in the middle, which represents the assignment on the left. And which is represented by this question mark in the middle, which is the symbol of the Y3 platform. And this platform dedicated to proof of programs, then generates formulas. So you can see an example of a bit of a formula
05:00
in this SMT lib syntax on the bottom right. And these formulas are dispatched to various provers, in particular, automatic provers, like Altego, CVC4, and V3, which are all included in the Spark technology. So in Spark, we emphasize the fact that proof is not an all or nothing endeavor.
05:23
So you can start at some bottom level, which we call the stone level, where you have only the guarantees of having a better, safer subset of the language. And then you can go up the scale here with the bronze level for checking constraints
05:40
of data and information flow, and making sure that everything is initialized. A silver level is about making sure that there are no runtime errors, and particularly no CVW in the codes. At the gold level, you can start proving key integrity properties, whether it's their reality to safety or security. And at the platinum level, you can prove fully functionally the code.
06:03
And so typically, the platinum level is applied to a much smaller subset of the codes than where you can apply lower levels. And the main target usually is the silver level, so absence of endeavors. But here in this project, we're going to target this platinum level,
06:20
so fully functionally describing the behavior and proving that the code complies with this specification. So first, a little motivating example for this project. And so we're going back to 2012, when we were adding support for big integers in that. So mathematical integers inside the compiler
06:43
were motivated by a feature in Spark to allow intermediate computations without overflows. So we do them using full mathematical possibilities to ignore the possibility of overflows in some proof. And implementation was done by the late,
07:01
great developer, Robert Dewar, so a founder of EdiCorps. And he used GNU 2's algorithm in D for this multi-precision division. So you have integers in a number of machine integers. So you have array of machine integers to represent large integers.
07:20
And this algorithm is described in the art of computer programming, volume two. So he used the second edition from 1981 and this will have an importance later, that's why I'm mentioning it here. At the time, so the reviewer told him that in the code that he had written, there was a possible overflow in this large piece of code, this large expression.
07:44
But Robert, knowing that he had implemented the code from a GNU's book correctly, and assuming that the book was correct, was not convinced by this possibility of an overflow and asked for an actual issue. So the reviewer went back to the codes
08:02
and finally came up with this example. So try this long multiplication division, which corresponds to activating this expression leading to another flow. And indeed, Robert recognized that the true results was different from the computation
08:21
in the codes given back then. So what happened? Well, even the best, like Knuth and Robert Dewar can get it wrong, especially when it comes to these very low level details related to possible runtime errors, and especially when it comes to overflows.
08:41
And regarding this specific computation, in fact, the bug had been already fixed in an area of volume two in 1995. So that's this part here, this test, which needs to be done to prevent the possible overflow. But that's not the end of it. So 10 years later, this test was fixed again.
09:01
So it was not actually an equality that should be done here, but a greater or equal test. So hopefully after that, we have a correct description of the algorithm that can be implemented without overflows. So that's what we did. But obviously, algorithm gets implemented in many places,
09:20
and that was the case in that compiler. So this algorithm was used in two other units. In this unit, you impeach for arbitrary prison computation during the compilation. And in this other unit system, that's R8-64 to support fixed point arithmetic, because fixed points are represented internally
09:41
by the compiler integers with some scale. And so you need this kind of computations. But obviously, no two implementations are alike. There are different constraints in the, that are represented. And so on the one side, we fixed the computation in UNPISH. Although we couldn't find an obvious bug,
10:01
but the computation was the one that could be fixed. In a system that's R8-64, the test was done differently. And so we didn't find a bug. So we didn't apply the fix and hoped that it was okay. Now, fast forward to 2019.
10:23
Here we were, as we usually do at EdiCore, doing a runtime specification for space. And one of the external reviewers, looking at these units for fixed point support, and in particular, at algorithm D implemented in scale device,
10:43
made the remark that we should increase common frequency to better implement, good to better understand the working, in the working of the algorithm. So that led to a new internal review. And during this internal review, we detected the two possible silence of applause in another related function.
11:02
So double divide and the missing exception. So some case which should raise an exception, but here was not doing it in this scale device. So that's not good. That was not so bad in fact, because as I said, the overflows were silence. So we're doing the right thing in the end.
11:22
And the missing exception was just on incorrect inputs. Still a colleague from the specification team challenged us, the Spark team, to prove the unit. So we set on doing that. And one week of work later, we got all the algorithm except this scale device
11:44
and implementing algorithm D, which was more complex proof. So we tried to have a discussion with the specification team, but priorities took on and while everyone moved on. Until recently, so last year during a summer internship,
12:01
have a good intern, Pierre-Alexandre Bazin, updated the proof that we had done two years before, and finally proved this scale device implementation. And so now it has moved. So it's in this new file as I already do, because it's a generic implementation now for 64 and 128 bits.
12:21
So you have these big contracts at first, but which is quite readable. So you can look at the past condition of scale device. Indeed, it says that if you go to big integers, that's this conversion to big for all the values involved here. The result R is really the remnants,
12:40
the result of the remnants of the multiplication of X times Y divided by Z. And for Q, if you ignore rounding, which is just a slightly more complex case, the quotient Q is really the quotient of X time Y in mathematics divided by Z.
13:01
And the pre-condition is just to prevent an overflow during this competition. So great. That was proved, we were very happy to learn that finally our implementation that had been certified was indeed probably correct. So we say, well, let's go from there
13:21
and prove everything. But the runtime is not exactly in Spark. There are a lot of uses of untyped memory for many good reasons to handle the cigarette stack, for array comparisons for things that are not necessarily even aligned, for also ports to get to the tags of objects,
13:43
dynamic types, for biding to C-strings. So many reasons to using Ada addresses, so type address, and doing unchecked conversions between address and pointer types. And this is something that is not at all supported by the ownership system that we have in Spark, which is fully typed.
14:03
Plus, not everything is provable in these units. There are a lot of support for low-level floating-point operations for some language attributes in Ada regarding floats. There are also low-level support for numerics, like trigonometry.
14:21
There's things that do double arithmetic for double using floats, so two floats for doing a double. So all that depends on the representation of floats, in particular, those overlays between various types. Each uses the representation of NaN,
14:41
not a number, and infinities, which are not in Spark, and it does complex floating-point reasoning. So all these things, both at the monol level for NaN and infinities and overlays, and at the level of reasoning about this floating-point computation, is not supported by provers. So we cannot expect to both specify
15:02
these functionalities in great detail and prove them automatically in Spark. So we settled for something less ambitious. Let's prove everything that fits the Spark subset and can be both expressed and proved. So let's prove all the Spark things. So first example of that is the interface to C.
15:23
So let's take the unit interfaces.c. Here, we had to express things in addition to what was in the unit, just to be able to specify some of the functionalities. So we add, for example, a ghost function, c length ghost, which adds what it means to have the length
15:42
of a C string, which ends at the null character. And then this ghost function can be used in contact, and it's self-implemented and proved. So the proof makes heavy use of advanced Spark features like loop invariance for loops to summarize the state
16:00
of the current iteration of the loop, or relaxed initialization for things that are locally uninitialized, but are progressively initialized inside the loop. But all of these uses are quite simple, and I'm going to show you. So here is this c length ghost function. And you can see that it's implemented here
16:22
with a simple loop to get to the point where you have the null character, and you have a loop invariance, and you would expect to prove in Spark when you have a loop to say that so far, no character was found to be null. And this c length function can be used then
16:42
to specify other functions like this function to eta, which takes this carry and return the string, because depending on the value of this other parameter trim null, it's going to do something different up to the null character or not.
17:01
And again, in this to eta, you will see a loop invariance for loops to summarize the work done so far. And here, something else is that when we declare a variable here without initializing it in the array, we can declare it with relaxed initialization.
17:22
And then inside the loop, we need to specify up to which index this array is initialized. And so proof is going to take care of approving initialization of this variable. If you don't, then it's done by phone indices in a much more, a closer way. And it cannot be applied here
17:41
because the array is progressively initialized. Okay, now let's move on to fixed point support. So returning to this scale divide and other functionalities. So it's implemented here in these various units,
18:01
array 32, array 64, array double, so which is the generic instantiates in array 64, for example. And here, we took the commands in the code, which were quite detailed and translated them into spot contacts. So you can see an example with this add with offload check.
18:21
So we have a function here in 64 range, which says when an argument, which is a big integer, so arbitrary integer not bounded, is within the range of assign in 64. And so this is a ghost function again, so something that's only for specification and proof.
18:42
And inside the function add with offload check, now we can add a precondition that says for this function to operate properly, it needs to take arguments, which won't overflow when you add them. So when you do this summation in big integers, then it fits in the assign integer 64.
19:03
Then the result will indeed be the result of the addition. And so let's look at that. So in the integer 64 bits spec, it's here. And the implementation here just renames the generic.
19:24
So let's look at the generic spec and implementation. So that's just what we describe in term of spec. And the implementation here uses a number of what we call lemmas. So things, procedures that are ghosts,
19:42
so only here for proof, which prove a given property, the postcondition from another property given in precondition. So that's a way to isolate a proof so that the automatic provers can do it much more easily. So this proof can be quite involved, as you can see here,
20:01
with a number of cases being described, assertions by the provers, even some lemmas. So these lemmas are, again, the same as what I just showed, except they are marginal. So I've extracted them here in a different part of the file.
20:22
And in the end, the code is not obstructed by the use of all these codes. We're just calling the lemmas where they are needed to prove the postcondition in this case. So that's a rather simple case, in fact. So now if we turn to the dreaded scale divides,
20:45
this is much more complex because here we're mixing sign integer arithmetic, unsigned, so modular integer arithmetic, and arbitrary bounded integer arithmetic with these big integers. And you can see that you have quite a big lemmas.
21:03
And these are also proved with more complex reasoning. And in the end, the implementation has to call these lemmas at the right places in the right order for the proof to go through automatically.
21:26
So we have also approved character and string handling. So for character, it's in ada characters.endling. And I've example just at the bottom of the slides. And for string, the bounded string, the fixed string, and maps, plus supporting units in that,
21:44
that implement part of these functionalities. And here, the specification comes directly from the Ada reference manual. So the description was translated into Spark contracts. An example, very simple example of that is this function is control in characters handling.
22:00
So it's specified as true if item is a control character, and the control character is defined as the character whose position is in one of the ranges, zero 31 or 127, 159. And that's exactly what you have in the post condition here. The result of this function call is whether
22:21
the position of the item argument is in these ranges. So specification can be a bit more complex for more involved functions. So for example, here in ada.strings.fixed, you can see this function index, which is going to look for a position
22:41
of a given pattern in the source string. And here, well, there are many cases described in the specification which turn into these large contract cases. So we're using a special form of contracts, which gives, depending on various cases here,
23:03
before the row, the result that is expected here. And so here, this unit is in fact, based on another implementation in another unit. And so this other implementation has a similar contacts
23:22
and each body is verified against this contact. And here it goes other variants of index, which are themselves proved against their specification. But let's move now to explanation.
23:41
So there are various implementation of explanation for sign integers, model integers, and depending on the value of the module. So for example, here you have the binary modular is the simplest. So it's specified at the top here as just well the explanation left at the exponent right.
24:05
The sign version is a bit more complex because we need to make sure that there's no overflow. So it has a precondition that uses this computation in big integers. So we're doing the explanation big integers and checking that the result fits in the range.
24:20
And even more complex case is a modular explanation with a non-binary modulus. So when the modulus is not two to the power of something, but can be 42 say. And here, the way to specify it is to say that the results here, X modular tick results,
24:40
when considered as a big integer is really the operation done here in big integer modulo the value of the modules. So we have to do that because just doing it in modular machine integers, we'll do a double modulo and we've been correct. So if we look now at the code,
25:03
so as I said, the simplest one is this modular explanation and here it's a simple loop with as you would expect, a loop invariance and a few assertions. Now, if you look at the sign version,
25:21
well, it's likely more complex. So there are a number of lemmas relating how the operation works in big integers, especially because exponential is more difficult to reason about with automatic pullers. And so the implementation also has more ghost codes to try the proof
25:41
and calls to these lemmas to help progress. And the most complex is this explanation of a module type with a non-bin binary modules, because here we have sign integers, and sign integers and explanation with big integers.
26:04
And so we have many more lemmas and we have much more effort to drive the first word and the next proof. I'd like to finish with the support for a tick image and tick value. So a tick image is a way to print values of various types
26:23
and tick values does the converse, so it takes a string and returns the value. And the goal here is to be able to show that the image and value function in runtime are a reverse function. So give a sufficiently precise post-condition for value, for the value function for type,
26:41
so that the post-condition of the corresponding image can state the value applied to the result of image of v gives back v. So that's what we do here in this image boolean, in this code snippet. So you can see here at the bottom that indeed,
27:00
when we call value boolean on the results, s string from one to p, because p and s are the result of this procedure, it gives back the input of the image boolean. And we are in the process of doing that for all of the other types. So if we look now just at this,
27:23
I wanted to show the specification that is needed for this s value, for this value for unsigned integers. So it's here. Oops. Yeah, scan and sign is one of the functions used here.
27:42
And you can see that it has quite complex post-condition because we need to describe what happens with the blank characters and what happens with sign and the various ways to specify the value. And so it depends on all these other ghost functions that describe how the base and the value pass the base
28:06
or describe and the exponents, et cetera. So that's all for this project. So the current status is that we managed to find a few mistakes and fix them,
28:22
just possible overflow and run checks. That was the good news. And a couple of that is the simple tests. So if you compile these codes, well, you will get an error, but not necessarily the one you expect. So here we are trying to get a boolean value
28:41
from the string, which just contains a blank character. So this is incorrect and what you would expect and you will get in the next version is this last line, a constraint error is raised because it's a bad input for the attributing value here. Well, if you use a flat community
29:01
with 2020 version or previous, you will get the segmentation fault, in fact, because underneath there's a level flow in the runtime support code here. And you end up reading and writing much past the string here. And this overflow happens as you would expect
29:20
because the string of one character is located with the index naturality class. So at the extreme value of possible indices here. Sanitation is slightly better with the latest version of net community 2021. Then here, instead of the segmentation fault,
29:41
you get the constraint error, but not the one you would expect. In fact, in this version of net community, the runtime was compiled with runtime checks on, but not overflows. So the overflow is silence, but then you get a runtime check figure when we're trying to access the array S beyond itself.
30:03
So you get this index check field. So what we are with that, we have a partial proof of the net lifetime library. So for 35 units, so that's not nothing, but that's far from the total number of units here. So as I said, using the X86-64 version
30:25
around 180 units. The daily proof takes one hour and 30 minutes on a quite big server. So a 63 cores Linux server. And we do all the configurations that I mentioned here.
30:41
So for ARM or X86 Linux with VEXworks or bare metal. In total, we added many specifications inside these units. So almost 400 preconditions, 500 post-conditions. The proof also requires more
31:01
than just the specifications to drive the provers towards proof. So what we call ghost code, which is not executed in the end in particular, because inside these units, we specify that ghost code should be ignored during the final compilation. So we have to add almost 150 loop invariants,
31:21
almost 400 assertions and almost 300 ghost entities. So types, variables, and many of these are actually lemmas. So 150 lemmas, that's what I showed you. Ways to approve a given property in a smaller context so that automatic provers can do it automatically.
31:42
And that leaves us with two questions for the future. Can this effort benefit the future specifications of the runtime by adding more guarantees to what we can do today with testing only? And also, what can we do beyond what Spark supports currently? Can we do something in particular
32:01
for units that use these addresses and conversion to pointers that currently are not supported? Well, thank you for your attention, and I'm waiting for your questions.
32:25
Don't you consider that having 60-plus lines of contracts for five lines of AF for- Okay, I'll continue, it seems you disconnected. So the question was, do you consider that having 60-plus lines of contract
32:40
for a declaration in data, which is initially five lines, makes the specification unreadable? And so initially, I understood this question wrong. I thought he was talking about five lines body. And indeed, there should be a relationship between the complexity of the function that you are trying to specify and the specification.
33:02
And then it depends how far you want to go in terms of specification. So here, we went for the platinum level, we wanted to fully specify functionally this function. And so the fact that the function declaration in data is five lines is a bit irrelevant. It doesn't say really the complexity of the function
33:21
that you're trying to implement. You could have underneath the wall a system that you're implementing or just a really small leaf function. And so that's where I think it matters. Do you learn something by specifying this larger contract, like these 60 lines of contract?
33:40
And so here in this case, it was pointing at the index function, which I pointed that in my talk for string manipulation. And the contract is actually quite readable. So it specify exactly what these cases are in the index function. And if you don't write this as a form of contract, well, you have English prose that you will find in the ELA reference manual,
34:02
which is itself usually not self-contained. So you have various paragraph of the reference manual, which end up defining the behavior of the function. So I think in the end, so there are two answers. The contract should matter to you. So it should say something interesting, otherwise just maybe don't do that.
34:23
So it relates also to the level at which you want to prove the code. And then in terms of use of IDEs, I hope that in the future, we have ideas which allow to hide these contextual codes, like we hide the comments.
34:41
And so that's something we've discussed, for example, for our future support of Spark in various IDEs, whether it's a visual studio code or just to you. Thank you. Another question, a previous speaker made some comments regarding provers having to work together to prove everything.
35:00
How does it work in your experience? Did you use all three, one? So yes, Spark is tailored to benefit the most from the combination of provers so that you have the least to do in terms of helping the prover. If you just limit yourself to one prover, just you're cutting yourself from two thirds of the automation.
35:22
And so that's just a pain. And in fact, what I did was to use the four provers that we have now. So there's one called Colibri, which is not enabled by default because we're still working with the developers for having a better integration. But it's inside the technology, you can enable it.
35:41
So there's a switch prover all to have all four provers and here it's useful. So yes, we use constantly, as soon as you have more complex proof that go beyond basic type safety. So even the proof that Rod Chapman showed about more complex predicates and types, here he needed the three provers
36:02
and here I needed even the four provers that were not. Okay, thank you. Estefan asks, how do you debug, identify the issues when you write a complex contract and it fails during execution? Yeah, so here it didn't really apply
36:20
because the way we use contracts for the runtime library is that we don't want these contracts to be executed. So we never execute them. We have a pragma assertion policy that we use all over the runtime to say that this contract should never be executed. So these contracts are really here only for proof. And so if you want to make sure
36:42
that the precondition particular are correct, you have to read them. And in general, when you develop contracts, what you should be careful about is that the contracts at the border with the things that are not approved, typically the preconditions for library, for example, when you call it from elsewhere,
37:00
if the code that uses this library is not approved, the precondition could fail. So either it's a good thing because then you prevent getting into your API with the wrong context, or you don't want it to happen and then you have to test enough. And so, yeah, how do you, how do you identify that precondition for example is wrong?
37:24
Well, here, the failure in the test, for example, would give you a scenario which you can debug. And so in contracts in Ada or Spark, or just like code, you can debug and test them. Okay, thank you. We have about a minute.
37:42
Frederick asks, did the proofs require a lot of ghost functions? Yes, so there was quite a lot of ghost functions like I mentioned, but even more ghost lemmas. So things that you need to prove in isolation, because then the context is smaller for proof. And I also wanted to address one question,
38:00
which is, is it worth it? So that was the same question as for Rod. For us here, yes, at least in terms of making sure we are sufficiently confident in this runtime to be seen if we can exploit that more generally in certification. So for here, I cannot say right now, for example, that we will benefit in certification from this proof
38:22
compared to the traditional approach of specification and testing. Okay, so we have 10 seconds. There are questions that have not been answered. The room will now open and everybody's more than welcome to you. Thank you, Yannick. Thank you.