Ignore:
Timestamp:
Jun 19, 2012, 4:43:50 PM (7 years ago)
Author:
boender
Message:
  • renamed medium to absolute jump
  • revised proofs of policy, some daemons removed
  • reverted earlier change in extralib, bounded quantification now again uses lt
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r2059 r2101  
    1313(* The different properties that we want/need to prove at some point *)
    1414(* During our iteration, everything not yet seen is None, and vice versa *)
    15 definition out_of_program_none: list labelled_instruction → ppc_pc_map → Prop ≝
    16   λprefix.λsigma.
    17   ∀i:ℕ.i < 2^16 → (i > |prefix| ↔ bvt_lookup_opt … (bitvector_of_nat 16 i) (\snd sigma) = None ?).
     15definition out_of_program_none ≝
     16  λprefix:list labelled_instruction.λsigma:ppc_pc_map.
     17  ∀i.i < 2^16 → (i > |prefix| ↔ bvt_lookup_opt … (bitvector_of_nat ? i) (\snd sigma) = None ?).
    1818
    1919(* If instruction i is a jump, then there will be something in the policy at
     
    7777  ].
    7878 
    79 definition jump_not_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝
    80   λprefix.λsigma.
     79definition not_jump_default ≝
     80  λprefix:list labelled_instruction.λsigma:ppc_pc_map.
    8181  ∀i:ℕ.i < |prefix| →
    8282  ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment []〉)) →
    83   \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉) = short_jump.
    84 
    85 (* if the instruction 〈p,a〉 is a jump to label l, then label l is at address a *)
    86 (* definition labels_okay: label_map → ppc_pc_map → Prop ≝
    87   λlabels.λsigma.
    88   bvt_forall ?? (\snd sigma) (λn.λx.
    89    let 〈pc,addr_nat〉 ≝ x in
    90    ∃id:Identifier.lookup_def … labels id 0 = addr_nat
    91   ). *)
    92  
     83  \snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = short_jump.
     84 
    9385(* Between two policies, jumps cannot decrease *)
    9486definition jmpeqb: jump_length → jump_length → bool ≝
     
    9688  match j1 with
    9789  [ short_jump ⇒ match j2 with [ short_jump ⇒ true | _ ⇒ false ]
    98   | medium_jump ⇒ match j2 with [ medium_jump ⇒ true | _ ⇒ false ]
     90  | absolute_jump ⇒ match j2 with [ absolute_jump ⇒ true | _ ⇒ false ]
    9991  | long_jump ⇒ match j2 with [ long_jump ⇒ true | _ ⇒ false ]
    10092  ].
     
    114106    | _          ⇒ True
    115107    ]
    116   | medium_jump ⇒
     108  | absolute_jump ⇒
    117109    match j2 with
    118110    [ long_jump ⇒ True
     
    125117  λj1.λj2.jmple j1 j2 ∨ j1 = j2.
    126118 
    127 definition policy_increase: list labelled_instruction → ppc_pc_map →
    128   ppc_pc_map → Prop ≝
    129  λprogram.λop.λp.
    130  ∀i.i ≤ |program| →
    131    let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,short_jump〉 in
    132    let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉 in
     119definition jump_increase ≝
     120 λprefix:list labelled_instruction.λop:ppc_pc_map.λp:ppc_pc_map.
     121 ∀i.i ≤ |prefix| →
     122   let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd op) 〈0,short_jump〉 in
     123   let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd p) 〈0,short_jump〉 in
    133124     (*opc ≤ pc ∧*) jmpleq oj j.
    134125     
     
    139130  match jmp_len with
    140131  [ short_jump ⇒ [ RealInstruction (i (RELATIVE (zero 8))) ]
    141   | medium_jump ⇒ [ ] (* this should not happen *)
     132  | absolute_jump ⇒ [ ] (* this should not happen *)
    142133  | long_jump ⇒
    143134    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
     
    202193    match jmp_len with
    203194    [ short_jump ⇒ [ ] (* this should not happen *)
    204     | medium_jump ⇒ [ ACALL (ADDR11 (zero 11)) ]
     195    | absolute_jump ⇒ [ ACALL (ADDR11 (zero 11)) ]
    205196    | long_jump ⇒ [ LCALL (ADDR16 (zero 16)) ]
    206197    ]
     
    211202    match jmp_len with
    212203    [ short_jump ⇒ [ SJMP (RELATIVE (zero 8)) ]
    213     | medium_jump ⇒ [ AJMP (ADDR11 (zero 11)) ]
     204    | absolute_jump ⇒ [ AJMP (ADDR11 (zero 11)) ]
    214205    | long_jump ⇒ [ LJMP (ADDR16 (zero 16)) ]
    215206    ]
     
    222213qed.
    223214
    224 definition policy_compact_unsafe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝
    225  λprogram.λlabels.λsigma.
    226  ∀n:ℕ.n < |program| →
     215definition sigma_compact_unsafe ≝
     216 λprefix:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.
     217 ∀n.n < |prefix| →
    227218  match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with
    228219  [ None ⇒ False
     
    231222    [ None ⇒ False
    232223    | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in
    233        pc1 = pc + instruction_size_jmplen j (\snd (nth n ? program 〈None ?, Comment []〉))
     224       pc1 = pc + instruction_size_jmplen j (\snd (nth n ? prefix 〈None ?, Comment []〉))
    234225    ]
    235226  ].
    236227   
    237 (* new safety condition: policy corresponds to program and resulting program is compact *)
    238 definition policy_compact: list labelled_instruction → label_map → ppc_pc_map → Prop
    239  λprogram.λlabels.λsigma.
    240  ∀n:ℕ.n < |program| →
     228(* new safety condition: sigma corresponds to program and resulting program is compact *)
     229definition sigma_compact
     230 λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.
     231 ∀n.n < |program| →
    241232  match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with
    242233  [ None ⇒ False
     
    251242    ]
    252243  ].
     244
     245(* jumps are of the proper size *)
     246definition sigma_safe ≝
     247 λprefix:list labelled_instruction.λlabels:label_map.λadded:ℕ.
     248 λold_sigma:ppc_pc_map.λsigma:ppc_pc_map.
     249 ∀i.i < |prefix| →
     250 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in
     251 let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in
     252 let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment [ ]〉 in
     253 ∀dest.is_jump_to instr dest →
     254   let paddr ≝ lookup_def … labels dest 0 in
     255   let addr ≝ bitvector_of_nat ? (if leb i paddr (* forward jump *)
     256   then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) + added
     257   else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)) in
     258   match j with
     259   [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧
     260      ¬is_call instr
     261   | absolute_jump ⇒  \fst (absolute_jump_cond pc_plus_jmp_length addr) = true ∧
     262       \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧
     263       ¬is_relative_jump instr
     264   | long_jump   ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧
     265       \fst (absolute_jump_cond pc_plus_jmp_length addr) = false
     266   ].
     267
    253268 
    254269(* Definitions and theorems for the jump_length type (itself defined in Assembly) *)
     
    257272  match j1 with
    258273  [ long_jump   ⇒ long_jump
    259   | medium_jump ⇒
     274  | absolute_jump ⇒
    260275    match j2 with
    261     [ medium_jump ⇒ medium_jump
     276    [ absolute_jump ⇒ absolute_jump
    262277    | _           ⇒ long_jump
    263278    ]
     
    283298  %2 @nmk #H destruct (H)
    284299qed.
    285  
    286 (* definition policy_isize_sum ≝
    287   λprefix:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.
    288   (\fst sigma) = foldl_strong (option Identifier × pseudo_instruction)
    289   (λacc.ℕ)
    290   prefix
    291   (λhd.λx.λtl.λp.λacc.
    292     acc + (instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))
    293     (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
    294     (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
    295     (bitvector_of_nat 16 (\fst sigma)) (\snd x)))
    296   0. *)
    297300 
    298301(* The function that creates the label-to-address map *)
     
    340343            + added
    341344    else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉)) in
    342   let 〈mj_possible, disp〉 ≝ medium_jump_cond pc_plus_jmp_length addr in   
    343   if mj_possible
    344   then medium_jump
     345  let 〈aj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length addr in   
     346  if aj_possible
     347  then absolute_jump
    345348  else long_jump.
    346349 
     
    411414    match policy with
    412415    [ None ⇒ True
    413     | Some p ⇒
    414        And (And (And (And (And (And (out_of_program_none (pi1 ?? program) p)
    415        (jump_not_in_policy (pi1 ?? program) p))
    416        (policy_compact_unsafe program labels p))
     416    | Some p ⇒ And (And (And (And (And (And (And
     417       (out_of_program_none (pi1 ?? program) p)
     418       (not_jump_default (pi1 ?? program) p))
     419       (sigma_compact_unsafe program labels p))
    417420       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
     421       (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
    418422       (∀i.i ≤ |program| → ∃pc.
    419423         bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉))
    420        (bvt_lookup_opt … (bitvector_of_nat ? (|program|)) (\snd p) =
    421          Some ? 〈\fst p,short_jump〉))
     424       (bvt_lookup_opt … (bitvector_of_nat ? (|program|)) (\snd p) = Some ? 〈\fst p,short_jump〉))
    422425       (\fst p < 2^16)
    423426    ] ≝
    424427  λprogram.λlabels.
    425428  let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction)
    426   (λprefix.Σpolicy:ppc_pc_map.
    427     And (And (And (And (And (out_of_program_none prefix policy)
    428     (jump_not_in_policy prefix policy))
    429     (policy_compact_unsafe prefix labels policy))
     429  (λprefix.Σpolicy:ppc_pc_map.And (And (And (And (And (And
     430    (out_of_program_none prefix policy)
     431    (not_jump_default prefix policy))
     432    (sigma_compact_unsafe prefix labels policy))
    430433    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
     434    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
    431435    (∀i.i ≤ |prefix| → ∃pc.
    432436      bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉))
     
    447451| lapply p -p generalize in match (foldl_strong ?????); * #p #Hp #hg
    448452  @conj [ @Hp | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ]
    449 | @conj [ @conj [ @conj [ @conj [ @conj
     453| @conj [ @conj [ @conj [ @conj [ @conj [ @conj
    450454  [ (* out_of_program_none *)
    451455    #i #Hi2 >append_length <commutative_plus @conj
     
    453457      cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi
    454458      [ >lookup_opt_insert_miss
    455         [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2))
     459        [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi2))
    456460          @le_S_to_le @le_S_to_le @Hi
    457461        | @bitvector_of_nat_abs
     
    463467      | >lookup_opt_insert_miss
    464468        [ <Hi
    465           @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) (S (S (|prefix|))) ?))
     469          @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) (S (S (|prefix|))) ?))
    466470          [ >Hi @Hi2
    467471          | @le_S @le_n
     
    479483      | #Hi >lookup_opt_insert_miss
    480484        [ #Hl
    481           elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2) Hl))
     485          elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi2) Hl))
    482486          [ #Hi3 @Hi3
    483487          | #Hi3 @⊥ @(absurd ? Hi3) @sym_neq @Hi
     
    492496      ]
    493497    ]
    494   | (* jump_not_in_policy *) cases p -p #p cases p -p #pc #sigma #Hp
     498  | (* not_jump_default *) cases p -p #p cases p -p #pc #sigma #Hp
    495499    cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi
    496500    normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    497501    [ >lookup_insert_miss
    498       [ lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi)
     502      [ lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))))) i Hi)
    499503        >nth_append_first
    500504        [ #H #H2 @H @H2
     
    526530    [ >lookup_opt_insert_miss
    527531      [ >lookup_opt_insert_miss
    528         [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)
     532        [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi)
    529533          lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) sigma))
    530534          cases (bvt_lookup_opt … (bitvector_of_nat ? i) sigma) in ⊢ (???% → %);
     
    566570    ]
    567571  ]
    568   | (* lookup 0 = 0 *)
     572  | (* 0 ↦ 0 *)
    569573    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
    570574    >lookup_insert_miss
    571     [ @(proj2 ?? (proj1 ?? (proj1 ?? Hp)))
     575    [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))
    572576    | @bitvector_of_nat_abs
    573577      [ / by /
     
    577581      ]
    578582    ]
     583  ]
     584  | (* fst p = pc *)
     585    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
     586    >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
    579587  ]
    580588  | (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi;
     
    599607    / by refl/
    600608  ]
    601 | @conj [ @conj [ @conj [ @conj [ @conj
     609| @conj [ @conj [ @conj [ @conj [ @conj [ @conj
    602610  [ #i cases i
    603611    [ #Hi2 @conj
     
    629637  | >lookup_insert_hit @refl
    630638  ]
     639  | >lookup_insert_hit @refl
     640  ]
    631641  | #i cases i
    632642    [ #Hi >lookup_opt_insert_hit @(ex_intro ?? 0) @refl
     
    643653 * if we have not added anything to the pc, we only know the PC hasn't changed,
    644654 * there might still have been a short/medium jump change *)
    645 definition policy_pc_equal ≝
     655definition sigma_pc_equal ≝
    646656  λprogram:list labelled_instruction.λp1,p2:ppc_pc_map.
    647   (∀n:ℕ.n ≤ |program| →
     657  (∀n.n ≤ |program| →
    648658    \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) =
    649659    \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)).
    650660
    651 definition policy_jump_equal ≝
     661definition sigma_jump_equal ≝
    652662  λprogram:list labelled_instruction.λp1,p2:ppc_pc_map.
    653   (∀n:ℕ.n < |program| →
     663  (∀n.n < |program| →
    654664    \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) =
    655665    \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)).
     
    750760qed.
    751761
    752 definition policy_safe: list labelled_instruction → label_map → ℕ → ppc_pc_map → ppc_pc_map → Prop ≝
    753  λprogram.λlabels.λadded.λold_sigma.λsigma.
    754  ∀i.i < |program| →
    755  let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉 in
    756  let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in
    757  let 〈label,instr〉 ≝ nth i ? program 〈None ?, Comment [ ]〉 in
    758  ∀dest.is_jump_to instr dest →
    759    let paddr ≝ lookup_def … labels dest 0 in
    760    let addr ≝ bitvector_of_nat ? (if leb i paddr (* forward jump *)
    761    then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added
    762    else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,short_jump〉)) in
    763    match j with
    764    [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧
    765       ¬is_call instr
    766    | medium_jump ⇒  \fst (medium_jump_cond pc_plus_jmp_length addr) = true ∧
    767        \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧
    768        ¬is_relative_jump instr
    769    | long_jump   ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧
    770        \fst (medium_jump_cond pc_plus_jmp_length addr) = false
    771    ].
    772 
    773762lemma not_true_is_false:
    774763  ∀b:bool.b ≠ true → b = false.
Note: See TracChangeset for help on using the changeset viewer.