Changeset 1886


Ignore:
Timestamp:
Apr 11, 2012, 2:36:47 PM (8 years ago)
Author:
boender
Message:
  • improvements for disambiguation and quick(er) typing
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r1879 r1886  
    1818(* The different properties that we want/need to prove at some point *)
    1919(* 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.
     20definition out_of_program_none: list labelled_instruction → jump_expansion_policy → Prop
     21  λprefixpolicy.
    2222  ∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) (\snd policy) = None ?.
    2323
     
    4949  ].
    5050
    51 definition jump_in_policy
    52   λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
     51definition jump_in_policy: list labelled_instruction → jump_expansion_policy → Prop
     52  λprefixpolicy.
    5353  ∀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.
    5656     lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈p,a,j〉).
    5757
    58 definition labels_okay
    59   λlabels:label_map.λpolicy:jump_expansion_policy.
     58definition labels_okay: label_map → jump_expansion_policy → Prop
     59  λlabelspolicy.
    6060  bvt_forall ?? (\snd policy) (λn.λx.
    6161   let 〈pc,addr_nat,j〉 ≝ x in
     
    152152
    153153lemma 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.
    156156 #i #p #l generalize in match i; elim p
    157157 [ #i >nth_nil #H @⊥ @H
     
    159159   [ cases h #hi #hp cases hi
    160160     [ 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 ????);
    162162       whd in Heq; >Heq
    163163       >eq_identifier_refl / by refl/
    164164     ]
    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 ????);
    167167     cases h #hi #hp cases hi normalize nodelta
    168168     [ @(IH i) @H
     
    178178definition expand_relative_jump_internal_unsafe:
    179179  jump_length → ([[relative]] → preinstruction [[relative]]) → option (list instruction) ≝
    180   λjmp_len,i.
     180  λjmp_len:jump_length.λi.
    181181  match jmp_len with
    182182  [ short_jump ⇒ Some ? [ RealInstruction (i (RELATIVE (zero 8))) ]
     
    193193definition expand_relative_jump_unsafe:
    194194  jump_length → preinstruction Identifier → option (list instruction) ≝
    195   λjmp_len,i.
     195  λjmp_len:jump_length.λi.
    196196  match i with
    197197  [ JC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JC ?)
     
    284284  (Σlabels:label_map.
    285285    ∀i:ℕ.lt i (|program|) →
    286     ∀l.occurs_exactly_once l program →
     286    ∀l.occurs_exactly_once ?? l program →
    287287    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
    288288    ∃a.lookup … labels l = Some ? 〈i,a〉
     
    293293    (λprefix.ℕ × (Σlabels.
    294294      ∀i:ℕ.lt i (|prefix|) →
    295       ∀l.occurs_exactly_once l prefix →
     295      ∀l.occurs_exactly_once ?? l prefix →
    296296      is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
    297297      ∃a.lookup … labels l = Some ? 〈i,a〉)
     
    304304       match label with
    305305       [ None   ⇒ labels
    306        | Some l ⇒ add labels l 〈|prefix|, pc〉
     306       | Some l ⇒ add ? (ℕ×ℕ) labels l 〈|prefix|, pc〉
    307307       ] in
    308308     let 〈i1,i2,jmp_len〉 ≝
     
    316316      lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 
    317317      % [ @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;
    319319      @eq_identifier_elim #Heq #Hocc
    320320      [ normalize in Hocc;
     
    441441  ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    442442  Σ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〉)
    447447  λprogram.
    448448  foldl_strong (option Identifier × pseudo_instruction)
    449449  (λ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〉))
    454454  program
    455455  (λprefix.λx.λtl.λprf.λp.
     
    725725qed.
    726726
     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
    727736(* One step in the search for a jump expansion fixpoint. *)
    728737definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    729   ∀labels:(Σlm:label_map.∀i:ℕ.lt i (|program|) →
    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 →
    732741    ∃a.lookup … lm l = Some ? 〈i,a〉).
    733742  ∀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).
    736746  (Σx:bool × (option jump_expansion_policy).
    737747    let 〈ch,y〉 ≝ x in
    738748    match y with
    739749    [ None ⇒ nec_plus_ultra program old_policy
    740     | Some p ⇒ out_of_program_none program p ∧ labels_okay labels p ∧
    741         jump_in_policy program p ∧
    742         policy_increase program old_policy p ∧ policy_safe p ∧
    743         (ch = false → policy_equal_int program old_policy p (*sic!*)) ∧
    744         policy_isize_sum program p ∧ \fst p < 2^16
     750    | 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
    745755    ])
    746756    ≝
     
    792802  [ @leb_true_to_le <geb_to_leb @p1
    793803  | @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 *)
    796805  ]
    797806| normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2
     
    12101219  ].*)
    12111220
    1212 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (|l|) 2^16) (n: ℕ)
     1221let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (length ? l) 2^16) (n: ℕ)
    12131222  on n:(Σx:bool × (option jump_expansion_policy).
    12141223    let 〈c,pol〉 ≝ x in
     
    13891398  [ / by refl/
    13901399  | #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〉))
    13921401    [ normalize nodelta @Hd
    13931402    |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
     
    14711480| #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*|t|)
    14721481  [ 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;
    14741483    normalize nodelta
    14751484    [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
     
    14831492  [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi))
    14841493  | #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;
    14861495    normalize nodelta
    14871496    [ >Hmt normalize <plus_n_O >(commutative_plus (|t|) (S (|t|)))
Note: See TracChangeset for help on using the changeset viewer.