Status of matita port of CompCert 1.6 C semantics ================================================= Last seen working with matita svn r11115. - Most of the memory model has been ported (common/Mem.v -> Mem.ma). The main exception is minor arithmetic results than were proven with omega, which we hope to prove using matita's automation at some point. For the C semantics deliverable these (unnecessary) properties have been commented out. - The memory model is executable; some small tests can be found in test/memorymodel.ma. - The Clight syntax file has been ported, minus a few lemmas that are not used by the semantics. - The small-step inductively defined Clight semantics has been ported. - A collection of definitions and lemmas that probably ought to be in matita's standard library can be found in extralib.ma. - Some of the theory about machine integers (i.e., integers modulo) are given as axioms in Integers.ma. Proving them should be routine now that we have a binary representation of integers. The CompCert version is given as a functor on the word size - we don't have an equivalent of this yet. * The executable semantics can be found in Cexec.ma, which uses the error monad in Errors.ma and the resumption monad defined in IOMonad.ma. * The patch in acc-0.1.spaces.patch adds a -ma option to the prototype compiler which outputs a matita file containing the Clight program as a definition usable by the semantics. It also adds parsing support for the memory space extensions (__data and friends). * The patch in compcert-1.7.1-matita.patch adds a -dmatita option to output a matita file containing a definition for the C program. Note that there must be a "main" function. (This was made against 1.7.1 for convenience - the Clight syntax is the same as 1.6.) This is an older version of the prototype compiler patch, and lacks the memory extensions. There is a more recent version of compcert available with a revised memory model that may be more closely suited to our needs. matita issues and workarounds ----------------------------- No unfold tactic yet; use reduction or rewriting instead. Normalization of term containing large definitions (such as some of the Integers library) can be prohibitive. This is a particular problem because ndestruct currently normalizes the goal and every hypothesis that is rewritten. For ndestruct, getting rid of irrelevant information (e.g., replacing the goal with False) sometimes helps, an extra lemma can be used, or the definitions can make careful use of 'nlet rec' to prevent reduction. Some of the pattern matching in the C syntax has had to be unfolded in a rather unpleasant way (where matching on pairs was used in the original). The use of records in place of modules is a little delicate: large records tend to use a lot of memory and processor at the moment, and the names of the fields tend to clash a lot. The lack of sections has been replaced by duplicating the variables in some places, and adding a record in others. The meminj_no_overlap definition in Mem.ma uses the logical Or explicitly rather than the ∨ notation to regain reasonable performance. (This is presumably due to disambiguation - the notation is also used for booleans.) There are a couple of places in Mem.ma where rewriting had to be done carefully to avoid assertions during unification; I'm not really sure what the problem is. Detail per-file --------------- AST.ma Program transformation sections mostly left alone. CexecComplete.ma [new] Completeness of steps of executable semantics wrt inductive CexecEquiv.ma [new] Equivalence of complete executions to inductive semantics Cexec.ma [new] Definition of executable semantics CexecSound.ma Soundness of individual steps of executable semantics wrt inductive Coqlib.ma Only essential parts: - align - some 2^n lemmas (which could go into the binary libraries) - option_map - parts of list disjointness and non-repetition CostLabel.ma [new] Definition of cost labels Csem.ma The small step semantics have been ported. None of the big step semantics or the equivalence proof has been ported. Csyntax.ma Everything except for a few minor definitions / lemmas that are not required by the semantics. Errors.ma Only a basic definition without error messages. Events.ma Most of the definitions; haven't needed many of the lemmas yet. extralib.ma [new] Definitions which probably belong in the matita libraries, if anywhere. Floats.ma Axiomatised, but so was the original! Likely to be removed because we do not intend to support floating point. Globalenvs.ma Basic definition only; sufficient for animating the semantics. Integers.ma The operations have been ported, although the results about them generally have not. The equality results have been left axiomatised because they require proof irrelevance because each integer carries a proof that it is in range. The use of the Coq module system to abstract over the word size has been left out for now. IOMonad.ma [new] Definition and properties of the resumption+error monad for I/O. Maps.ma Only a basic definition. Mem.ma Everything except for omega in proofs. Smallstep.ma Ported definitions for multiple steps and program behaviour; left alternative definitions, some lemmas, plus most of the simulations sections for later. Values.ma The definitions about operations relevant to the Clight semantics have been ported. The other definitions and most of the lemmas still remain to be done.