Changeset 1973


Ignore:
Timestamp:
May 21, 2012, 4:57:23 PM (5 years ago)
Author:
boender
Message:
  • removed superfluous match
  • displaced 'cases daemon'
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r1965 r1973  
    434434   let 〈label,instr〉 ≝ x in
    435435   let isize ≝ instruction_size_jmplen short_jump instr in
    436    〈pc + isize,
    437    match instr with
    438    [ Instruction i ⇒ match i with
    439      [ JC jmp ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
    440      | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
    441      | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
    442      | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
    443      | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
    444      | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
    445      | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
    446      | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
    447      | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
    448      | _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
    449      ]
    450    | Call c ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
    451    | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
    452    | _      ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma
    453    ]〉
     436   〈pc + isize, bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma〉
    454437  ) 〈0, Stub ? ?〉 in
    455438  if geb (\fst final_policy) 2^16 then
     
    464447    #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2
    465448    cases (le_to_or_lt_eq … Hi) -Hi #Hi
    466     cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi cases pi
    467       [1,7: #id cases id normalize nodelta
    468         [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:
    469           [1,2,3,6,7,24,25: #x #y
    470           |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] >lookup_opt_insert_miss
    471           [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    472             @bitvector_of_nat_abs
    473             [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
    474               @Hi2
    475             |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
    476               @(transitive_lt … Hi2) @le_S_to_le @Hi
    477             |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
    478               @sym_neq @lt_to_not_eq @le_S_to_le @Hi
    479             ]
    480           ]
    481           @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    482         |38,39,40,41,42,43,44,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74:
    483           [1,2,3,6,7,24,25: #x #y
    484           |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    485           >lookup_opt_insert_miss
    486           [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    487             @bitvector_of_nat_abs
    488             [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
    489                @Hi2
    490             |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
    491               @(transitive_lt … Hi2) <Hi @le_n
    492             |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
    493               @sym_neq @lt_to_not_eq <Hi @le_n
    494             ]
    495           ]
    496           <Hi @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
    497           >Hi @Hi2
    498         |9,10,11,12,13,14,15,16,17:
    499           [1,2,6,7: #x |3,4,5,8,9: #x #id] >lookup_opt_insert_miss
    500           [2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
    501             [1,4,7,10,13,16,19,22,25: @Hi2
    502             |2,5,8,11,14,17,20,23,26: @(transitive_lt … Hi2) @le_S_to_le @Hi
    503             |3,6,9,12,15,18,21,24,27: @sym_neq @lt_to_not_eq @le_S_to_le @Hi
    504             ]
    505           |1,3,5,7,9,11,13,15,17:
    506             @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    507           ]
    508         |46,47,48,49,50,51,52,53,54:
    509           [1,2,6,7: #x |3,4,5,8,9: #x #id] >lookup_opt_insert_miss
    510           [2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
    511             [1,4,7,10,13,16,19,22,25: @Hi2
    512             |2,5,8,11,14,17,20,23,26: @(transitive_lt … Hi2) <Hi @le_n
    513             |3,6,9,12,15,18,21,24,27: @sym_neq @lt_to_not_eq <Hi @le_n
    514             ]
    515           |1,3,5,7,9,11,13,15,17:
    516             @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) <Hi @le_S @le_n
    517           ]
    518         ]
    519       |2,3,6,8,9,12: [3,6: #w] #z >lookup_opt_insert_miss
    520         [2,4,6,8,10,12: @bitvector_of_nat_abs
    521           [1,4,7,10,13,16: @Hi2
    522           |2,8,11: @(transitive_lt … Hi2) @le_S_to_le @Hi
    523           |5,14,17: @(transitive_lt … Hi2) <Hi @le_n
    524           |3,9,12: @sym_neq @lt_to_not_eq @le_S_to_le @Hi
    525           |6,15,18: <Hi @sym_neq @lt_to_not_eq @le_n
    526           ]
    527         ]
    528         [1,3,4: @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    529         |2,5,6:
    530           <Hi @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
    531           >Hi @Hi2
    532         ]
    533       |4,5,10,11: #dst normalize nodelta >lookup_opt_insert_miss
    534         [2,4,6,8: @bitvector_of_nat_abs
    535           [1,4,7,10: @Hi2
    536           |2,5: @(transitive_lt … Hi2) @le_S_to_le @Hi
    537           |8,11: @(transitive_lt … Hi2) <Hi @le_n
    538           |3,6: @sym_neq @lt_to_not_eq @le_S_to_le @Hi
    539           |9,12: @sym_neq @lt_to_not_eq <Hi @le_n
    540           ]         
    541         |1,3: @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    542         |5,7: @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) <Hi @le_S @le_n
     449    cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi
     450    [ >lookup_opt_insert_miss
     451      [ @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     452      | @bitvector_of_nat_abs
     453        [ @Hi2
     454        | @(transitive_lt … Hi2) @le_S_to_le @Hi
     455        | @sym_neq @lt_to_not_eq @le_S_to_le @Hi
    543456        ]
    544457      ]
    545 | (* jump_not_in_policy *) #i >append_length <commutative_plus
    546   #Hi normalize in Hi; cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    547   [ cases p -p #p cases p -p #pc #sigma #Hp cases x #l #ins cases ins
    548     [ #pi cases pi normalize nodelta
    549       [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:
    550         [1,2,3,6,7,24,25: #x #y
    551         |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] >lookup_insert_miss
    552         [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
    553           >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)
    554         |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    555           @bitvector_of_nat_abs
    556           [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
    557             @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
    558             @le_plus_a @Hi
    559           |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
    560             @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
    561             @le_plus_n_r
    562           |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
    563             @lt_to_not_eq @Hi
    564           ]
    565         ]
    566       |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] >lookup_insert_miss
    567         [1,3,5,7,9,11,13,15,17:
    568           >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)
    569         |2,4,6,8,10,12,14,16,18:
    570           @bitvector_of_nat_abs
    571           [1,4,7,10,13,16,19,22,25:
    572             @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
    573             @le_plus_a @Hi
    574           |2,5,8,11,14,17,20,23,26:
    575             @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
    576             @le_plus_n_r
    577           |3,6,9,12,15,18,21,24,27:
    578             @lt_to_not_eq @Hi
    579           ]
     458    | >lookup_opt_insert_miss
     459      [ <Hi @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
     460        >Hi @Hi2
     461      | @bitvector_of_nat_abs
     462        [ @Hi2
     463        | @(transitive_lt … Hi2) <Hi @le_n
     464        | @sym_neq @lt_to_not_eq <Hi @le_n
    580465        ]
    581466      ]
    582     |2,3,4,5,6: #x [5: #y] >lookup_insert_miss
    583       [1,3,5,7,9:
    584         >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)
    585       |2,4,6,8,10:
    586         @bitvector_of_nat_abs
    587         [1,4,7,10,13:
    588           @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
     467    ]
     468  | (* jump_not_in_policy *) #i >append_length <commutative_plus
     469    #Hi normalize in Hi; cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     470    [ cases p -p #p cases p -p #pc #sigma #Hp cases x #l #ins >lookup_insert_miss
     471      [ >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)
     472      | @bitvector_of_nat_abs
     473        [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
    589474          @le_plus_a @Hi
    590         |2,5,8,11,14:
    591           @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
     475        | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
    592476          @le_plus_n_r
    593         |3,6,9,12,15:
    594           @lt_to_not_eq @Hi
     477        | @lt_to_not_eq @Hi
    595478        ]
    596479      ]
    597     ]
    598   | >Hi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
    599     cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #ins cases ins
    600     normalize nodelta
    601     [2,3,6: #x [3: #y] >lookup_insert_hit #_ / by /
    602     |4,5: #x #H @⊥ cases H #H2 @H2 / by I/
    603     |1: #pi cases pi
    604       [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:
    605         [1,2,3,6,7,24,25: #x #y
    606         |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    607         #_ >lookup_insert_hit / by /
    608       |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    609         #H @⊥ cases H #H2 @H2 / by I/
    610       ]
    611     ]
    612   ]
    613 ]
    614 | (* policy_compact *) cases daemon (*XXX*)
    615 ]
    616 | (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi;
    617  cases p -p #p cases p -p #pc #sigma #Hp cases x
    618   #lbl #instr cases instr normalize nodelta
    619   [ #pi cases pi normalize nodelta
    620     [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:
    621       [1,2,3,6,7,24,25: #x #y
    622       |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    623       cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    624       [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
    625         >lookup_insert_miss
    626         [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
    627           @((proj2 ?? Hp) i Hi)
    628         |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    629           @bitvector_of_nat_abs
    630           [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
    631             @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
    632             @le_plus_a @Hi
    633           |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
    634             @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
    635             @le_plus_n_r
    636           |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
    637             @lt_to_not_eq @Hi
    638           ]
    639         ]
    640       |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    641         >Hi >lookup_insert_hit @refl
    642       ]
    643     |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    644       cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    645       [1,3,5,7,9,11,13,15,17: >lookup_insert_miss
    646         [1,3,5,7,9,11,13,15,17: @((proj2 ?? Hp) i Hi)
    647         |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
    648           [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
    649             >append_length >commutative_plus @le_plus_a @Hi
    650           |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
    651             >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    652           |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi
    653           ]
    654         ]
    655       |2,4,6,8,10,12,14,16,18: >Hi >lookup_insert_hit @refl
    656       ]
    657     ]
    658   |2,3,4,5,6: #x [5: #y] cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    659     [1,3,5,7,9: >lookup_insert_miss
    660       [1,3,5,7,9: @((proj2 ?? Hp) i Hi)
    661       |2,4,6,8,10: @bitvector_of_nat_abs
    662         [1,4,7,10,13: @(transitive_lt … (pi2 ?? program)) >prf >append_length
    663           >commutative_plus @le_plus_a @Hi
    664         |2,5,8,11,14: @(transitive_lt … (pi2 ?? program)) >prf >append_length
    665           <plus_n_Sm @le_S_S @le_plus_n_r
    666         |3,6,9,12,15: @lt_to_not_eq @Hi
     480    | >Hi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
     481      cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #ins
     482      >lookup_insert_hit #_ / by /
     483    ]
     484  ]
     485  | (* policy_compact *) cases daemon
     486  ]       
     487  | (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi;
     488    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
     489    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     490    [ >lookup_insert_miss
     491      [ @((proj2 ?? Hp) i Hi)
     492      | @bitvector_of_nat_abs
     493        [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
     494          @le_plus_a @Hi
     495        | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
     496          @le_plus_n_r
     497        | @lt_to_not_eq @Hi
    667498        ]
    668499      ]
    669     |2,4,6,8,10: >Hi >lookup_insert_hit @refl
    670     ]
    671   ]
    672 ]
     500    | >Hi >lookup_insert_hit @refl
     501    ]
     502  ]
    673503| @conj [ @conj [ @conj
    674504  [ #i #_ #Hi2 / by refl/
    675   | #i #H @⊥ @(absurd … H) @not_le_Sn_O
    676   ]
    677   | #i #H @⊥ @(absurd … H) @not_le_Sn_O
    678   ]
    679   | #i #H @⊥ @(absurd … H) @not_le_Sn_O
    680   ]
     505  ]]]
     506  #i #H @⊥ @(absurd … H) @not_le_Sn_O
    681507]
    682508qed.
     
    690516    \snd pc1 = \snd pc2).
    691517   
    692 (*definition nec_plus_ultra ≝
    693   λprogram:list labelled_instruction.λp:ppc_pc_mapjump_expansion_policy.
    694   ¬(∀i.i < |program| → \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,0,short_jump〉) = long_jump). *)
     518definition nec_plus_ultra ≝
     519  λprogram:list labelled_instruction.λp:ppc_pc_map.
     520  ¬(∀i.i < |program| → is_jump (\snd (nth i ? program 〈None ?, Comment []〉)) →
     521  \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉) = long_jump).
    695522 
    696523(*include alias "common/Identifiers.ma".*)
     
    809636    ]
    810637  ]
    811 qed. 
     638qed.
    812639
    813640lemma etblorp: ∀a,b,i.is_jump i →
     
    885712    let 〈no_ch,y〉 ≝ x in
    886713    match y with
    887     [ None ⇒ (* nec_plus_ultra program old_policy *) True
     714    [ None ⇒ nec_plus_ultra program old_policy
    888715    | Some p ⇒ And (And (And (And (And (out_of_program_none program p)
    889716       (jump_not_in_policy program p))
     
    940767    else
    941768      〈eqb final_added 0, Some ? final_policy〉.
    942 [ / by I/
     769[ normalize nodelta cases daemon (* XXX nec_plus_ultra *)
    943770| normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2
    944771  >H2 in H; normalize nodelta -H2 -x #H @conj
     
    17021529        | #Hfull cases (jump_expansion_step program (create_label_map program) «Fp,?») in ⊢ (???% → %);
    17031530          #x cases x -x #Gch #Gpol cases Gpol normalize nodelta
    1704           [ cases daemon (* XXX will need some form of nec_plus_ultra here
    1705             #H #EQ2 @⊥ @(absurd ?? H) @Hfull *)
     1531          [ #H #EQ2 @⊥ @(absurd ?? H) @Hfull
    17061532          | #Gp #HGp #EQ2 cases Fch
    17071533            [ normalize nodelta #i #Hi
Note: See TracChangeset for help on using the changeset viewer.