Changeset 909 for src

Timestamp:

Jun 9, 2011, 1:27:57 AM (10 years ago)

Author:

sacerdot

Message:

Back to the main theorem.

File:

• src/ASM/AssemblyProof.ma (modified) (4 diffs)

src/ASM/AssemblyProof.ma

@@ -1449 +1449 @@
     | Some p ⇒
        let cm ≝ load_code_memory (\fst p) in
-       let pc ≝ sigma' pap (program_counter ? ps) in
+       let pc ≝ sigma pap (program_counter ? ps) in
         Some …
          (mk_PreStatus (BitVectorTrie Byte 16)
@@ -1463 +1463 @@
            (clock … ps)) ].
 
+(*
 definition write_at_stack_pointer':
  ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
@@ -1521 +1522 @@
  cases not_implemented
 qed.
-
+*)
 (*
 lemma execute_code_memory_unchanged:
@@ -1561 +1562 @@
     | Some _ ⇒ ∃w. status_of_pseudo_status ps' = Some … w
     ].
- #ps #ps' #H whd in ⊢ (mat
- ch % with [ _ ⇒ ? | _ ⇒ ? ])
+ #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
  generalize in match (refl … (assembly (code_memory … ps)))
  cases (assembly ?) in ⊢ (???% → %)
   [ #K whd whd in ⊢ (??%?) <H >K %
   | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
-qed.*)
-
-let rec encoding_check' (code_memory: BitVectorTrie Byte 16) (pc: Word) (encoding: list Byte) on encoding: Prop ≝
-  match encoding with
-  [ nil ⇒ True
-  | cons hd tl ⇒
-    let 〈new_pc, byte〉 ≝ next code_memory pc in
-      hd = byte ∧ encoding_check' code_memory new_pc tl
-  ].
- 
+qed.
+
 lemma main_thm:
  ∀ticks_of.