Changeset 2188 for src/ASM


Ignore:
Timestamp:
Jul 16, 2012, 11:28:11 PM (7 years ago)
Author:
sacerdot
Message:
  1. Policy specification generalized
  2. All invariants but the main one closed again under weaker specification
File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Assembly.ma

    r2161 r2188  
    709709     (nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction < 2^16
    710710     ∨
    711      S (nat_of_bitvector … ppc) = |instr_list| ∧
     711     (∀ppc'. ∀ppc_ok':nat_of_bitvector … ppc' < |instr_list|. nat_of_bitvector … ppc < nat_of_bitvector … ppc' →
     712       let instruction' ≝ \fst (fetch_pseudo_instruction instr_list ppc' ppc_ok') in
     713       instruction_size lookup_labels sigma policy ppc' instruction' = 0)
     714     ∧
    712715     nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction = 2^16).
    713716
    … …  
    893896         ppc = bitvector_of_nat … (|pre|) ∧
    894897         |code| ≤ 2^16 ∧
    895          (|code| = 2^16 → |pre| = |instr_list|) ∧
     898         True(*(ppc = zero … → code = [])*) ∧
    896899         (nat_of_bitvector … (sigma ppc) = |code| ∨
    897           sigma ppc = zero … ∧ |code| = 2^16) ∧
     900          sigma ppc = zero … ∧ |code| = 2^16 ∧
     901          (|pre| < 2^16 → ∀ppc'. ∀ppc_ok':nat_of_bitvector … ppc' < |instr_list|. nat_of_bitvector … ppc ≤ nat_of_bitvector … ppc' →
     902            let instruction' ≝ \fst (fetch_pseudo_instruction instr_list ppc' ppc_ok') in
     903            instruction_size lookup_labels sigma policy ppc' instruction' = 0)
     904         ) ∧
    898905         ∀ppc'.∀ppc_ok'.
    899906          (nat_of_bitvector … ppc' < nat_of_bitvector … ppc ∨ |pre| = 2^16) →
    … …  
    917924  [ cases (foldl_strong ? (λx.Σy.?) ???) in p1; #ignore_revcode #Hfold #EQignore_revcode
    918925    >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok
    919     cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * * #Hfold1 #Hfold4 #Hfold5 #Hfold3 #Hfold2 whd
     926    cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * * #Hfold1 #Hfold4 #_ #Hfold5 #Hfold3 whd
    920927    <eq_create_label_cost_map whd %
    921     [2: #ppc #LTppc @Hfold2 >Hfold1 @(eqb_elim (|instr_list|) 2^16)
     928    [2: #ppc #LTppc @Hfold3 >Hfold1 @(eqb_elim (|instr_list|) 2^16)
    922929      [ #limit %2 @limit
    923930      | #nlimit %1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
    924931        @not_eq_to_le_to_lt assumption ]
    925     | >length_reverse % try assumption cases Hfold3 -Hfold3
    926       [ #Hfold3 <Hfold3 % >Hfold1 %
    927       | #Hfold5 %2 <Hfold1 assumption ]]
     932    | >length_reverse % try assumption cases Hfold5 -Hfold5
     933      [ #Hfold5 <Hfold5 % >Hfold1 %
     934      | * #Hfold51 #Hfold52 %2 <Hfold1 assumption ]]
    928935  | * #sigma_pol_ok1 #_ #instr_list_ok %
    929     [ % % [%] // [#abs change with (0=S ?) in abs; destruct(abs) | >sigma_pol_ok1 % ]]
     936    [ % % [%] // >sigma_pol_ok1 % ]
    930937    #ppc' #ppc_ok' #abs @⊥ cases abs
    931938     [#abs2 cases (not_le_Sn_O ?) [#H @(H abs2) | skip]
    … …  
    933940  | * #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
    934941    #IH cases (IH ? instr_list_ok) [2: % assumption ] -IH
    935     * * * #IH1 #IH2 #IH4 *
    936     [2: * #_ #H @⊥ lapply (IH4 H) >prf >length_append
    937         >(plus_n_O (|prefix|)) in ⊢ (??%? → ?); #X
    938         lapply (injective_plus_r … X) >length_append normalize #abs' destruct(abs')]
    939     #IH3 #IH5
     942    * * * #IH1 #IH2 #IH2' #IH3 #IH4
    940943    cut (|prefix| < |instr_list|)
    941944    [ >prf >length_append normalize <plus_n_Sm @le_S_S // ] #LT_prefix_instr_list
    … …  
    963966      >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels [ >p2 | skip] % ]
    964967    #EQpc_delta2
    965     cases (sigma_pol_ok2 … ppc_ok) -sigma_pol_ok2
     968    cases (sigma_pol_ok2 … ppc_ok)
    966969    <eq_fetch_pseudo_instruction <eq_create_label_cost_map <EQpc_delta2
    967970    #sigma_pol3 #sigma_pol4
    968971    % [ % [% [% ] ] ]
    969972    [ >length_append normalize nodelta >IH1 @sym_eq @add_bitvector_of_nat
    970     | >length_append >length_reverse <IH3 <EQpc_delta >commutative_plus
    971       cases sigma_pol4 [ #LT @(transitive_le … LT) // | * #_ #EQ >EQ % ]
    972     | >length_append >commutative_plus >length_reverse <IH3 <EQpc_delta
     973    | >length_append >length_reverse <EQpc_delta
     974      cases IH3 -IH3
     975      [ #IH3 <IH3 >commutative_plus
     976        cases sigma_pol4 [ #LT @(transitive_le … LT) // | * #_ #EQ >EQ % ]
     977      | * * #IH3a #IH3b #IH3c >IH3b <EQpc_delta >EQpc_delta2 >eq_fetch_pseudo_instruction
     978        >IH3c try % assumption ]
     979(*        cut (ppc ≠ zero …)
     980        [% #EQppc_zero @(absurd … IH3b) >IH2' [ @not_eq_O_S ] assumption ] #Not_eq_ppc_zero
     981        cut (bitvector_of_nat ? (S (pred (nat_of_bitvector … ppc))) = ppc)
     982        [ inversion (nat_of_bitvector … ppc)
     983          [2: #p #_ #H normalize in match (pred ?);
     984              lapply(eq_f … (bitvector_of_nat 16) … H) >bitvector_of_nat_inverse_nat_of_bitvector
     985              #H' <H' %
     986          | #H @⊥
     987            lapply(eq_f … (bitvector_of_nat 16) … H) >bitvector_of_nat_inverse_nat_of_bitvector
     988            #H' @(absurd ?? Not_eq_ppc_zero) >H' % ]] #EQppc lapply ppc_ok; <EQppc #S_pred_ppc_ok
     989        cases (sigma_pol_ok2 (bitvector_of_nat 16 (pred (nat_of_bitvector 16 ppc))) ?)
     990        [2: @(transitive_lt … ppc_ok) >nat_of_bitvector_bitvector_of_nat_inverse
     991            [2: cases daemon (*CSC: True *) | cases daemon (*CSC: True*) ]
     992        | #Sigma_pol1 *
     993          [ cases daemon (*??????????*)
     994          | * #Sigma_pol2 #Sigma_pol3 lapply (Sigma_pol2 … S_pred_ppc_ok ?)
     995            [ cases daemon (*CSC: True *) ]
     996            whd in ⊢ (% → ?); <eq_create_label_cost_map #H >H % ]]]*)
     997    | %(* >length_append >commutative_plus >length_reverse <IH3 <EQpc_delta
    973998       #abs >abs in sigma_pol4; *
    974999       [ #abs' cases (absurd ? abs' (not_le_Sn_n …))
    9751000       | * #abs' #_ <abs' >length_append <plus_n_Sm <plus_n_O @eq_f >IH1
    976          >nat_of_bitvector_bitvector_of_nat_inverse // ]
    977     | >length_append >length_reverse <IH3 <EQpc_delta cases sigma_pol4
    978       [ #LT %1 >sigma_pol3 >nat_of_bitvector_add
    979         [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption]
    980         >nat_of_bitvector_bitvector_of_nat_inverse try assumption //
    981       | * #EQ1 #EQ2 %2 %
    982         [ lapply (eq_f … (bitvector_of_nat 16) … EQ2) <add_bitvector_of_nat_plus
    983           >bitvector_of_nat_inverse_nat_of_bitvector <sigma_pol3 #X >X @bitvector_of_nat_exp_zero
    984         | >commutative_plus assumption ]]
     1001         >nat_of_bitvector_bitvector_of_nat_inverse // ]*)
     1002    | >length_append >length_reverse
     1003      cases IH3 -IH3
     1004      [ #IH3 <IH3 <EQpc_delta cases sigma_pol4
     1005        [ #LT %1 >sigma_pol3 >nat_of_bitvector_add
     1006          [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption]
     1007          >nat_of_bitvector_bitvector_of_nat_inverse try assumption //
     1008        | * #EQ1 #EQ2 %2 %
     1009          [ lapply (eq_f … (bitvector_of_nat 16) … EQ2) <add_bitvector_of_nat_plus
     1010            >bitvector_of_nat_inverse_nat_of_bitvector <sigma_pol3 #X >X % //
     1011          | #LLT_prefix
     1012            cut (S (nat_of_bitvector … ppc) < 2^16)
     1013            [ >length_append in LLT_prefix; <plus_n_Sm <plus_n_O #LLT_prefix
     1014              >IH1 >nat_of_bitvector_bitvector_of_nat_inverse assumption ]
     1015            -LLT_prefix #LLT_prefix
     1016            #ppc' #ppc_ok' #LEQ_newppc_ppc' whd >EQ1 try %
     1017            @(lt_to_le_to_lt … LEQ_newppc_ppc') normalize nodelta
     1018            >nat_of_bitvector_add >nat_of_bitvector_bitvector_of_nat_inverse // ]]
     1019      | * * #IH5 #IH6 #IH7 %2 % [% ]
     1020        [ normalize nodelta >sigma_pol3 >IH5
     1021          >add_commutative <add_zero >nat_of_bitvector_bitvector_of_nat_inverse try assumption
     1022          >EQpc_delta2 >eq_fetch_pseudo_instruction >IH7 try % assumption
     1023        | >IH6 <EQpc_delta >EQpc_delta2 >eq_fetch_pseudo_instruction >IH7 try %
     1024          assumption
     1025        | #LLT_prefix
     1026          cut (S (nat_of_bitvector … ppc) < 2^16)
     1027          [ >length_append in LLT_prefix; <plus_n_Sm <plus_n_O #LLT_prefix
     1028            >IH1 >nat_of_bitvector_bitvector_of_nat_inverse assumption ]
     1029          -LLT_prefix #LLT_prefix
     1030          #ppc' #ppc_ok' #LEQ_newppc_ppc' whd @IH7 try assumption
     1031          @(transitive_le … LEQ_newppc_ppc') normalize nodelta
     1032          >nat_of_bitvector_add >nat_of_bitvector_bitvector_of_nat_inverse // ]]
    9851033  | #ppc' #LTppc' cases hd in prf p2 EQpc_delta2 eq_fetch_pseudo_instruction; #label #pi #prf #p2
    9861034    #EQpc_delta2 #eq_fetch_pseudo_instruction *
    987     [2: #eq_S_prefix_bound (*@(IH5 ? LTppc')
     1035    [2: #eq_S_prefix_bound
     1036      cut (instr_list = prefix @ [〈label,pi〉 ]) [ cases daemon (*CSC: easy *) ] #EQinstr_list
    9881037      @pair_elim #pi' #newppc' #eq_fetch_pseudo_instruction'
    989       @pair_elim*) cases daemon
     1038      @pair_elim #len #assembledi #eq_assembly_1_pseudoinstruction %
     1039      [
     1040      |
     1041      ]
    9901042    | #LTppc_ppc
    9911043      cases (le_to_or_lt_eq … LTppc_ppc)
    … …  
    10051057          [2,4: @(lt_to_le_to_lt … LTj) <EQpc_delta @(transitive_le … pc_delta_ok) %2 %
    10061058          |3: (*CSC: TRUE, NEEDS LEMMA *) cases daemon ]
    1007           >reverse_append >reverse_reverse >IH3 <(length_reverse … code)
    1008           @nth_safe_prepend
     1059          >reverse_append >reverse_reverse
     1060          cases IH3 -IH3
     1061          [ #IH3 >IH3 <(length_reverse … code) @nth_safe_prepend
     1062          | cases daemon (*CSC: ?????????? *) ]
    10091063      | #LTppc''
    10101064        cut (nat_of_bitvector … ppc' < |instr_list|)
    … …  
    10251079                  @(transitive_le … H) //
    10261080              | @le_S_S //*) ]]]]
    1027       #X lapply (IH5 ppc' X)
     1081      #X lapply (IH4 ppc' X)
    10281082      @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction
    10291083      @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH
    … …  
    10351089      | #j #LTj >reverse_append >reverse_reverse #K
    10361090        >IH
    1037         [2: >length_reverse <IH3 (*CSC: USE MONOTONICITY *) cases daemon
     1091        [2: >length_reverse (*CSC: ?????????? <IH3 (*CSC: USE MONOTONICITY *)*) cases daemon
    10381092        | @shift_nth_prefix ]]]]]
    10391093(*        |3: @le_S_S_to_le @(transitive_le … LTppc'') >nat_of_bitvector_add
    … …  
    10451099               [ // | <p_refl in instr_list_ok; >prf >length_append #H @(transitive_le … H) // ]]]]
    10461100*)
     1101cases daemon
    10471102qed.
    10481103
Note: See TracChangeset for help on using the changeset viewer.