Changeset 2081


Ignore:
Timestamp:
Jun 14, 2012, 12:04:02 PM (5 years ago)
Author:
sacerdot
Message:

Type of assembly fixed to be compatible with the old one and to take as
a new assumption the correctness of the policy. One more daemon closed,
all daemons can be closed now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2079 r2081  
    789789definition assembly:
    790790    ∀p: pseudo_assembly_program.
    791     |\snd p| < 2^16 →
    792791    ∀sigma: Word → Word.
    793792    ∀policy: Word → bool.
    794793      Σres:list Byte × (BitVectorTrie costlabel 16).
     794       sigma_policy_specification p sigma policy →
    795795       let 〈preamble,instr_list〉 ≝ p in
     796       |instr_list| < 2^16 →
    796797       let 〈assembled,costs〉 ≝ res in
    797798       let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
     
    808809            assembled K
    809810
    810   λp. λinstr_list_ok.
     811  λp.
    811812  λsigma.
    812813  λpolicy.
     
    820821      (option Identifier × pseudo_instruction)
    821822      (λpre. Σppc_code:(Word × (list Byte)).
     823       sigma_policy_specification 〈preamble,instr_list〉 sigma policy →
     824        |instr_list| < 2^16 →
    822825        let 〈ppc,code〉 ≝ ppc_code in
    823826         ppc = bitvector_of_nat … (|pre|) ∧
     
    842845      fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉.
    843846  [ cases (foldl_strong ? (λx.Σy.?) ???) in p2; #ignore_revcode #Hfold #EQignore_revcode
    844     >EQignore_revcode in Hfold; * * #Hfold1 #Hfold3 #Hfold2 whd >p1 whd #ppc #LTppc @Hfold2
     847    >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok
     848    cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * #Hfold1 #Hfold3 #Hfold2 whd >p1 whd #ppc #LTppc @Hfold2
    845849    >Hfold1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
    846     <p_refl in instr_list_ok; #H @H
    847   | %
    848     [ % // (*CSC: NEW INVARIANT FOR JAAP!*) cases daemon ]
     850  | * #sigma_pol_ok1 #_ #instr_list_ok %
     851    [ % // >sigma_pol_ok1 % ]
    849852    #ppc' #ppc_ok' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs) | skip]
    850   | cases ppc_code in p1; -ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; -EQppc_code
    851     * * #IH1 #IH3 #IH2 whd % [%
     853  | * #sigma_pol_ok1 #sigma_pol_ok2 #instr_list_ok cases ppc_code in p1; -ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; -EQppc_code
     854    #IH cases (IH ? instr_list_ok) [2: % assumption ] * #IH1 #IH3 #IH2 whd % [%
    852855    [ >length_append normalize nodelta >IH1 (*CSC: TRUE, LEMMA NEEDED *) cases daemon
    853856    |2: (*CSC: NEES JAAP INVARIANT*) cases daemon]]
Note: See TracChangeset for help on using the changeset viewer.