Ignore:
Timestamp:
Jul 3, 2012, 6:12:24 PM (8 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)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.