Changeset 2144


Ignore:
Timestamp:
Jul 2, 2012, 3:59:09 PM (5 years ago)
Author:
sacerdot
Message:
  1. Policy specification fixed
  2. Proof of monotonicity of sigma
Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2138 r2144  
    698698  λpolicy: Word → bool.
    699699  sigma (zero …) = zero … ∧
    700   ∀ppc: Word. ∀ppc_ok.
    701     let instr_list ≝ \snd program in
     700  let instr_list ≝ \snd program in
     701  ∀ppc: Word. ∀ppc_ok: nat_of_bitvector … ppc < |instr_list|.
    702702    let pc ≝ sigma ppc in
    703703    let labels ≝ \fst (create_label_cost_map instr_list) in
     
    705705    let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in
    706706    let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in
    707      (nat_of_bitvector … ppc ≤ |instr_list| →
    708        next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels sigma policy ppc instruction)))
    709      ∧       
    710       (  (nat_of_bitvector … ppc < |instr_list| → nat_of_bitvector … pc < nat_of_bitvector … next_pc)
    711        ∨ (nat_of_bitvector … ppc = |instr_list| → nat_of_bitvector … pc < nat_of_bitvector … next_pc ∨ next_pc = (zero …))).
     707     next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels sigma policy ppc instruction))
     708     ∧
     709     (nat_of_bitvector … pc < nat_of_bitvector … next_pc ∨
     710      nat_of_bitvector … ppc = |instr_list| ∧ next_pc = zero …).
    712711
    713712definition assembly:
  • src/ASM/AssemblyProof.ma

    r2143 r2144  
    340340qed.
    341341
     342(*CSC: move elsewhere *)
    342343lemma m_lt_1_to_m_refl_0:
    343344  ∀m: nat.
     
    351352
    352353(*CSC: move elsewhere*)         
    353 axiom lt_to_lt_nat_of_bitvector_add:
     354axiom le_to_le_nat_of_bitvector_add:
     355  ∀n,v,m1,m2.
     356    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 ≤ m2 →
     357      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) ≤
     358      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
     359
     360(*CSC: move elsewhere*)         
     361lemma lt_to_lt_nat_of_bitvector_add:
    354362  ∀n,v,m1,m2.
    355363    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 →
    356364      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <
    357365      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
     366#n #v #m1 #m2 #m2_ok #bounded #H
     367lapply (le_to_le_nat_of_bitvector_add n v (S m1) m2 ??) try assumption
     368#K @(transitive_le … (K H))
     369cases daemon (*CSC: TRUE, complete*)
     370qed.
     371
     372lemma monotone_sigma:
     373 ∀program. |\snd program| ≤ 2^16 →
     374 ∀sigma: Word → Word. ∀policy: Word → bool.
     375  sigma_policy_specification program sigma policy →
     376   ∀ppc1,ppc2.
     377    nat_of_bitvector … ppc1 < |\snd program| → nat_of_bitvector … ppc2 < |\snd program| →
     378    nat_of_bitvector … ppc1 ≤ nat_of_bitvector … ppc2 →
     379     nat_of_bitvector … (sigma ppc1) ≤ nat_of_bitvector … (sigma ppc2).
     380 #program #program_bounded #sigma #policy * #SIGMAOK1 #SIGMAOK2 #ppc1 #ppc2
     381 #ppc1_ok #ppc2_ok #LE
     382 <(bitvector_of_nat_inverse_nat_of_bitvector … ppc1)
     383 <(bitvector_of_nat_inverse_nat_of_bitvector … ppc2)
     384 lapply (le_n … (nat_of_bitvector … ppc2))
     385 elim LE in ⊢ (?%? → %);
     386 [ #_ %
     387 | #m #LE_ppc1_m #IH #BOUNDED @(transitive_le … (IH …)) -IH
     388   [@(transitive_le … BOUNDED) %2 %]
     389   cut (m < |\snd program|) [ @(transitive_le … ppc2_ok) %2 /by/ ] #m_ok
     390   cases (SIGMAOK2 (bitvector_of_nat … m) ?)
     391   [2: >nat_of_bitvector_bitvector_of_nat_inverse /by/
     392       @(lt_to_le_to_lt … program_bounded) assumption ]
     393   #_ *
     394   [2: * #abs @⊥ @(absurd ?? (lt_to_not_eq … m_ok))
     395       >nat_of_bitvector_bitvector_of_nat_inverse in abs; [#H @H]
     396       @(lt_to_le_to_lt … m_ok program_bounded) ]
     397   #LT <add_bitvector_of_nat_Sm >add_commutative @(transitive_le … LT) %2 %
     398qed.
    358399
    359400(* This is a trivial consequence of fetch_assembly_pseudo + load_code_memory_ok. *)     
     
    399440      >snd_fetch_pseudo_instruction
    400441      cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) -H
    401       #spw1 #_ >spw1 -spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f
     442      #spw1 #_ >spw1 -spw1 @eq_f @eq_f
    402443      >eq_fetch_pseudo_instruction whd in match instruction_size;
    403444      normalize nodelta >create_label_cost_refl
Note: See TracChangeset for help on using the changeset viewer.