Changeset 2194


Ignore:
Timestamp:
Jul 17, 2012, 10:18:01 AM (5 years ago)
Author:
sacerdot
Message:
  1. monotone moved to Assembly
  2. some easier daemons, one shows an impossible case and needs more work
Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2193 r2194  
    853853qed.
    854854
     855lemma monotone_sigma:
     856 ∀program. |\snd program| ≤ 2^16 →
     857 ∀sigma: Word → Word. ∀policy: Word → bool.
     858  sigma_policy_specification program sigma policy →
     859   ∀ppc1,ppc2.
     860    nat_of_bitvector … ppc2 ≤ |\snd program| →
     861    nat_of_bitvector … ppc1 ≤ nat_of_bitvector … ppc2 →
     862     (nat_of_bitvector … (sigma ppc1) ≤ nat_of_bitvector … (sigma ppc2) ∨
     863      sigma ppc2 = zero …).
     864 #program #program_bounded #sigma #policy * #SIGMAOK1 #SIGMAOK2 #ppc1 #ppc2
     865 #ppc2_ok #LE
     866 <(bitvector_of_nat_inverse_nat_of_bitvector … ppc1)
     867 <(bitvector_of_nat_inverse_nat_of_bitvector … ppc2)
     868 lapply (le_n … (nat_of_bitvector … ppc2))
     869 elim LE in ⊢ (?%? → %);
     870 [ #_ % %
     871 | #m #LE_ppc1_m #IH #BOUNDED
     872   cases (IH ?)
     873   [3: @(transitive_le … BOUNDED) %2 %
     874   |2: #eq_zero %2 cases daemon (*CSC: True from spec *) ]
     875   -IH #IH
     876   cut (m < |\snd program|) [ @(lt_to_le_to_lt … ppc2_ok) assumption ] #LT1
     877   cut (m < 2^16) [ @(lt_to_le_to_lt … program_bounded) assumption ] #LT2
     878   cases (SIGMAOK2 (bitvector_of_nat … m) ?) -SIGMAOK2
     879   [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption ]
     880   #H *
     881   [ #LTsigma_m %1 @(transitive_le … IH) -IH
     882     <add_bitvector_of_nat_Sm >add_commutative >H -H
     883     >nat_of_bitvector_add
     884     [ //
     885     | >nat_of_bitvector_bitvector_of_nat_inverse try assumption lapply LTsigma_m
     886       whd in match instruction_size; normalize nodelta
     887       inversion (assembly_1_pseudoinstruction ??????) #len #assembled #EQ #X
     888       @(transitive_le … X) @le_S_S //
     889     ]
     890   | * #EQ1 #EQ2 %2
     891     <add_bitvector_of_nat_Sm >add_commutative >H
     892     lapply (eq_f … (bitvector_of_nat 16) … EQ2)
     893     <add_bitvector_of_nat_plus
     894     >bitvector_of_nat_inverse_nat_of_bitvector #X >X @bitvector_of_nat_exp_zero
     895   ]]
     896qed.
     897
    855898definition assembly:
    856899    ∀p: pseudo_assembly_program.
     
    937980     [#abs2 cases (not_le_Sn_O ?) [#H @(H abs2) | skip]
    938981     |#abs2 change with (0 = S ?) in abs2; destruct(abs2) ]
    939   | * #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
     982  | #sigma_pol_ok cases sigma_pol_ok #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
    940983    #IH cases (IH ? instr_list_ok) [2: % assumption ] -IH
    941984    * * #IH1 #IH2 #IH3 #IH4
     
    10081051          >nat_of_bitvector_add >nat_of_bitvector_bitvector_of_nat_inverse // ]]
    10091052  | #ppc' #LTppc' cases hd in prf p2 EQpc_delta2 eq_fetch_pseudo_instruction; #label #pi #prf #p2
    1010     #EQpc_delta2 #eq_fetch_pseudo_instruction #OR_lt_eq
    1011     cut (ppc' = ppc ∨ ppc' ≠ ppc) [cases daemon (*CSC: True*)] *
     1053    #EQpc_delta2 #eq_fetch_pseudo_instruction #OR_lt_eq @(eq_bv_elim … ppc' ppc)
    10121054    [ #EQppc' >EQppc' in LTppc'; -ppc' >prf
    10131055      >IH1 #LTppc lapply LTppc
     
    10721114      | #j #LTj >reverse_append >reverse_reverse #K
    10731115        >IH
    1074         [2: >length_reverse (*CSC: ?????????? <IH3 (*CSC: USE MONOTONICITY *)*) cases daemon
    1075         | @shift_nth_prefix ]]]]]
     1116        [ @shift_nth_prefix
     1117        | >length_reverse
     1118          @(lt_to_le_to_lt …
     1119            (nat_of_bitvector … (add … (sigma ppc') (bitvector_of_nat … (|assembledi'|)))))
     1120          [ @lt_to_lt_nat_of_bitvector_add try assumption
     1121            [ cases daemon (*CSC: True*)
     1122            | cases daemon (*CSC: True*)
     1123            ]
     1124          | cases IH3 -IH3
     1125            [ #eq_code <eq_code
     1126              @(transitive_le … (nat_of_bitvector … (sigma (add …  ppc' (bitvector_of_nat … 1)))))
     1127              [ cases daemon (*CSC: True*)
     1128              | cases (monotone_sigma … sigma_pol_ok … (add … ppc' (bitvector_of_nat … 1)) ppc ??)
     1129                try assumption
     1130                [ #X @X
     1131                | cases daemon (*CSC: False, sigma ppc = zero! *)
     1132                | @(transitive_le … ppc_ok) %2 %
     1133                | cases daemon (*CSC: True*)
     1134                ]]
     1135            | * * #_ #relevant #_ >relevant
     1136              @(transitive_le … (S ?) … (lt_nat_of_bitvector …)) [%2 % | skip]]]
     1137        ]]]]]
    10761138qed.
    10771139
  • src/ASM/AssemblyProof.ma

    r2160 r2194  
    179179    | _ ⇒ True
    180180    ].
    181 
    182 lemma monotone_sigma:
    183  ∀program. |\snd program| ≤ 2^16 →
    184  ∀sigma: Word → Word. ∀policy: Word → bool.
    185   sigma_policy_specification program sigma policy →
    186    ∀ppc1,ppc2.
    187     nat_of_bitvector … ppc2 ≤ |\snd program| →
    188     nat_of_bitvector … ppc1 ≤ nat_of_bitvector … ppc2 →
    189      (nat_of_bitvector … (sigma ppc1) ≤ nat_of_bitvector … (sigma ppc2) ∨
    190       sigma ppc2 = zero … ∧ nat_of_bitvector … ppc2 = |\snd program|).
    191  #program #program_bounded #sigma #policy * #SIGMAOK1 #SIGMAOK2 #ppc1 #ppc2
    192  #ppc2_ok #LE
    193  <(bitvector_of_nat_inverse_nat_of_bitvector … ppc1)
    194  <(bitvector_of_nat_inverse_nat_of_bitvector … ppc2) in ⊢ (?%(?%?));
    195  lapply (le_n … (nat_of_bitvector … ppc2))
    196  elim LE in ⊢ (?%? → %);
    197  [ #_ % %
    198  | #m #LE_ppc1_m #IH #BOUNDED
    199    cases (IH ?)
    200    [3: @(transitive_le … BOUNDED) %2 %
    201    |2: * #_ #abs @⊥ <abs in ppc2_ok; #abs'
    202        @(absurd ?? (not_le_Sn_n m))
    203        @(transitive_le … BOUNDED abs') ]
    204    -IH #IH
    205    cut (m < |\snd program|) [ @(lt_to_le_to_lt … ppc2_ok) assumption ] #LT1
    206    cut (m < 2^16) [ @(lt_to_le_to_lt … program_bounded) assumption ] #LT2
    207    cases (SIGMAOK2 (bitvector_of_nat … m) ?) -SIGMAOK2
    208    [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption ]
    209    #H *
    210    [ #LTsigma_m %1 @(transitive_le … IH) -IH
    211      <add_bitvector_of_nat_Sm >add_commutative >H -H
    212      >nat_of_bitvector_add
    213      [ //
    214      | >nat_of_bitvector_bitvector_of_nat_inverse try assumption lapply LTsigma_m
    215        whd in match instruction_size; normalize nodelta
    216        inversion (assembly_1_pseudoinstruction ??????) #len #assembled #EQ #X
    217        @(transitive_le … X) @le_S_S //
    218      ]
    219    | * #EQ1 #EQ2 %2 %
    220      [ <add_bitvector_of_nat_Sm >add_commutative >H
    221        lapply (eq_f … (bitvector_of_nat 16) … EQ2)
    222        <add_bitvector_of_nat_plus
    223        >bitvector_of_nat_inverse_nat_of_bitvector #X >X @bitvector_of_nat_exp_zero
    224      | <(nat_of_bitvector_bitvector_of_nat_inverse 16 m) try assumption
    225      ]]]
    226 qed.
    227181
    228182(* This is a non trivial consequence of fetch_assembly_pseudo +
Note: See TracChangeset for help on using the changeset viewer.