Changeset 1041 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 24, 2011, 5:05:21 PM (10 years ago)

Author:

sacerdot

Message:

fetch_assembly is still working after bug fix

File:

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

src/ASM/AssemblyProof.ma

@@ -1136 +1136 @@
    \snd (fetch trivial_status (zero ?)).
 
-axiom fetch_assembly:
+lemma fetch_assembly:
   ∀pc,i,code_memory,assembled.
     assembled = assembly1 i →
@@ -1145 +1145 @@
       let 〈instr,pc'〉 ≝ instr_pc in
        (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
-(* #pc #i #code_memory #assembled cases i [8: *]
+ #pc #i #code_memory #assembled cases i [8: *]
  [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
  [47,48,49:
@@ -1160 +1160 @@
  [92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
   normalize in ⊢ (???% → ?)]
- #H >H * #H1 try (change in ⊢ (% → ?) with (? ∧ ?) * #H2)
- try (change in ⊢ (% → ?) with (? ∧ ?) * #H3) whd in ⊢ (% → ?) #H4
+ #H >H * #H1 try (whd in ⊢ (% → ?) * #H2)
+ try (whd in ⊢ (% → ?) * #H3) whd in ⊢ (% → ?) #H4
  change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??)
  whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
@@ -1169 +1169 @@
   69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
  whd >eq_instruction_refl >H4 @eq_bv_refl
-qed. *)
+qed.
 
 let rec fetch_many code_memory final_pc pc expected on expected: Prop ≝