Changeset 2059 for src/ASM/Policy.ma


Ignore:
Timestamp:
Jun 13, 2012, 3:44:20 PM (8 years ago)
Author:
boender
Message:
  • updated Policy to work better
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2055 r2059  
    77let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (S (|l|)) 2^16) (n: ℕ)
    88  on n:(Σx:bool × (option ppc_pc_map).
    9     let 〈c,pol〉 ≝ x in
     9    let 〈no_ch,pol〉 ≝ x in
    1010    And
    1111    (match pol with
    1212    [ None ⇒ True
    1313    | Some x ⇒
    14       And (And (And (And
     14      And (And (And (And (And
    1515        (out_of_program_none program x)
    1616        (jump_not_in_policy program x))
    17         (n > 0 → policy_compact program (create_label_map program) x))
     17        (no_ch = true → policy_compact program (create_label_map program) x))
    1818        (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd x) 〈0,short_jump〉) = 0))
     19        (\fst x = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd x) 〈0,short_jump〉)))
    1920        (\fst x < 2^16)
    20     ]) (n = 0 → c = true)) ≝
     21    ]) (n = 0 → no_ch = false)) ≝
    2122  let labels ≝ create_label_map program in
    2223  match n return λx.n = x → Σa:bool × (option ppc_pc_map).? with
    23   [ O   ⇒ λp.〈true,pi1 ?? (jump_expansion_start program labels)〉
    24   | S m ⇒ λp.let 〈ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
     24  [ O   ⇒ λp.〈false,pi1 ?? (jump_expansion_start program labels)〉
     25  | S m ⇒ λp.let 〈no_ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
    2526          match z return λx. z=x → Σa:bool × (option ppc_pc_map).? with
    2627          [ None    ⇒ λp2.〈false,None ?〉
    27           | Some op ⇒ λp2.if ch
    28             then pi1 ?? (jump_expansion_step program labels «op,?»)
    29             else pi1 ?? (jump_expansion_internal program m)
     28          | Some op ⇒ λp2.if no_ch
     29            then pi1 ?? (jump_expansion_internal program m)
     30            else pi1 ?? (jump_expansion_step program labels «op,?»)
    3031          ] (refl … z)
    3132  ] (refl … n).
     
    3334  #x cases x -x
    3435  [ #H @conj / by I/
    35   | #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj
     36  | #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj [ @conj
    3637    [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    37     | >p #H @⊥ @(absurd ? H) @le_to_not_lt @le_n
     38    | >p #H destruct (H)
    3839    ]
    3940    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
    4041    ]
     42    | cases daemon (* XXX add this to jump_expansion_start *)
     43    ]
    4144    | @(proj2 ?? H)
    4245    ]
     
    4548  ]
    4649| normalize nodelta @conj [ / by I/ | >p #H destruct (H) ]
    47 | cases ch in p1; #p1
    48   [ normalize nodelta
    49     cases (jump_expansion_step program (create_label_map program) «op,?»)
     50| 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    ]
     56  | cases (jump_expansion_step program (create_label_map program) «op,?»)
    5057    #x cases x -x #ch2 #z2 cases z2 normalize nodelta
    5158    [ #_ @conj [ / by I/ | >p #H2 destruct (H2) ]
    52     | #j2 #H2 @conj [ @conj [ @conj [ @conj
    53       [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))
    54       | #_ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))
     59    | #j2 #H2 @conj [ @conj [ @conj [ @conj [ @conj
     60      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))))
     61      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))
     62      ]
     63      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))
    5564      ]
    5665      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
     
    6069      | >p #H3 destruct (H3)
    6170      ]
    62     ]
    63   | normalize nodelta lapply (pi2 ?? (jump_expansion_internal program m))
    64     <p1 >p2 normalize nodelta #H @conj [ @conj [ @conj [ @conj
    65     [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
    66     | >p #Hm cases (le_to_or_lt_eq … Hm) -Hm #Hm
    67       [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @(le_S_S_to_le … Hm)
    68       | lapply ((proj2 ?? H) (sym_eq … (injective_S … Hm))) #H2 destruct (H2)
    69       ]
    70     ]
    71     | @(proj2 ?? (proj1 ?? (proj1 ?? H)))
    72     ]
    73     | @(proj2 ?? (proj1 ?? H))
    74     ]
    75     | >p #H2 destruct (H2)
    7671    ]
    7772  ]
     
    8075  [ #_ >p2 #ABS destruct (ABS)
    8176  | #map >p2 normalize nodelta
    82     #H #eq destruct (eq) @conj [ @conj
    83     [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     77    #H #eq destruct (eq) @conj [ @conj [ @conj
     78    [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
     79    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     80    ]
    8481    | @(proj2 ?? (proj1 ?? (proj1 ?? H)))
    8582    ]
     
    9087qed.
    9188
    92 lemma pe_int_refl: ∀program.reflexive ? (policy_equal program).
     89lemma pe_int_refl: ∀program.reflexive ? (policy_jump_equal program).
    9390#program whd #x whd #n #Hn
    9491cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,short_jump〉)
     
    9693qed.
    9794
    98 lemma pe_int_sym: ∀program.symmetric ? (policy_equal program).
     95lemma pe_int_sym: ∀program.symmetric ? (policy_jump_equal program).
    9996#program whd #x #y #Hxy whd #n #Hn
    10097lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉)
     
    104101qed.
    105102 
    106 lemma pe_int_trans: ∀program.transitive ? (policy_equal program).
    107 #program whd #x #y #z whd in match (policy_equal ???); whd in match (policy_equal ?y ?);
    108 whd in match (policy_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
     103lemma 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 ?);
     105whd in match (policy_jump_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
    109106lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉)
    110107#x1 #x2
     
    118115  match p1 with
    119116  [ Some x1 ⇒ match p2 with
    120               [ Some x2 ⇒ policy_equal program x1 x2
     117              [ Some x2 ⇒ policy_jump_equal program x1 x2
    121118              | _       ⇒ False
    122119              ]
     
    252249    jump_not_in_policy program p ∧
    253250    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
     251    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
    254252    \fst p < 2^16.
    255253  ∀l.|l| ≤ |program| → ∀acc:ℕ.
     
    265263  [ / by I/
    266264  | #x normalize nodelta #Hx #Hjeq
    267     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx))))) (|t|) Hp)
     265    lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))))) (|t|) (le_S_to_le … Hp))
    268266    whd in match (measure_int ???); whd in match (measure_int ? x ?);
    269267    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd (pi1 ?? policy)) 〈0,short_jump〉)
     
    336334    out_of_program_none program p ∧ jump_not_in_policy program p ∧
    337335    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
     336    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
    338337    \fst p < 2^16.
    339338  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with
    340339  [ None ⇒ True
    341   | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_equal program policy p ].
     340  | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_jump_equal program policy p ].
    342341#program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program) policy)))
    343342cases (jump_expansion_step program (create_label_map program) policy) in ⊢ (???% → %);
     
    347346  @(list_ind ?  (λx.|x| ≤ |pi1 ?? program| →
    348347      measure_int x policy 0 = measure_int x p 0 →
    349       policy_equal x policy p) ?? (pi1 ?? program))
     348      policy_jump_equal x policy p) ?? (pi1 ?? program))
    350349 [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @le_to_not_lt @le_O_n
    351350 | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … (le_S_S_to_le …  Hi)) -Hi #Hi
     
    353352     [ @(transitive_le … Hp) / by /
    354353     | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
    355        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))))) (|t|) Hp) #Hinc
    356        cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm Hinc; #x1 #x2
    357        cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉); #y1 #y2
    358        #Hm #Hinc lapply Hm -Hm; lapply Hinc -Hinc; normalize nodelta
     354       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) (|t|) (le_S_to_le … Hp))
     355       #Hinc cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm Hinc;
     356       #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉);
     357       #y1 #y2 #Hm #Hinc lapply Hm -Hm; lapply Hinc -Hinc; normalize nodelta
    359358       cases x2 cases y2 normalize nodelta
    360359       [1: / by /
     
    376375     ]
    377376   | >Hi whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
    378      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))))) (|t|) Hp)
     377     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) (|t|) (le_S_to_le … Hp))
    379378     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm;
    380379     #x1 #x2
     
    436435      [ None ⇒ True
    437436      | Some pol ⇒ And (out_of_program_none program pol)
    438       ((pi1 ?? program) ≠ [] → policy_compact program (create_label_map program) pol)
     437      (policy_compact program (create_label_map program) pol)
    439438      ])
    440439    (∃n.∀k.n < k →
     
    442441#program @(\snd (pi1 ?? (jump_expansion_internal program (2*|program|)))) @conj
    443442[ lapply (pi2 ?? (jump_expansion_internal program (2*|program|)))
    444     cases (jump_expansion_internal program (2*|program|)) #p cases p -p
    445     #c #pol #Hp cases pol
    446     [ normalize nodelta //
    447     | #x normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    448     | #Hneq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) cases (pi1 ?? program) in Hneq;
    449       [ #H cases H #H @⊥ @H @refl
    450       | #h #t #_ / by /
    451       ] ]
    452     ]
     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  ]
    453452| cases (dec_bounded_exists (λk.policy_equal_opt (pi1 ?? program)
    454453   (\snd (pi1 ?? (jump_expansion_internal program k)))
     
    477476      >EQ normalize nodelta
    478477      lapply (refl ? (jump_expansion_step program (create_label_map program) «Fp,?»))
    479       [ @conj [ @conj
    480       [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))
    481       | @(proj2 ?? (proj1 ?? (proj1 ?? HFp))) ]
    482       | @(proj2 ?? (proj1 ?? HFp)) ]
     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      ]
    483486      | lapply (measure_full program Fp ?)
    484487        [ @le_to_le_to_eq
     
    517520                    [ cases (jump_expansion_internal program x) in Hxpol;
    518521                      #z cases z -z #xch #xpol normalize nodelta #H #H2 >(proj1 ?? H2) in H;
    519                       normalize nodelta #H @conj [ @conj
    520                       [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     522                      normalize nodelta #H @conj [ @conj [ @conj
     523                      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
     524                      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) ]
    521525                      | @(proj2 ?? (proj1 ?? (proj1 ?? H))) ]
    522526                      | @(proj2 ?? (proj1 ?? H)) ]
     
    524528                      lapply (refl ? (jump_expansion_internal program x))
    525529                      lapply Hxpol -Hxpol
    526                       whd in match (jump_expansion_internal program (S x));
     530                      cases daemon (* this whd takes an enormous amount of time *)
     531                      (* whd in match (pi1 ?? (jump_expansion_internal program (S x)));
    527532                      cases (jump_expansion_internal program x) in ⊢ (% → ???% → %);
    528533                      #z cases z -z #xch #b normalize nodelta #H #Heq >(proj1 ?? Heq) in H;
    529534                      #H #Heq2 cases xch in H Heq2; #H #Heq2 normalize nodelta
    530535                      [ lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»))
    531                         [ @conj [ @conj
    532                           [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     536                        [ @conj [ @conj [ @conj
     537                          [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     538                          | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) ]
    533539                          | @(proj2 ?? (proj1 ?? (proj1 ?? H))) ]
    534540                          | @(proj2 ?? (proj1 ?? H)) ]
     
    559565                          ]
    560566                        ]
    561                       ]
     567                      ] *)
    562568                    ]
    563569                  ]
     
    572578          [ #H #EQ2 @⊥ @(absurd ?? H) @Hfull
    573579          | #Gp #HGp #EQ2 cases Fch
    574             [ normalize nodelta #i #Hi
     580            [ normalize nodelta /2 by pe_int_refl/
     581            | normalize nodelta #i #Hi
    575582              cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) #Hj
    576               [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))) i Hi)
     583              [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))))) i (le_S_to_le … Hi))
    577584                lapply (Hfull i Hi Hj)
    578585                cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
     
    583590                |3: #_ @refl
    584591                ]
    585               | >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))))) i Hi Hj)
    586                 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) i Hi Hj) @refl
     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
    587594              ]
    588             | normalize nodelta /2 by pe_int_refl/
    589595            ]
    590596          ]
     
    599605  cases npol in Hnpol; cases Spol in HSpol;
    600606  [ #Hnpol #HSpol %1 //
    601   |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal ???); //
     607  |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); //
    602608    #H destruct (H)
    603   |4: #np #Hnp #Sp #HSp whd in match (policy_equal ???); cases program #p #_ cases p
     609  |4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); cases program #p #_ cases p
    604610    [ %1 #m #Hm @⊥ @(absurd ? Hm) @le_to_not_lt @le_O_n
    605611    | #h #t elim (dec_bounded_forall ?? (|t|))
Note: See TracChangeset for help on using the changeset viewer.