| 1 | Status of matita port of CompCert 1.6 C semantics |
|---|
| 2 | ================================================= |
|---|
| 3 | |
|---|
| 4 | Last seen working with matita svn r11115. |
|---|
| 5 | |
|---|
| 6 | - Most of the memory model has been ported (common/Mem.v -> Mem.ma). |
|---|
| 7 | The main exception is minor arithmetic results than were proven with |
|---|
| 8 | omega, which we hope to prove using matita's automation at some |
|---|
| 9 | point. For the C semantics deliverable these (unnecessary) properties |
|---|
| 10 | have been commented out. |
|---|
| 11 | |
|---|
| 12 | - The memory model is executable; some small tests can be found in |
|---|
| 13 | test/memorymodel.ma. |
|---|
| 14 | |
|---|
| 15 | - The Clight syntax file has been ported, minus a few lemmas that are not used |
|---|
| 16 | by the semantics. |
|---|
| 17 | |
|---|
| 18 | - The small-step inductively defined Clight semantics has been ported. |
|---|
| 19 | |
|---|
| 20 | - A collection of definitions and lemmas that probably ought to be in |
|---|
| 21 | matita's standard library can be found in extralib.ma. |
|---|
| 22 | |
|---|
| 23 | - Some of the theory about machine integers (i.e., integers modulo) are |
|---|
| 24 | given as axioms in Integers.ma. Proving them should be routine now that |
|---|
| 25 | we have a binary representation of integers. The CompCert version is given |
|---|
| 26 | as a functor on the word size - we don't have an equivalent of this yet. |
|---|
| 27 | |
|---|
| 28 | * The executable semantics can be found in Cexec.ma, which uses the |
|---|
| 29 | error monad in Errors.ma and the resumption monad defined in IOMonad.ma. |
|---|
| 30 | |
|---|
| 31 | * The patch in acc-0.1.spaces.patch adds a -ma option to the prototype |
|---|
| 32 | compiler which outputs a matita file containing the Clight program as |
|---|
| 33 | a definition usable by the semantics. It also adds parsing support for |
|---|
| 34 | the memory space extensions (__data and friends). |
|---|
| 35 | |
|---|
| 36 | * The patch in compcert-1.7.1-matita.patch adds a -dmatita option to |
|---|
| 37 | output a matita file containing a definition for the C program. |
|---|
| 38 | Note that there must be a "main" function. (This was made against |
|---|
| 39 | 1.7.1 for convenience - the Clight syntax is the same as 1.6.) |
|---|
| 40 | This is an older version of the prototype compiler patch, and lacks the |
|---|
| 41 | memory extensions. |
|---|
| 42 | |
|---|
| 43 | There is a more recent version of compcert available with a revised memory |
|---|
| 44 | model that may be more closely suited to our needs. |
|---|
| 45 | |
|---|
| 46 | matita issues and workarounds |
|---|
| 47 | ----------------------------- |
|---|
| 48 | |
|---|
| 49 | No unfold tactic yet; use reduction or rewriting instead. |
|---|
| 50 | |
|---|
| 51 | Normalization of term containing large definitions (such as some of the |
|---|
| 52 | Integers library) can be prohibitive. This is a particular problem because |
|---|
| 53 | ndestruct currently normalizes the goal and every hypothesis that is rewritten. |
|---|
| 54 | For ndestruct, getting rid of irrelevant information (e.g., replacing the goal |
|---|
| 55 | with False) sometimes helps, an extra lemma can be used, or the definitions |
|---|
| 56 | can make careful use of 'nlet rec' to prevent reduction. |
|---|
| 57 | |
|---|
| 58 | Some of the pattern matching in the C syntax has had to be unfolded in |
|---|
| 59 | a rather unpleasant way (where matching on pairs was used in the original). |
|---|
| 60 | |
|---|
| 61 | The use of records in place of modules is a little delicate: large records |
|---|
| 62 | tend to use a lot of memory and processor at the moment, and the names of the |
|---|
| 63 | fields tend to clash a lot. |
|---|
| 64 | |
|---|
| 65 | The lack of sections has been replaced by duplicating the variables in some |
|---|
| 66 | places, and adding a record in others. |
|---|
| 67 | |
|---|
| 68 | The meminj_no_overlap definition in Mem.ma uses the logical Or explicitly |
|---|
| 69 | rather than the ∨ notation to regain reasonable performance. (This is |
|---|
| 70 | presumably due to disambiguation - the notation is also used for booleans.) |
|---|
| 71 | |
|---|
| 72 | There are a couple of places in Mem.ma where rewriting had to be done carefully |
|---|
| 73 | to avoid assertions during unification; I'm not really sure what the problem |
|---|
| 74 | is. |
|---|
| 75 | |
|---|
| 76 | Detail per-file |
|---|
| 77 | --------------- |
|---|
| 78 | |
|---|
| 79 | AST.ma |
|---|
| 80 | |
|---|
| 81 | Program transformation sections mostly left alone. |
|---|
| 82 | |
|---|
| 83 | CexecComplete.ma [new] |
|---|
| 84 | |
|---|
| 85 | Completeness of steps of executable semantics wrt inductive |
|---|
| 86 | |
|---|
| 87 | CexecEquiv.ma [new] |
|---|
| 88 | |
|---|
| 89 | Equivalence of complete executions to inductive semantics |
|---|
| 90 | |
|---|
| 91 | Cexec.ma [new] |
|---|
| 92 | |
|---|
| 93 | Definition of executable semantics |
|---|
| 94 | |
|---|
| 95 | CexecSound.ma |
|---|
| 96 | |
|---|
| 97 | Soundness of individual steps of executable semantics wrt inductive |
|---|
| 98 | |
|---|
| 99 | Coqlib.ma |
|---|
| 100 | |
|---|
| 101 | Only essential parts: |
|---|
| 102 | - align |
|---|
| 103 | - some 2^n lemmas (which could go into the binary libraries) |
|---|
| 104 | - option_map |
|---|
| 105 | - parts of list disjointness and non-repetition |
|---|
| 106 | |
|---|
| 107 | CostLabel.ma [new] |
|---|
| 108 | |
|---|
| 109 | Definition of cost labels |
|---|
| 110 | |
|---|
| 111 | Csem.ma |
|---|
| 112 | |
|---|
| 113 | The small step semantics have been ported. None of the big step semantics or |
|---|
| 114 | the equivalence proof has been ported. |
|---|
| 115 | |
|---|
| 116 | Csyntax.ma |
|---|
| 117 | |
|---|
| 118 | Everything except for a few minor definitions / lemmas that are not required |
|---|
| 119 | by the semantics. |
|---|
| 120 | |
|---|
| 121 | Errors.ma |
|---|
| 122 | |
|---|
| 123 | Only a basic definition without error messages. |
|---|
| 124 | |
|---|
| 125 | Events.ma |
|---|
| 126 | |
|---|
| 127 | Most of the definitions; haven't needed many of the lemmas yet. |
|---|
| 128 | |
|---|
| 129 | extralib.ma [new] |
|---|
| 130 | |
|---|
| 131 | Definitions which probably belong in the matita libraries, if anywhere. |
|---|
| 132 | |
|---|
| 133 | Floats.ma |
|---|
| 134 | |
|---|
| 135 | Axiomatised, but so was the original! Likely to be removed because we do |
|---|
| 136 | not intend to support floating point. |
|---|
| 137 | |
|---|
| 138 | Globalenvs.ma |
|---|
| 139 | |
|---|
| 140 | Basic definition only; sufficient for animating the semantics. |
|---|
| 141 | |
|---|
| 142 | Integers.ma |
|---|
| 143 | |
|---|
| 144 | The operations have been ported, although the results about them generally |
|---|
| 145 | have not. The equality results have been left axiomatised because they |
|---|
| 146 | require proof irrelevance because each integer carries a proof that it is |
|---|
| 147 | in range. The use of the Coq module system to abstract over the word size |
|---|
| 148 | has been left out for now. |
|---|
| 149 | |
|---|
| 150 | IOMonad.ma [new] |
|---|
| 151 | |
|---|
| 152 | Definition and properties of the resumption+error monad for I/O. |
|---|
| 153 | |
|---|
| 154 | Maps.ma |
|---|
| 155 | |
|---|
| 156 | Only a basic definition. |
|---|
| 157 | |
|---|
| 158 | Mem.ma |
|---|
| 159 | |
|---|
| 160 | Everything except for omega in proofs. |
|---|
| 161 | |
|---|
| 162 | Smallstep.ma |
|---|
| 163 | |
|---|
| 164 | Ported definitions for multiple steps and program behaviour; left |
|---|
| 165 | alternative definitions, some lemmas, plus most of the simulations sections |
|---|
| 166 | for later. |
|---|
| 167 | |
|---|
| 168 | Values.ma |
|---|
| 169 | |
|---|
| 170 | The definitions about operations relevant to the Clight semantics have been |
|---|
| 171 | ported. The other definitions and most of the lemmas still remain to be done. |
|---|
| 172 | |
|---|
| 173 | |
|---|
