Tracking formal verification status

[emmanuelsearch]

Based on the current use of hax and with regards to our draft manifesto, the question arises of where/how to track where we currently are at, now that initial integration has begun e.g. with #126.

[emmanuelsearch]

to give a concrete example: based on https://github.com/future-proof-iot/RIOT-rs/blob/main/src/riot-rs-runqueue/proofs/fstar/extraction/Makefile how/where should we express (for laypeople) what verification(s) are currently provided by CI for the scheduler? @W95Psp @franziskuskiefer obviously we'd very much value your suggestions on this ;)

[franziskuskiefer]

So do we have panic freedom already? If yes, then you should think about the contracts (pre- and post-conditions) the functions have and if there's something interesting that should be proven.
In parallel, adding more crates to the extraction, lax typechecking, etc. pipeline.

To the documentation, I think panic freedom should be documented when the extracted code typechecks in F*.
Additional properties should then come from the contracts the functions get and get described accordingly.

[emmanuelsearch]

@franziskuskiefer thanks for the input. A more basic question then: what is the fundamental difference between typechecking and lax typechecking ? (I seem to remember @W95Psp hinting that RunQueue was lax typechecking already, but I am not sure if my memory plays tricks on me, or how to check that myself ;)

[franziskuskiefer]

I think the easiest description is

• lax typechecking -> valid F* code is generated and all dependencies (like from the Rust core library) are defined
• typechecking -> panic freedom (F* proved that no panic occurs in the code)

[ROMemories]

@W95Psp Could you detail the steps that would now be required to typecheck the riot-rs-runqueue crate and prove panic-freedom? The hax.yml CI workflow currently only does lax typechecking if I understand correctly.

[ROMemories]

The Makefile we had indeed only did lax typechecking (e.g., symbol resolution checking). #404 updated the hax setup; CI is still configured to only do lax typechecking, but it would now be easy to enable full typechecking which, if successful, proves panic-freedom.