This repository contains some simple examples of dargent programs. The goal is to prove the correspondence between the monadic program (generated by AutoCorres from the C program) and the update semantics.
- my branch
dargentisa
of cogent; - my version of AutoCorres (this version fixes an issue that made some C programs systematically fail).
cd
in a subdirectory of an example- Compile the example and generate the theory files with the cogent compiler
- Edit the generated
.table
file so that it matches the specific format for custom layouts, giving the name of the custom getters/setters (the compiler should be adapted at some point so that this step is no longer necessary) - Check that the theory file ending with with
_CorresProof.thy
compile.
This theory file indeed attempts to prove the correspondance between the monadic and the update semantics.
On my computer, for step 2, I use the command
2. . ../compiles.sh branch cogent_file
(branch can be master or dargentisa)
This will generates a directory build_cogent_file_branch
with all the theory
files in it.
In principle, any example should work: there is some cheating tactic in the
generated _CorresSetup
theory file which automatically prove the get/set
lemmas. Currently, the only get/set lemmas that are proven without cheating
are the ones stating the correspondence between the direct and the monadic
definition of custom getters/setters.
The remaining task is to replace this cheating tactic with a proper automatic proof tactic.
-
The (dargent) formalization theoretically requires the custom getters to be generated, as they are used to define the value relation. In practice (but this could be refined), it also requires the custom setters to be generated. However, the cogent compiler may not generate custom getters/setters if they are not used.
-
The formalization assumes that there is only one custom getter for each field. However, the compiler may generate two of them: one for the member operation, and one for the take operation, although they seem to be the same.
TODO: The C compilation generates useless masks in the parts of the getters for custom layouts TODO: check examples with different layouts for the same record (I fear a clash in the table file, as the layout is always undefined)