Changeset 2236


Ignore:
Timestamp:
Jul 23, 2012, 10:46:06 PM (7 years ago)
Author:
sacerdot
Message:

One subproof made shorter.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2225 r2236  
    103103qed.
    104104
    105 (*
     105lemma destination_of_None_to_is_jump_false:
     106 ∀instr. destination_of instr = None … → is_jump' instr = false.
     107 * normalize // try (#H1 #H2 #abs) try (#H1 #abs) destruct(abs)
     108qed.
     109
     110lemma destination_of_Some_to_is_jump_true:
     111 ∀instr,dst. destination_of instr = Some … dst → is_jump' instr = true.
     112 #instr #dst cases instr normalize // try (#H1 #H2 #abs) try (#H1 #abs) try #abs
     113 destruct(abs)
     114qed.
     115
    106116lemma jump_expansion_step3:
    107 (*
    108  program :
    109   (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)
    110  labels :
    111   (Σlm:label_map
    112    .(∀l:identifier ASMTag
     117∀program.(* :
     118  (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)*)
     119 ∀labels :
     120  label_map(*Σlm:label_map
     121   .∀l:identifier ASMTag
    113122     .occurs_exactly_once ASMTag pseudo_instruction l program
    114123      →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
    115        =address_of_word_labels_code_mem program l))*)
     124       =address_of_word_labels_code_mem program l).*).
    116125 ∀old_sigma :
    117126   Σpolicy:ppc_pc_map
    118    .True(*not_jump_default program policy
    119     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
     127   .not_jump_default program policy
     128    (*∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
    120129                 〈O,short_jump〉)
    121130     =O
     
    125134    ∧sigma_compact_unsafe program labels policy
    126135    ∧\fst  policy≤ 2 \sup 16*).
    127  ∀prefix : list (option Identifier×pseudo_instruction). (*
    128  x : (option Identifier×pseudo_instruction)
    129  tl : (list (option Identifier×pseudo_instruction))
    130  prf : (program=prefix@[x]@tl)
     136 ∀prefix : list (option Identifier×pseudo_instruction).
     137 ∀x : option Identifier×pseudo_instruction.
     138 ∀tl : list (option Identifier×pseudo_instruction).
     139 ∀prf : program=prefix@[x]@tl.(*
    131140 acc :
    132141  (Σx0:ℕ×ppc_pc_map
     
    149158                   (\snd  old_sigma) 〈O,short_jump〉)
    150159       +added
    151      ∧sigma_safe prefix labels added old_sigma policy))
    152  inc_added : ℕ
    153  inc_pc_sigma : ppc_pc_map
     160     ∧sigma_safe prefix labels added old_sigma policy))*)
     161 ∀inc_added : ℕ.
     162 ∀inc_pc_sigma : ppc_pc_map. (*
    154163 p : (acc≃〈inc_added,inc_pc_sigma〉)*)
    155164 ∀label : option Identifier.
    156  ∀instr : pseudo_instruction.(*
    157  p1 : (x≃〈label,instr〉)
     165 ∀instr : pseudo_instruction.
     166 ∀p1 : x≃〈label,instr〉.(*
    158167 add_instr ≝
    159168  match instr
     
    172181   Some jump_length
    173182   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    174   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
    175  inc_pc : ℕ
    176  inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
    177  Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
    178  old_pc : ℕ
    179  old_length : jump_length
    180  Holdeq :
    181   (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
     183  |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]*)
     184 ∀inc_pc : ℕ.
     185 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).(*
     186 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)*)
     187 ∀old_pc : ℕ.
     188 ∀old_length : jump_length.
     189 Holdeq :
     190  lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
    182191   〈O,short_jump〉
    183    =〈old_pc,old_length〉)
    184  Hpolicy :
    185   (not_jump_default prefix 〈inc_pc,inc_sigma〉
     192   =〈old_pc,old_length〉.
     193 Hpolicy :
     194  (*not_jump_default prefix 〈inc_pc,inc_sigma〉
    186195   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
    187196                〈O,short_jump〉)
     
    190199    =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
    191200                 〈O,short_jump〉)
    192    ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
     201   ∧*)jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉(*
    193202   ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
    194203   ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
     
    198207                〈O,short_jump〉)
    199208    =old_pc+inc_added
    200    ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)
    201  added : ℕ*)
     209   ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*).
     210(* added : ℕ*)
    202211 ∀policy : ppc_pc_map.
    203  (*new_length : jump_length
    204  isize : ℕ
    205  Heq1 :
    206   (match 
     212 ∀new_length : jump_length.
     213 ∀isize : ℕ.
     214 Heq1 :
     215   match 
    207216   match instr
    208217    in pseudo_instruction
     
    220229    Some jump_length
    221230    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    222    |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
     231   |Mov (_:[[dptr]]) (_:Identifier)⇒None jump_length]
    223232    in option
    224     return λ_0:(option jump_length).(jump_length×ℕ)
     233    return λ_:(option jump_length).(jump_length×ℕ)
    225234    with 
    226235   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
     
    228237    〈max_length old_length pl,
    229238    instruction_size_jmplen (max_length old_length pl) instr〉]
    230    =〈new_length,isize〉)
    231  prefix_ok1 : (S (|prefix|)< 2 \sup 16 )
    232  prefix_ok : (|prefix|< 2 \sup 16 )
     239   =〈new_length,isize〉.
     240 ∀prefix_ok1 : S (|prefix|)< 2 \sup 16.
     241 ∀prefix_ok : |prefix|< 2 \sup 16.(*
    233242 Heq2a :
    234243  (match 
     
    255264   |Some (x0:jump_length)⇒
    256265    inc_added+(isize-instruction_size_jmplen old_length instr)]
    257    =added)
    258  Heq2b :
    259   (〈inc_pc+isize,
     266   =added)*)
     267 Heq2b :
     268  〈inc_pc+isize,
    260269   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
    261270   〈inc_pc+isize,
     
    264273   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    265274    〈inc_pc,new_length〉 inc_sigma)〉
    266    =policy)*)
     275   =policy.
    267276 jump_increase (prefix@[〈label,instr〉]) old_sigma policy.
    268  #old_sigma #prefix #label #instr #policy
     277 #program #labels #old_sigma #prefix #x #tl #prf #inc_added #inc_pc_sigma #label
     278 #instr #p1 #inc_pc #inc_sigma #old_pc #old_length #Holdeq #Hpolicy #policy #new_length
     279 #isize #Heq1 #prefix_ok1 #prefix_ok #Heq2
    269280    #i >append_length >commutative_plus #Hi normalize in Hi;
    270281    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    271282    [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    272283      [ (* USE[pass]: jump_increase *)
    273         lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i (le_S_to_le … Hi))
    274         <(proj2 ?? (pair_destruct ?????? Heq2))
     284        lapply (Hpolicy i (le_S_to_le … Hi))
     285        <Heq2
    275286        @pair_elim #opc #oj #EQ1 >lookup_insert_miss
    276287        [ >lookup_insert_miss
     
    278289          | @bitvector_of_nat_abs
    279290            [ @(transitive_lt ??? Hi) ]
    280             [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
    281               @le_S_S @le_plus_n_r
     291            [1,2: assumption
    282292            | @lt_to_not_eq @Hi
    283293            ]
     
    285295        | @bitvector_of_nat_abs
    286296          [ @(transitive_lt ??? Hi) @le_S_to_le ]
    287           [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
    288             >append_length @le_S_S <plus_n_Sm @le_plus_n_r
     297          [1,2: assumption
    289298          | @lt_to_not_eq @le_S @Hi
    290299          ]
    291300        ]
    292       | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >Holdeq normalize nodelta
     301      | >Hi <Heq2 >Holdeq normalize nodelta
     302        cut (|prefix| < |program|)
     303        [ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r ] #lt_prefix_program
    293304        >lookup_insert_miss
    294         [ >lookup_insert_hit cases (dec_is_jump instr)
     305        [ >lookup_insert_hit inversion (is_jump instr) normalize nodelta
    295306          [ cases instr in Heq1; normalize nodelta
    296             [ #pi cases pi
    297               [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:
    298                 [1,2,3,6,7,24,25: #x #y
    299                 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj
    300               |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    301                 whd in match jump_expansion_step_instruction; normalize nodelta #Heq1
    302                 #_ <(proj1 ?? (pair_destruct ?????? Heq1))
    303                 @jmpleq_max_length
    304               ]
    305             |2,3,6: #x [3: #y] #_ #Hj cases Hj
     307            [ #pi whd in match jump_expansion_step_instruction; normalize nodelta
     308              lapply (destination_of_None_to_is_jump_false pi)
     309              cases (destination_of ?) normalize nodelta
     310              [ #abs #_ whd in match is_jump; normalize nodelta >abs try % #abs'
     311                destruct(abs')
     312              | #tgt #_ #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
     313              ]
     314            |2,3,6: #x [3: #y] #_ #Hj normalize in Hj; destruct(Hj)
    306315            |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
    307316            ]
    308           | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta
    309             [ #pi cases pi
    310               [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:
    311                 [1,2,3,6,7,24,25: #x #y
    312                 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    313                 whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1
    314                 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
    315                 (* USE: not_jump_default (from old_sigma) *)
    316                 lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
    317                 [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:
    318                   >prf >nth_append_second
    319                   [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:
    320                     <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
    321                   |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:
    322                     @le_n
    323                   ]
    324                 |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:
    325                   >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    326                 |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:
    327                   >Holdeq #EQ2 >EQ2 %2 @refl
     317          | lapply Heq1 -Heq1; inversion instr normalize nodelta
     318            [ 4,5: #x #_ #_ #abs @⊥ normalize in abs; destruct(abs)
     319            | #pi #Heqi whd in match jump_expansion_step_instruction; normalize nodelta
     320              lapply (destination_of_Some_to_is_jump_true pi)
     321              cases (destination_of pi) normalize nodelta
     322              [2: #tgt #abs #_ whd in match is_jump; normalize nodelta >abs try %
     323                  #abs' destruct(abs')]
     324              #_
     325            |*: #x [3: #y] #Heqi ]
     326            #Hj #Hx <(proj1 ?? (pair_destruct ?????? Hj))
     327              lapply (pi2 ?? old_sigma (|prefix|) ??)
     328              [1,4,7,10: >prf >nth_append_second
     329                [1,3,5,7: <minus_n_n whd in match (nth ????); >p1 >Heqi >Hj try % >Hx %
     330                |*: @le_n
    328331                ]
    329               |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    330                 #_ #_ #abs @⊥ @(absurd ? I abs)
    331               ]
    332             |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
    333               (* USE: not_jump_default (from old_sigma) *)
    334               lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
    335               [1,4,7: >prf >nth_append_second
    336                 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
    337                 |2,4,6: @le_n
    338                 ]
    339               |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    340               |3,6,9: >Holdeq #EQ2 >EQ2 %2 @refl
    341               ]
    342             |4,5: #x #_ #_ #abs @⊥ @(absurd ? I abs)
    343             ]
    344           ]
     332              |2,5,8,11: @lt_prefix_program
     333              |*: >Holdeq #EQ2 >EQ2 %2 @refl]]
    345334        | @bitvector_of_nat_abs
    346335          [ @le_S_to_le ]
    347           [1,2: @(transitive_lt … (proj1 ?? (pi2 … program))) @le_S_S >prf
    348             >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     336          [1,2: assumption
    349337          | @lt_to_not_eq @le_n
    350338          ]
    351339        ]
    352340      ]
    353     | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
     341    | <Heq2 >Hi >lookup_insert_hit
    354342      normalize nodelta
    355343      cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉)
    356344      #a #b normalize nodelta %2 @refl
    357345    ]
    358   ]
    359 qed.*)
     346qed.
    360347
    361348(* One step in the search for a jump expansion fixpoint. *)
Note: See TracChangeset for help on using the changeset viewer.