Status of matita port of CompCert C semantics
=============================================
Last seen working with matita svn r10871.
- 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.
- The memory model is executable; some small tests can be found in
test/memorymodel.ma. Note that the handling of integer values is
axiomatised, so conversions are not yet evaluated.
- The C syntax has been ported, minus a few lemmas that are not used by
the semantics.
- Most of the small-step C semantics has been ported, although much of the
underlying arithmetic and environment functions are only present as axioms,
including the type of identifiers.
- Nonetheless, this is sufficient to show the semantics of a trivial C program
in test/trivial.ma.
- 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 machine integers (i.e., integers modulo) results are
given as axioms in Integers.ma. Implementing them could be
difficult if we keep using a unary representation of integers as
formalisation involves constants like 2^32.
matita issues and workarounds
-----------------------------
No unfold tactic yet; use reduction or rewriting instead.
ndestruct often takes too long; getting rid of irrelevant information (e.g.,
replacing the goal with False) sometimes helps, or an extra lemma can be used.
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.
Detail per-file
---------------
AST.ma
No concrete type for ident.
Program transformation sections left alone.
Coqlib.ma
Only essential parts:
- "align" is axiomatised
- option_map
- parts of list disjointness and non-repetition
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.
Floats.ma
Axiomatised, but so was the original!
Globalenvs.ma
Basic definition only.
Integers.ma
Most of the operations have been ported, although some have been left as
axioms because the underlying operation is not present. The use of the
Coq module system to abstract over the word size has been left out for
now.
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 simulations sections for later.
Values.ma
The definitions about values which don't rely on arithmetics operations that
haven't been ported yet are done. The other definitions and most of the
lemmas still remain to be done.