Changeset 2101


Ignore:
Timestamp:
Jun 19, 2012, 4:43:50 PM (5 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
Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2081 r2101  
    1212inductive jump_length: Type[0] ≝
    1313  | short_jump: jump_length
    14   | medium_jump: jump_length
     14  | absolute_jump: jump_length
    1515  | long_jump: jump_length.
    1616 
     
    2626      〈eq_bv 9 upper (zero …), false:::lower〉.
    2727 
    28 definition medium_jump_cond: Word → Word → (*pseudo_instruction →*)
     28definition absolute_jump_cond: Word → Word → (*pseudo_instruction →*)
    2929  bool × (BitVector 11) ≝
    3030  λpc_plus_jmp_length.λaddr.(*λinstr.*)
     
    528528    let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    529529    let lookup_address ≝ sigma (lookup_labels call) in
    530     let 〈mj_possible, disp〉 ≝ medium_jump_cond pc_plus_jmp_length lookup_address in
     530    let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
    531531    let do_a_long ≝ policy ppc in
    532532    if mj_possible ∧ ¬ do_a_long then
     
    549549        [ SJMP address ]
    550550    else
    551       let 〈mj_possible, disp2〉 ≝ medium_jump_cond pc_plus_jmp_length lookup_address in
     551      let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
    552552      if mj_possible ∧ ¬ do_a_long then
    553553        let address ≝ ADDR11 disp2 in
  • src/ASM/Policy.ma

    r2078 r2101  
    88  on n:(Σx:bool × (option ppc_pc_map).
    99    let 〈no_ch,pol〉 ≝ x in
    10     And
    11     (match pol with
     10    match pol with
    1211    [ None ⇒ True
    1312    | Some x ⇒
    1413      And (And (And (And (And
    1514        (out_of_program_none program x)
    16         (jump_not_in_policy program x))
    17         (no_ch = true → policy_compact program (create_label_map program) x))
     15        (not_jump_default program x))
    1816        (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd x) 〈0,short_jump〉) = 0))
    1917        (\fst x = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd x) 〈0,short_jump〉)))
    20         (\fst x < 2^16)
    21     ]) (n = 0 → no_ch = false)) ≝
    22   let labels ≝ create_label_map program in
     18        (\fst x < 2^16))
     19        (no_ch = true → sigma_compact program (create_label_map program) x)
     20    ]) ≝
     21 let labels ≝ create_label_map program in
    2322  match n return λx.n = x → Σa:bool × (option ppc_pc_map).? with
    2423  [ O   ⇒ λp.〈false,pi1 ?? (jump_expansion_start program labels)〉
     
    3332[ normalize nodelta cases (jump_expansion_start program (create_label_map program))
    3433  #x cases x -x
    35   [ #H @conj / by I/
    36   | #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj [ @conj
    37     [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    38     | >p #H destruct (H)
     34  [ #H / by I/
     35  | #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj
     36    [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))
     37    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    3938    ]
    4039    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
    4140    ]
    42     | cases daemon (* XXX add this to jump_expansion_start *)
    43     ]
    4441    | @(proj2 ?? H)
    4542    ]
    46     | / by /
    47     ]
    48   ]
    49 | normalize nodelta @conj [ / by I/ | >p #H destruct (H) ]
     43    | #H destruct (H)
     44    ]
     45  ]
     46| / by I/
    5047| cases no_ch in p1; #p1
    51   [ normalize nodelta lapply (pi2 ?? (jump_expansion_internal program m))
    52     <p1 >p2 normalize nodelta #H @conj
    53     [ @(proj1 ?? H)
    54     | >p #H2 destruct (H2)
    55     ]
     48  [ @(pi2 ?? (jump_expansion_internal program m))
    5649  | cases (jump_expansion_step program (create_label_map program) «op,?»)
    5750    #x cases x -x #ch2 #z2 cases z2 normalize nodelta
    58     [ #_ @conj [ / by I/ | >p #H2 destruct (H2) ]
    59     | #j2 #H2 @conj [ @conj [ @conj [ @conj [ @conj
     51    [ #_ / by I/
     52    | #j2 #H2 @conj [ @conj [ @conj [ @conj
    6053      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))))
     54      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))
     55      ]
     56      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
     57      ]     
     58      | @(proj2 ?? H2)
     59      ]
    6160      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))
    62       ]
    63       | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))
    64       ]
    65       | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
    66       ]
    67       | @(proj2 ?? H2)
    68       ]
    69       | >p #H3 destruct (H3)
    7061      ]
    7162    ]
     
    7566  [ #_ >p2 #ABS destruct (ABS)
    7667  | #map >p2 normalize nodelta
    77     #H #eq destruct (eq) @conj [ @conj [ @conj
    78     [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    79     | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
    80     ]
    81     | @(proj2 ?? (proj1 ?? (proj1 ?? H)))
    82     ]
    83     | @(proj2 ?? (proj1 ?? H))
    84     ]
    85   ]
    86 ]
    87 qed.
    88 
    89 lemma pe_int_refl: ∀program.reflexive ? (policy_jump_equal program).
     68    #H #eq destruct (eq) @(proj1 ?? H)
     69  ]
     70]
     71qed.
     72
     73lemma pe_int_refl: ∀program.reflexive ? (sigma_jump_equal program).
    9074#program whd #x whd #n #Hn
    9175cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,short_jump〉)
     
    9377qed.
    9478
    95 lemma pe_int_sym: ∀program.symmetric ? (policy_jump_equal program).
     79lemma pe_int_sym: ∀program.symmetric ? (sigma_jump_equal program).
    9680#program whd #x #y #Hxy whd #n #Hn
    9781lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉)
     
    10185qed.
    10286 
    103 lemma pe_int_trans: ∀program.transitive ? (policy_jump_equal program).
    104 #program whd #x #y #z whd in match (policy_jump_equal ???); whd in match (policy_jump_equal ?y ?);
    105 whd in match (policy_jump_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
     87lemma pe_int_trans: ∀program.transitive ? (sigma_jump_equal program).
     88#program whd #x #y #z whd in match (sigma_jump_equal ???); whd in match (sigma_jump_equal ?y ?);
     89whd in match (sigma_jump_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
    10690lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉)
    10791#x1 #x2
     
    11599  match p1 with
    116100  [ Some x1 ⇒ match p2 with
    117               [ Some x2 ⇒ policy_jump_equal program x1 x2
     101              [ Some x2 ⇒ sigma_jump_equal program x1 x2
    118102              | _       ⇒ False
    119103              ]
     
    161145 #x1 cases x1 #p1 #j1 -x1; #H1 #Heqj #Hj #k elim k
    162146[ <plus_n_O >Heqj @Hj
    163 | #k' -k <plus_n_Sm (*whd in match (jump_expansion_internal program (S (n+k')));*)
     147| #k' -k <plus_n_Sm
    164148  lapply (refl ? (jump_expansion_internal program (n+k')))
    165149  cases (jump_expansion_internal program (n+k')) in ⊢ (???% → %);
     
    209193 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) with
    210194   [ long_jump   ⇒ measure_int t policy (acc + 2)
    211    | medium_jump ⇒ measure_int t policy (acc + 1)
     195   | absolute_jump ⇒ measure_int t policy (acc + 1)
    212196   | _           ⇒ measure_int t policy acc
    213197   ]
     
    247231  ∀policy:Σp:ppc_pc_map.
    248232    out_of_program_none program p ∧
    249     jump_not_in_policy program p ∧
     233    not_jump_default program p ∧
    250234    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
    251235    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
     
    332316lemma measure_special: ∀program:(Σl:list labelled_instruction.(S (|l|)) < 2^16).
    333317  ∀policy:Σp:ppc_pc_map.
    334     out_of_program_none program p ∧ jump_not_in_policy program p ∧
     318    out_of_program_none program p ∧ not_jump_default program p ∧
    335319    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
    336320    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
     
    338322  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with
    339323  [ None ⇒ True
    340   | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_jump_equal program policy p ].
     324  | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → sigma_jump_equal program policy p ].
    341325#program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program) policy)))
    342326cases (jump_expansion_step program (create_label_map program) policy) in ⊢ (???% → %);
     
    346330  @(list_ind ?  (λx.|x| ≤ |pi1 ?? program| →
    347331      measure_int x policy 0 = measure_int x p 0 →
    348       policy_jump_equal x policy p) ?? (pi1 ?? program))
     332      sigma_jump_equal x policy p) ?? (pi1 ?? program))
    349333 [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @le_to_not_lt @le_O_n
    350334 | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … (le_S_S_to_le …  Hi)) -Hi #Hi
     
    432416definition je_fixpoint: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).
    433417  Σp:option ppc_pc_map.
    434     And (match p with
     418    match p with
    435419      [ None ⇒ True
    436       | Some pol ⇒ And (out_of_program_none program pol)
    437       (policy_compact program (create_label_map program) pol)
    438       ])
    439     (∃n.∀k.n < k →
    440       policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program k))) p).
    441 #program @(\snd (pi1 ?? (jump_expansion_internal program (2*|program|)))) @conj
    442 [ lapply (pi2 ?? (jump_expansion_internal program (2*|program|)))
    443   cases (jump_expansion_internal program (2*|program|)) #p cases p -p
    444   #c #pol #Hp cases pol
    445   [ normalize nodelta //
    446   | #x normalize nodelta #H @conj
    447     [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))
    448     | #Hneq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    449       cases daemon (* XXX add invariant here *)
    450     ]
    451   ]
    452 | cases (dec_bounded_exists (λk.policy_equal_opt (pi1 ?? program)
     420      | Some pol ⇒ And (And (out_of_program_none program pol)
     421      (sigma_compact program (create_label_map program) pol))
     422      (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0)
     423      ].
     424#program @(\snd (jump_expansion_internal program (S (2*|program|))))
     425cases (dec_bounded_exists (λk.policy_equal_opt (pi1 ?? program)
    453426   (\snd (pi1 ?? (jump_expansion_internal program k)))
    454427   (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*|program|))
    455 [ #Hex elim Hex -Hex #x #Hx @(ex_intro … x) #k #Hk
    456   @pe_trans
    457   [ @(\snd (pi1 ?? (jump_expansion_internal program x)))
    458   | @pe_sym @equal_remains_equal
    459     [ @(proj2 ?? Hx)
    460     | @le_S_S_to_le @le_S @Hk
    461     ]
    462   | @equal_remains_equal
    463     [ @(proj2 ?? Hx)
    464     | @(proj1 ?? Hx)
    465     ]   
    466   ]
    467 | #Hnex lapply (not_exists_forall … Hnex) -Hnex; #Hfa
    468   @(ex_intro … (2*|program|)) #k #Hk @pe_sym @equal_remains_equal
    469   [ lapply (refl ? (jump_expansion_internal program (2*|program|)))
    470     cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %);
    471     #x cases x -x #Fch #Fpol normalize nodelta #HFpol cases Fpol in HFpol; normalize nodelta
    472     [ (* if we're at None in 2*|program|, we're at None in S 2*|program| too *)
    473       #HFpol #EQ whd in match (jump_expansion_internal ??); >EQ
    474       normalize nodelta / by /
    475     | #Fp #HFp #EQ whd in match (jump_expansion_internal ??);
    476       >EQ normalize nodelta
    477       lapply (refl ? (jump_expansion_step program (create_label_map program) «Fp,?»))
    478       [ @conj [ @conj [ @conj
    479       [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))))
    480       | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))
    481       ]
    482       | @(proj2 ?? (proj1 ?? (proj1 ?? HFp)))
    483       ]
    484       | @(proj2 ?? (proj1 ?? HFp))
    485       ]
    486       | lapply (measure_full program Fp ?)
    487         [ @le_to_le_to_eq
    488           [ @measure_le
    489           | cut (∀x:ℕ.x ≤ 2*|program| →
    490              ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧
    491                 x ≤ measure_int program p 0))
    492             [ #x elim x
    493               [ #Hx lapply (refl ? (jump_expansion_start program (create_label_map program)))
    494                 cases (jump_expansion_start program (create_label_map program)) in ⊢ (???% → %);
    495                 #z cases z -z normalize nodelta
    496                 [ #Waar #Heqn @⊥ elim (le_to_eq_plus ?? Hx) #k #Hk
    497                   @(absurd … (step_none program 0 ? k))
    498                   [ whd in match (jump_expansion_internal ??); >Heqn @refl
    499                   | <Hk >EQ @nmk #H destruct (H)
    500                   ]
    501                 | #pol #Hpol #Heqpol @(ex_intro ?? pol) @conj
    502                   [ whd in match (jump_expansion_internal ??); >Heqpol @refl
    503                   | @le_O_n
    504                   ]
    505                 ]
    506               | -x #x #Hind #Hx
    507                 lapply (refl ? (jump_expansion_internal program (S x)))
    508                 cases (jump_expansion_internal program (S x)) in ⊢ (???% → %);
    509                 #z cases z -z #Sxch #Sxpol cases Sxpol -Sxpol normalize nodelta
    510                 [ #H #HeqSxpol @⊥ elim (le_to_eq_plus ?? Hx) #k #Hk
    511                   @(absurd … (step_none program (S x) ? k))
    512                   [ >HeqSxpol / by /
    513                   | <Hk >EQ @nmk #H destruct (H)
    514                   ]
    515                 | #Sxpol #HSxpol #HeqSxpol @(ex_intro ?? Sxpol) @conj
    516                   [ @refl
    517                   | elim (Hind (transitive_le … (le_n_Sn x) Hx))
    518                     #xpol #Hxpol @(le_to_lt_to_lt … (proj2 ?? Hxpol))
    519                     lapply (measure_incr_or_equal program xpol program (le_n (|program|)) 0)
    520                     [ cases (jump_expansion_internal program x) in Hxpol;
    521                       #z cases z -z #xch #xpol normalize nodelta #H #H2 >(proj1 ?? H2) in H;
    522                       normalize nodelta #H @conj [ @conj [ @conj
    523                       [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    524                       | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) ]
    525                       | @(proj2 ?? (proj1 ?? (proj1 ?? H))) ]
    526                       | @(proj2 ?? (proj1 ?? H)) ]
    527                     | lapply (Hfa x (le_S_to_le … Hx)) lapply HeqSxpol -HeqSxpol
    528                       lapply (refl ? (jump_expansion_internal program x))
    529                       lapply Hxpol -Hxpol
    530                       cases daemon (* this whd takes an enormous amount of time *)
    531                       (* whd in match (pi1 ?? (jump_expansion_internal program (S x)));
    532                       cases (jump_expansion_internal program x) in ⊢ (% → ???% → %);
    533                       #z cases z -z #xch #b normalize nodelta #H #Heq >(proj1 ?? Heq) in H;
    534                       #H #Heq2 cases xch in H Heq2; #H #Heq2 normalize nodelta
    535                       [ lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»))
    536                         [ @conj [ @conj [ @conj
    537                           [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
    538                           | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) ]
    539                           | @(proj2 ?? (proj1 ?? (proj1 ?? H))) ]
    540                           | @(proj2 ?? (proj1 ?? H)) ]
    541                         | cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z -z #a #c
    542                           normalize nodelta cases c normalize nodelta
    543                           [ #H1 #Heq #H2 destruct (H2)
    544                           | #d #H1 #Heq #H2 destruct (H2) #Hfull #H2 elim (le_to_or_lt_eq … H2)
    545                             [ / by /
    546                             | #H3 lapply (measure_special program «xpol,?»)
    547                               [ @conj [ @conj
    548                                 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
    549                                 | @(proj2 ?? (proj1 ?? (proj1 ?? H))) ]
    550                                 | @(proj2 ?? (proj1 ?? H)) ]
    551                               | >Heq normalize nodelta #H4 @⊥ @(absurd … (H4 H3)) @Hfull
    552                               ]
    553                             ]
    554                           ]
    555                         ]
    556                       | lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»))
    557                         [ @conj [ @conj
    558                           [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
    559                           | @(proj2 ?? (proj1 ?? (proj1 ?? H))) ]
    560                           | @(proj2 ?? (proj1 ?? H)) ]
    561                         | cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z -z #a #c
    562                           normalize nodelta cases c normalize nodelta
    563                           [ #H1 #Heq #H2 #H3 #_ @⊥ @(absurd ?? H3) @pe_refl
    564                           | #d #H1 #Heq #H2 #H3 @⊥ @(absurd ?? H3) @pe_refl
    565                           ]
    566                         ]
    567                       ] *)
    568                     ]
    569                   ]
    570                 ]
    571               ]
    572             | #H elim (H (2*|program|) (le_n ?)) #plp >EQ #Hplp
    573               >(Some_eq ??? (proj1 ?? Hplp)) @(proj2 ?? Hplp)
    574             ]
    575           ]
    576         | #Hfull cases (jump_expansion_step program (create_label_map program) «Fp,?») in ⊢ (???% → %);
    577           #x cases x -x #Gch #Gpol cases Gpol normalize nodelta
    578           [ #H #EQ2 @⊥ @(absurd ?? H) @Hfull
    579           | #Gp #HGp #EQ2 cases Fch
    580             [ normalize nodelta /2 by pe_int_refl/
    581             | normalize nodelta #i #Hi
    582               cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) #Hj
    583               [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))))) i (le_S_to_le … Hi))
    584                 lapply (Hfull i Hi Hj)
    585                 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
    586                 #fp #fj #Hfj >Hfj normalize nodelta
    587                 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Gp) 〈0,short_jump〉)
    588                 #gp #gj cases gj normalize nodelta
    589                 [1,2: #H cases H #H2 cases H2 destruct (H2)
    590                 |3: #_ @refl
    591                 ]
    592               | >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))))) i Hi Hj)
    593                 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))) i Hi Hj) @refl
     428[ #Hex cases Hex -Hex #k #Hk
     429  lapply (refl ? (jump_expansion_internal program (S (2*|program|))))
     430  cases (jump_expansion_internal ? (S (2*|program|))) in ⊢ (???% → %);
     431  #x cases x -x #Gno_ch #Go cases Go normalize nodelta
     432  [ #H #Heq / by I/
     433  | -Go #Gp #HGp #Geq
     434    cut (policy_equal_opt program (\snd (jump_expansion_internal program (2*|program|)))
     435      (\snd (jump_expansion_internal program (S (2*|program|)))))
     436    [ @(pe_trans … (equal_remains_equal program k (proj2 ?? Hk) (S (2*|program|)) (le_S … (le_S_to_le … (proj1 ?? Hk)))))
     437      @pe_sym @equal_remains_equal [ @(proj2 ?? Hk) | @(le_S_to_le … (proj1 ?? Hk)) ]
     438    | >Geq lapply (refl ? (jump_expansion_internal program (2*|program|)))
     439      cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %);
     440      #x cases x -x #Fno_ch #Fo cases Fo normalize nodelta
     441      [ #H #Feq whd in match policy_equal_opt; normalize nodelta #ABS destruct (ABS)
     442      | -Fo #Fp #HFp #Feq whd in match policy_equal_opt; normalize nodelta #Heq
     443        @conj [ @conj
     444        [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))))
     445        | @(proj2 ?? HGp) whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*80s*)
     446          >Feq in Geq; cases Fno_ch in HFp Feq; normalize nodelta #HFp #Feq #Geq
     447          [ destruct (Geq) / by /
     448          | cases (jump_expansion_step program (create_label_map (pi1 ?? program)) «Fp,?») in Geq;
     449            #x cases x -x #Sch #So normalize nodelta cases So
     450            [ normalize nodelta #_ #ABS destruct (ABS)
     451            | -So normalize nodelta #Sp #HSp #Seq <(proj1 ?? (pair_destruct ?????? (pi1_eq ???? Seq)))
     452              cases Sch in HSp Seq; #HSp #Seq
     453              [ @refl
     454              | normalize nodelta in Seq; @(proj2 ?? (proj1 ?? HSp))
     455                >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Seq))))
     456                @Heq
    594457              ]
    595458            ]
    596459          ]
    597460        ]
    598       ]
    599     ]
    600   | @le_S_S_to_le @le_S @Hk
     461        | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
     462        ]
     463      ]
     464    ]
     465  ]
     466| #Hnex lapply (not_exists_forall … Hnex) -Hnex #Hfa
     467  lapply (refl ? (jump_expansion_internal program (2*|program|)))
     468  cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %);
     469  #x cases x -x #Fno_ch #Fo cases Fo normalize nodelta
     470  [ (* None *)
     471     #HF #Feq lapply (step_none program (2*|program|) ? 1) >Feq / by /
     472    <plus_n_Sm <plus_n_O #H >H -H normalize nodelta / by I/
     473  | -Fo #Fp #HFp #Feq lapply (measure_full program Fp ?)
     474    [ @le_to_le_to_eq
     475      [ @measure_le
     476      | cut (∀x:ℕ.x ≤ 2*|program| →
     477         ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧
     478          x ≤ measure_int program p 0))
     479        [ #x elim x
     480          [ #Hx lapply (refl ? (jump_expansion_start program (create_label_map program)))
     481            cases (jump_expansion_start program (create_label_map program)) in ⊢ (???% → %);
     482             #z cases z -z normalize nodelta
     483             [ #H #Heqn @⊥ elim (le_to_eq_plus ?? Hx) #n #Hn
     484               @(absurd … (step_none program 0 ? n))
     485               [ whd in match (jump_expansion_internal ??); >Heqn @refl
     486               | <Hn >Feq @nmk #H destruct (H)
     487               ]
     488             | #Zp #HZp #Zeq @(ex_intro ?? Zp) @conj
     489               [ whd in match (jump_expansion_internal ??); >Zeq @refl
     490               | @le_O_n
     491               ]
     492             ]
     493          | -x #x #Hind #Hx
     494            lapply (refl ? (jump_expansion_internal program (S x)))
     495            cases (jump_expansion_internal program (S x)) in ⊢ (???% → %);
     496            #z cases z -z #Sno_ch #So cases So -So
     497            [ #HSp #Seq normalize nodelta @⊥ elim (le_to_eq_plus ?? Hx) #k #Hk
     498              @(absurd … (step_none program (S x) ? k))
     499              [ >Seq @refl
     500              | <Hk >Feq @nmk #H destruct (H)
     501              ]
     502            | #Sp #HSp #Seq @(ex_intro ?? Sp) @conj
     503              [ @refl
     504              | elim (Hind (transitive_le … (le_n_Sn x) Hx))
     505                #pol #Hpol @(le_to_lt_to_lt … (proj2 ?? Hpol))
     506                lapply (proj1 ?? Hpol) -Hpol
     507                lapply (refl ? (jump_expansion_internal program x))
     508                cases (jump_expansion_internal program x) in ⊢ (???% → %);
     509                #z cases z -z #Xno_ch #Xo cases Xo
     510                [ #HXp #Xeq #abs destruct (abs)
     511                | normalize nodelta #Xp #HXp #Xeq #H <(Some_eq ??? H) -H -pol
     512                  lapply (Hfa x Hx) >Xeq >Seq whd in match policy_equal_opt;
     513                  normalize nodelta #Hpe
     514                  lapply (measure_incr_or_equal program Xp program (le_n (|program|)) 0)
     515                  [ @(proj1 ?? HXp)
     516                  | lapply (Hfa x Hx) >Xeq >Seq
     517                    lapply (measure_special program «Xp,?»)
     518                    [ @(proj1 ?? HXp)
     519                    | lapply Seq whd in match (jump_expansion_internal program (S x)); (*340s*)
     520                      >Xeq normalize nodelta cases Xno_ch in HXp Xeq; #HXp #Xeq
     521                      [ normalize nodelta #EQ
     522                        >(proj2 ?? (pair_destruct ?????? (pi1_eq ???? EQ)))
     523                        #_ #abs @⊥ @(absurd ?? abs) / by /
     524                      | normalize nodelta cases (jump_expansion_step ???);
     525                        #z cases z -z #stch #sto cases sto   
     526                        [ normalize nodelta #_ #ABS destruct (ABS)
     527                        | -sto #stp normalize nodelta #Hstp #steq
     528                          >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? steq))))
     529                          #Hms #Hneq #glerp elim (le_to_or_lt_eq … glerp)
     530                          [ / by /
     531                          | #glorp @⊥ @(absurd ?? Hneq) @Hms @glorp
     532                          ]
     533                        ]
     534                      ]
     535                    ]
     536                  ]
     537                ]
     538              ]
     539            ]
     540          ]
     541        | #H elim (H (2*|program|) (le_n ?)) #plp >Feq #Hplp
     542          >(Some_eq ??? (proj1 ?? Hplp)) @(proj2 ?? Hplp)
     543        ]
     544      ]
     545    | #Hfull
     546      whd in match (jump_expansion_internal program (S (2*|program|))); (*65s*)
     547      >Feq normalize nodelta cases Fno_ch in HFp Feq; #HFp #Feq
     548      normalize nodelta
     549      [ @conj [ @conj
     550        [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))))
     551        | @((proj2 ?? HFp) (refl ? true)) ]
     552        | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))
     553        ]
     554      | cases (jump_expansion_step ???); #z cases z -z #stch #sto cases sto
     555        [ #_ / by I/
     556        | -sto #stp normalize nodelta #Hstp @conj [ @conj
     557          [ @(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
     570              ]
     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
     573            ]
     574          ]
     575        | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))) ]
     576        ]
     577      ]
     578    ]
    601579  ]
    602580| #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
     
    607585  |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); //
    608586    #H destruct (H)
    609   |4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); cases program #p #_ cases p
    610     [ %1 #m #Hm @⊥ @(absurd ? Hm) @le_to_not_lt @le_O_n
    611     | #h #t elim (dec_bounded_forall ?? (|t|))
    612       [1: #Hyp %1 #m #Hm @(Hyp m) @(le_S_S_to_le … Hm)
    613       |2: #Hyp %2 @nmk #H @(absurd ?? Hyp) #m #Hm @(H m) @(le_S_S … Hm)
    614       | #m cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉)
    615         #x1 #x2
    616         cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉)
    617         #y1 #y2 normalize nodelta
    618         @dec_eq_jump_length
    619       ]
    620      
    621     ] 
    622   ]
    623 ]
     587  |4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m
     588      cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉)
     589      #x1 #x2
     590      cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉)
     591      #y1 #y2 normalize nodelta
     592      @dec_eq_jump_length
     593  ]
     594]
    624595qed.
    625596
     
    627598include alias "basics/logic.ma".
    628599
     600lemma 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]
     610qed.
     611
    629612(* The glue between Policy and Assembly. *)
    630 (*CSC: modified to really use the specification in Assembly.ma.
    631   I have modified all that follows in vi without testing it in Matita.
    632   Jaap, please repair it *)
     613(*CSC: modified to really use the specification in Assembly.ma.*)
    633614definition jump_expansion':
    634615∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16).
    635616 option (Σsigma_policy:(Word → Word) × (Word → bool).
    636617   let 〈sigma,policy〉≝ sigma_policy in
    637    sigma_policy_specification program sigma policy
    638 
     618   sigma_policy_specification 〈\fst program,\snd program〉 sigma policy)
     619   
    639620 λprogram.
    640   let policy ≝ pi1 … (je_fixpoint (\snd program)) in
    641   match policy with
    642   [ None ⇒ None ?
    643   | Some x ⇒ Some ?
     621  let f: option ppc_pc_map ≝ je_fixpoint (\snd program) in
     622  match f return λx.f = x → ? with
     623  [ None ⇒ λp.None ?
     624  | Some x ⇒ λp.Some ?
    644625      «〈(λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
    645626          bitvector_of_nat 16 pc),
    646627         (λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
    647628          jmpeqb jl long_jump)〉,?»
    648   ].
    649  #ppc normalize nodelta cases daemon
    650 qed.
     629  ] (refl ? f).
     630normalize nodelta in p; whd in match sigma_policy_specification; normalize nodelta
     631lapply (pi2 ?? (je_fixpoint (\snd program))) >p normalize nodelta cases x
     632#fpc #fpol #Hfpol
     633@conj
     634[ lapply (proj2 ?? Hfpol) cases (bvt_lookup ??? fpol 〈0,short_jump〉)
     635  #x #y #Hx normalize nodelta >Hx / by refl/
     636| #ppc #ppc_ok @conj
     637  [ #Hppc lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector 16 ppc) ppc_ok)
     638    >bitvector_of_nat_inverse_nat_of_bitvector
     639    lapply (refl ? (lookup_opt … ppc fpol)) cases (lookup_opt … ppc fpol) in ⊢ (???% → %);
     640    [ normalize nodelta #_ #abs cases abs
     641    | #x cases x -x #x1 #y1 normalize nodelta #Hl_ppc
     642      >(plus_n_O (nat_of_bitvector 16 ppc)) >plus_n_Sm <add_bitvector_of_nat_plus
     643      >bitvector_of_nat_inverse_nat_of_bitvector
     644      lapply (refl ? (lookup_opt … (add 16 ppc (bitvector_of_nat 16 1)) fpol))
     645      cases (lookup_opt … (add 16 ppc (bitvector_of_nat 16 1)) fpol) in ⊢ (???% → %);
     646      [ normalize nodelta #_ #abs cases abs
     647      | #x cases x -x #x2 #y2 normalize nodelta #Hl_Sppc
     648        #Hcompact >(lookup_opt_lookup_hit … Hl_Sppc 〈0,short_jump〉)
     649        >(lookup_opt_lookup_hit … Hl_ppc 〈0,short_jump〉) normalize nodelta
     650        >add_bitvector_of_nat_plus whd in match (fetch_pseudo_instruction ???);
     651        >(nth_safe_nth … 〈None ?, Comment []〉)
     652        >Hcompact <plus_n_O
     653        cases (nth (nat_of_bitvector ? ppc) ? (\snd program) ?) #a #b normalize nodelta
     654        whd in match instruction_size; normalize nodelta
     655        whd in match assembly_1_pseudoinstruction; normalize nodelta
     656        whd in match expand_pseudo_instruction; normalize nodelta
     657        cases b
     658        [2,3,6: #p [3: #q] normalize nodelta @refl
     659        |4,5: #p normalize nodelta
     660          >(lookup_opt_lookup_hit … Hl_Sppc 〈0,short_jump〉) normalize nodelta
     661          >(lookup_opt_lookup_hit … Hl_ppc 〈0,short_jump〉) normalize nodelta
     662          whd in match (create_label_map ?);
     663          cases (lookup ?? (bitvector_of_nat ?
     664          (lookup_def ?? (\fst (create_label_cost_map (\snd program))) p 0)) fpol 〈0,short_jump〉)
     665          #z1 #z2 normalize nodelta @refl
     666        |1: #pi cases pi
     667          [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
     668            [1,2,3,6,7,24,25: #p #q
     669            |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #p]
     670            normalize nodelta @refl
     671          |9,10,11,12,13,14,15,16,17: [1,2,6,7: #p |3,4,5,8,9: #q #p] normalize nodelta
     672            whd in match expand_relative_jump; normalize nodelta
     673            whd in match expand_relative_jump_internal; normalize nodelta
     674            >(lookup_opt_lookup_hit … Hl_Sppc 〈0,short_jump〉) normalize nodelta
     675            >(lookup_opt_lookup_hit … Hl_ppc 〈0,short_jump〉) normalize nodelta
     676            whd in match (create_label_map ?);
     677            cases (lookup ?? (bitvector_of_nat ?
     678            (lookup_def ?? (\fst (create_label_cost_map (\snd program))) p 0)) fpol 〈0,short_jump〉)
     679            #z1 #z2 normalize nodelta @refl
     680          ]
     681        ]
     682      ]
     683    ]
     684  | cases daemon (* XXX remains to be done *)
     685  ]
     686]
     687qed.           
     688     
     689
     690       
     691
     692    >(add_bitvector_of_nat_plus ?? ppc)
     693     
     694qed.
  • 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.
  • src/ASM/PolicyStep.ma

    r2059 r2101  
    1212  ∀old_policy:(Σpolicy:ppc_pc_map.
    1313    And (And (And (And (out_of_program_none program policy)
    14     (jump_not_in_policy program policy))
     14    (not_jump_default program policy))
    1515    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
    1616    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd policy) 〈0,short_jump〉)))
     
    2121    [ None ⇒ nec_plus_ultra program old_policy
    2222    | Some p ⇒ And (And (And (And (And (And (And (And (out_of_program_none program p)
    23        (jump_not_in_policy program p))
    24        (policy_increase program old_policy p))
    25        (no_ch = true → policy_compact program labels p))
     23       (not_jump_default program p))
     24       (jump_increase program old_policy p))
     25       (no_ch = true → sigma_compact program labels p))
    2626       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
    2727       (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
    28        (no_ch = true → policy_pc_equal program old_policy p))
    29        (policy_jump_equal program old_policy p → no_ch = true))
     28       (no_ch = true → sigma_pc_equal program old_policy p))
     29       (sigma_jump_equal program old_policy p → no_ch = true))
    3030       (\fst p < 2^16)
    3131    ])
     
    3737      let 〈added,policy〉 ≝ x in
    3838      And (And (And (And (And (And (And (And (out_of_program_none prefix policy)
    39       (jump_not_in_policy prefix policy))
    40       (policy_increase prefix old_sigma policy))
    41       (policy_compact_unsafe prefix labels policy))
    42       (policy_safe prefix labels added old_sigma policy))
     39      (not_jump_default prefix policy))
     40      (jump_increase prefix old_sigma policy))
     41      (sigma_compact_unsafe prefix labels policy))
     42      (sigma_safe prefix labels added old_sigma policy))
    4343      (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
    4444      (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
    45       (added = 0 → policy_pc_equal prefix old_sigma policy))
    46       (policy_jump_equal prefix old_sigma policy → added = 0))
     45      (added = 0 → sigma_pc_equal prefix old_sigma policy))
     46      (sigma_jump_equal prefix old_sigma policy → added = 0))
    4747    program
    4848    (λprefix.λx.λtl.λprf.λacc.
     
    165165                (* USE: added = 0 → policy_pc_equal *)
    166166                >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?)
    167                 [2,4,6,8: cases daemon (* XXX *) ]
     167                [2,4,6,8: lapply ((pi2 ?? labels) x)
     168                  whd in match address_of_word_labels_code_mem;
     169                  normalize nodelta cases daemon (* XXX *) ]
    168170                [1,5: >(eqb_true_to_eq … Hch) <plus_n_O]
    169171                cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
     
    177179                |1,3,9,11: #_ normalize nodelta @refl
    178180                ]
    179              |2,5: whd in match short_jump_cond; whd in match medium_jump_cond;
     181             |2,5: whd in match short_jump_cond; whd in match absolute_jump_cond;
    180182                lapply (refl ? (leb i (lookup_def ?? labels x 0)))
    181183                cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab
     
    192194                cases (get_index' bool 2 0 flags) normalize nodelta
    193195                #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl
    194              |3,6: whd in match short_jump_cond; whd in match medium_jump_cond;
     196             |3,6: whd in match short_jump_cond; whd in match absolute_jump_cond;
    195197                lapply (refl ? (leb i (lookup_def ?? labels x 0)))
    196198                cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab
  • src/utilities/extralib.ma

    r2006 r2101  
    8181
    8282lemma dec_bounded_forall:
    83   ∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ∀k.(∀n.n ≤ k → P n) + ¬(∀n.n ≤ k → P n).
     83  ∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ∀k.(∀n.n < k → P n) + ¬(∀n.n < k → P n).
    8484 #P #HP_dec #k elim k -k
    85  [ cases (HP_dec 0)
    86    [ #HP %1 #n #Hn <(le_n_O_to_eq … Hn) @HP
    87    | #HP %2 @nmk #H cases HP #H2 @H2 @H @le_n
    88    ]
     85 [ %1 #n #Hn @⊥ @(absurd (n < 0) Hn) @not_le_Sn_O
    8986 | #k #Hind cases Hind
    90    [ #Hk cases (HP_dec (S k))
    91      [ #HPk %1 #n #Hn elim (le_to_or_lt_eq … Hn)
     87   [ #Hk cases (HP_dec k)
     88     [ #HPk %1 #n #Hn cases (le_to_or_lt_eq … Hn)
    9289       [ #H @(Hk … (le_S_S_to_le … H))
    93        | #H >H @HPk
     90       | #H >(injective_S … H) @HPk
    9491       ]
    95      | #HPk %2 @nmk #Habs @(absurd (P (S k))) [ @(Habs … (le_n (S k))) | @HPk ]
     92     | #HPk %2 @nmk #Habs @(absurd (P k)) [ @(Habs … (le_n (S k))) | @HPk ]
    9693     ]
    97    | #Hk %2 @nmk #Habs @(absurd (∀n.nk→P n)) [ #n' #Hn' @(Habs … (le_S … Hn')) | @Hk ]
     94   | #Hk %2 @nmk #Habs @(absurd (∀n.n<k→P n)) [ #n' #Hn' @(Habs … (le_S … Hn')) | @Hk ]
    9895   ]
    9996 ]
     
    10198
    10299lemma dec_bounded_exists:
    103   ∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n ≤ k ∧ P n) + ¬(∃n.n ≤ k ∧ P n).
     100  ∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n < k ∧ P n) + ¬(∃n.n < k ∧ P n).
    104101 #P #HP_dec #k elim k -k
    105  [ cases (HP_dec 0)
    106    [ #HP %1 @(ex_intro ?? 0) @conj [ @le_n | @HP ]
    107    | #HP %2 @nmk #Habs @(absurd ?? HP) elim Habs #k #Hk
    108      >(le_n_O_to_eq … (proj1 ?? Hk)) @(proj2 ?? Hk)
    109    ]
     102 [ %2 @nmk #Habs elim Habs #n #Hn @(absurd (n < 0) (proj1 … Hn)) @not_le_Sn_O
    110103 | #k #Hind cases Hind
    111104   [ #Hk %1 elim Hk #n #Hn @(ex_intro … n) @conj [ @le_S @(proj1 … Hn) | @(proj2 … Hn) ]
    112    | #Hk cases (HP_dec (S k))
    113      [ #HPk %1 @(ex_intro … (S k)) @conj [ @le_n | @HPk ]
     105   | #Hk cases (HP_dec k)
     106     [ #HPk %1 @(ex_intro … k) @conj [ @le_n | @HPk ]
    114107     | #HPk %2 @nmk #Habs elim Habs #n #Hn cases (le_to_or_lt_eq … (proj1 … Hn))
    115        [ #H @(absurd (∃n.n k ∧ P n)) [ @(ex_intro … n) @conj
     108       [ #H @(absurd (∃n.n < k ∧ P n)) [ @(ex_intro … n) @conj
    116109         [ @(le_S_S_to_le … H) | @(proj2 … Hn) ] | @Hk ]
    117        | #H @(absurd (P (S k))) [ <H @(proj2 … Hn) | @HPk ]
     110       | #H @(absurd (P k)) [ <(injective_S … H) @(proj2 … Hn) | @HPk ]
    118111       ] 
    119112     ]
     
    138131
    139132lemma not_exists_forall:
    140   ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x ≤ k ∧ P x) → ∀x.x ≤ k → ¬P x.
     133  ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x < k ∧ P x) → ∀x.x < k → ¬P x.
    141134 #k #P #Hex #x #Hx @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x)
    142135 @conj [ @Hx | @Habs ]
     
    144137
    145138lemma not_forall_exists:
    146   ∀k:ℕ.∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ¬(∀x.x ≤ k → P x) → ∃x.x ≤ k ∧ ¬P x.
     139  ∀k:ℕ.∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ¬(∀x.x < k → P x) → ∃x.x < k ∧ ¬P x.
    147140 #k #P #Hdec elim k
    148  [ #Hfa @(ex_intro … 0) @conj
    149    [ @le_n
    150    | @nmk #HP @(absurd ?? Hfa) #i #Hi <(le_n_O_to_eq … Hi) @HP
    151    ]
    152  | -k #k #Hind #Hfa cases (Hdec (S k))
     141 [ #Hfa @⊥ @(absurd ?? Hfa) #z #Hz @⊥ @(absurd ? Hz) @not_le_Sn_O
     142 | -k #k #Hind #Hfa cases (Hdec k)
    153143   [ #HP elim (Hind ?)
    154144     [ -Hind; #x #Hx @(ex_intro ?? x) @conj [ @le_S @(proj1 ?? Hx) | @(proj2 ?? Hx) ]
    155145     | @nmk #H @(absurd ?? Hfa) #x #Hx cases (le_to_or_lt_eq ?? Hx)
    156146       [ #H2 @H @(le_S_S_to_le … H2)
    157        | #H2 >H2 @HP
     147       | #H2 >(injective_S … H2) @HP
    158148       ]
    159149     ]
    160    | #HP @(ex_intro … (S k)) @conj [ @le_n | @HP ]
     150   | #HP @(ex_intro … k) @conj [ @le_n | @HP ]
    161151   ]
    162152 ]
Note: See TracChangeset for help on using the changeset viewer.