Ignore:
Timestamp:
Jun 24, 2011, 5:05:21 PM (8 years ago)
Author:
sacerdot
Message:

fetch_assembly is still working after bug fix

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1039 r1041  
    11361136   \snd (fetch trivial_status (zero ?)).
    11371137
    1138 axiom fetch_assembly:
     1138lemma fetch_assembly:
    11391139  ∀pc,i,code_memory,assembled.
    11401140    assembled = assembly1 i →
     
    11451145      let 〈instr,pc'〉 ≝ instr_pc in
    11461146       (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
    1147 (* #pc #i #code_memory #assembled cases i [8: *]
     1147 #pc #i #code_memory #assembled cases i [8: *]
    11481148 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
    11491149 [47,48,49:
     
    11601160 [92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
    11611161  normalize in ⊢ (???% → ?)]
    1162  #H >H * #H1 try (change in ⊢ (% → ?) with (? ∧ ?) * #H2)
    1163  try (change in ⊢ (% → ?) with (? ∧ ?) * #H3) whd in ⊢ (% → ?) #H4
     1162 #H >H * #H1 try (whd in ⊢ (% → ?) * #H2)
     1163 try (whd in ⊢ (% → ?) * #H3) whd in ⊢ (% → ?) #H4
    11641164 change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??)
    11651165 whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
     
    11691169  69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
    11701170 whd >eq_instruction_refl >H4 @eq_bv_refl
    1171 qed. *)
     1171qed.
    11721172
    11731173let rec fetch_many code_memory final_pc pc expected on expected: Prop ≝
Note: See TracChangeset for help on using the changeset viewer.