Changeset 2141 for src/ASM/Policy.ma


Ignore:
Timestamp:
Jun 28, 2012, 8:08:58 PM (7 years ago)
Author:
boender
Message:
  • committed working version
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2101 r2141  
    55include alias "basics/logic.ma".
    66
    7 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (S (|l|)) 2^16) (n: ℕ)
     7let rec jump_expansion_internal (program: Σl:list labelled_instruction.
     8  lt (S (|l|)) 2^16 ∧ is_well_labelled_p l) (n: ℕ)
    89  on n:(Σx:bool × (option ppc_pc_map).
    910    let 〈no_ch,pol〉 ≝ x in
     
    3435  [ #H / by I/
    3536  | #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj
    36     [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))
     37    [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    3738    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    3839    ]
     
    5253    | #j2 #H2 @conj [ @conj [ @conj [ @conj
    5354      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))))
    54       | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))
    55       ]
    56       | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
     55      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))))
     56      ]
     57      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))
    5758      ]     
    5859      | @(proj2 ?? H2)
    5960      ]
    60       | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))
    61       ]
     61      | #Ht @(equal_compact_unsafe_compact ?? op)
     62        [ @(proj2 ?? (proj1 ?? (proj1 ?? H2))) @Ht
     63        | cases daemon (* add to invvariants *)
     64        | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
     65        ]
     66      ]
    6267    ]
    6368  ]
     
    6671  [ #_ >p2 #ABS destruct (ABS)
    6772  | #map >p2 normalize nodelta
    68     #H #eq destruct (eq) @(proj1 ?? H)
     73    #H #eq destruct (eq) cases daemon (* change order *)
    6974  ]
    7075]
     
    157162qed.
    158163
    159 lemma pe_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).
     164lemma pe_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
    160165  ∀n.policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program n)))
    161166   (\snd (pi1 ?? (jump_expansion_internal program (S n)))) →
     
    166171qed.
    167172
    168 (* this is in the stdlib, but commented out, why? *)
    169 theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.
    170   #n (elim n) normalize /2 by S_pred/ qed.
    171  
    172 lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).∀n:ℕ.
     173lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.
     174  S (|l|) < 2^16 ∧ is_well_labelled_p l).∀n:ℕ.
    173175  policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n)))
    174176   (\snd (pi1 … (jump_expansion_internal program (S n)))) →
     
    228230
    229231(* uses the second part of policy_increase *)
    230 lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.S (|l|) <2^16.
     232lemma measure_incr_or_equal: ∀program:(Σl:list labelled_instruction.
     233  S (|l|) <2^16 ∧ is_well_labelled_p l).
    231234  ∀policy:Σp:ppc_pc_map.
    232     out_of_program_none program p ∧
     235    (*out_of_program_none program p ∧*)
    233236    not_jump_default program p ∧
    234237    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
    235238    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
     239    sigma_compact_unsafe program (create_label_map program) p ∧
    236240    \fst p < 2^16.
    237241  ∀l.|l| ≤ |program| → ∀acc:ℕ.
     
    247251  [ / by I/
    248252  | #x normalize nodelta #Hx #Hjeq
    249     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))))) (|t|) (le_S_to_le … Hp))
     253    lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (|t|) (le_S_to_le … Hp))
    250254    whd in match (measure_int ???); whd in match (measure_int ? x ?);
    251255    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd (pi1 ?? policy)) 〈0,short_jump〉)
     
    266270qed.
    267271
    268 (* these lemmas seem superfluous, but not sure how *)
    269 lemma bla: ∀a,b:ℕ.a + a = b + b → a = b.
    270  #a elim a
    271  [ normalize #b //
    272  | -a #a #Hind #b cases b [ /2 by le_n_O_to_eq/ | -b #b normalize
    273    <plus_n_Sm <plus_n_Sm #H
    274    >(Hind b (injective_S ?? (injective_S ?? H))) // ]
    275  ]
    276 qed.
    277 
    278 lemma sth_not_s: ∀x.x ≠ S x.
    279  #x cases x
    280  [ // | #y // ]
    281 qed.
    282  
    283272lemma measure_full: ∀program.∀policy.
    284273  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
     
    314303
    315304(* uses second part of policy_increase *)
    316 lemma measure_special: ∀program:(Σl:list labelled_instruction.(S (|l|)) < 2^16).
     305lemma measure_special: ∀program:(Σl:list labelled_instruction.
     306    (S (|l|)) < 2^16 ∧ is_well_labelled_p l).
    317307  ∀policy:Σp:ppc_pc_map.
    318     out_of_program_none program p ∧ not_jump_default program p ∧
     308    not_jump_default program p ∧
    319309    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
    320310    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
     311    sigma_compact_unsafe program (create_label_map program) p ∧
    321312    \fst p < 2^16.
    322313  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with
     
    336327     [ @(transitive_le … Hp) / by /
    337328     | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
    338        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) (|t|) (le_S_to_le … Hp))
     329       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) (le_S_to_le … Hp))
    339330       #Hinc cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm Hinc;
    340331       #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉);
     
    359350     ]
    360351   | >Hi whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
    361      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) (|t|) (le_S_to_le … Hp))
     352     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) (le_S_to_le … Hp))
    362353     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm;
    363354     #x1 #x2
     
    379370qed.
    380371
    381 lemma le_to_eq_plus: ∀n,z.
    382   n ≤ z → ∃k.z = n + k.
    383  #n #z elim z
    384  [ #H cases (le_to_or_lt_eq … H)
    385    [ #H2 @⊥ @(absurd … H2) @not_le_Sn_O
    386    | #H2 @(ex_intro … 0) >H2 //
    387    ]
    388  | #z' #Hind #H cases (le_to_or_lt_eq … H)
    389    [ #H' elim (Hind (le_S_S_to_le … H')) #k' #H2 @(ex_intro … (S k'))
    390      >H2 >plus_n_Sm //
    391    | #H' @(ex_intro … 0) >H' //
    392    ]
    393  ]
    394 qed.
    395 
    396 lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.S (|l|) < 2^16.
     372lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.
     373  S (|l|) < 2^16 ∧ is_well_labelled_p l.
    397374  match jump_expansion_start program (create_label_map program) with
    398375  [ None ⇒ True
     
    406383   [ / by refl/
    407384   | #h #t #Hind #Hp whd in match (measure_int ???);
    408      elim (proj2 ?? (proj1 ?? (proj1 ?? Hpl)) (|t|) (le_S_to_le … Hp))
     385     elim (proj2 ?? (proj1 ?? Hpl) (|t|) (le_S_to_le … Hp))
    409386     #pc #Hpc >(lookup_opt_lookup_hit … Hpc 〈0,short_jump〉) normalize nodelta @Hind
    410387     @(transitive_le … Hp) @le_n_Sn
     
    414391
    415392(* the actual computation of the fixpoint *)
    416 definition je_fixpoint: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).
     393definition je_fixpoint: ∀program:(Σl:list labelled_instruction.
     394  S (|l|) < 2^16 ∧ is_well_labelled_p l).
    417395  Σp:option ppc_pc_map.
    418396    match p with
     
    513491                  normalize nodelta #Hpe
    514492                  lapply (measure_incr_or_equal program Xp program (le_n (|program|)) 0)
    515                   [ @(proj1 ?? HXp)
     493                  [ cases daemon (* reorder *)
    516494                  | lapply (Hfa x Hx) >Xeq >Seq
    517495                    lapply (measure_special program «Xp,?»)
    518                     [ @(proj1 ?? HXp)
     496                    [ cases daemon (* reorder *)
    519497                    | lapply Seq whd in match (jump_expansion_internal program (S x)); (*340s*)
    520498                      >Xeq normalize nodelta cases Xno_ch in HXp Xeq; #HXp #Xeq
     
    556534        | -sto #stp normalize nodelta #Hstp @conj [ @conj
    557535          [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))))
    558           | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))
    559             @(proj2 ?? (proj1 ?? Hstp)) #i #Hi
    560             cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
    561             [ #Hj
    562               lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))) i (le_S_to_le … Hi))
    563               lapply (Hfull i Hi Hj)
    564               cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
    565               #fp #fj #Hfj >Hfj normalize nodelta
    566               cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉)
    567               #stp #stj cases stj normalize nodelta
    568               [1,2: #H cases H #H2 cases H2 destruct (H2)
    569               |3: #_ @refl
     536          | @(equal_compact_unsafe_compact ?? Fp)
     537            [ @(proj2 ?? (proj1 ?? (proj1 ?? Hstp))) @(proj2 ?? (proj1 ?? Hstp))
     538              #i #Hi
     539              cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
     540              [ #Hj
     541                lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))) i (le_S_to_le … Hi))
     542                lapply (Hfull i Hi Hj)
     543                cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
     544                #fp #fj #Hfj >Hfj normalize nodelta
     545                cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉)
     546                #stp #stj cases stj normalize nodelta
     547                [1,2: #H cases H #H2 cases H2 destruct (H2)
     548                |3: #_ @refl
     549                ]
     550              | #Hj >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))) i Hi Hj)
     551                >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) i Hi Hj) @refl
    570552              ]
    571             | #Hj >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))) i Hi Hj)
    572               >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) i Hi Hj) @refl
     553            | cases daemon 
     554            | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))
    573555            ]
    574556          ]
     
    597579include alias "arithmetics/nat.ma".
    598580include alias "basics/logic.ma".
    599 
    600 lemma nth_safe_nth:
    601   ∀A:Type[0].∀l:list A.∀i.∀proof:i < |l|.∀x.nth_safe A i l proof = nth i A l x.
    602 #A #l elim l
    603 [ #i #prf @⊥ @(absurd ? prf) @le_to_not_lt @le_O_n
    604 | -l #h #t #Hind #i elim i
    605   [ #prf #x normalize @refl
    606   | -i #i #Hind2 #prf #x whd in match (nth ????); whd in match (tail ??);
    607     whd in match (nth_safe ????); @Hind
    608   ]
    609 ]
    610 qed.
    611581
    612582(* The glue between Policy and Assembly. *)
     
    686656]
    687657qed.           
    688      
    689 
    690        
    691 
    692     >(add_bitvector_of_nat_plus ?? ppc)
    693      
    694 qed.
Note: See TracChangeset for help on using the changeset viewer.