Changeset 2151


Ignore:
Timestamp:
Jul 3, 2012, 6:12:24 PM (6 years ago)
Author:
sacerdot
Message:
  1. Lemmas from AssemblyProof? anticipated to Assembly.ma
  2. Jaap's specification strengthened again a little bit (for simplicity of use)
  3. 3/4 of the proof in Assembly.ma closed (up to 3 daemons)
Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Assembly.ma

    r2148 r2151  
    708708     ∧
    709709     (nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction < 2^16
    710       (*nat_of_bitvector … pc < nat_of_bitvector … next_pc*) ∨
    711       S (nat_of_bitvector … ppc) = |instr_list| ∧ next_pc = zero …).
     710     ∨
     711     S (nat_of_bitvector … ppc) = |instr_list| ∧
     712     nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction = 2^16).
     713
     714
     715(*CSC: move elsewhere*)
     716axiom add_bitvector_of_nat:
     717 ∀n,m1,m2.
     718  bitvector_of_nat n (m1 + m2) =
     719   add n (bitvector_of_nat n m1) (bitvector_of_nat n m2).
     720
     721lemma fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels:
     722 ∀lookup_labels,sigma,policy,ppc,pi.
     723  ∀lookup_datalabels1,lookup_datalabels2.
     724   \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels1 pi) =
     725   \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels2 pi).
     726#lookup_labels #sigma #policy #ppc #pi #lookup_datalabels1 #lookup_datalabels2
     727cases pi //
     728qed.
     729
     730lemma fst_snd_assembly_1_pseudoinstruction:
     731 ∀lookup_labels,sigma,policy,ppc,pi,lookup_datalabels,len,assembled.
     732   assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi
     733   = 〈len,assembled〉 →
     734    len = |assembled|.
     735#lookup #sigma #policy #ppc #pi #lookup_datalabels #len #assembled
     736inversion (assembly_1_pseudoinstruction ??????) #len' #assembled'
     737whd in ⊢ (??%? → ?); #EQ1 #EQ2 destruct %
     738qed.
    712739
    713740definition assembly:
    … …  
    736763           nth_safe ? (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat ? j)))
    737764            assembled K
    738 ≝ ?. cases daemon(*
     765≝
    739766  λp.
    740767  λsigma.
    741768  λpolicy.
    742769  deplet 〈preamble, instr_list〉 as p_refl ≝ p in
    743   let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
     770  deplet 〈labels_to_ppc,ppc_to_costs〉 as eq_create_label_cost_map ≝ create_label_cost_map instr_list in
    744771  let datalabels ≝ construct_datalabels preamble in
    745772  let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in
    … …  
    753780        let 〈ppc,code〉 ≝ ppc_code in
    754781         ppc = bitvector_of_nat … (|pre|) ∧
     782         |code| ≤ 2^16 ∧
    755783         (nat_of_bitvector … (sigma ppc) = |code| ∨
    756784          sigma ppc = zero … ∧ |code| = 2^16) ∧
    … …  
    760788           let 〈len,assembledi〉 ≝
    761789            assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in
     790           |assembledi| ≤ |reverse … code| ∧
    762791           ∀j:nat. ∀H: j < |assembledi|. ∀K.
    763792            nth_safe ? j assembledi H =
    … …  
    773802     〈reverse … revcode,
    774803      fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉.
    775   [ cases (foldl_strong ? (λx.Σy.?) ???) in p2; #ignore_revcode #Hfold #EQignore_revcode
     804  [ cases (foldl_strong ? (λx.Σy.?) ???) in p1; #ignore_revcode #Hfold #EQignore_revcode
    776805    >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok
    777     cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * #Hfold1 #Hfold3 #Hfold2 whd >p1 whd %
     806    cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * #Hfold1 #Hfold4 #Hfold3 #Hfold2 whd
     807    <eq_create_label_cost_map whd %
    778808    [2: #ppc #LTppc @Hfold2 >Hfold1 @(eqb_elim (|instr_list|) 2^16)
    779809      [ #limit %2 @limit
    780810      | #nlimit %1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
    781811        @not_eq_to_le_to_lt assumption ]
    782     | >length_reverse <Hfold3 %
    783       [ @(transitive_le … (S (nat_of_bitvector … (sigma next_pc))))
    784         [ // | change with (? < ?); @lt_nat_of_bitvector ]
    785       | >Hfold1 % ]]
     812    | >length_reverse % try assumption cases Hfold3 -Hfold3
     813      [ #Hfold3 <Hfold3 % >Hfold1 %
     814      | #Hfold5 %2 <Hfold1 assumption ]]
    786815  | * #sigma_pol_ok1 #_ #instr_list_ok %
    787     [ % // >sigma_pol_ok1 % ]
     816    [ % % // >sigma_pol_ok1 % ]
    788817    #ppc' #ppc_ok' #abs @⊥ cases abs
    789818     [#abs2 cases (not_le_Sn_O ?) [#H @(H abs2) | skip]
    790819     |#abs2 change with (0 = S ?) in abs2; destruct(abs2) ]
    791820  | * #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
    792     #IH cases (IH ? instr_list_ok) [2: % assumption ] * #IH1 #IH3 #IH2 whd % [%
     821    #IH cases (IH ? instr_list_ok) [2: % assumption ] -IH
     822    * * #IH1 #IH2 *
     823    [2: #H @⊥ cases daemon (*CSC: impossible case, using Jaaps's ? *)]
     824    #IH3 #IH5
     825    cut (|prefix| < |instr_list|)
     826    [ >prf >length_append normalize <plus_n_Sm @le_S_S // ] #LT_prefix_instr_list
     827    cut (|prefix| < 2^16)
     828    [ @(lt_to_le_to_lt … (|instr_list|)) assumption ] #prefix_ok
     829    cut (nat_of_bitvector … ppc < |instr_list|)
     830    [ >IH1 >nat_of_bitvector_bitvector_of_nat_inverse assumption ] #ppc_ok
     831    cut (\snd hd = \fst (fetch_pseudo_instruction instr_list ppc ppc_ok))
     832    [ >prf in ppc_ok; >IH1 >(add_zero … (bitvector_of_nat … (|prefix|)))
     833      >fetch_pseudo_instruction_append
     834      [ #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
     835        whd in match (nth_safe ????); [ cases hd // | normalize // ]
     836      | <add_zero >nat_of_bitvector_bitvector_of_nat_inverse
     837        [ <prf assumption | assumption ]
     838      | skip
     839      | <prf assumption
     840      ]] #eq_fetch_pseudo_instruction
     841    lapply (fst_snd_assembly_1_pseudoinstruction … p2) #EQpc_delta
     842    cut (pc_delta < 2^16)
     843    [cases daemon (*CSC: DA FARE*) ] #pc_delta_ok
     844    % [ % [% ] ]
     845    [ >length_append normalize nodelta >IH1 @sym_eq @add_bitvector_of_nat
     846    | >length_append >length_reverse <IH3 cases daemon (*CSC: maybe, using monotonicity*)
     847    | cases (sigma_pol_ok2 … ppc_ok)
     848      whd in match instruction_size; normalize nodelta >p2 <eq_fetch_pseudo_instruction
     849      <eq_create_label_cost_map
     850      >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels [ >p2 | skip]
     851      #sigma_ok >sigma_ok #sigma_pol_ok3 -sigma_pol_ok2
     852      >length_append >length_reverse <IH3 <EQpc_delta cases sigma_pol_ok3
     853      [ #LT %1 >nat_of_bitvector_add
     854        [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption]
     855        >nat_of_bitvector_bitvector_of_nat_inverse try assumption //
     856      | * #EQ1 #EQ2 %2 %
     857        [ lapply (eq_f … (bitvector_of_nat 16) … EQ2) <add_bitvector_of_nat_plus
     858          >bitvector_of_nat_inverse_nat_of_bitvector #X >X @bitvector_of_nat_exp_zero
     859        | >commutative_plus assumption ]]
     860  | cases daemon
     861  ]
     862   
     863(*   
     864   
     865     % [%
    793866    [ >length_append normalize nodelta >IH1 (*CSC: TRUE, LEMMA NEEDED *) cases daemon
    794867    |2: (*CSC: NEES JAAP INVARIANT*) cases daemon]]

  • src/ASM/AssemblyProof.ma

    r2149 r2151  
    179179    | _ ⇒ True
    180180    ].
    181 
    182 lemma fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels:
    183  ∀lookup_labels,sigma,policy,ppc,pi.
    184   ∀lookup_datalabels1,lookup_datalabels2.
    185    \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels1 pi) =
    186    \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels2 pi).
    187 #lookup_labels #sigma #policy #ppc #pi #lookup_datalabels1 #lookup_datalabels2
    188 cases pi //
    189 qed.
    190 
    191 lemma fst_snd_assembly_1_pseudoinstruction:
    192  ∀lookup_labels,sigma,policy,ppc,pi,lookup_datalabels,len,assembled.
    193    assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi
    194    = 〈len,assembled〉 →
    195     len = |assembled|.
    196 #lookup #sigma #policy #ppc #pi #lookup_datalabels #len #assembled
    197 inversion (assembly_1_pseudoinstruction ??????) #len' #assembled'
    198 whd in ⊢ (??%? → ?); #EQ1 #EQ2 destruct %
    199 qed.
    200181
    201182(* XXX: easy but tedious *)
    … …  
    355336     ]
    356337   | * #EQ1 #EQ2 %2 %
    357      [ <add_bitvector_of_nat_Sm >add_commutative assumption
     338     [ <add_bitvector_of_nat_Sm >add_commutative >H
     339       lapply (eq_f … (bitvector_of_nat 16) … EQ2)
     340       <add_bitvector_of_nat_plus
     341       >bitvector_of_nat_inverse_nat_of_bitvector #X >X @bitvector_of_nat_exp_zero
    358342     | <(nat_of_bitvector_bitvector_of_nat_inverse 16 m) try assumption
    359343     ]]]
    … …  
    437421          [2: * #EQ1 #EQ2 @⊥ <EQ1 in EQlen_assembled';
    438422              <add_bitvector_of_nat_Sm >add_commutative
    439               >bitvector_of_nat_inverse_nat_of_bitvector >OK >EQ2 assumption ]
     423              >bitvector_of_nat_inverse_nat_of_bitvector >OK >EQ2
     424              lapply (eq_f … (bitvector_of_nat 16) … EQ2) -EQ2
     425              <add_bitvector_of_nat_plus >bitvector_of_nat_inverse_nat_of_bitvector
     426              #X >X #Y @NOT_EMPTY <Y >bitvector_of_nat_exp_zero % ]
    440427          cases (le_to_or_lt_eq … instr_list_ok)
    441428          [2: #abs @⊥ >abs in EQlen_assembled'; >bitvector_of_nat_exp_zero >sigma_zero
Note: See TracChangeset for help on using the changeset viewer.