Changeset 2225 for src/ASM/PolicyStep.ma


Ignore:
Timestamp:
Jul 20, 2012, 6:15:40 PM (8 years ago)
Author:
sacerdot
Message:

Minor and major improvements everywhere, shortened proofs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2220 r2225  
    44include alias "basics/logic.ma".
    55
     6lemma not_is_jump_to_destination_of_Nome:
     7 ∀pi. ¬is_jump (Instruction pi) → destination_of pi = None ….
     8 * try (#x #y #H) try (#y #H) try #H cases H %
     9qed.
     10
    611lemma jump_expansion_step1:
    7  ∀program : Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l.
    8  ∀prefix,x,tl. pi1 … program=prefix@[x]@tl →
     12 ∀prefix: list labelled_instruction. S (|prefix|) < 2^16 → |prefix| < 2^16 → (*redundant*)
    913 ∀labels: label_map.
    1014 ∀old_sigma : ppc_pc_map.
     
    3842   = policy.
    3943  not_jump_default (prefix@[〈label,instr〉]) policy.
    40  #program #prefix #x #tl #prf #labels #old_sigma #inc_added #inc_pc_sigma #label #instr #inc_pc
    41  #inc_sigma #old_length #Hpolicy #policy #new_length #isize #Heq1 #Heq2 
     44 #prefix #prefix_ok1 #prefix_ok #labels #old_sigma #inc_added #inc_pc_sigma #label #instr #inc_pc
     45 #inc_sigma #old_length #Hpolicy #policy #new_length #isize #Heq1 #Heq2
    4246 #i >append_length <commutative_plus #Hi normalize in Hi;
    4347 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     
    4650     [ >(nth_append_first ? i prefix ?? Hi)
    4751       @(Hpolicy i Hi)
    48      | @bitvector_of_nat_abs
    49        [ @(transitive_lt ??? Hi) ]
    50        [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
    51          @le_plus_n_r
    52        | @lt_to_not_eq @Hi
    53        ]
     52     | @bitvector_of_nat_abs try assumption
     53       [ @(transitive_lt ??? Hi) assumption ]
     54       @lt_to_not_eq @Hi
    5455     ]
    55    | @bitvector_of_nat_abs
    56      [ @(transitive_lt ??? Hi) @le_S_to_le ]
    57      [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
    58        <plus_n_Sm @le_S_S @le_plus_n_r
    59      | @lt_to_not_eq @le_S @Hi
    60      ]
     56   | @bitvector_of_nat_abs try assumption
     57     [ @(transitive_lt ??? Hi) assumption ]
     58     @lt_to_not_eq @le_S @Hi
    6159   ]
    6260 | <Heq2 >Hi >lookup_insert_miss
    6361   [ >lookup_insert_hit cases instr in Heq1;
    6462     [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
    65      |4,5: #x normalize nodelta #Heq1 #H @⊥ cases H #H @H >nth_append_second
    66        [1,3: <minus_n_n whd in match (nth ????); %
    67        |2,4: @le_n
    68        ]
    69      |1: #pi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); cases pi
    70        [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:
    71          [1,2,3,6,7,24,25: #x #y
    72          |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta #Heq1
    73          <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
    74        |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta
    75          #_ #H @⊥ cases H #H2 @H2 %
    76        ]
    77      ]
    78    | @bitvector_of_nat_abs
    79      [ @le_S_to_le ]
    80      [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S
    81        >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    82      | @lt_to_not_eq @le_n
    83      ]
    84    ]
    85  ]
     63     |4,5: #x normalize nodelta #Heq1 >nth_append_second try %
     64           <minus_n_n #abs cases abs
     65     |1: #pi normalize nodelta >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
     66         #H #non_jump whd in match (jump_expansion_step_instruction ??????) in H;
     67         >not_is_jump_to_destination_of_Nome in H; normalize nodelta // ]         
     68   | @bitvector_of_nat_abs [3: // | @le_S_to_le ] assumption ]]
    8669qed.
     70
     71lemma jump_expansion_step2:
     72 ∀prefix: list labelled_instruction. S (|prefix|) < 2^16 → |prefix| < 2^16 → (*redundant*)
     73 ∀labels : label_map.
     74 ∀old_sigma : ppc_pc_map.
     75 ∀inc_pc : ℕ.
     76 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
     77 ∀Hpolicy1 :
     78  \fst  (lookup … (bitvector_of_nat … O) inc_sigma 〈O,short_jump〉) = O.
     79 ∀Hpolicy2:
     80   inc_pc =\fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉).
     81 ∀policy : ppc_pc_map.
     82 ∀new_length : jump_length.
     83 ∀isize : ℕ.
     84 ∀Heq2 :
     85  〈inc_pc+isize,
     86   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     87   〈inc_pc+isize,
     88   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     89               (\snd  old_sigma) 〈O,short_jump〉)〉
     90   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     91    〈inc_pc,new_length〉 inc_sigma)〉
     92   = policy.
     93 \fst  (lookup … (bitvector_of_nat … O) (\snd  policy) 〈O,short_jump〉) = O.
     94 #prefix #prefix_ok1 #prefix_ok #labels #old_sigma #inc_pc
     95 #inc_sigma #Hpolicy1 #Hpolicy2 #policy #new_length #isize #Heq2
     96 <Heq2 >lookup_insert_miss
     97 [ cases (decidable_eq_nat 0 (|prefix|))
     98   [ #Heq <Heq >lookup_insert_hit >Hpolicy2 <Heq @Hpolicy1
     99   | #Hneq >lookup_insert_miss
     100     [ @Hpolicy1
     101     | @bitvector_of_nat_abs try assumption @lt_O_S ]]
     102 | @bitvector_of_nat_abs [ @lt_O_S | @prefix_ok1 | 3: @lt_to_not_eq @lt_O_S ] ]
     103qed.
     104
     105(*
     106lemma 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
     113     .occurs_exactly_once ASMTag pseudo_instruction l program
     114      →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
     115       =address_of_word_labels_code_mem program l))*)
     116 ∀old_sigma :
     117   Σpolicy:ppc_pc_map
     118   .True(*not_jump_default program policy
     119    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
     120                 〈O,short_jump〉)
     121     =O
     122    ∧\fst  policy
     123     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
     124                  (\snd  policy) 〈O,short_jump〉)
     125    ∧sigma_compact_unsafe program labels policy
     126    ∧\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)
     131 acc :
     132  (Σx0:ℕ×ppc_pc_map
     133   .(let 〈added,policy〉 ≝x0 in 
     134     not_jump_default prefix policy
     135     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
     136                  〈O,short_jump〉)
     137      =O
     138     ∧\fst  policy
     139      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     140                   (\snd  policy) 〈O,short_jump〉)
     141     ∧jump_increase prefix old_sigma policy
     142     ∧sigma_compact_unsafe prefix labels policy
     143     ∧(sigma_jump_equal prefix old_sigma policy→added=O)
     144     ∧(added=O→sigma_pc_equal prefix old_sigma policy)
     145     ∧out_of_program_none prefix policy
     146     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     147                  (\snd  policy) 〈O,short_jump〉)
     148      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     149                   (\snd  old_sigma) 〈O,short_jump〉)
     150       +added
     151     ∧sigma_safe prefix labels added old_sigma policy))
     152 inc_added : ℕ
     153 inc_pc_sigma : ppc_pc_map
     154 p : (acc≃〈inc_added,inc_pc_sigma〉)*)
     155 ∀label : option Identifier.
     156 ∀instr : pseudo_instruction.(*
     157 p1 : (x≃〈label,instr〉)
     158 add_instr ≝
     159  match instr
     160   in pseudo_instruction
     161   return λ_:pseudo_instruction.(option jump_length)
     162   with 
     163  [Instruction (i:(preinstruction Identifier))⇒
     164   jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     165   (|prefix|) i
     166  |Comment (_:String)⇒None jump_length
     167  |Cost (_:costlabel)⇒None jump_length
     168  |Jmp (j:Identifier)⇒
     169   Some jump_length
     170   (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     171  |Call (c:Identifier)⇒
     172   Some jump_length
     173   (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)
     182   〈O,short_jump〉
     183   =〈old_pc,old_length〉)
     184 Hpolicy :
     185  (not_jump_default prefix 〈inc_pc,inc_sigma〉
     186   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
     187                〈O,short_jump〉)
     188    =O
     189   ∧inc_pc
     190    =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
     191                 〈O,short_jump〉)
     192   ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
     193   ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
     194   ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
     195   ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
     196   ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
     197   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
     198                〈O,short_jump〉)
     199    =old_pc+inc_added
     200   ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)
     201 added : ℕ*)
     202 ∀policy : ppc_pc_map.
     203 (*new_length : jump_length
     204 isize : ℕ
     205 Heq1 :
     206  (match 
     207   match instr
     208    in pseudo_instruction
     209    return λ_:pseudo_instruction.(option jump_length)
     210    with 
     211   [Instruction (i:(preinstruction Identifier))⇒
     212    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     213    (|prefix|) i
     214   |Comment (_:String)⇒None jump_length
     215   |Cost (_:costlabel)⇒None jump_length
     216   |Jmp (j:Identifier)⇒
     217    Some jump_length
     218    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     219   |Call (c:Identifier)⇒
     220    Some jump_length
     221    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     222   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
     223    in option
     224    return λ_0:(option jump_length).(jump_length×ℕ)
     225    with 
     226   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
     227   |Some (pl:jump_length)⇒
     228    〈max_length old_length pl,
     229    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 )
     233 Heq2a :
     234  (match 
     235   match instr
     236    in pseudo_instruction
     237    return λ_0:pseudo_instruction.(option jump_length)
     238    with 
     239   [Instruction (i:(preinstruction Identifier))⇒
     240    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     241    (|prefix|) i
     242   |Comment (_0:String)⇒None jump_length
     243   |Cost (_0:costlabel)⇒None jump_length
     244   |Jmp (j:Identifier)⇒
     245    Some jump_length
     246    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     247   |Call (c:Identifier)⇒
     248    Some jump_length
     249    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     250   |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
     251    in option
     252    return λ_0:(option jump_length).ℕ
     253    with 
     254   [None⇒inc_added
     255   |Some (x0:jump_length)⇒
     256    inc_added+(isize-instruction_size_jmplen old_length instr)]
     257   =added)
     258 Heq2b :
     259  (〈inc_pc+isize,
     260   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     261   〈inc_pc+isize,
     262   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     263               (\snd  old_sigma) 〈O,short_jump〉)〉
     264   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     265    〈inc_pc,new_length〉 inc_sigma)〉
     266   =policy)*)
     267 jump_increase (prefix@[〈label,instr〉]) old_sigma policy.
     268 #old_sigma #prefix #label #instr #policy
     269    #i >append_length >commutative_plus #Hi normalize in Hi;
     270    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
     271    [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     272      [ (* 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))
     275        @pair_elim #opc #oj #EQ1 >lookup_insert_miss
     276        [ >lookup_insert_miss
     277          [ @pair_elim #pc #j #EQ2 #X @X
     278          | @bitvector_of_nat_abs
     279            [ @(transitive_lt ??? Hi) ]
     280            [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
     281              @le_S_S @le_plus_n_r
     282            | @lt_to_not_eq @Hi
     283            ]
     284          ]
     285        | @bitvector_of_nat_abs
     286          [ @(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
     289          | @lt_to_not_eq @le_S @Hi
     290          ]
     291        ]
     292      | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >Holdeq normalize nodelta
     293        >lookup_insert_miss
     294        [ >lookup_insert_hit cases (dec_is_jump instr)
     295          [ 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
     306            |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
     307            ]
     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
     328                ]
     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          ]
     345        | @bitvector_of_nat_abs
     346          [ @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
     349          | @lt_to_not_eq @le_n
     350          ]
     351        ]
     352      ]
     353    | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
     354      normalize nodelta
     355      cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉)
     356      #a #b normalize nodelta %2 @refl
     357    ]
     358  ]
     359qed.*)
    87360
    88361(* One step in the search for a jump expansion fixpoint. *)
     
    190463  [ (* USE: policy_jump_equal → added = 0 (from fold) *)
    191464    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi
    192     cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
     465    inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
    193466    [ #Hj
    194467      (* USE: policy_increase (from fold) *)
    195468      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi))
    196       lapply (Habs i Hi Hj)
     469      lapply (Habs i Hi ?) [ >Hj %]
    197470      cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉)
    198471      #opc #oj
     
    204477    | #Hnj
    205478      (* USE: not_jump_default (from fold and old_sigma) *)
    206       >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi Hnj)
    207       >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi Hnj)
    208       @refl
     479      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi ?)
     480      [2: >Hnj %]
     481      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi ?) try %
     482      >Hnj %
    209483    ]
    210484  | #abs >abs in Hsig; #Hsig
     
    232506  #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta
    233507  #Heq1 #Heq2
    234   @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
     508 cut (S (|prefix|) < 2^16)
     509 [ @(transitive_lt … (proj1 … (pi2 ?? program))) @le_S_S >prf >append_length
     510   <plus_n_Sm @le_S_S @le_plus_n_r ] #prefix_ok1
     511 cut (|prefix| < 2^16) [ @(transitive_lt … prefix_ok1) %] #prefix_ok
     512 cases (pair_destruct ?????? Heq2) -Heq2 #Heq2a #Heq2b
     513  % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
    235514  (* NOTE: to save memory and speed up work, there's cases daemon here. They can be
    236515   * commented out for full proofs, but this needs a lot of memory and time *)
    237516  [ (* not_jump_default *)
    238     cases (pair_destruct ?????? Heq2) -Heq2 #_ #Heq2
    239     @(jump_expansion_step1 … prf … Heq1 Heq2)
     517    @(jump_expansion_step1 … Heq1 Heq2b) try assumption
    240518    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
    241519  | (* 0 ↦ 0 *)
    242     <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    243     [ cases (decidable_eq_nat 0 (|prefix|))
    244       [ #Heq <Heq >lookup_insert_hit
    245         (* USE: inc_pc = fst policy *)
    246         >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    247         <Heq
    248         (* USE[pass]: 0 ↦ 0 *)
    249         @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ??  (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
    250       | #Hneq >lookup_insert_miss
    251         [ (* USE[pass]: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
    252         | @bitvector_of_nat_abs
    253           [3: @Hneq]
    254         ]
    255       ]
    256     | @bitvector_of_nat_abs
    257       [3: @lt_to_not_eq @lt_O_S ]
    258     ]
    259     [1,3: @lt_O_S
    260     |2,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
    261       [2: <plus_n_Sm @le_S_S]
    262       @le_plus_n_r
    263     ]
    264   ]
    265   | (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2))
    266     >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
    267   ]
    268   | (* jump_increase *) (* cases daemon *)
    269     #i >append_length >commutative_plus #Hi normalize in Hi;
    270     cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    271     [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    272       [ (* 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))
    275         @pair_elim #opc #oj #EQ1 >lookup_insert_miss
    276         [ >lookup_insert_miss
    277           [ @pair_elim #pc #j #EQ2 #X @X
    278           | @bitvector_of_nat_abs
    279             [ @(transitive_lt ??? Hi) ]
    280             [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
    281               @le_S_S @le_plus_n_r
    282             | @lt_to_not_eq @Hi
    283             ]
    284           ]
    285         | @bitvector_of_nat_abs
    286           [ @(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
    289           | @lt_to_not_eq @le_S @Hi
    290           ]
    291         ]
    292       | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >Holdeq normalize nodelta
    293         >lookup_insert_miss
    294         [ >lookup_insert_hit cases (dec_is_jump instr)
    295           [ 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
    306             |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
    307             ]
    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
    328                 ]
    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           ]
    345         | @bitvector_of_nat_abs
    346           [ @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
    349           | @lt_to_not_eq @le_n
    350           ]
    351         ]
    352       ]
    353     | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
    354       normalize nodelta
    355       cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉)
    356       #a #b normalize nodelta %2 @refl
    357     ]
    358   ]
    359   | (* sigma_compact_unsafe *)
     520    @(jump_expansion_step2 … Heq2b) try assumption
     521    [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ??  (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
     522    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) ]
     523  | (* inc_pc = fst of policy *)
     524    <Heq2b >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
     525  | (* jump_increase *)
     526    cases daemon (*XXX*)
     527  | (* sigma_compact_unsafe *) cases daemon (*
    360528    #i >append_length <commutative_plus #Hi normalize in Hi;
    361529    <(proj2 ?? (pair_destruct ?????? Heq2))
     
    461629      ]
    462630    ]
    463   ]
    464   | (* policy_jump_equal → added = 0 *)
     631  ] *)
     632  | (* policy_jump_equal → added = 0 *) cases daemon (*
    465633    <(proj2 ?? (pair_destruct ?????? Heq2))
    466634    #Heq <(proj1 ?? (pair_destruct ?????? Heq2))
     
    530698      ]
    531699    ]
    532   ]
     700  ] *)
    533701  | (* added = 0 → policy_pc_equal *) cases daemon
    534702    (* USE[pass]: added = 0 → policy_pc_equal *)
     
    831999      ]
    8321000    ] *)
    833   ]
    8341001  | (* out_of_program_none *) cases daemon
    8351002    (* #i #Hi2 >append_length <commutative_plus @conj
     
    8701037      ]
    8711038    ] *)
    872   ]
    8731039  | (* lookup p = lookup old_sigma + added *) cases daemon
    8741040    (* <(proj2 ?? (pair_destruct ?????? Heq2)) >append_length <plus_n_Sm <plus_n_O
     
    10031169      ]
    10041170    ] *)
    1005   ]
    10061171  | (* sigma_safe *) cases daemon (*#i >append_length >commutative_plus #Hi normalize in Hi;
    10071172    elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     
    10241189                    [1,4,7: *)
    10251190                 
    1026   ]        
    1027 | normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
     1191  ]       
     1192| normalize nodelta % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
    10281193  [ #i cases i
    10291194    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    10301195    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
    10311196    ]
     1197  | >lookup_insert_hit @refl
    10321198  | >lookup_insert_hit @refl
    1033   ]
    1034   | >lookup_insert_hit @refl
    1035   ]
    10361199  | #i #Hi <(le_n_O_to_eq … Hi)
    10371200    >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉)
    10381201    #a #b normalize nodelta %2 @refl
    1039   ]
    10401202  | #i cases i
    10411203    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    10421204    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    10431205    ]
    1044   ]
    10451206  | #_ %
    1046   ]
    10471207  | #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit
    10481208    (* USE: 0 ↦ 0 (from old_sigma) *)
    10491209    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))))
    1050   ]
    10511210  | #i cases i
    10521211    [ #Hi2 @conj
     
    10661225      ]
    10671226    ]
    1068   ]
    10691227  | >lookup_insert_hit (* USE: 0 ↦ 0 (from old_sigma) *)
    10701228    >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) <plus_n_O %
    1071   ]
    10721229  | #i cases i
    10731230    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     
    10771234]
    10781235qed.
    1079 
Note: See TracChangeset for help on using the changeset viewer.