Changeset 839 for src/ASM/AssemblyProof.ma

Timestamp:

May 25, 2011, 1:31:15 PM (10 years ago)

Author:

sacerdot

Message:

More experiments.

File:

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

src/ASM/AssemblyProof.ma

@@ -95 +95 @@
 (* END RUSSELL **)
 
-definition write_at_stack_pointer:
+definition write_at_stack_pointer':
  ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
   λM: Type[0].
@@ -138 +138 @@
       let s ≝ set_8051_sfr ? s SFR_SP new_sp in
       let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
-      let s ≝ write_at_stack_pointer ? s pc_bl in
+      let s ≝ write_at_stack_pointer' ? s pc_bl in
       let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
       let s ≝ set_8051_sfr ? s SFR_SP new_sp in
-      let s ≝ write_at_stack_pointer ? s pc_bu in
+      let s ≝ write_at_stack_pointer' ? s pc_bu in
         set_program_counter ? s a
     | Mov dptr ident ⇒
@@ -154 +154 @@
  | %
  ]
-qed.
-
-
-
-
+ cases not_implemented
+qed.
+
+(*
 lemma execute_code_memory_unchanged:
  ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
@@ -188 +187 @@
   cases not_implemented
 qed.
-
-lemma foo:
+*)
+
+lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
+ ∀ps,ps': PseudoStatus.
+  code_memory … ps = code_memory … ps' →
+   match status_of_pseudo_status ps with
+    [ None ⇒ status_of_pseudo_status ps' = None …
+    | Some _ ⇒ ∃w. status_of_pseudo_status ps' = Some … w
+    ].
+ #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.
+ 
+lemma main_thm:
  ∀ticks_of.
  ∀ps: PseudoStatus.
@@ -201 +215 @@
  cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
  whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
+ generalize in match (sig2 … (execute_1_pseudo_instruction' ticks_of ps))
+ 
  cases (status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps)) [%] #s'' whd