Changeset 12

Timestamp:

Jul 7, 2010, 6:46:46 PM (11 years ago)

Author:

campbell

Message:

Make memory model tests more readable.
Update README.

Location:

C-semantics

Files:

• README (modified) (6 diffs)
• test/memorymodel.ma (modified) (1 diff)

C-semantics/README

@@ -2 +2 @@
 =================================================
 
-Last seen working with matita svn r10877 with the patch at the bottom of this
-file.
+Last seen working with matita svn r10890.
 
 - Most of the memory model has been ported (common/Mem.v -> Mem.ma).
@@ -28 +27 @@
 
 - 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.
+  given as axioms in Integers.ma.  Implementing 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.
 
 * Some experimental work on an executable semantics has been started in
@@ -67 +66 @@
 AST.ma
 
-  No concrete type for ident.
   Program transformation sections left alone.
 
@@ -73 +71 @@
 
   Only essential parts:
-  - "align" is axiomatised
+  - align
+  - some 2^n lemmas (which could go into the binary libraries)
   - option_map
   - parts of list disjointness and non-repetition
@@ -116 +115 @@
 Mem.ma
 
-  Everything except for omega in proofs.
+  Everything except for omega in proofs.  Much of the transformations sections
+  are commented out until Integers.ma is done properly.
 
 Smallstep.ma
@@ -130 +130 @@
 
 
-
-
-Index: matita/nlibrary/arithmetics/Z.ma
-===================================================================
---- matita/nlibrary/arithmetics/Z.ma    (revision 10877)
-+++ matita/nlibrary/arithmetics/Z.ma    (working copy)
-@@ -13,6 +13,7 @@
- (**************************************************************************)
- 
- include "arithmetics/nat.ma".
-+include "arithmetics/compare.ma".
- 
- ninductive Z : Type %G≝%@
-   OZ : Z
-@@ -508,7 +509,7 @@
-    ##[//
-    ##|#n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);//
-    ##|//]
--##|ncases y;//
-+##|ncases y;/2/
- ##|ncases y
-    ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);
-       nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);//

C-semantics/test/memorymodel.ma

@@ -24 +24 @@
 ndefinition store1 : mem ≝ fst ?? store1block.
 ndefinition block := snd ?? store1block.
+
 (* write a value *)
 ndefinition store2 : mem.
   nletin r ≝ (store Mint16unsigned store1 block 0 (Vint one));
+
   nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
   ##| #rr; #_; napply rr ##] nqed.
+
 (* overwrite the first byte of the value *)
 ndefinition store3 : mem.
   nletin r ≝ (store Mint8unsigned store1 block 0 (Vint one));
+
   nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
   ##| #rr; #_; napply rr ##] nqed.
   
-ndefinition vl := load Mint16signed store3 block 0.
 (* The size checking rejects the read and gives us Some Vundef. *)
-nremark vl_undef: vl = Some ? Vundef. //; nqed.
+nremark vl_undef: load Mint16signed store3 block 0 = Some ? Vundef. //; nqed.
 
-ndefinition vl' := load Mint8unsigned store3 block 0.
 (* The read is successful and returns a signed version of the value. *)
-nremark vl_ok': vl' = Some ? (Vint (zero_ext 8 one)). //; nqed.
+nremark vl_ok': load Mint8unsigned store3 block 0 = Some ? (Vint (zero_ext 8 one)). //; nqed.
 
-ndefinition store4 := free store3 block.
 (* NB: Double frees are allowed by the memory model (although not necessarily
        by the language). *)
+ndefinition store4 := free store3 block.
 ndefinition store5 : mem. nletin r ≝ (free store3 block); nwhd in r; napply r; nqed.