Changeset 2110 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jun 26, 2012, 4:05:15 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2108 r2110  
    801801(*CSC: move elsewhere *)
    802802lemma fetch_pseudo_instruction_append:
    803  ∀l1,l2. |l1@l2| < 2^16 → ∀ppc,ppc_ok,ppc_ok'.
     803 ∀l1,l2. |l1@l2| 2^16 → ∀ppc,ppc_ok,ppc_ok'.
    804804  let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
    805805  fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
     
    807807 #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
    808808 cut (|l1| + nat_of_bitvector … ppc < 2^16)
    809  [ @(transitive_lt … l1l2_ok) >length_append /2 by monotonic_lt_plus_r/ ]
     809 [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ]
    810810 -l1l2_ok #l1ppc_ok >nat_of_bitvector_add
    811811 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
     
    833833       ∨ (nat_of_bitvector … ppc = |instr_list| → next_pc = (zero …))).
    834834
     835(*CSC: Move elsewhere *)
     836axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n.
     837
    835838definition assembly:
    836839    ∀p: pseudo_assembly_program.
     
    840843       sigma_policy_specification p sigma policy →
    841844       let 〈preamble,instr_list〉 ≝ p in
    842        |instr_list| < 2^16 →
     845       |instr_list| 2^16 →
    843846       let 〈assembled,costs〉 ≝ res in
     847       |assembled| ≤ 2^16 ∧
    844848       let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
    845849       let datalabels ≝ construct_datalabels preamble in
    846        let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in
     850       let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in
    847851       let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
    848852       ∀ppc. ∀ppc_ok:nat_of_bitvector … ppc < |instr_list|.
     
    861865  let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
    862866  let datalabels ≝ construct_datalabels preamble in
    863   let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in
     867  let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in
    864868  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
    865869  let 〈ignore,revcode〉 ≝ pi1 … (
     
    868872      (λpre. Σppc_code:(Word × (list Byte)).
    869873       sigma_policy_specification 〈preamble,instr_list〉 sigma policy →
    870         |instr_list| < 2^16 →
     874        |instr_list| 2^16 →
    871875        let 〈ppc,code〉 ≝ ppc_code in
    872876         ppc = bitvector_of_nat … (|pre|) ∧
    873877         nat_of_bitvector … (sigma ppc) = |code| ∧
    874878         ∀ppc'.∀ppc_ok'.
    875           nat_of_bitvector … ppc' < nat_of_bitvector … ppc
     879          (nat_of_bitvector … ppc' < nat_of_bitvector … ppc ∨ |pre| = 2^16)
    876880           let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' ppc_ok' in
    877881           let 〈len,assembledi〉 ≝
     
    892896  [ cases (foldl_strong ? (λx.Σy.?) ???) in p2; #ignore_revcode #Hfold #EQignore_revcode
    893897    >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok
    894     cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * #Hfold1 #Hfold3 #Hfold2 whd >p1 whd #ppc #LTppc @Hfold2
    895     >Hfold1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
     898    cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * #Hfold1 #Hfold3 #Hfold2 whd >p1 whd %
     899    [2: #ppc #LTppc @Hfold2 >Hfold1 @(eqb_elim (|instr_list|) 2^16)
     900      [ #limit %2 @limit
     901      | #nlimit %1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
     902        @not_eq_to_le_to_lt assumption ]
     903    | >length_reverse <Hfold3
     904      @(transitive_le … (S (nat_of_bitvector … (sigma ignore))))
     905      [ // | change with (? < ?); @lt_nat_of_bitvector ]]
    896906  | * #sigma_pol_ok1 #_ #instr_list_ok %
    897907    [ % // >sigma_pol_ok1 % ]
    898     #ppc' #ppc_ok' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs) | skip]
     908    #ppc' #ppc_ok' #abs @⊥ cases abs
     909     [#abs2 cases (not_le_Sn_O ?) [#H @(H abs2) | skip]
     910     |#abs2 change with (0 = S ?) in abs2; destruct(abs2) ]
    899911  | * #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
    900912    #IH cases (IH ? instr_list_ok) [2: % assumption ] * #IH1 #IH3 #IH2 whd % [%
    901913    [ >length_append normalize nodelta >IH1 (*CSC: TRUE, LEMMA NEEDED *) cases daemon
    902914    |2: (*CSC: NEES JAAP INVARIANT*) cases daemon]]
    903     #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 #LTppc_ppc
    904     cases (le_to_or_lt_eq … LTppc_ppc)
    905     [2: #S_S_eq normalize nodelta in S_S_eq;
    906         (*CSC: TRUE, NEEDS SOME WORK *)
    907         cut (ppc' = ppc) [ cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc'  >prf
    908         >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc lapply LTppc
    909         >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → match % with [_ ⇒ ?]);
    910         >fetch_pseudo_instruction_append
    911         [3: @le_S_S @le_O_n
    912         |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H
    913         |4: <prf <p_refl in instr_list_ok; #H @H ]
    914         #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2
    915         #j #LTj >nat_of_bitvector_add
    916         >nat_of_bitvector_bitvector_of_nat_inverse
    917         [2,4: (* CSC: TRUE, NEEDS LEMMA, MAYBE ALREADY PROVED *) cases daemon
    918         |3: (*CSC: TRUE, NEEDS LEMMA *) cases daemon ]
    919         >reverse_append >reverse_reverse >IH3 <(length_reverse … code)
    920         @nth_safe_prepend
    921     | #LTppc''
    922       cut (nat_of_bitvector … ppc' < |instr_list|)
    923       [ normalize nodelta in LTppc'';
    924         @(transitive_le … (nat_of_bitvector … ppc))
    925         [2: >IH1 >prf >length_append >nat_of_bitvector_bitvector_of_nat_inverse
    926            [ //
    927            | <p_refl in instr_list_ok; #instr_list_ok
    928              @(transitive_le … (S (|instr_list|))) try assumption >prf >length_append // ]
    929         | @le_S_S_to_le >nat_of_bitvector_add in LTppc'';
    930           [ >commutative_plus #H @H
    931           | >nat_of_bitvector_bitvector_of_nat_inverse [2: // ] >commutative_plus
    932             @(transitive_le … (S (|instr_list|)))
    933             [2: <p_refl in instr_list_ok;  #instr_list_ok assumption
    934             | >IH1 >prf >length_append @le_S_S >(commutative_plus (|prefix|))
    935               >length_append >nat_of_bitvector_bitvector_of_nat_inverse
    936               [2: <p_refl in instr_list_ok; >prf >length_append #H
    937                   @(transitive_le … H) //
    938               | @le_S_S // ]]]]]
     915    #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 *
     916    cases daemon (*
     917    ?????????????? PRIMA NON C'ERA L'OR :-(
     918    MANTENERE LO SCHEMA DI PRIMA CON DUE CASI, MA IN UN CASO ppc=0 OVERFLOWED
     919    [2: #eq_S_prefix_bound -IH @(IH2 ? LTppc')
     920      @pair_elim #pi' #newppc' #eq_fetch_pseudo_instruction'
     921      @pair_elim
     922    | #LTppc_ppc
     923      cases (le_to_or_lt_eq … LTppc_ppc)
     924      [2: #S_S_eq normalize nodelta in S_S_eq;
     925          (*CSC: TRUE, NEEDS SOME WORK *)
     926          cut (ppc' = ppc) [ cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc'  >prf
     927          >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc lapply LTppc
     928          >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → match % with [_ ⇒ ?]);
     929          >fetch_pseudo_instruction_append
     930          [3: @le_S_S @le_O_n
     931          |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H
     932          |4: <prf <p_refl in instr_list_ok; #H @H ]
     933          #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2
     934          #j #LTj >nat_of_bitvector_add
     935          >nat_of_bitvector_bitvector_of_nat_inverse
     936          [2,4: (* CSC: TRUE, NEEDS LEMMA, MAYBE ALREADY PROVED *) cases daemon
     937          |3: (*CSC: TRUE, NEEDS LEMMA *) cases daemon ]
     938          >reverse_append >reverse_reverse >IH3 <(length_reverse … code)
     939          @nth_safe_prepend
     940      | #LTppc''
     941        cut (nat_of_bitvector … ppc' < |instr_list|)
     942        [ normalize nodelta in LTppc'';
     943          @(transitive_le … (nat_of_bitvector … ppc))
     944          [2: >IH1 >prf >length_append >nat_of_bitvector_bitvector_of_nat_inverse
     945             [ //
     946             | <p_refl in instr_list_ok; #instr_list_ok
     947               @(transitive_le … (S (|instr_list|))) try assumption >prf >length_append // ]
     948          | @le_S_S_to_le >nat_of_bitvector_add in LTppc'';
     949            [ >commutative_plus #H @H
     950            | >nat_of_bitvector_bitvector_of_nat_inverse [2: // ] >commutative_plus
     951              @(transitive_le … (|instr_list|))
     952              [2: <p_refl in instr_list_ok;  #instr_list_ok assumption
     953              | >IH1 >prf >length_append @le_S_S >(commutative_plus (|prefix|))
     954                >length_append >nat_of_bitvector_bitvector_of_nat_inverse
     955                [2: <p_refl in instr_list_ok; >prf >length_append #H
     956                    @(transitive_le … H) //
     957                | @le_S_S // ]]]]]
    939958      #X lapply (IH2 ppc' X)
    940959      @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction
     
    952971           | >prf >length_append >length_append <plus_n_Sm >nat_of_bitvector_bitvector_of_nat_inverse
    953972             [ // | <p_refl in instr_list_ok; >prf >length_append #H @(transitive_le … H) // ]]]]
    954 qed.
     973*)qed.
    955974
    956975definition assembly_unlabelled_program:
Note: See TracChangeset for help on using the changeset viewer.