Ignore:
Timestamp:
May 22, 2012, 5:37:09 PM (8 years ago)
Author:
mulligan
Message:

Most proof obligations closed in main_lemma apart from those of the `false' cases in conditional jumps.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1983 r1984  
    14351435  [ nil ⇒ eq_bv … pc final_pc = true
    14361436  | cons i tl ⇒
    1437       (∃pc': Word. 〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧
     1437    let pc' ≝ add 16 pc (bitvector_of_nat 16 (|assembly1 … i|)) in
     1438      (〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧
    14381439        fetch_many code_memory final_pc pc' tl)
    14391440  ].
     
    15071508    lapply (conjunction_true ?? H3) * #H4 #H5
    15081509    lapply (conjunction_true … H4) * #B1 #B2
    1509     %{pc'} <(eq_instruction_to_eq … B1) >(eq_bv_eq … H5)
    1510     >(eqb_true_to_refl … B2) % try % @IH @H2
     1510    >(eq_instruction_to_eq … B1) >(eq_bv_eq … H5) %
     1511    >(eqb_true_to_refl … B2) >(eq_instruction_to_eq … B1) try % @IH @H2
    15111512  ]
    15121513qed.
     
    23642365  //
    23652366qed.
     2367
     2368(* XXX: easy but tedious *)
     2369axiom assembly1_lt_128:
     2370  ∀i: instruction.
     2371    |(assembly1 i)| < 128.
     2372
     2373axiom most_significant_bit_zero:
     2374  ∀size, m: nat.
     2375  ∀size_proof: 0 < size.
     2376    m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false.
     2377  normalize in size_proof; /2/
     2378qed.
     2379
     2380lemma bitvector_of_nat_sign_extension_equivalence:
     2381  ∀m: nat.
     2382  ∀size_proof: m < 128.
     2383    sign_extension … (bitvector_of_nat 8 m) = bitvector_of_nat 16 m.
     2384  #m #size_proof whd in ⊢ (??%?);
     2385  >most_significant_bit_zero
     2386  [1:
     2387    cases daemon
     2388  |2:
     2389    assumption
     2390  |3:
     2391    //
     2392  ]
     2393qed.
Note: See TracChangeset for help on using the changeset viewer.