Changeset 1934 for src/ASM/Policy.ma


Ignore:
Timestamp:
May 10, 2012, 3:37:07 PM (8 years ago)
Author:
boender
Message:
  • various & sundry moves of lemmas to better places
  • integrated Policy and Assembly
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r1933 r1934  
    1414(* Internal types *)
    1515
    16 (* label_map: identifier ↦ pseudo program counter *)
    17 definition label_map ≝ identifier_map ASMTag ℕ.
    18 
    1916(* ppc_pc_map: program length × (pseudo program counter ↦ 〈pc, jump_length〉) *)
    20 definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × (option jump_length)) 16).
     17definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × bool) 16).
    2118
    2219(* The different properties that we want/need to prove at some point *)
     
    7269  ].
    7370 
    74 definition jump_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝
     71(*definition jump_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝
    7572  λprefix.λsigma.
    7673  ∀i:ℕ.i < |prefix| →
    7774  iff (is_jump (nth i ? prefix 〈None ?, Comment []〉))
    7875   (∃x:jump_length.
    79    \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,None ?〉) = Some ? x).
     76   \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,None ?〉) = Some ? x).*)
    8077
    8178(* if the instruction 〈p,a〉 is a jump to label l, then label l is at address a *)
     
    111108 λprogram.λop.λp.
    112109 ∀i.i < |program| →
    113    let 〈opc,ox〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,None ?〉 in
    114    let 〈pc,x〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,None ?〉 in
    115      opc ≤ pc ∧
    116      match ox with
     110   let 〈opc,ox〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,false〉 in
     111   let 〈pc,x〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,false〉 in
     112     opc ≤ pc.
     113     (*∧ match ox with
    117114     [ Some oj ⇒
    118115       match x with
     
    121118       ]
    122119     | _ ⇒ True
    123      ].
     120     ].*)
     121
     122(*
    124123
    125124(* Policy safety *)
    126 definition policy_safe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝
     125(*definition policy_safe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝
    127126 λprogram.λlabels.λsigma.
    128127 ∀i.i < |program| →
    129  let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,None ?〉 in
     128 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,false〉 in
    130129 let 〈label,instr〉 ≝ nth i ? program 〈None ?, Comment [ ]〉 in
    131130 ∀dest.is_jump_to instr dest →
    132131   let paddr ≝ lookup_def … labels dest 0 in
    133    let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,None ?〉) in
     132   let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,false〉) in
    134133   match j with
    135134   [ None ⇒ True
     
    147146     | long_jump   ⇒ True
    148147     ]
    149    ].
     148   ].*)
    150149
    151150(* this is the instruction size as determined by the distance from origin to destination *)
     
    291290  %2 @nmk #H destruct (H)
    292291qed.
    293 
    294 (* Labels *)
    295 definition is_label ≝
    296   λx:labelled_instruction.λl:Identifier.
    297   let 〈lbl,instr〉 ≝ x in
    298   match lbl with
    299   [ Some l' ⇒ l' = l
    300   | _       ⇒ False
    301   ].
    302 
    303 lemma label_does_not_occur:
    304   ∀i:ℕ.∀p:list labelled_instruction.∀l:Identifier.
    305   is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur ?? l p = false.
    306  #i #p #l generalize in match i; elim p
    307  [ #i >nth_nil #H cases H
    308  | #h #t #IH #i cases i -i
    309    [ cases h #hi #hp cases hi
    310      [ normalize #H cases H
    311      | #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ????);
    312        whd in Heq; >Heq
    313        >eq_identifier_refl / by refl/
    314      ]
    315    | #i #H whd in match (does_not_occur ????);
    316      whd in match (instruction_matches_identifier ????);
    317      cases h #hi #hp cases hi normalize nodelta
    318      [ @(IH i) @H
    319      | #l' @eq_identifier_elim
    320        [ normalize / by /
    321        | normalize #_ @(IH i) @H
    322        ]
    323      ]
    324    ]
    325  ]
    326 qed.
    327292 
    328293definition policy_isize_sum ≝
     
    343308    lookup ?? labels l = Some ? i
    344309  ) ≝
    345   λprogram.
    346   foldl_strong (option Identifier × pseudo_instruction)
    347   (λprefix.Σlabels:label_map.
    348     ∀i:ℕ.lt i (|prefix|) →
    349     ∀l.occurs_exactly_once ?? l prefix →
    350     is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
    351     lookup … labels l = Some ? i
    352   )
    353   program
    354   (λprefix.λx.λtl.λprf.λlabels.
    355    let 〈label,instr〉 ≝ x in
    356      match label with
    357      [ None   ⇒ labels
    358      | Some l ⇒ add … labels l (|prefix|)
    359      ]
    360    ) (empty_map …).
    361 [1,2: #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
    362   [ #Hi #lbl #Hocc #Hlbl lapply (occurs_exactly_once_Some_stronger ?????? Hocc) -Hocc
    363     @eq_identifier_elim
    364     [ #Heq #Hocc normalize in Hocc; >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) in Hlbl; #Hl
    365       @⊥ @(absurd … Hocc) >(label_does_not_occur i … Hl) normalize nodelta /2 by nmk/
    366     | #Heq #Hocc normalize in Hocc; >lookup_add_miss
    367       [ @(pi2 … labels i (le_S_S_to_le … Hi))
    368         [ @Hocc
    369         | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by /
    370         ]
    371       | @sym_neq @Heq
    372       ]
    373     ]
    374   | #Hi #lbl #Hocc >(injective_S … Hi) >nth_append_second
    375     [ <minus_n_n #Hl normalize in Hl; >Hl @lookup_add_hit
    376     | @le_n
    377     ]
    378   | #Hi #lbl >occurs_exactly_once_None #Hocc #Hlbl
    379     @(pi2 … labels i (le_S_S_to_le … Hi))
    380     [ @Hocc
    381     | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by /
    382     ]
    383   | #Hi #lbl #Hocc >(injective_S … Hi) >nth_append_second
    384     [ <minus_n_n #Hl cases Hl
    385     | @le_n
    386     ]
    387   ]
    388 | #i #Hi #l #Hl cases Hl
    389 ]
     310 λprogram.
     311 
    390312qed.
    391313
     
    19461868] *)
    19471869qed.
     1870*)
    19481871
    19491872(* The glue between Policy and Assembly. *)
    19501873definition jump_expansion':
    19511874 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
    1952  Σf:ℕ → ℕ × (option jump_length).
    1953    ∀ppc.match je_fixpoint (\snd program) with
    1954    [ None ⇒ True
    1955    | Some pol ⇒ \fst (f ppc) +
    1956       (instruction_size_sigma (create_label_map (\snd program)) pol (bitvector_of_nat ? (\fst (f ppc)))
    1957       (\snd (nth ppc ? (\snd program) 〈None ?, Comment []〉)))
    1958      = \fst (f (S ppc))
    1959    ] ≝
     1875  option (Σsigma:Word → Word × bool.
     1876   ∀ppc.
     1877    \snd
     1878     (half_add ?
     1879      (\fst (sigma ppc))
     1880      (bitvector_of_nat ?
     1881       (instruction_size
     1882        (λid. bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) id 0))
     1883        sigma ppc (\fst (fetch_pseudo_instruction (\snd program) ppc)))))
     1884    = \fst (sigma (\snd (half_add ? ppc (bitvector_of_nat ? 1)))))
     1885≝ ?.
     1886(*
    19601887λprogram.λppc:ℕ.
    19611888  let policy ≝ pi1 … (je_fixpoint (\snd program)) in
     
    19631890  [ None ⇒ 〈0, Some ? long_jump〉
    19641891  | Some x ⇒ bvt_lookup ?? (bitvector_of_nat 16 ppc) (\snd x) 〈0,Some ? long_jump〉
    1965   ].
     1892  ].*)
    19661893 cases daemon
    19671894qed.
Note: See TracChangeset for help on using the changeset viewer.