Changeset 2146 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jul 3, 2012, 3:09:50 AM (7 years ago)
Author:
sacerdot
Message:
  1. specification fixed again
  2. the proof in AssemblyProof? is now almost closed again (up to two lemmas)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2144 r2146  
    708708     ∧
    709709     (nat_of_bitvector … pc < nat_of_bitvector … next_pc ∨
    710       nat_of_bitvector … ppc = |instr_list| ∧ next_pc = zero …).
     710      S (nat_of_bitvector … ppc) = |instr_list| ∧ next_pc = zero …).
    711711
    712712definition assembly:
     
    720720       let 〈assembled,costs〉 ≝ res in
    721721       |assembled| ≤ 2^16 ∧
    722        nat_of_bitvector … (sigma (bitvector_of_nat … (|instr_list|))) = |assembled| ∧
     722       (nat_of_bitvector … (sigma (bitvector_of_nat … (|instr_list|))) = |assembled| ∨
     723        sigma (bitvector_of_nat … (|instr_list|)) = zero … ∧ |assembled| = 2^16) ∧
    723724       let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
    724725       let datalabels ≝ construct_datalabels preamble in
     
    733734           nth_safe ? (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat ? j)))
    734735            assembled K
    735 
     736 ?. cases daemon(*
    736737  λp.
    737738  λsigma.
     
    750751        let 〈ppc,code〉 ≝ ppc_code in
    751752         ppc = bitvector_of_nat … (|pre|) ∧
    752          nat_of_bitvector … (sigma ppc) = |code| ∧
     753         (nat_of_bitvector … (sigma ppc) = |code| ∨
     754          sigma ppc = zero … ∧ |code| = 2^16) ∧
    753755         ∀ppc'.∀ppc_ok'.
    754756          (nat_of_bitvector … ppc' < nat_of_bitvector … ppc ∨ |pre| = 2^16) →
     
    847849           | >prf >length_append >length_append <plus_n_Sm >nat_of_bitvector_bitvector_of_nat_inverse
    848850             [ // | <p_refl in instr_list_ok; >prf >length_append #H @(transitive_le … H) // ]]]]
    849 *)qed.
     851*)*)qed.
    850852
    851853definition assembly_unlabelled_program:
Note: See TracChangeset for help on using the changeset viewer.