1 | Status of matita port of CompCert 1.6 C semantics |
---|
2 | ================================================= |
---|
3 | |
---|
4 | Last seen working with matita svn r10877 with the patch at the bottom of this |
---|
5 | file. |
---|
6 | |
---|
7 | - Most of the memory model has been ported (common/Mem.v -> Mem.ma). |
---|
8 | The main exception is minor arithmetic results than were proven with |
---|
9 | omega, which we hope to prove using matita's automation at some |
---|
10 | point. |
---|
11 | |
---|
12 | - The memory model is executable; some small tests can be found in |
---|
13 | test/memorymodel.ma. Note that the handling of integer values is |
---|
14 | axiomatised, so conversions are not yet evaluated. |
---|
15 | |
---|
16 | - The C syntax has been ported, minus a few lemmas that are not used by |
---|
17 | the semantics. |
---|
18 | |
---|
19 | - Most of the small-step C semantics has been ported, although much of the |
---|
20 | underlying arithmetic and environment functions are only present as axioms, |
---|
21 | including the type of identifiers. |
---|
22 | |
---|
23 | - Nonetheless, this is sufficient to show the semantics of a trivial C program |
---|
24 | in test/trivial.ma. |
---|
25 | |
---|
26 | - A collection of definitions and lemmas that probably ought to be in |
---|
27 | matita's standard library can be found in extralib.ma. |
---|
28 | |
---|
29 | - Some of the machine integers (i.e., integers modulo) results are |
---|
30 | given as axioms in Integers.ma. Implementing them could be |
---|
31 | difficult if we keep using a unary representation of integers as |
---|
32 | formalisation involves constants like 2^32. |
---|
33 | |
---|
34 | * Some experimental work on an executable semantics has been started in |
---|
35 | Cexec.ma. At present only a small subset of expressions and statements |
---|
36 | are handled. |
---|
37 | |
---|
38 | * The patch in compcert-1.7.1-matita.patch adds a -dmatita option to |
---|
39 | output a matita file containing a definition for the C program. |
---|
40 | Note that there must be a "main" function. (This was made against |
---|
41 | 1.7.1 for convenience - the Clight syntax is the same as 1.6.) |
---|
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 | ndestruct often takes too long; getting rid of irrelevant information (e.g., |
---|
52 | replacing the goal with False) sometimes helps, or an extra lemma can be used. |
---|
53 | |
---|
54 | Some of the pattern matching in the C syntax has had to be unfolded in |
---|
55 | a rather unpleasant way (where matching on pairs was used in the original). |
---|
56 | |
---|
57 | The use of records in place of modules is a little delicate: large records |
---|
58 | tend to use a lot of memory and processor at the moment, and the names of the |
---|
59 | fields tend to clash a lot. |
---|
60 | |
---|
61 | The lack of sections has been replaced by duplicating the variables in some |
---|
62 | places, and adding a record in others. |
---|
63 | |
---|
64 | Detail per-file |
---|
65 | --------------- |
---|
66 | |
---|
67 | AST.ma |
---|
68 | |
---|
69 | No concrete type for ident. |
---|
70 | Program transformation sections left alone. |
---|
71 | |
---|
72 | Coqlib.ma |
---|
73 | |
---|
74 | Only essential parts: |
---|
75 | - "align" is axiomatised |
---|
76 | - option_map |
---|
77 | - parts of list disjointness and non-repetition |
---|
78 | |
---|
79 | Csem.ma |
---|
80 | |
---|
81 | The small step semantics have been ported. None of the big step semantics or |
---|
82 | the equivalence proof has been ported. |
---|
83 | |
---|
84 | Csyntax.ma |
---|
85 | |
---|
86 | Everything except for a few minor definitions / lemmas that are not required |
---|
87 | by the semantics. |
---|
88 | |
---|
89 | Errors.ma |
---|
90 | |
---|
91 | Only a basic definition without error messages. |
---|
92 | |
---|
93 | Events.ma |
---|
94 | |
---|
95 | Most of the definitions; haven't needed many of the lemmas yet. |
---|
96 | |
---|
97 | Floats.ma |
---|
98 | |
---|
99 | Axiomatised, but so was the original! |
---|
100 | |
---|
101 | Globalenvs.ma |
---|
102 | |
---|
103 | Basic definition only. |
---|
104 | |
---|
105 | Integers.ma |
---|
106 | |
---|
107 | Most of the operations have been ported, although some have been left as |
---|
108 | axioms because the underlying operation is not present. The use of the |
---|
109 | Coq module system to abstract over the word size has been left out for |
---|
110 | now. |
---|
111 | |
---|
112 | Maps.ma |
---|
113 | |
---|
114 | Only a basic definition. |
---|
115 | |
---|
116 | Mem.ma |
---|
117 | |
---|
118 | Everything except for omega in proofs. |
---|
119 | |
---|
120 | Smallstep.ma |
---|
121 | |
---|
122 | Ported definitions for multiple steps and program behaviour; left |
---|
123 | alternative definitions, some lemmas, plus simulations sections for later. |
---|
124 | |
---|
125 | Values.ma |
---|
126 | |
---|
127 | The definitions about values which don't rely on arithmetics operations that |
---|
128 | haven't been ported yet are done. The other definitions and most of the |
---|
129 | lemmas still remain to be done. |
---|
130 | |
---|
131 | |
---|
132 | |
---|
133 | |
---|
134 | Index: matita/nlibrary/arithmetics/Z.ma |
---|
135 | =================================================================== |
---|
136 | --- matita/nlibrary/arithmetics/Z.ma (revision 10877) |
---|
137 | +++ matita/nlibrary/arithmetics/Z.ma (working copy) |
---|
138 | @@ -13,6 +13,7 @@ |
---|
139 | (**************************************************************************) |
---|
140 | |
---|
141 | include "arithmetics/nat.ma". |
---|
142 | +include "arithmetics/compare.ma". |
---|
143 | |
---|
144 | ninductive Z : Type %Gâ%@ |
---|
145 | OZ : Z |
---|
146 | @@ -508,7 +509,7 @@ |
---|
147 | ##[// |
---|
148 | ##|#n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);// |
---|
149 | ##|//] |
---|
150 | -##|ncases y;// |
---|
151 | +##|ncases y;/2/ |
---|
152 | ##|ncases y |
---|
153 | ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?); |
---|
154 | nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);// |
---|