Changeset 1041 for src/ASM/AssemblyProof.ma
- Timestamp:
- Jun 24, 2011, 5:05:21 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r1039 r1041 1136 1136 \snd (fetch trivial_status (zero ?)). 1137 1137 1138 axiomfetch_assembly:1138 lemma fetch_assembly: 1139 1139 ∀pc,i,code_memory,assembled. 1140 1140 assembled = assembly1 i → … … 1145 1145 let 〈instr,pc'〉 ≝ instr_pc in 1146 1146 (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: *] 1148 1148 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]] 1149 1149 [47,48,49: … … 1160 1160 [92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)] 1161 1161 normalize in ⊢ (???% → ?)] 1162 #H >H * #H1 try ( change in ⊢ (% → ?) with (? ∧?) * #H2)1163 try ( change in ⊢ (% → ?) with (? ∧?) * #H3) whd in ⊢ (% → ?) #H41162 #H >H * #H1 try (whd in ⊢ (% → ?) * #H2) 1163 try (whd in ⊢ (% → ?) * #H3) whd in ⊢ (% → ?) #H4 1164 1164 change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??) 1165 1165 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] 1170 1170 whd >eq_instruction_refl >H4 @eq_bv_refl 1171 qed. *)1171 qed. 1172 1172 1173 1173 let rec fetch_many code_memory final_pc pc expected on expected: Prop ≝
Note: See TracChangeset
for help on using the changeset viewer.