Ignore:
Timestamp:
Jun 8, 2011, 10:59:01 AM (9 years ago)
Author:
sacerdot
Message:

Proof completed, fetch and assembly are mutual inverses.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r896 r897  
    744744 [1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3]
    745745 normalize in ⊢ (???% → ?)
    746  [42,93,95: @split_elim #vl #vm #E >E -E; normalize in ⊢ (???% → ?)
    747  |92,94: @split_elim #v1 #v2 #E >E -E; @(bitvector_3_elim_prop … v1) normalize in ⊢ (???% → ?)
    748    #H >H * #H1 try (change in ⊢ (% → ?) with (? ∧ ?) * #H2)
    749    try (change in ⊢ (% → ?) with (? ∧ ?) * #H3) whd in ⊢ (% → ?) #H4
    750    change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??)
    751    whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
    752    <H2 whd >eq_instruction_refl >H4 @eq_bv_refl]
     746 [92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
     747  normalize in ⊢ (???% → ?)]
    753748 #H >H * #H1 try (change in ⊢ (% → ?) with (? ∧ ?) * #H2)
    754749 try (change in ⊢ (% → ?) with (? ∧ ?) * #H3) whd in ⊢ (% → ?) #H4
    755750 change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??)
    756751 whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
    757  [1,2,3,4,5,6,7,8,9,10,15,18,19,20,21,22: <H3]
    758  [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,27,29,32,33,36,
    759   37,38,39,40,41,44,45, 46,49,50,53,54,57,58,62,64,65,68,69,79,82,85,86,87,88,
    760   89,90,91,92,93,94: <H2]
     752 [17,18,19,20,21,22,23,24,25,26,31,34,35,36,37,38: <H3]
     753 [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,
     754  30,31,32,33,34,35,36,37,38,39,40,43,45,48,49,52,53,54,55,56,57,60,61,62,65,66,
     755  69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
    761756 whd >eq_instruction_refl >H4 @eq_bv_refl
    762757qed.
Note: See TracChangeset for help on using the changeset viewer.