Changeset 1810


Ignore:
Timestamp:
Mar 7, 2012, 7:16:55 PM (7 years ago)
Author:
boender
Message:
  • new version of policy that compiles up to the final glue
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r1809 r1810  
    506506    j1 = j2.
    507507   
     508definition nec_plus_ultra ≝
     509  λprogram:list labelled_instruction.λp:jump_expansion_policy.
     510  ¬(∀i.i < |program| → \snd (bvt_lookup … (bitvector_of_nat 16 i) p 〈0,0,short_jump〉) = long_jump).
     511 
    508512(* One step in the search for a jump expansion fixpoint. *)
    509513definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
     
    517521    let 〈changed,pc,y〉 ≝ x in
    518522    match y with
    519     [ None ⇒ pc > 2^16
     523    [ None ⇒ pc > 2^16 ∧ nec_plus_ultra program old_policy
    520524    | Some p ⇒ out_of_program_none program p ∧ labels_okay labels p ∧
    521525        jump_in_policy program p ∧
     
    562566    else
    563567      〈final_changed,final_pc,Some jump_expansion_policy final_policy〉.
    564 [ normalize nodelta @leb_true_to_le @p2
     568[ normalize nodelta @conj
     569  [ @leb_true_to_le @p2
     570  | @nmk #Hfull (* XXX *) cases daemon
     571  ]
    565572| normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2
    566573  >H2 in H; >p1 normalize nodelta //
     
    955962
    956963(* This function executes n steps from the starting point. *)
    957 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (|l|) 2^16)
    958   (n: ℕ) on n:(Σx:ℕ × (option jump_expansion_policy).
    959     let 〈pc,y〉 ≝ x in
     964(*let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (|l|) 2^16)
     965  (n: ℕ) on n:(Σx:bool × ℕ × (option jump_expansion_policy).
     966    let 〈ch,pc,y〉 ≝ x in
    960967    match y with
    961968    [ None ⇒ pc > 2^16
     
    965972  [ O   ⇒ 〈0,Some ? (pi1 … (jump_expansion_start program))〉
    966973  | S m ⇒ let 〈ch,pc,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
    967           match z return λx. z=x → Σa:ℕ × (option jump_expansion_policy).? with
     974          match z return λx. z=x → Σa:bool × ℕ × (option jump_expansion_policy).? with
    968975          [ None    ⇒ λp2.〈pc,None ?〉
    969976          | Some op ⇒ λp2.pi1 … (jump_expansion_step program (create_label_map program op) «op,?»)
    970977          ] (refl … z)
     978  ].*)
     979
     980let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (|l|) 2^16) (n: ℕ)
     981  on n:(Σx:bool × ℕ × (option jump_expansion_policy).
     982    let 〈c,pc,y〉 ≝ x in
     983    match y with
     984    [ None ⇒ pc > 2^16
     985    | Some p ⇒ And (out_of_program_none program p) (jump_in_policy program p)
     986    ]) ≝
     987  match n with
     988  [ O   ⇒ 〈true,0,Some ? (pi1 ?? (jump_expansion_start program))〉
     989  | S m ⇒ let 〈ch,pc,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
     990          match z return λx. z=x → Σa:bool × ℕ × (option jump_expansion_policy).? with
     991          [ None    ⇒ λp2.〈false,pc,None ?〉
     992          | Some op ⇒ λp2.if ch
     993            then pi1 ?? (jump_expansion_step program (create_label_map program op) «op,?»)
     994            else (jump_expansion_internal program m)
     995          ] (refl … z)
    971996  ].
    972997[ normalize nodelta @(proj1 ?? (pi2 ?? (jump_expansion_start program)))
    973 | normalize nodelta lapply (pi2 ?? (jump_expansion_internal program m))
    974     <p1 >p2 / by /
    975 |4: cases (jump_expansion_step program (create_label_map program op) «op,?»)
    976     #p cases p #q #r cases r normalize nodelta
    977     [ / by /
    978     | #j #H @conj
    979       [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
    980       | @(proj2 ?? (proj1 ?? (proj1 ?? H)))
    981       ]
    982     ]
    983 | lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 / by /
     998| lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /
     999|3: lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /
     1000| normalize nodelta cases (jump_expansion_step program (create_label_map program op) «op,?»)
     1001  #p cases p -p #p cases p -p #p #q #r cases r normalize nodelta
     1002  [ #H @(proj1 ?? H)
     1003  | #j #H @conj
     1004    [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
     1005    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     1006    ]
     1007  ]
    9841008]
    9851009qed.
    986  
     1010
    9871011lemma pe_int_refl: ∀program.reflexive ? (policy_equal_int program).
    9881012#program whd #x whd #n #Hn
     
    10601084 #x1 cases x1 #p1 #j1 -x1; #H1 #Heqj #Hj #k elim k
    10611085[ <plus_n_O >Heqj @Hj
    1062 | #k' -k <plus_n_Sm lapply (refl ? (jump_expansion_internal program (n+k')))
     1086| #k' -k <plus_n_Sm whd in match (jump_expansion_internal program (S (n+k')));
     1087  lapply (refl ? (jump_expansion_internal program (n+k')))
    10631088  cases (jump_expansion_internal program (n+k')) in ⊢ (???% → % → %);
    1064   #x2 cases x2 #p2 #j2 -x2; normalize nodelta #H #Heqj2
     1089  #x2 cases x2 -x2 #x2 cases x2 -x2 #c2 #p2 #j2 normalize nodelta #H #Heqj2
    10651090  cases j2 in H Heqj2;
    10661091  [ #H #Heqj2 #_ whd in match (jump_expansion_internal ??);
     
    11541179| #h #t #Hind #Hp #acc
    11551180  lapply (refl ? (jump_expansion_step program (create_label_map program policy) policy))
    1156   cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 #p #q -pi1; cases q
     1181  cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 -pi1 #pi1 cases pi1
     1182  #p #q #r -pi1; cases r
    11571183  [ //
    1158   | #x #Hx #Hjeq normalize nodelta lapply (proj2 ?? (proj1 ?? Hx) (|t|) Hp)
     1184  | #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? Hx)) (|t|) Hp)
    11591185    whd in match (measure_int ???); whd in match (measure_int ? x ?);
    11601186    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)
     
    11691195        |3: @(transitive_le ? (measure_int t x (acc+1)))
    11701196        ]
    1171         [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus //]
     1197        [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/]
    11721198        >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
    11731199        ]
    11741200    | #Heq >Heq cases y3 normalize nodelta
    1175       [2,3: >measure_plus >measure_plus @le_plus //]
     1201      [2,3: >measure_plus >measure_plus @le_plus / by le_n/]
    11761202      >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
    11771203    ]
     
    12341260#program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy)))
    12351261cases (jump_expansion_step program (create_label_map program policy) policy) in ⊢ (???% → %);
    1236 #p cases p #pc #pol normalize nodelta cases pol
     1262#p cases p -p #p cases p -p #ch #pc #pol normalize nodelta cases pol
    12371263[ //
    12381264| #p normalize nodelta #Hpol #eqpol lapply (le_n (|program|))
     
    12451271     [ @(transitive_le … Hp) //
    12461272     | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
    1247        lapply (proj2 ?? (proj1 ?? Hpol) (|t|) Hp)
     1273       lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpol)) (|t|) Hp)
    12481274       cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
    12491275       #x cases x -x #x1 #x2 #x3
     
    12541280       |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
    12551281         lapply (measure_incr_or_equal program policy t ? 0)
    1256          [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol //
     1282         [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
    12571283       |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
    12581284       |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
     
    12621288          #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
    12631289          lapply (measure_incr_or_equal program policy t ? 0)
    1264           [ @(transitive_le … Hp) @le_n_Sn ] >eqpol //
     1290          [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
    12651291       |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
    12661292         #H #_ @(injective_plus_r … H)
     
    12701296   | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
    12711297     whd in match (measure_int ? p ?) in Hm;
    1272      lapply (proj2 ?? (proj1 ?? Hpol) (|t|) Hp)
     1298     lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpol)) (|t|) Hp)
    12731299     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in   
    12741300Hm;
     
    13331359    policy_equal program (\snd (pi1 ?? (jump_expansion_internal program k))) p.
    13341360#program @(\snd (pi1 ?? (jump_expansion_internal program (2*|program|))))
    1335 (*@(ex_intro … (2*|program|)) #k #Hk*)
    13361361cases (dec_bounded_exists (λk.policy_equal (pi1 ?? program)
    13371362   (\snd (pi1 ?? (jump_expansion_internal program k)))
    13381363   (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*|program|))
    1339 [ #Hex elim Hex -Hex #x #Hx @(ex_intro … x) #k @pe_trans
     1364[ #Hex elim Hex -Hex #x #Hx @(ex_intro … x) #k #Hk
     1365  @pe_trans
    13401366  [ @(\snd (pi1 ?? (jump_expansion_internal program x)))
    13411367  | @pe_sym @equal_remains_equal
    13421368    [ @(proj2 ?? Hx)
    1343     | @(transitive_le ? (2*|program|))
    1344       [ @le_S_S_to_le @le_S @(proj1 ?? Hx)
    1345       | @le_S_S_to_le @le_S @Hk
    1346       ]
     1369    | @le_S_S_to_le @le_S @Hk
    13471370    ]
    13481371  | @equal_remains_equal
     
    13511374    ]   
    13521375  ]
    1353 | #Hnex lapply (not_exists_forall … Hnex) -Hnex; #Hfa @pe_sym @equal_remains_equal
     1376| #Hnex lapply (not_exists_forall … Hnex) -Hnex; #Hfa @(ex_intro … (2*|program|)) #k #Hk
     1377  @pe_sym @equal_remains_equal
    13541378  [ lapply (refl ? (jump_expansion_internal program (2*|program|)))
    13551379    cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %);
    1356     #jep cases jep #pc #x -jep cases x normalize nodelta
    1357     [ #Hjep #Heqx >Heqx lapply (step_none program (2*|pi1 ?? program|) ? 1)
    1358       [ >Heqx // | <plus_n_Sm <plus_n_O #H >H // ]
    1359     | #pol_2prog #H2prog #Heq2prog lapply (measure_full (pi1 ?? program) pol_2prog) #Hfull
    1360       whd in match (policy_equal ???); lapply Heq2prog -Heq2prog;
    1361       lapply (refl ? (jump_expansion_internal program (2*|program|)))
    1362       cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → % → %);
    1363       #z cases z #fpc #pol -z cases pol normalize nodelta
    1364       [ #Heq2prog #Hjep #Hploq destruct (Hploq)
    1365       | #p #Heq2prog #Hjep #Hploq whd in match (jump_expansion_internal ??);
    1366         >Hjep normalize nodelta
    1367         lapply (refl ? (jump_expansion_step program (create_label_map program p) «p,?»))
    1368         [2: cases (jump_expansion_step program (create_label_map program p) «p,?») in ⊢ (???% → %);
    1369         #x cases x #Spc #Spol -x cases Spol normalize nodelta
    1370         [ #Hy #Hgnarf cases daemon (* XXX *)
    1371         | #y #Hy #Hgnarf #i #Hi lapply (proj2 ?? (proj1 ?? Hy) i Hi)
    1372           lapply (Hfull ? i Hi)
    1373           [2: lapply (sym_eq ??? (proj1 ?? Hpy)) #Hblp >(Some_eq ??? Hblp)
    1374                 >(Some_eq ??? (pair_eq2 ?????? (pi1_eq ???? Hploq)))
    1375                 cases (bvt_lookup ?? (bitvector_of_nat 16 i) pol_2prog 〈0,0,short_jump〉)
    1376                 #blp cases blp #a #b #c -blp #EQ >EQ normalize nodelta
    1377                 cases (bvt_lookup ?? (bitvector_of_nat 16 i) y 〈0,0,short_jump〉)
    1378                 #blp cases blp #d #e #f -blp normalize nodelta cases f
    1379                 [1,2: #H elim H #H2 [1,3: @⊥ @H2 |2,4: destruct (H2) ]
    1380                 | #_ //
    1381                 ]
    1382             | @le_to_le_to_eq
    1383               [ @measure_le
    1384               | cut (∀x.x ≤ (2*|pi1 ?? program|) →
    1385                   ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧
    1386                       x ≤ measure_int program p 0))
    1387                 [ #n elim n
    1388                   [ #_ whd in match (jump_expansion_internal program 0);
    1389                     @(ex_intro … (jump_expansion_start program)) % [ @refl |
    1390                     >measure_zero @le_n ]
    1391                   | -n #n' #Hind #Hn' elim (le_to_or_lt_eq … Hn')
    1392                     [ #H2n' elim (Hind ?)
    1393                       [ -Hgnarf #pn' lapply (refl ? (jump_expansion_internal program (S n')))
    1394                         cases (jump_expansion_internal program (S n')) in ⊢ (???% → %);
    1395                         #x cases x -x #npc #npol cases npol normalize nodelta
    1396                         [ #Hbla #Hnone #Hsome lapply (step_none program (S n'))
    1397                           >Hnone normalize nodelta #Ht elim (le_to_eq_plus ?? Hn')
    1398                           #k #Hk lapply (Ht ? k) [ // | <Hk >Hjep #H destruct (H) ]
    1399                         | #Spol #Hbla #HSpol #H3 @(ex_intro ?? Spol) @conj [ @refl |
    1400                           lapply (measure_incr_or_equal program pn' program)
    1401                           lapply (pi2 ?? (jump_expansion_internal program n'))
    1402                           >(proj1 ?? H3)
    1403                           lapply (refl ? (jump_expansion_internal program n'))
    1404                           lapply H3 -H3
    1405                           cases (jump_expansion_internal program n') in ⊢ (% → ???% → %);
    1406                           #x cases x -x #npc #npol normalize nodelta #Hbli #H3 #EQ
    1407                           >(proj1 ?? H3) in Hbli EQ; #Hbli #EQ
    1408                           whd in match (jump_expansion_internal program (S n')) in HSpol;
    1409                           >EQ in HSpol; normalize nodelta
    1410                         ] ]                       
    1411                        
    1412                        
    1413                        
    1414                       |
    1415                       ]
    1416                      |
    1417                      ]
    1418                    ]
    1419                    
    1420                 | #gloeirks elim (gloeirks (2*|program|) (le_n ?)) #q
    1421                   >Hjep >(Some_eq ??? (pair_eq2 ?????? (pi1_eq ???? Hploq)))
    1422                   #H >(Some_eq ??? (proj1 ?? H)) @(proj2 ?? H)
    1423                 ]
     1380    #x cases x -x #x cases x #Fch #Fpc #Fpol normalize nodelta #HFpol cases Fpol in HFpol;
     1381    [ (* if we're at None in 2*|program|, we're at None in S 2*|program| too *)
     1382      #HFpol #EQ whd in match (jump_expansion_internal ??); >EQ
     1383      normalize nodelta //
     1384    | #Fp #HFp #EQ whd in match (jump_expansion_internal ??);
     1385      >EQ normalize nodelta
     1386      lapply (refl ? (jump_expansion_step program (create_label_map program Fp) «Fp,?»))
     1387      [ @HFp
     1388      | lapply (measure_full program Fp ?)
     1389        [ @le_to_le_to_eq
     1390          [ @measure_le
     1391          | (* XXX *) cases daemon
     1392          ]
     1393        | #Hfull cases (jump_expansion_step program (create_label_map program Fp) «Fp,?») in ⊢ (???% → %);
     1394          #x cases x -x #x cases x -x #Gch #Gpc #Gpol cases Gpol normalize nodelta
     1395          [ #H #EQ2 @⊥ @(absurd ?? (proj2 ?? H)) @Hfull
     1396          | #Gp #HGp #EQ2 cases Fch
     1397            [ normalize nodelta #i #Hi
     1398              lapply (refl ? (lookup ?? (bitvector_of_nat 16 i) Fp 〈0,0,short_jump〉))
     1399              cases (lookup ?? (bitvector_of_nat 16 i) Fp 〈0,0,short_jump〉) in ⊢ (???% → %);
     1400              #x cases x -x #p #a #j normalize nodelta #H
     1401              lapply (proj2 ?? (proj1 ?? (proj1 ?? HGp)) i Hi) lapply (Hfull i Hi) >H
     1402              #H2 >H2 normalize nodelta cases (lookup ?? (bitvector_of_nat 16 i) Gp 〈0,0,short_jump\rangle)
     1403              #x cases x -x #p #a #j' cases j' normalize nodelta #H elim H -H #H
     1404              [1,3: @⊥ @H
     1405              |2,4: destruct (H)
     1406              |5,6: @refl
    14241407              ]
     1408            | normalize nodelta /2 by pe_int_refl/
    14251409            ]
    14261410          ]
    1427         ]]
    1428       ]
    1429     ]
    1430   | @le_S_to_le @Hk
    1431   ]
    1432 | (* TO BE CHANGED *)
    1433   #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
    1434   [ %1 //
    1435   |2,3: #x %2 @nmk whd in match (policy_equal ???); [2: //]
    1436     whd in match (eject_policy_opt ???); #H destruct (H)
    1437   |4: #p1 #p2 whd in match (policy_equal ???); @dec_bounded_forall #m
     1411        ]
     1412      ]
     1413    ]
     1414  | @le_S_S_to_le @le_S @Hk
     1415  ]
     1416| #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
     1417  #x cases x -x #x cases x -x #nch #npc #npol normalize nodelta #Hnpol
     1418  #x cases x -x #x cases x -x #Sch #Scp #Spol normalize nodelta #HSpol
     1419  cases npol in Hnpol; cases Spol in HSpol;
     1420  [ #Hnpol #HSpol %1 //
     1421  |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal ???); //
     1422    #H destruct (H)
     1423  |4: #np #Hnp #Sp #HSp whd in match (policy_equal ???); @dec_bounded_forall #m
    14381424      cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉)
    14391425      #x cases x -x #x1 #x2 #x3
     
    14431429  ]
    14441430]
     1431qed.
    14451432
    14461433(* Take a policy of 〈pc, addr, jump_length〉 tuples, and transform it into
     
    14621449definition jump_expansion':
    14631450 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
    1464  policy_type
    1465  λprogram.λpc.
     1451 ∀lookup_labels.policy_type lookup_labels
     1452 λprogram.λlookup_labels.λpc.
    14661453  let policy ≝
    14671454    transform_policy (|\snd program|) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in
    1468   lookup ? ? pc policy long_jump.
     1455  (* here we must use jump_length_ok *)
     1456  bvt_lookup ? ? pc policy long_jump.
    14691457/2 by Stub, mk_Sig/
    14701458qed.
Note: See TracChangeset for help on using the changeset viewer.