Changeset 2237 for src/ASM


Ignore:
Timestamp:
Jul 23, 2012, 11:11:27 PM (7 years ago)
Author:
sacerdot
Message:

Even shorter version.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2236 r2237  
    115115
    116116lemma jump_expansion_step3:
    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
    122      .occurs_exactly_once ASMTag pseudo_instruction l program
    123       →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
    124        =address_of_word_labels_code_mem program l).*).
    125  ∀old_sigma :
    126    Σpolicy:ppc_pc_map
    127    .not_jump_default program policy
    128     (*∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
    129                  〈O,short_jump〉)
    130      =O
    131     ∧\fst  policy
    132      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
    133                   (\snd  policy) 〈O,short_jump〉)
    134     ∧sigma_compact_unsafe program labels policy
    135     ∧\fst  policy≤ 2 \sup 16*).
    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.(*
    140  acc :
    141   (Σx0:ℕ×ppc_pc_map
    142    .(let 〈added,policy〉 ≝x0 in 
    143      not_jump_default prefix policy
    144      ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
    145                   〈O,short_jump〉)
    146       =O
    147      ∧\fst  policy
    148       =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    149                    (\snd  policy) 〈O,short_jump〉)
    150      ∧jump_increase prefix old_sigma policy
    151      ∧sigma_compact_unsafe prefix labels policy
    152      ∧(sigma_jump_equal prefix old_sigma policy→added=O)
    153      ∧(added=O→sigma_pc_equal prefix old_sigma policy)
    154      ∧out_of_program_none prefix policy
    155      ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    156                   (\snd  policy) 〈O,short_jump〉)
    157       =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    158                    (\snd  old_sigma) 〈O,short_jump〉)
    159        +added
    160      ∧sigma_safe prefix labels added old_sigma policy))*)
     117 ∀program.
     118 ∀labels : label_map.
     119 ∀old_sigma : Σpolicy:ppc_pc_map.not_jump_default program policy.
     120 ∀prefix,x,tl. program=prefix@[x]@tl →
    161121 ∀inc_added : ℕ.
    162  ∀inc_pc_sigma : ppc_pc_map. (*
    163  p : (acc≃〈inc_added,inc_pc_sigma〉)*)
     122 ∀inc_pc_sigma : ppc_pc_map.
    164123 ∀label : option Identifier.
    165124 ∀instr : pseudo_instruction.
    166  ∀p1 : x≃〈label,instr〉.(*
    167  add_instr ≝
    168   match instr
    169    in pseudo_instruction
    170    return λ_:pseudo_instruction.(option jump_length)
    171    with 
    172   [Instruction (i:(preinstruction Identifier))⇒
    173    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    174    (|prefix|) i
    175   |Comment (_:String)⇒None jump_length
    176   |Cost (_:costlabel)⇒None jump_length
    177   |Jmp (j:Identifier)⇒
    178    Some jump_length
    179    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    180   |Call (c:Identifier)⇒
    181    Some jump_length
    182    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    183   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]*)
     125 ∀p1 : x≃〈label,instr〉.
    184126 ∀inc_pc : ℕ.
    185  ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).(*
    186  Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)*)
     127 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
    187128 ∀old_pc : ℕ.
    188129 ∀old_length : jump_length.
    189130 ∀Holdeq :
    190131  lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
    191    〈O,short_jump〉
    192    =〈old_pc,old_length〉.
    193  ∀Hpolicy :
    194   (*not_jump_default prefix 〈inc_pc,inc_sigma〉
    195    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
    196                 〈O,short_jump〉)
    197     =O
    198    ∧inc_pc
    199     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
    200                  〈O,short_jump〉)
    201    ∧*)jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉(*
    202    ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
    203    ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
    204    ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
    205    ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
    206    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
    207                 〈O,short_jump〉)
    208     =old_pc+inc_added
    209    ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*).
    210 (* added : ℕ*)
     132   〈O,short_jump〉 =〈old_pc,old_length〉.
     133 ∀Hpolicy : jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉.
    211134 ∀policy : ppc_pc_map.
    212135 ∀new_length : jump_length.
     
    239162   =〈new_length,isize〉.
    240163 ∀prefix_ok1 : S (|prefix|)< 2 \sup 16.
    241  ∀prefix_ok : |prefix|< 2 \sup 16.(*
    242  Heq2a :
    243   (match 
    244    match instr
    245     in pseudo_instruction
    246     return λ_0:pseudo_instruction.(option jump_length)
    247     with 
    248    [Instruction (i:(preinstruction Identifier))⇒
    249     jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    250     (|prefix|) i
    251    |Comment (_0:String)⇒None jump_length
    252    |Cost (_0:costlabel)⇒None jump_length
    253    |Jmp (j:Identifier)⇒
    254     Some jump_length
    255     (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    256    |Call (c:Identifier)⇒
    257     Some jump_length
    258     (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    259    |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
    260     in option
    261     return λ_0:(option jump_length).ℕ
    262     with 
    263    [None⇒inc_added
    264    |Some (x0:jump_length)⇒
    265     inc_added+(isize-instruction_size_jmplen old_length instr)]
    266    =added)*)
     164 ∀prefix_ok : |prefix|< 2 \sup 16.
    267165 ∀Heq2b :
    268166  〈inc_pc+isize,
     
    303201        [ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r ] #lt_prefix_program
    304202        >lookup_insert_miss
    305         [ >lookup_insert_hit inversion (is_jump instr) normalize nodelta
    306           [ cases instr in Heq1; normalize nodelta
    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)
    315             |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
    316             ]
    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
    331                 ]
    332               |2,5,8,11: @lt_prefix_program
    333               |*: >Holdeq #EQ2 >EQ2 %2 @refl]]
     203        [ >lookup_insert_hit normalize nodelta
     204          inversion instr in Heq1; normalize nodelta
     205          [4,5: #x #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
     206          | #pi #Heqi whd in match jump_expansion_step_instruction; normalize nodelta
     207            lapply (destination_of_None_to_is_jump_false pi)
     208            lapply (destination_of_Some_to_is_jump_true pi)
     209            cases (destination_of ?) normalize nodelta
     210            [ #tgt #Hx
     211            | #tgt #_ #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
     212            ]
     213          |2,3,6: #x [3: #y] #Heqi ]
     214          #Hj <(proj1 ?? (pair_destruct ?????? Hj))
     215          lapply (pi2 ?? old_sigma (|prefix|) ??) try assumption
     216          [1,3,5,7: >prf >nth_append_second try @le_n
     217            <minus_n_n whd in match (nth ????); >p1 >Heqi
     218            whd in match is_jump; normalize nodelta try % >Hx %
     219          |*: >Holdeq #EQ2 >EQ2 %2 %]
    334220        | @bitvector_of_nat_abs
    335221          [ @le_S_to_le ]
     
    511397    <Heq2b >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
    512398  | (* jump_increase *)
     399    @(jump_expansion_step3 …)
    513400    cases daemon (*XXX*)
    514401  | (* sigma_compact_unsafe *) cases daemon (*
Note: See TracChangeset for help on using the changeset viewer.