Changeset 2138 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jun 28, 2012, 4:47:42 PM (7 years ago)
Author:
sacerdot
Message:

Invariant exported from proof of assembly_ok.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2137 r2138  
    721721       let 〈assembled,costs〉 ≝ res in
    722722       |assembled| ≤ 2^16 ∧
     723       nat_of_bitvector … (sigma (bitvector_of_nat … (|instr_list|))) = |assembled| ∧
    723724       let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
    724725       let datalabels ≝ construct_datalabels preamble in
     
    742743  let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in
    743744  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
    744   let 〈ignore,revcode〉 ≝ pi1 … (
     745  let 〈next_pc,revcode〉 ≝ pi1 … (
    745746     foldl_strong
    746747      (option Identifier × pseudo_instruction)
     
    776777      | #nlimit %1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
    777778        @not_eq_to_le_to_lt assumption ]
    778     | >length_reverse <Hfold3
    779       @(transitive_le … (S (nat_of_bitvector … (sigma ignore))))
    780       [ // | change with (? < ?); @lt_nat_of_bitvector ]]
     779    | >length_reverse <Hfold3 %
     780      [ @(transitive_le … (S (nat_of_bitvector … (sigma next_pc))))
     781        [ // | change with (? < ?); @lt_nat_of_bitvector ]
     782      | >Hfold1 % ]]
    781783  | * #sigma_pol_ok1 #_ #instr_list_ok %
    782784    [ % // >sigma_pol_ok1 % ]
Note: See TracChangeset for help on using the changeset viewer.