Changeset 2199


Ignore:
Timestamp:
Jul 17, 2012, 5:40:00 PM (5 years ago)
Author:
sacerdot
Message:

No longer used lemma containing the last daemon removed.
The proof is now fully finished up to commutations.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2197 r2199  
    851851| #dptr #id normalize in ⊢ (?%?); //
    852852]
    853 qed.
    854 
    855 lemma 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    ]]
    896853qed.
    897854
Note: See TracChangeset for help on using the changeset viewer.