Changeset 1950 for src/ASM/Policy.ma


Ignore:
Timestamp:
May 15, 2012, 6:20:31 PM (8 years ago)
Author:
boender
Message:
  • advances in policy
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r1942 r1950  
    3939 
    4040definition is_jump ≝
    41   λx:labelled_instruction.
    42   let 〈label,instr〉 ≝ x in
     41  λinstr:pseudo_instruction.
    4342  match instr with
    4443  [ Instruction i   ⇒ is_jump' i
     
    6766  ].
    6867 
    69 (*definition jump_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝
     68definition jump_not_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝
    7069  λprefix.λsigma.
    7170  ∀i:ℕ.i < |prefix| →
    72   iff (is_jump (nth i ? prefix 〈None ?, Comment []〉))
    73    (∃x:jump_length.
    74    \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,None ?〉) = Some ? x).*)
     71  ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment []〉)) →
     72  \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉) = short_jump.
    7573
    7674(* if the instruction 〈p,a〉 is a jump to label l, then label l is at address a *)
     
    122120   let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,short_jump〉 in
    123121   let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉 in
    124      opc ≤ pc ∧ jmpleq oj j.
     122     (*opc ≤ pc ∧*) jmpleq oj j.
    125123
    126124(* Policy safety *)
     
    307305    (bitvector_of_nat 16 (\fst sigma)) (\snd x)))
    308306  0.
    309 
     307 
    310308(* The function that creates the label-to-address map *)
    311309definition create_label_map: ∀program:list labelled_instruction.
    312310  (Σlabels:label_map.
    313     ∀i:ℕ.lt i (|program|) →
    314311    ∀l.occurs_exactly_once ?? l program →
    315     is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
    316     lookup ?? labels l = Some ? i
     312    bitvector_of_nat ? (lookup_def ?? labels l 0) =
     313     address_of_word_labels_code_mem program l
    317314  ) ≝
    318315 λprogram.
    319316   \fst (create_label_cost_map program).
    320  #i #Hi #l #Hl1 #Hl2 lapply (pi2 ?? (create_label_cost_map program)) @pair_elim
    321  #labels #costs #EQ normalize nodelta #H @(H i Hi l Hl1 Hl2)
     317 #l #Hl lapply (pi2 ?? (create_label_cost_map program)) @pair_elim
     318 #labels #costs #EQ normalize nodelta #H @(H l Hl)
    322319qed.
    323320
     
    388385
    389386lemma dec_is_jump: ∀x.Sum (is_jump x) (¬is_jump x).
    390 #x cases x #l #i cases i
     387#i cases i
    391388[#id cases id
    392389 [1,2,3,6,7,33,34:
     
    408405qed.
    409406
    410 (*lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
    411  ∀policy:(Σp:ppc_pc_map.
    412  out_of_program_none prefix p ∧ jump_in_policy prefix p).
    413   ∀i:ℕ.i < |prefix| →
    414   iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉))
    415   (\snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd policy) 〈0,None ?〉) = None ?).
    416  #prefix #policy #i #Hi @conj
    417 [ #Hnotjmp lapply (refl ? (bvt_lookup … (bitvector_of_nat 16 i) (\snd policy) 〈0,None ?〉))
    418   cases (bvt_lookup … (bitvector_of_nat 16 i) (\snd policy) 〈0,None ?〉) in ⊢ (???% → ?);
    419   #pc #j cases j
    420   [ #H >H @refl
    421   | #x #H >H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
    422     >H @(ex_intro ?? x ?) / by /
    423   ]
    424 | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj)
    425   #H elim H -H; #x #H >H in Hnone; #abs destruct (abs)
    426 
    427 qed.*)
    428 
    429407(* The first step of the jump expansion: everything to short.
    430408 * The third condition of the dependent type implies jump_in_policy;
     
    438416    | Some p ⇒
    439417       And (And (out_of_program_none (pi1 ?? program) p)
    440        (policy_isize_sum (pi1 ?? program) labels p))
     418       (jump_not_in_policy (pi1 ?? program) p))
    441419       (\fst p < 2^16)
    442420    ] ≝
     
    445423  (λprefix.Σpolicy:ppc_pc_map.
    446424    And (out_of_program_none prefix policy)
    447     (policy_isize_sum prefix labels policy))
     425    (jump_not_in_policy prefix policy))
    448426  program
    449427  (λprefix.λx.λtl.λprf.λp.
     
    560538        ]
    561539      ]
    562 | cases daemon
     540| (* jump_not_in_policy *) #i >append_length <commutative_plus
     541  #Hi normalize in Hi; cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     542  [ cases p -p #p cases p -p #pc #sigma #Hp cases x #l #ins cases ins
     543    [ #pi cases pi normalize nodelta
     544      [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:
     545        [1,2,3,6,7,24,25: #x #y
     546        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] >lookup_insert_miss
     547        [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:
     548          >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? Hp) i Hi)
     549        |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:
     550          @bitvector_of_nat_abs
     551          [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:
     552            @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
     553            @le_plus_a @Hi
     554          |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:
     555            @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
     556            @le_plus_n_r
     557          |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:
     558            @lt_to_not_eq @Hi
     559          ]
     560        ]
     561      |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] >lookup_insert_miss
     562        [1,3,5,7,9,11,13,15,17:
     563          >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? Hp) i Hi)
     564        |2,4,6,8,10,12,14,16,18:
     565          @bitvector_of_nat_abs
     566          [1,4,7,10,13,16,19,22,25:
     567            @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
     568            @le_plus_a @Hi
     569          |2,5,8,11,14,17,20,23,26:
     570            @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
     571            @le_plus_n_r
     572          |3,6,9,12,15,18,21,24,27:
     573            @lt_to_not_eq @Hi
     574          ]
     575        ]
     576      ]
     577    |2,3,4,5,6: #x [5: #y] >lookup_insert_miss
     578      [1,3,5,7,9:
     579        >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? Hp) i Hi)
     580      |2,4,6,8,10:
     581        @bitvector_of_nat_abs
     582        [1,4,7,10,13:
     583          @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
     584          @le_plus_a @Hi
     585        |2,5,8,11,14:
     586          @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
     587          @le_plus_n_r
     588        |3,6,9,12,15:
     589          @lt_to_not_eq @Hi
     590        ]
     591      ]
     592    ]
     593  | >Hi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
     594    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #ins cases ins
     595    normalize nodelta
     596    [2,3,6: #x [3: #y] >lookup_insert_hit #_ / by /
     597    |4,5: #x #H @⊥ cases H #H2 @H2 / by I/
     598    |1: #pi cases pi
     599      [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:
     600        [1,2,3,6,7,24,25: #x #y
     601        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     602        #_ >lookup_insert_hit / by /
     603      |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
     604        #H @⊥ cases H #H2 @H2 / by I/
     605      ]
     606    ]
     607  ]
    563608]
    564609| @conj
    565610  [ #i #_ #Hi2 / by refl/
    566   | whd in match policy_isize_sum; normalize nodelta
    567     cases daemon
     611  | #i #H @⊥ @(absurd … H) @not_le_Sn_O
    568612  ]
    569613]
     
    576620    let pc1 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 in
    577621    let pc2 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉 in
    578     pc1 = pc2).
     622    \snd pc1 = \snd pc2).
    579623   
    580624(*definition nec_plus_ultra ≝
     
    588632include alias "basics/logic.ma".
    589633
     634lemma blerpque: ∀a,b,i.
     635  is_jump i → instruction_size_jmplen (max_length a b) i = instruction_size_jmplen a i →
     636  (max_length a b) = a.
     637 #a #b #i cases i
     638 [1: #pi cases pi
     639   [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:
     640     [1,2,3,6,7,24,25: #x #y
     641     |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     642     #H cases H
     643   |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
     644     #_ cases a cases b
     645     [1,5,7,8,9: #_ / by refl/
     646     |10,14,16,17,18: #_ / by refl/
     647     |19,23,25,26,27: #_ / by refl/
     648     |28,32,34,35,36: #_ / by refl/
     649     |37,41,43,44,45: #_ / by refl/
     650     |46,50,52,53,54: #_ / by refl/
     651     |55,59,61,62,63: #_ / by refl/
     652     |64,68,70,71,72: #_ / by refl/
     653     |73,77,79,80,81: #_ / by refl/
     654     |2,3,4,6: cases x #a cases a
     655       [1,2,3,4,8,9,16,17,18,19: #b #Hb cases Hb
     656       |20,21,22,23,27,28,35,36,37,38: #b #Hb cases Hb
     657       |39,40,41,42,46,47,54,55,56,57: #b #Hb cases Hb
     658       |58,59,60,61,65,66,73,74,75,76: #b #Hb cases Hb
     659       |5,6,7,10,11,12,13,14: #Hb cases Hb
     660       |24,25,26,29,30,31,32,33: #Hb cases Hb
     661       |43,44,45,48,49,50,51,52: #Hb cases Hb
     662       |62,63,64,67,68,69,70,71: #Hb cases Hb
     663       |15,34,53,72: #b #Hb #H normalize in H; destruct (H)
     664       ]
     665     |11,12,13,15: cases x #a cases a
     666       [1,2,3,4,8,9,16,17,18,19: #b #Hb cases Hb
     667       |20,21,22,23,27,28,35,36,37,38: #b #Hb cases Hb
     668       |39,40,41,42,46,47,54,55,56,57: #b #Hb cases Hb
     669       |58,59,60,61,65,66,73,74,75,76: #b #Hb cases Hb
     670       |5,6,7,10,11,12,13,14: #Hb cases Hb
     671       |24,25,26,29,30,31,32,33: #Hb cases Hb
     672       |43,44,45,48,49,50,51,52: #Hb cases Hb
     673       |62,63,64,67,68,69,70,71: #Hb cases Hb
     674       |15,34,53,72: #b #Hb #H normalize in H; destruct (H)
     675       ]
     676     |20,21,22,24: cases x #a cases a
     677       [1,2,3,4,8,9,16,17,18,19: #b #Hb cases Hb
     678       |20,21,22,23,27,28,35,36,37,38: #b #Hb cases Hb
     679       |39,40,41,42,46,47,54,55,56,57: #b #Hb cases Hb
     680       |58,59,60,61,65,66,73,74,75,76: #b #Hb cases Hb
     681       |5,6,7,10,11,12,13,14: #Hb cases Hb
     682       |24,25,26,29,30,31,32,33: #Hb cases Hb
     683       |43,44,45,48,49,50,51,52: #Hb cases Hb
     684       |62,63,64,67,68,69,70,71: #Hb cases Hb
     685       |15,34,53,72: #b #Hb #H normalize in H; destruct (H)
     686       ]
     687     |29,30,31,33: cases x #a cases a #a1 #a2
     688       [1,3,5,7: cases a2 #b cases b
     689         [2,3,4,9,15,16,17,18,19: #b #Hb cases Hb
     690         |21,22,23,28,34,35,36,37,38: #b #Hb cases Hb
     691         |40,41,42,47,53,54,55,56,57: #b #Hb cases Hb
     692         |59,60,61,66,72,73,74,75,76: #b #Hb cases Hb
     693         |5,6,7,10,11,12,13,14: #Hb cases Hb
     694         |24,25,26,29,30,31,32,33: #Hb cases Hb
     695         |43,44,45,48,49,50,51,52: #Hb cases Hb
     696         |62,63,64,67,68,69,70,71: #Hb cases Hb
     697         |1,8: #b #Hb #H normalize in H; destruct (H)
     698         |20,27: #b #Hb #H normalize in H; destruct (H)
     699         |39,46: #b #Hb #H normalize in H; destruct (H)
     700         |58,65: #b #Hb #H normalize in H; destruct (H)
     701         ]
     702       |2,4,6,8: cases a1 #b cases b
     703         [1,3,8,9,15,16,17,18,19: #b #Hb cases Hb
     704         |20,22,27,28,34,35,36,37,38: #b #Hb cases Hb
     705         |39,41,46,47,53,54,55,56,57: #b #Hb cases Hb
     706         |58,60,65,66,72,73,74,75,76: #b #Hb cases Hb
     707         |5,6,7,10,11,12,13,14: #Hb cases Hb
     708         |24,25,26,29,30,31,32,33: #Hb cases Hb
     709         |43,44,45,48,49,50,51,52: #Hb cases Hb
     710         |62,63,64,67,68,69,70,71: #Hb cases Hb
     711         |2,4: #b #Hb #H normalize in H; destruct (H)
     712         |21,23: #b #Hb #H normalize in H; destruct (H)
     713         |40,42: #b #Hb #H normalize in H; destruct (H)
     714         |59,61: #b #Hb #H normalize in H; destruct (H)
     715         ]
     716       ]
     717     |38,39,40,42: cases x #a cases a
     718       [2,3,8,9,15,16,17,18,19: #b #Hb cases Hb
     719       |21,22,27,28,34,35,36,37,38: #b #Hb cases Hb
     720       |40,41,46,47,53,54,55,56,57: #b #Hb cases Hb
     721       |59,60,65,66,72,73,74,75,76: #b #Hb cases Hb
     722       |5,6,7,10,11,12,13,14: #Hb cases Hb
     723       |24,25,26,29,30,31,32,33: #Hb cases Hb
     724       |43,44,45,48,49,50,51,52: #Hb cases Hb
     725       |62,63,64,67,68,69,70,71: #Hb cases Hb
     726       |1,4: #b #Hb #H normalize in H; destruct (H)
     727       |20,23: #b #Hb #H normalize in H; destruct (H)
     728       |39,42: #b #Hb #H normalize in H; destruct (H)
     729       |58,61: #b #Hb #H normalize in H; destruct (H)
     730       ]
     731     |47,48,49,51: cases x #a #H normalize in H; destruct (H)
     732     |56,57,58,60: cases x #a #H normalize in H; destruct (H)
     733     |65,66,67,69: cases x #a #H normalize in H; destruct (H)
     734     |74,75,76,78: cases x #a #H normalize in H; destruct (H)
     735     ]
     736   ]
     737  |2,3,6: #x [3: #y] #H cases H
     738  |4,5: #id #_ cases a cases b
     739    [2,3,4,6,11,12,13,15: normalize #H destruct (H)
     740    |1,5,7,8,9,10,14,16,17,18: #H / by refl/
     741    ]
     742  ]
     743qed.
     744
     745lemma etblorp: ∀a,b,i.is_jump i →
     746  instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i.
     747 #a #b #i cases i
     748 [2,3,6: #x [3: #y] #H cases H
     749 |4,5: #id #_ cases a cases b / by le_n/
     750 |1: #pi cases pi
     751   [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:
     752     [1,2,3,6,7,24,25: #x #y
     753     |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     754     #H cases H
     755   |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
     756     #_ cases a cases b
     757     [2,3: cases x #ad cases ad
     758       [15,34: #b #Hb / by le_n/
     759       |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb
     760     |1,4,5,6,7,8,9: / by le_n/
     761     |11,12: cases x #ad cases ad
     762       [15,34: #b #Hb / by le_n/
     763       |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb
     764     |10,13,14,15,16,17,18: / by le_n/
     765     |20,21: cases x #ad cases ad
     766       [15,34: #b #Hb / by le_n/
     767       |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb
     768     |19,22,23,24,25,26,27: / by le_n/
     769     |29,30: cases x #ad cases ad #a1 #a2
     770       [ cases a2 #ad2 cases ad2
     771       ]
     772     ]
     773   ]
     774 ]
     775 cases daemon (* XXX see if it works first *)
     776qed.
     777
     778lemma minus_zero_to_le: ∀n,m:ℕ.n - m = 0 → n ≤ m.
     779 #n
     780 elim n
     781 [ #m #_ @le_O_n
     782 | #n' #Hind #m cases m
     783   [ #H -n whd in match (minus ??) in H; >H @le_n
     784   | #m' -m #H whd in match (minus ??) in H; @le_S_S @Hind @H
     785   ]
     786 ]
     787qed.
     788
     789lemma plus_zero_zero: ∀n,m:ℕ.n + m = 0 → m = 0.
     790 #n #m #Hn @sym_eq @le_n_O_to_eq <Hn >commutative_plus @le_plus_n_r
     791qed.
     792
    590793(* One step in the search for a jump expansion fixpoint. *)
    591794definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
     
    596799  ∀old_policy:(Σpolicy:ppc_pc_map.
    597800    And (And (out_of_program_none program policy)
    598     (policy_isize_sum program labels policy))
     801    (jump_not_in_policy program policy))
    599802    (\fst policy < 2^16)).
    600803  (Σx:bool × (option ppc_pc_map).
     
    602805    match y with
    603806    [ None ⇒ (* nec_plus_ultra program old_policy *) True
    604     | Some p ⇒ And (And (And (And (And (out_of_program_none (pi1 ?? program) p)
    605        (policy_isize_sum program labels p))
     807    | Some p ⇒ And (And (And (And (And (out_of_program_none program p)
     808       (jump_not_in_policy program p))
    606809       (policy_increase program old_policy p))
    607810       (policy_compact program labels p))
     
    616819      let 〈added,policy〉 ≝ x in
    617820      And (And (And (And (out_of_program_none prefix policy)
    618       (policy_isize_sum prefix labels policy))
     821      (jump_not_in_policy prefix policy))
    619822      (policy_increase prefix old_sigma policy))
    620823      (policy_compact prefix labels policy))
     
    666869  ]
    667870| lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma
    668   cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
    669   #old_pc #old_length #Hpolicy @pair_elim #added #policy normalize nodelta
     871  lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉))
     872  cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) in ⊢ (???% → %);
     873  #old_pc #old_length #Holdeq #Hpolicy @pair_elim #added #policy normalize nodelta
    670874  @pair_elim #new_length #isize normalize nodelta #Heq1 #Heq2
    671875  @conj [ @conj [ @conj [ @conj
     
    681885      ]
    682886    ]
    683   | cases daemon (* XXX *)
     887  | (* jump_not_in_policy *) #i >append_length <commutative_plus #Hi normalize in Hi;
     888    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     889    [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
     890      [ >(nth_append_first ? i prefix ?? Hi)
     891        @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi)
     892      | @bitvector_of_nat_abs
     893        [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
     894          @le_plus_a @Hi
     895        | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
     896          @le_plus_n_r
     897        | @lt_to_not_eq @Hi
     898        ]
     899      ]
     900    | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_hit
     901      >nth_append_second
     902      [ <minus_n_n whd in match (nth ????); cases instr in Heq1;
     903        [4,5: #x #_ #H cases H #H2 @⊥ @H2 / by I/
     904        |2,3,6: #x [3: #y] #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ / by /
     905        |1: #pi cases pi
     906          [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:
     907            [1,2,3,6,7,24,25: #x #y
     908            |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #Heq1
     909              <(proj1 ?? (pair_destruct ?????? Heq1)) #_ / by /
     910          |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
     911            #_ #H @⊥ cases H #H2 @H2 / by I/
     912          ]
     913        ]
     914      | @le_n
     915      ]
     916    ]
    684917  ]
    685918  | (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi;
    686     cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    687     [ lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi))
     919    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi; #Hi
     920    [ lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i Hi)
    688921      <(proj2 ?? (pair_destruct ?????? Heq2))     
    689922      @pair_elim #opc #oj #EQ1 >lookup_insert_miss
     
    691924      | @bitvector_of_nat_abs
    692925        [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus @le_plus_a
    693           @(le_S_S_to_le … Hi)
     926          @Hi
    694927        | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    695         | @lt_to_not_eq @(le_S_S_to_le … Hi)
     928        | @lt_to_not_eq @Hi
    696929        ]
    697930      ]
    698     | <(proj2 ?? (pair_destruct ?????? Heq2)) >(injective_S … Hi) >lookup_insert_hit
    699       cases instr in Heq1 Heq2;
    700       [2,3,6: #x [3: #y] normalize nodelta #Heq1 #Heq2 <(proj1 ?? (pair_destruct ?????? Heq1))
    701       cases daemon
    702       |1,4,5: cases daemon
    703       ]
    704     ]
    705   ]
    706   | (* policy_compact *) cases daemon
    707   ]
    708   | (* added = 0 → policy_equal *) cases daemon
    709   ]
     931    | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_hit
     932      cases (dec_is_jump instr)
     933      [ cases instr in Heq1; normalize nodelta
     934        [ #pi cases pi
     935          [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:
     936            [1,2,3,6,7,24,25: #x #y
     937            |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj
     938          |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
     939            whd in match jump_expansion_step_instruction; normalize nodelta #Heq1
     940            <(proj1 ?? (pair_destruct ?????? Heq1)) #_ >Holdeq normalize nodelta
     941            @jmpleq_max_length
     942          ]
     943        |2,3,6: #x [3: #y] #_ #Hj cases Hj
     944        |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq normalize nodelta
     945          @jmpleq_max_length
     946        ]
     947      | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta
     948        [ #pi cases pi
     949          [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:
     950            [1,2,3,6,7,24,25: #x #y
     951            |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     952            whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1
     953            #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
     954            lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??)
     955            [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:
     956              >prf >nth_append_second
     957              [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:
     958                <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
     959              |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:
     960                @le_n
     961              ]
     962            |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:
     963              >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     964            |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:
     965              cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
     966              #a #b #H >H normalize nodelta %2 @refl
     967            ]
     968          |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
     969            #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
     970          ]
     971        |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
     972          lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??)
     973          [1,4,7: >prf >nth_append_second
     974            [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
     975            |2,4,6: @le_n
     976            ]
     977          |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     978          |3,6,9: cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
     979            #a #b #H >H normalize nodelta %2 @refl
     980          ]
     981        |4,5: #x #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
     982        ]
     983      ]
     984    ]
     985  ]
     986  | (* policy_compact *) (*XXX*) cases daemon
     987  ]
     988  | (* added = 0 → policy_equal *) lapply (proj2 ?? Hpolicy)
     989    lapply Heq2 -Heq2 lapply Heq1 -Heq1 lapply (refl ? instr)
     990    cases instr in ⊢ (???% → % → % → %); normalize nodelta
     991    [ #pi cases pi normalize nodelta
     992      [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:
     993        [1,2,3,6,7,24,25: #x #y
     994        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     995        #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) #Hadded
     996        #i >append_length >commutative_plus #Hi normalize in Hi;
     997        cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     998        [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:
     999          <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
     1000          [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:
     1001            @(Hold Hadded i Hi)
     1002          |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:
     1003            @bitvector_of_nat_abs
     1004            [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:
     1005              @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
     1006              @le_plus_a @Hi
     1007            |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:
     1008              @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
     1009              @le_plus_n_r
     1010            |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:
     1011              @lt_to_not_eq @Hi
     1012            ]
     1013          ]
     1014        |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:
     1015           <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
     1016           lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??)
     1017           [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:
     1018             >prf >nth_append_second
     1019             [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:
     1020               <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H
     1021             |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:
     1022               @le_n
     1023             ]
     1024           |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:
     1025             >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     1026           |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:
     1027             cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
     1028             #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl
     1029           ]
     1030         ]
     1031       |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Heq2 #Hold
     1032         <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1))
     1033         #H #i >append_length >commutative_plus #Hi normalize in Hi;
     1034         cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     1035         [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq2))
     1036           >lookup_insert_miss
     1037           [1,3,5,7,9,11,13,15,17: @(Hold ? i Hi)
     1038             [1,2,3,4,5,6,7,8,9: @sym_eq @le_n_O_to_eq <H @le_plus_n_r]
     1039           ]
     1040           @bitvector_of_nat_abs
     1041           [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
     1042             >append_length >commutative_plus @le_plus_a @Hi
     1043           |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
     1044             >append_length <plus_n_Sm @le_S_S
     1045           |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi
     1046           ] @le_plus_n_r
     1047         |2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi
     1048           >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
     1049           >Holdeq normalize nodelta @sym_eq @blerpque
     1050           [3,6,9,12,15,18,21,24,27:
     1051             elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H)))
     1052             [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp
     1053             |2,4,6,8,10,12,14,16,18: #H @H
     1054             ]
     1055             / by I/
     1056           |2,5,8,11,14,17,20,23,26: / by I/
     1057           ]
     1058         ]
     1059       ]
     1060     |2,3,6: #x [3: #y] #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2))
     1061       #Hadded #i >append_length >commutative_plus #Hi normalize in Hi;
     1062       cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     1063       [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
     1064         [1,3,5: @(Hold Hadded i Hi)
     1065         |2,4,6: @bitvector_of_nat_abs
     1066           [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
     1067             @le_plus_a @Hi
     1068           |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
     1069             @le_plus_n_r
     1070           |3,6,9: @lt_to_not_eq @Hi
     1071           ]
     1072         ]
     1073       |2,4,6: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
     1074         lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??)
     1075         [1,4,7: >prf >nth_append_second
     1076           [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H
     1077           |2,4,6: @le_n
     1078           ]
     1079         |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     1080         |3,6,9: cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
     1081           #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl
     1082         ]
     1083       ]
     1084     |4,5: #x #Hins #Heq1 #Heq2 #Hold
     1085       <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1))
     1086       #H #i >append_length >commutative_plus #Hi normalize in Hi;
     1087       cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     1088       [1,3: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
     1089         [1,3: @(Hold ? i Hi)
     1090           [1,2: @sym_eq @le_n_O_to_eq <H @le_plus_n_r]
     1091         ]
     1092         @bitvector_of_nat_abs
     1093         [1,4: @(transitive_lt … (pi2 ?? program)) >prf
     1094           >append_length >commutative_plus @le_plus_a @Hi
     1095         |2,5: @(transitive_lt … (pi2 ?? program)) >prf
     1096           >append_length <plus_n_Sm @le_S_S
     1097         |3,6: @lt_to_not_eq @Hi
     1098         ] @le_plus_n_r
     1099         |2,4: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
     1100           <(proj1 ?? (pair_destruct ?????? Heq1))>Holdeq normalize nodelta
     1101           @sym_eq @blerpque
     1102           [3,6: elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H)))
     1103             [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp
     1104             |2,4: #H @H
     1105             ]
     1106             / by I/
     1107           |2,5: / by I/
     1108           ]
     1109         ]
     1110       ]
     1111     ]
    7101112| normalize nodelta @conj [ @conj [ @conj [ @conj
    7111113  [ #i #Hi / by refl/
     
    7161118]
    7171119qed.
     1120
    7181121     
    7191122(* old proof | lapply (pi2 ?? acc) >p #Hpolicy normalize nodelta in Hpolicy;
     
    16652068qed.
    16662069
    1667 include alias "arithmetics/nat.ma".
     2070nclude alias "arithmetics/nat.ma".
    16682071include alias "basics/logic.ma".
    16692072
     
    16722075(* The glue between Policy and Assembly. *)
    16732076definition jump_expansion':
    1674  ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
    1675   option (Σsigma:Word → Word × bool.
     2077∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
     2078 option (Σsigma:Word → Word × bool.
    16762079   ∀ppc: Word.
    16772080   let pc ≝ \fst (sigma ppc) in
     
    16872090      ∨
    16882091       (nat_of_bitvector … ppc = |\snd program| → next_pc = (zero …)))).
     2092≝ λprogram.
     2093  let policy ≝ pi1 … (je_fixpoint (\snd program)) in
     2094  match policy with
     2095  [ None ⇒ None ?
     2096  | Some x ⇒ Some ?
     2097      «λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
     2098        〈bitvector_of_nat 16 pc,jmpeqb jl long_jump〉,?»
     2099  ].
    16892100 cases daemon
    16902101qed.
Note: See TracChangeset for help on using the changeset viewer.