Changeset 2138


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

Invariant exported from proof of assembly_ok.

Location:
src/ASM
Files:
2 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 % ]
  • src/ASM/AssemblyProof.ma

    r2136 r2138  
    377377  #H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
    378378  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
    379   * #assembly_ok1 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
     379  * * #assembly_ok1 #assembly_ok3 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
    380380  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
    381381  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
     
    10511051*)
    10521052
    1053 (*CSC: ???*)
    1054 (* XXX: we need a precondition here stating that the PPC is within the
    1055         bounds of the instruction list in order for Jaap's specification to
    1056         apply.
    1057 *)
    10581053lemma snd_assembly_1_pseudoinstruction_ok:
    10591054  ∀program: pseudo_assembly_program.
Note: See TracChangeset for help on using the changeset viewer.