 Timestamp:
 Apr 11, 2012, 2:36:47 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r1879 r1886 18 18 (* The different properties that we want/need to prove at some point *) 19 19 (* Anything that's not in the program doesn't end up in the policy *) 20 definition out_of_program_none ≝21 λprefix :list labelled_instruction.λpolicy:jump_expansion_policy.20 definition out_of_program_none: list labelled_instruction → jump_expansion_policy → Prop ≝ 21 λprefix.λpolicy. 22 22 ∀i.i ≥ prefix → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) (\snd policy) = None ?. 23 23 … … 49 49 ]. 50 50 51 definition jump_in_policy ≝52 λprefix :list labelled_instruction.λpolicy:jump_expansion_policy.51 definition jump_in_policy: list labelled_instruction → jump_expansion_policy → Prop ≝ 52 λprefix.λpolicy. 53 53 ∀i:ℕ.i < prefix → 54 (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔55 ∃p:ℕ.∃a:ℕ.∃j:jump_length.54 iff (is_jump (nth i ? prefix 〈None ?, Comment []〉)) 55 (∃p:ℕ.∃a:ℕ.∃j:jump_length. 56 56 lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈p,a,j〉). 57 57 58 definition labels_okay ≝59 λlabels :label_map.λpolicy:jump_expansion_policy.58 definition labels_okay: label_map → jump_expansion_policy → Prop ≝ 59 λlabels.λpolicy. 60 60 bvt_forall ?? (\snd policy) (λn.λx. 61 61 let 〈pc,addr_nat,j〉 ≝ x in … … 152 152 153 153 lemma label_does_not_occur: 154 ∀i ,p,l.155 is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur l p = false.154 ∀i:ℕ.∀p:list labelled_instruction.∀l:Identifier. 155 is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur ?? l p = false. 156 156 #i #p #l generalize in match i; elim p 157 157 [ #i >nth_nil #H @⊥ @H … … 159 159 [ cases h #hi #hp cases hi 160 160 [ normalize #H @⊥ @H 161  #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ?? );161  #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ????); 162 162 whd in Heq; >Heq 163 163 >eq_identifier_refl / by refl/ 164 164 ] 165  #i #H whd in match (does_not_occur ?? );166 whd in match (instruction_matches_identifier ?? );165  #i #H whd in match (does_not_occur ????); 166 whd in match (instruction_matches_identifier ????); 167 167 cases h #hi #hp cases hi normalize nodelta 168 168 [ @(IH i) @H … … 178 178 definition expand_relative_jump_internal_unsafe: 179 179 jump_length → ([[relative]] → preinstruction [[relative]]) → option (list instruction) ≝ 180 λjmp_len ,i.180 λjmp_len:jump_length.λi. 181 181 match jmp_len with 182 182 [ short_jump ⇒ Some ? [ RealInstruction (i (RELATIVE (zero 8))) ] … … 193 193 definition expand_relative_jump_unsafe: 194 194 jump_length → preinstruction Identifier → option (list instruction) ≝ 195 λjmp_len ,i.195 λjmp_len:jump_length.λi. 196 196 match i with 197 197 [ JC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JC ?) … … 284 284 (Σlabels:label_map. 285 285 ∀i:ℕ.lt i (program) → 286 ∀l.occurs_exactly_once l program →286 ∀l.occurs_exactly_once ?? l program → 287 287 is_label (nth i ? program 〈None ?, Comment [ ]〉) l → 288 288 ∃a.lookup … labels l = Some ? 〈i,a〉 … … 293 293 (λprefix.ℕ × (Σlabels. 294 294 ∀i:ℕ.lt i (prefix) → 295 ∀l.occurs_exactly_once l prefix →295 ∀l.occurs_exactly_once ?? l prefix → 296 296 is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l → 297 297 ∃a.lookup … labels l = Some ? 〈i,a〉) … … 304 304 match label with 305 305 [ None ⇒ labels 306  Some l ⇒ add …labels l 〈prefix, pc〉306  Some l ⇒ add ? (ℕ×ℕ) labels l 〈prefix, pc〉 307 307 ] in 308 308 let 〈i1,i2,jmp_len〉 ≝ … … 316 316 lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 317 317 % [ @addr  @Haddr ] 318  #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger …Hocc) Hocc;318  #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger ?????? Hocc) Hocc; 319 319 @eq_identifier_elim #Heq #Hocc 320 320 [ normalize in Hocc; … … 441 441 ∀program:(Σl:list labelled_instruction.l < 2^16). 442 442 Σpolicy:jump_expansion_policy. 443 out_of_program_none program policy ∧444 jump_in_policy program policy ∧445 ∀i.i < program → is_jump (nth i ? program〈None ?, Comment []〉) →446 lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈0,0,short_jump〉 ≝443 And (And (out_of_program_none (pi1 ?? program) policy) 444 (jump_in_policy (pi1 ?? program) policy)) 445 (∀i.i < pi1 ?? program → is_jump (nth i ? (pi1 ?? program) 〈None ?, Comment []〉) → 446 lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈0,0,short_jump〉) ≝ 447 447 λprogram. 448 448 foldl_strong (option Identifier × pseudo_instruction) 449 449 (λprefix.Σpolicy:jump_expansion_policy. 450 out_of_program_none prefix policy ∧451 jump_in_policy prefix policy ∧452 ∀i.i < prefix → is_jump (nth i ? prefix 〈None ?, Comment []〉) →453 lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈0,0,short_jump〉) 450 And (And (out_of_program_none prefix policy) 451 (jump_in_policy prefix policy)) 452 (∀i.i < prefix → is_jump (nth i ? prefix 〈None ?, Comment []〉) → 453 lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈0,0,short_jump〉)) 454 454 program 455 455 (λprefix.λx.λtl.λprf.λp. … … 725 725 qed. 726 726 727 (*lemma foldl_strong_eq: 728 ∀A: Type[0]. 729 ∀P: list A → Type[0]. 730 ∀l: list A. 731 ∀H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]). 732 ∀acc: P [ ]. 733 foldl_strong_internal A P l H [ ] l acc (refl …).*) 734 735 727 736 (* One step in the search for a jump expansion fixpoint. *) 728 737 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.l < 2^16). 729 ∀labels:(Σlm:label_map.∀i:ℕ.lt i (p rogram) →730 ∀l.occurs_exactly_once l program→731 is_label (nth i ? program〈None ?, Comment [ ]〉) l →738 ∀labels:(Σlm:label_map.∀i:ℕ.lt i (pi1 ?? program) → 739 ∀l.occurs_exactly_once ?? l (pi1 ?? program) → 740 is_label (nth i ? (pi1 ?? program) 〈None ?, Comment [ ]〉) l → 732 741 ∃a.lookup … lm l = Some ? 〈i,a〉). 733 742 ∀old_policy:(Σpolicy:jump_expansion_policy. 734 out_of_program_none program policy ∧ jump_in_policy program policy ∧ (\fst policy < 2^16) ∧ 735 policy_isize_sum program policy). 743 out_of_program_none (pi1 ?? program) policy ∧ 744 jump_in_policy (pi1 ?? program) policy ∧ (\fst policy < 2^16) ∧ 745 policy_isize_sum (pi1 ?? program) policy). 736 746 (Σx:bool × (option jump_expansion_policy). 737 747 let 〈ch,y〉 ≝ x in 738 748 match y with 739 749 [ None ⇒ nec_plus_ultra program old_policy 740  Some p ⇒ out_of_program_none programp ∧ labels_okay labels p ∧741 jump_in_policy programp ∧742 policy_increase programold_policy p ∧ policy_safe p ∧743 (ch = false → policy_equal_int program old_policy p (*sic!*)) ∧744 policy_isize_sum programp ∧ \fst p < 2^16750  Some p ⇒ out_of_program_none (pi1 ?? program) p ∧ labels_okay labels p ∧ 751 jump_in_policy (pi1 ?? program) p ∧ 752 policy_increase (pi1 ?? program) old_policy p ∧ policy_safe p ∧ 753 (ch = false → policy_equal_int (pi1 ?? program) old_policy p) ∧ 754 policy_isize_sum (pi1 ?? program) p ∧ \fst p < 2^16 745 755 ]) 746 756 ≝ … … 792 802 [ @leb_true_to_le <geb_to_leb @p1 793 803  @lt_to_not_le @(le_to_lt_to_lt … (proj2 ?? (proj1 ?? (pi2 ?? old_policy)))) 794 >(proj2 ?? H) >(proj2 ?? (pi2 ?? old_policy)) 795 cases daemon (* XXX *) 804 >(proj2 ?? H) >(proj2 ?? (pi2 ?? old_policy)) cases daemon (* XXX *) 796 805 ] 797 806  normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2 … … 1210 1219 ].*) 1211 1220 1212 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt ( l) 2^16) (n: ℕ)1221 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (length ? l) 2^16) (n: ℕ) 1213 1222 on n:(Σx:bool × (option jump_expansion_policy). 1214 1223 let 〈c,pol〉 ≝ x in … … 1389 1398 [ / by refl/ 1390 1399  #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x); 1391 cases (\snd ( lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,0,short_jump〉))1400 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,0,short_jump〉)) 1392 1401 [ normalize nodelta @Hd 1393 1402 2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus … … 1471 1480  #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*t) 1472 1481 [ whd in match (measure_int ???) in Hm; 1473 cases (\snd ( lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,0,short_jump〉)) in Hm;1482 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,0,short_jump〉)) in Hm; 1474 1483 normalize nodelta 1475 1484 [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/ … … 1483 1492 [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi)) 1484 1493  #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 1485 cases (\snd ( lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,0,short_jump〉)) in Hm;1494 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,0,short_jump〉)) in Hm; 1486 1495 normalize nodelta 1487 1496 [ >Hmt normalize <plus_n_O >(commutative_plus (t) (S (t)))
Note: See TracChangeset
for help on using the changeset viewer.