Changeset 2110


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

...

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

    r2108 r2110  
    15111511lemma assembly_ok:
    15121512  ∀program.
    1513   ∀length_proof: |\snd program| < 2^16.
     1513  ∀length_proof: |\snd program| 2^16.
    15141514  ∀sigma: Word → Word.
    15151515  ∀policy: Word → bool.
     
    15331533                  sigma newppc = add … pc (bitvector_of_nat … len).
    15341534  #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'
    1535   @pair_elim #preamble #instr_list #EQprogram
    15361535  cases (assembly program sigma policy) * #assembled' #costs''
    1537   >EQprogram normalize nodelta
    1538   @pair_elim #labels #costs #EQcreate_label_cost_refl normalize nodelta
    1539   #assembly_ok #Pair_eq destruct(Pair_eq) whd
    1540   #ppc #ppc_ok
    1541   @pair_elim #pi #newppc #EQfetch_pseudo_instruction
    1542   >EQprogram in sigma_policy_witness; #sigma_policy_witness
    1543   lapply (assembly_ok sigma_policy_witness ? ppc ?)
    1544   [2: >EQprogram in length_proof; #length_proof; assumption ] try assumption
    1545   >EQfetch_pseudo_instruction normalize nodelta
     1536  @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
     1537  cut (|instr_list| ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok
     1538  #H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
     1539  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
     1540  * #assembly_ok1 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
     1541  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
     1542  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
     1543  lapply (assembly_ok2 ppc ?) try // -assembly_ok2
     1544  >eq_fetch_pseudo_instruction
    15461545  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<|assembledi|.?) → ?)
    1547   @pair_elim #len #assembledi #EQassembly_1_pseudo_instruction
    1548   letin lookup_labels ≝ (λx.sigma (bitvector_of_nat 16 (lookup_def ASMTag ℕ labels x O)))
    1549   letin lookup_datalabels ≝ (λx. lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16))
    1550   >(? : assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi = 〈len,assembledi〉)
    1551   [2: <EQassembly_1_pseudo_instruction % ]
    1552   whd in ⊢ (% → ?); #assembly_ok %
    1553   [2: (*CSC: Use Jaap's invariant here *) cases daemon
    1554   |1:
    1555     lapply (load_code_memory_ok assembledi ?)
    1556     [1:
    1557       lapply sigma_policy_witness whd in match sigma_policy_specification;
    1558       normalize nodelta * #_ #relevant
    1559       (* XXX: wait for Jaap to propagate the property that program
    1560               is less than 2^16.
    1561        *)
     1546  > (?:((λx.bitvector_of_nat ? (lookup_def … labels x 0)) =
     1547       (λx.address_of_word_labels_code_mem instr_list x)))
     1548  [2: lapply (create_label_cost_map_ok 〈preamble,instr_list〉) >create_label_cost_refl
     1549      #H (*CSC: REQUIRES FUNCTIONAL EXTENSIONALITY; REPHRASE THE LEMMA *) cases daemon ]
     1550  >eq_assembly_1_pseudoinstruction
     1551  whd in ⊢ (% → ?); #assembly_ok
     1552  %
     1553  [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))
     1554      >snd_fetch_pseudo_instruction
     1555      cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) -H
     1556      #spw1 #_ >spw1 -spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f
     1557      >eq_fetch_pseudo_instruction whd in match instruction_size;
     1558      normalize nodelta (*CSC: TRUE, NEEDS LEMMA AND FUNCTIONAL EXTENSIONALITY *)
    15621559      cases daemon
    1563     ]
     1560  | lapply (load_code_memory_ok assembled' ?) [ assumption ]
    15641561    #load_code_memory_ok
    1565     cut (len=|assembledi|)
     1562    cut (len=|assembled|)
    15661563    [1: (*CSC: provable before cleaning *)
    15671564        cases daemon
     
    15691566    #EQlen
    15701567    (* Nice statement here *)
    1571     cut (∀j. ∀H: j < |assembledi|.
    1572           nth_safe Byte j assembledi H =
     1568    cut (∀j. ∀H: j < |assembled|.
     1569          nth_safe Byte j assembled H =
    15731570          \snd (next (load_code_memory assembled')
    15741571          (bitvector_of_nat 16
     
    15791576    |2:
    15801577      -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
    1581       elim assembledi
     1578      elim assembled
    15821579      [1:
    1583         #pc #_ whd (* <add_zero %
    1584        | #hd #tl #IH #pc #H %
     1580        #pc #_ whd <add_zero %
     1581      | #hd #tl #IH #pc #H %
    15851582         [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H
    15861583           >H -H whd in ⊢ (??%?); <add_zero //
    15871584         | >(?: add … pc (bitvector_of_nat … (S (|tl|))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (|tl|)))
    1588            [2: (*CSC: TRUE, ARITHMETIC*) cases daemon]
     1585           [2: <add_bitvector_of_nat_Sm @add_associative ]
    15891586           @IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
    1590            <(nth_safe_prepend … [hd] … LTj) #IH >IH
    1591            (*CSC: TRUE, ARITHMETICS*)
    1592            cases daemon
    1593          ]
    1594     ] *) cases daemon
    1595   ]
    1596   cases daemon
     1587           <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm
     1588           >add_associative % ]]
     1589  ]]
    15971590qed.
    15981591
     
    16001593lemma fetch_assembly_pseudo2:
    16011594  ∀program.
    1602   ∀length_proof: |\snd program| < 2^16.
     1595  ∀length_proof: |\snd program| 2^16.
    16031596  ∀sigma.
    16041597  ∀policy.
     
    19731966        match pol lookup_labels ppc with
    19741967        [ short_jump ⇒ 〈2, 2〉
    1975         | medium_jump ⇒ ?
     1968        | absolute_jump ⇒ ?
    19761969        | long_jump ⇒ 〈4, 4〉
    19771970        ] *)
     
    19791972        match pol lookup_labels ppc with
    19801973        [ short_jump ⇒ 〈2, 2〉
    1981         | medium_jump ⇒ ?
     1974        | absolute_jump ⇒ ?
    19821975        | long_jump ⇒ 〈4, 4〉
    19831976        ] *)
     
    19851978        match pol lookup_labels ppc with
    19861979        [ short_jump ⇒ 〈2, 2〉
    1987         | medium_jump ⇒ ?
     1980        | absolute_jump ⇒ ?
    19881981        | long_jump ⇒ 〈4, 4〉
    19891982        ] *)
     
    19911984        match pol lookup_labels ppc with
    19921985        [ short_jump ⇒ 〈2, 2〉
    1993         | medium_jump ⇒ ?
     1986        | absolute_jump ⇒ ?
    19941987        | long_jump ⇒ 〈4, 4〉
    19951988        ] *)
     
    19971990        match pol lookup_labels ppc with
    19981991        [ short_jump ⇒ 〈2, 2〉
    1999         | medium_jump ⇒ ?
     1992        | absolute_jump ⇒ ?
    20001993        | long_jump ⇒ 〈4, 4〉
    20011994        ] *)
     
    20031996        match pol lookup_labels ppc with
    20041997        [ short_jump ⇒ 〈2, 2〉
    2005         | medium_jump ⇒ ?
     1998        | absolute_jump ⇒ ?
    20061999        | long_jump ⇒ 〈4, 4〉
    20072000        ] *)
     
    20092002        match pol lookup_labels  ppc with
    20102003        [ short_jump ⇒ 〈2, 2〉
    2011         | medium_jump ⇒ ?
     2004        | absolute_jump ⇒ ?
    20122005        | long_jump ⇒ 〈4, 4〉
    20132006        ] *)
     
    20152008        match pol lookup_labels ppc with
    20162009        [ short_jump ⇒ 〈2, 2〉
    2017         | medium_jump ⇒ ?
     2010        | absolute_jump ⇒ ?
    20182011        | long_jump ⇒ 〈4, 4〉
    20192012        ] *)
     
    20212014        match pol lookup_labels ppc with
    20222015        [ short_jump ⇒ 〈2, 2〉
    2023         | medium_jump ⇒ ?
     2016        | absolute_jump ⇒ ?
    20242017        | long_jump ⇒ 〈4, 4〉
    20252018        ] *)
     
    23202313lemma snd_assembly_1_pseudoinstruction_ok:
    23212314  ∀program: pseudo_assembly_program.
    2322   ∀program_length_proof: |\snd program| < 2^16.
     2315  ∀program_length_proof: |\snd program| 2^16.
    23232316  ∀sigma: Word → Word.
    23242317  ∀policy: Word → bool.
  • src/ASM/AssemblyProofSplitSplit.ma

    r2062 r2110  
    8181qed.
    8282
    83 lemma medium_jump_cond_ok:
     83lemma absolute_jump_cond_ok:
    8484  ∀v1, v2: Word.
    8585  ∀is_possible, offset, v1_upper, v1_lower.
    86     〈is_possible, offset〉 = medium_jump_cond v1 v2 →
     86    〈is_possible, offset〉 = absolute_jump_cond v1 v2 →
    8787      〈v1_upper, v1_lower〉 = vsplit ? 5 11 v1 →
    8888        is_possible → v2 = v1_upper @@ offset.
    8989  #v1 #v2 #is_possible #offset #v1_upper #v1_lower
    90   whd in match medium_jump_cond; normalize nodelta
     90  whd in match absolute_jump_cond; normalize nodelta
    9191  @pair_elim #fst_5_addr #rest_addr #vsplit_v2_refl
    9292  @pair_elim #fst_5_pc #rest_pc #vsplit_v1_refl
     
    202202    inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
    203203    [2:
    204       inversion (medium_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
     204      inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
    205205      inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
    206206    ]
     
    240240        [1:
    241241          >EQlookup_labels in mjc_refl; #mjc_refl
    242           @(medium_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
     242          @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
    243243          >(andb_true_l … mj_possible_refl) @I
    244244        ]
Note: See TracChangeset for help on using the changeset viewer.