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

Legend:

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