Changeset 2152


Ignore:
Timestamp:
Jul 4, 2012, 1:23:00 PM (6 years ago)
Author:
boender
Message:
  • this should compile
Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Policy.ma

    r2141 r2152  
    1212    [ None ⇒ True
    1313    | Some x ⇒
    14       And (And (And (And (And
    15         (out_of_program_none program x)
    16         (not_jump_default program x))
     14      And (And (And (And
     15        (not_jump_default program x)
    1716        (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd x) 〈0,short_jump〉) = 0))
    1817        (\fst x = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd x) 〈0,short_jump〉)))
    19         (\fst x < 2^16))
    20         (no_ch = true → sigma_compact program (create_label_map program) x)
     18        (sigma_compact_unsafe program (create_label_map program) x))
     19        (\fst x < 2^16)
    2120    ]) ≝
    2221 let labels ≝ create_label_map program in
    … …  
    3433  #x cases x -x
    3534  [ #H / by I/
    36   | #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj
    37     [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    38     | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    39     ]
    40     | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     35  | #sigma normalize nodelta #H @conj [ @conj
     36    [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))
     37    | (* #Ht destruct (Ht) *) @(proj2 ?? (proj1 ?? (proj1 ?? H)))
    4138    ]
    4239    | @(proj2 ?? H)
    43     ]
    44     | #H destruct (H)
    4540    ]
    4641  ]
    … …  
    5146    #x cases x -x #ch2 #z2 cases z2 normalize nodelta
    5247    [ #_ / by I/
    53     | #j2 #H2 @conj [ @conj [ @conj [ @conj
    54       [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))))
    55       | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))))
    56       ]
    57       | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))
    58       ]     
     48    | #j2 #H2 @conj [ @conj
     49      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))
     50      | (*#Ht @(equal_compact_unsafe_compact ?? op)
     51        [ @(proj2 ?? (proj1 ?? H2)) @Ht
     52        | cases daemon (* add sigma_safe to properties *)
     53        | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
     54        ]*)
     55        @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
     56      ]
    5957      | @(proj2 ?? H2)
    6058      ]
    61       | #Ht @(equal_compact_unsafe_compact ?? op)
    62         [ @(proj2 ?? (proj1 ?? (proj1 ?? H2))) @Ht
    63         | cases daemon (* add to invvariants *)
    64         | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
    65         ]
    66       ]
    6759    ]
    6860  ]
    … …  
    7163  [ #_ >p2 #ABS destruct (ABS)
    7264  | #map >p2 normalize nodelta
    73     #H #eq destruct (eq) cases daemon (* change order *)
     65    #H #eq destruct (eq) @H
    7466  ]
    7567]
    … …  
    396388    match p with
    397389      [ None ⇒ True
    398       | Some pol ⇒ And (And (out_of_program_none program pol)
    399       (sigma_compact program (create_label_map program) pol))
     390      | Some pol ⇒ And (*And (out_of_program_none program pol)*)
     391      (sigma_compact program (create_label_map program) pol)
    400392      (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0)
    401393      ].
    … …  
    419411      [ #H #Feq whd in match policy_equal_opt; normalize nodelta #ABS destruct (ABS)
    420412      | -Fo #Fp #HFp #Feq whd in match policy_equal_opt; normalize nodelta #Heq
    421         @conj [ @conj
    422         [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))))
    423         | @(proj2 ?? HGp) whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*80s*)
     413        @conj
     414        [ @(equal_compact_unsafe_compact ?? Fp)
     415          [ cases daemon
     416          | cases daemon
     417          | @(proj2 ?? (proj1 ?? HGp))
     418          ]
     419        (*| @(proj2 ?? HGp) whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*80s*)
    424420          >Feq in Geq; cases Fno_ch in HFp Feq; normalize nodelta #HFp #Feq #Geq
    425421          [ destruct (Geq) / by /
    … …  
    436432            ]
    437433          ]
     434        ]*)
     435        | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
    438436        ]
    439         | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
    440         ]
    441437      ]
    442438    ]
    … …  
    525521      >Feq normalize nodelta cases Fno_ch in HFp Feq; #HFp #Feq
    526522      normalize nodelta
    527       [ @conj [ @conj
    528         [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))))
    529         | @((proj2 ?? HFp) (refl ? true)) ]
     523      [ @conj
     524        [ cases daemon (* XXX *)
    530525        | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))
    531526        ]
    532527      | cases (jump_expansion_step ???); #z cases z -z #stch #sto cases sto
    533528        [ #_ / by I/
    534         | -sto #stp normalize nodelta #Hstp @conj [ @conj
    535           [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))))
    536           | @(equal_compact_unsafe_compact ?? Fp)
    537             [ @(proj2 ?? (proj1 ?? (proj1 ?? Hstp))) @(proj2 ?? (proj1 ?? Hstp))
     529        | -sto #stp normalize nodelta #Hstp @conj
     530          [ @(equal_compact_unsafe_compact ?? Fp)
     531            [ @(proj2 ?? (proj1 ?? Hstp)) @(proj2 ?? (proj1 ?? (proj1 ?? Hstp)))
    538532              #i #Hi
    539533              cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
    … …  
    548542                |3: #_ @refl
    549543                ]
    550               | #Hj >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))) i Hi Hj)
    551                 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) i Hi Hj) @refl
     544              | #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))) i Hi Hj)
     545                >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi Hj) @refl
    552546              ]
    553547            | cases daemon 
    554548            | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))
    555549            ]
     550          | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))))
    556551          ]
    557         | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))) ]
    558552        ]
    559553      ]
    … …  
    583577(*CSC: modified to really use the specification in Assembly.ma.*)
    584578definition jump_expansion':
    585 ∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16).
     579∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
    586580 option (Σsigma_policy:(Word → Word) × (Word → bool).
    587581   let 〈sigma,policy〉≝ sigma_policy in
    … …  
    604598[ lapply (proj2 ?? Hfpol) cases (bvt_lookup ??? fpol 〈0,short_jump〉)
    605599  #x #y #Hx normalize nodelta >Hx / by refl/
    606 | #ppc #ppc_ok @conj
     600| cases daemon (* leaving this until stabilisation of sigma predicate *)
     601  (*#ppc #ppc_ok normalize nodelta @conj
    607602  [ #Hppc lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector 16 ppc) ppc_ok)
    608603    >bitvector_of_nat_inverse_nat_of_bitvector
    … …  
    651646        ]
    652647      ]
    653     ]
     648    ] 
    654649  | cases daemon (* XXX remains to be done *)
    655   ]
     650  ] *)
    656651]
    657652qed.           

  • src/ASM/PolicyFront.ma

    r2141 r2152  
    400400    match policy with
    401401    [ None ⇒ True
    402     | Some p ⇒ And (And (And (And (And (And
    403        (out_of_program_none (pi1 ?? program) p)
    404        (not_jump_default (pi1 ?? program) p))
     402    | Some p ⇒ And (And (And (And (And
     403       (not_jump_default (pi1 ?? program) p)
    405404       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
    406405       (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
    … …  
    412411  λprogram.λlabels.
    413412  let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction)
    414   (λprefix.Σpolicy:ppc_pc_map.And (And (And (And (And
    415     (out_of_program_none prefix policy)
    416     (not_jump_default prefix policy))
     413  (λprefix.Σpolicy:ppc_pc_map.And (And (And (And
     414    (not_jump_default prefix policy)
    417415    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
    418416    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
    … …  
    434432| lapply p -p generalize in match (foldl_strong ?????); * #p #Hp #hg
    435433  @conj [ @Hp | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ]
    436 | @conj [ @conj [ @conj [ @conj [ @conj
     434| @conj [ @conj [ @conj [ @conj (*[@conj
    437435  [ (* out_of_program_none *)
    438436    #i #Hi2 >append_length <commutative_plus @conj
    … …  
    482480      ]
    483481    ]
    484   | (* not_jump_default *) cases p -p #p cases p -p #pc #sigma #Hp
     482  | *)
     483  [ (* not_jump_default *) cases p -p #p cases p -p #pc #sigma #Hp
    485484    cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi
    486485    normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    487486    [ >lookup_insert_miss
    488487      [ (* USE[pass]: not_jump_default *)
    489         lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi)
     488        lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)
    490489        >nth_append_first
    491490        [ #H #H2 @H @H2
    … …  
    511510      ]
    512511    ]
    513   ]
    514512  | (* 0 ↦ 0 *)
    515513    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
    516514    >lookup_insert_miss
    517515    [ (* USE[pass]: 0 ↦ 0 *)
    518       @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) 
     516      @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))
    519517    | @bitvector_of_nat_abs
    520518      [ / by /
    … …  
    596594    ]
    597595  ]
    598 | @conj [ @conj [ @conj [ @conj [ @conj
     596| @conj [ @conj [ @conj [ @conj (*[ @conj
    599597  [ #i cases i
    600598    [ #Hi2 @conj
    … …  
    613611      | #_ @le_S_S @le_O_n
    614612      ]
    615     ]
    616   | #i cases i
     613    ] *)
     614  [ #i cases i
    617615    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    618616    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
    619617    ]
    620   ] ] ]
     618  ] ]
    621619  >lookup_insert_hit @refl
    622620  | #i cases i
    … …  
    862860    ]
    863861qed.
     862
     863lemma instruction_size_irrelevant: ∀i.
     864  ¬is_jump i → ∀j1,j2.instruction_size_jmplen j1 i = instruction_size_jmplen j2 i.
     865 #i cases i
     866 [2,3,6: #x [3: #y] #Hj #j1 #j2 %
     867 |4,5: #x #Hi cases Hi #abs @⊥ @abs @I
     868 |1: #pi cases pi
     869   [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:
     870     [1,2,3,6,7,24,25: #x #y
     871     |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     872     #Hj #j1 #j2 %
     873   |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x]
     874     #Hi cases Hi #abs @⊥ @abs @I
     875   ]
     876 ]
     877qed.

  • src/ASM/PolicyStep.ma

    r2141 r2152  
    2222    match y with
    2323    [ None ⇒ nec_plus_ultra program old_policy
    24     | Some p ⇒ And (And (And (And (And (And (And (And (out_of_program_none program p)
    25        (not_jump_default program p))
     24    | Some p ⇒ And (And (And (And (And (And (And
     25       (not_jump_default program p)
    2626       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
    2727       (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
    2828       (jump_increase program old_policy p))
    2929       (sigma_compact_unsafe program labels p))
     30       (sigma_jump_equal program old_policy p → no_ch = true))
    3031       (no_ch = true → sigma_pc_equal program old_policy p))
    31        (sigma_jump_equal program old_policy p → no_ch = true))
    3232       (\fst p < 2^16)
    3333    ])
    … …  
    3838    (λprefix.Σx:ℕ × ppc_pc_map.
    3939      let 〈added,policy〉 ≝ x in
    40       And (And (And (And (And (And (And (And (And (out_of_program_none prefix policy)
    41       (not_jump_default prefix policy))
     40      And (And (And (And (And (And (And (And (And (not_jump_default prefix policy)
    4241      (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
    4342      (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
    … …  
    4645      (sigma_jump_equal prefix old_sigma policy → added = 0))
    4746      (added = 0 → sigma_pc_equal prefix old_sigma policy))
    48       (\fst (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd policy) 〈0,short_jump〉) =
    49        \fst (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉) + added))
     47      (out_of_program_none prefix policy))
     48      (\fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉) =
     49       \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) + added))
    5050      (sigma_safe prefix labels added old_sigma policy))
    5151    program
    … …  
    100100  #x #H #Heq >Heq in H; normalize nodelta -Heq -x #Hind
    101101  (* USE: inc_pc = fst of policy (from fold) *)
    102   >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))))) in p1;
     102  >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) in p1;
    103103  (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *)
    104104  lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))
    105105  #Hsig #Hge
    106106  (* USE: added = 0 → policy_pc_equal (from fold) *)
    107   lapply ((proj2 ?? (proj1 ?? (proj1 ?? Hind))) ? (|program|) (le_n (|program|)))
     107  lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))) ? (|program|) (le_n (|program|)))
    108108  [ (* USE: policy_jump_equal → added = 0 (from fold) *)
    109     @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))) #i #Hi
     109    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi
    110110    cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
    111111    [ #Hj
    112112      (* USE: policy_increase (from fold) *)
    113       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) i (le_S_to_le … Hi))
     113      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi))
    114114      lapply (Habs i Hi Hj)
    115115      cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉)
    … …  
    122122    | #Hnj
    123123      (* USE: not_jump_default (from fold and old_sigma) *)
    124       >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi Hnj)
     124      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi Hnj)
    125125      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi Hnj)
    126126      @refl
    … …  
    132132  >H2 in H; normalize nodelta -H2 -x #H @conj
    133133  [ @conj [ @conj
    134   [ (* USE[pass]: out_of_program_none, not_jump_default, 0 ↦ 0, inc_pc = fst policy,
     134  [ (* USE[pass]: not_jump_default, 0 ↦ 0, inc_pc = fst policy,
    135135     * jump_increase, sigma_compact_unsafe (from fold) *)
    136     @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     136    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
     137  | #H2 (* USE[pass]: sigma_jump_equal → added = 0 (from fold) *)
     138    @eq_to_eqb_true @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) @H2
     139  ]
    137140  | (* USE[pass]: added = 0 → sigma_pc_equal (from fold) *)
    138      #H2 @(proj2 ?? (proj1 ?? (proj1 ?? H))) @eqb_true_to_eq @H2
    139   ]
    140   | #H2 (* USE[pass]: sigma_jump_equal → added = 0 (from fold) *)
    141     @eq_to_eqb_true @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @H2
     141     #H2 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @eqb_true_to_eq @H2
    142142  ]
    143143  | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1
    … …  
    153153  (* NOTE: to save memory and speed up work, there's cases daemon here. They can be
    154154   * commented out for full proofs, but this needs a lot of memory and time *)
    155   [ (* out_of_program_none *) (* cases daemon *)
    156     #i #Hi2 >append_length <commutative_plus @conj
    157     [ (* → *) #Hi normalize in Hi;
    158       cases instr in Heq2; normalize nodelta
    159       #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss
    160       [1,3,5,7,9,11: >lookup_opt_insert_miss
    161         [1,3,5,7,9,11: (* USE[pass]: out_of_program_none → *)
    162           @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2))
    163           @le_S_to_le @Hi
    164         |2,4,6,8,10,12: @bitvector_of_nat_abs
    165           [1,4,7,10,13,16: @Hi2
    166           |2,5,8,11,14,17: @(transitive_lt … Hi2)
    167           |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
    168           ] @le_S_to_le @Hi
    169         ]
    170       |2,4,6,8,10,12: @bitvector_of_nat_abs
    171         [1,4,7,10,13,16: @Hi2
    172         |2,5,8,11,14,17: @(transitive_lt … Hi2)
    173         |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
    174         ] @Hi
    175       ]
    176     | (* ← *) <(proj2 ?? (pair_destruct ?????? Heq2)) #Hl
    177       elim (decidable_lt i (|prefix|))
    178       [ #Hi
    179         lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
    180         #Hl2 (* USE[pass]: out_of_program_none ← *)
    181         lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2) Hl2)
    182         #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3
    183       | #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi))
    184         [ #Hi3 elim (le_to_or_lt_eq … Hi3)
    185           [ / by /
    186           | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? Hl)) >X >eq_bv_refl #H normalize in H; destruct (H)
    187           ]
    188         | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
    189           >X >eq_bv_refl #H normalize in H; destruct (H)
    190         ]
    191       ]
    192     ]
    193   | (* not_jump_default *) (* cases daemon *)
     155  [ (* not_jump_default *) cases daemon (*
    194156    #i >append_length <commutative_plus #Hi normalize in Hi;
    195157    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    … …  
    236198        ]
    237199      ]
    238     ]
    239   ]
    240   | (* 0 ↦ 0 *) (* cases daemon *)
     200    ] *)
     201  | (* 0 ↦ 0 *) cases daemon (*
    241202    <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    242203    [ cases (decidable_eq_nat 0 (|prefix|))
    … …  
    260221      [2: <plus_n_Sm @le_S_S]
    261222      @le_plus_n_r
    262     ]
     223    ] *)
    263224  ]
    264225  | (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2))
    265226    >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
    266227  ]
    267   | (* jump_increase *) (* cases daemon *)
     228  | (* jump_increase *) cases daemon (*
    268229    #i >append_length >commutative_plus #Hi normalize in Hi;
    269230    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    … …  
    359320      cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉)
    360321      #a #b normalize nodelta %2 @refl
    361     ]
    362   ]
    363   | (* sigma_compact_unsafe *) (* cases daemon *)
     322    ] *)
     323  ]
     324  | (* sigma_compact_unsafe *) cases daemon (*
    364325    #i >append_length <commutative_plus #Hi normalize in Hi;
    365326    <(proj2 ?? (pair_destruct ?????? Heq2))
    … …  
    464425        ]
    465426      ]
    466     ]
    467   ]
    468   | (* policy_jump_equal → added = 0 *) (* cases daemon *)
     427    ] *)
     428  ]
     429  | (* policy_jump_equal → added = 0 *) cases daemon (*
    469430    <(proj2 ?? (pair_destruct ?????? Heq2))
    470431    #Heq <(proj1 ?? (pair_destruct ?????? Heq2))
    … …  
    535496    ] *)
    536497  ]
    537   | (* added = 0 → policy_pc_equal *) (* cases daemon *)
     498  | (* added = 0 → policy_pc_equal *) cases daemon (*
    538499    (* USE: added = 0 → policy_pc_equal *)
    539500    lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
    … …  
    565526        |2,4,6: >Hi >lookup_insert_miss
    566527          [1,3,5: >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|)))
    567             @sym_eq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     528            @sym_eq (* USE: fst p = lookup |prefix| *)
     529             @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    568530          |2,4,6: @bitvector_of_nat_abs
    569531            [3,6,9: @lt_to_not_eq @le_n
    … …  
    575537        ]
    576538      |2,4,6: >Hi >lookup_insert_hit
     539        (* USE fst p = lookup |prefix| *)
    577540        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    578541        <(Hold Hadded (|prefix|) (le_n (|prefix|)))
    579         (*<(proj2 ?? (pair_destruct ?????? Heq1))*)
    580542        (* USE: sigma_compact (from old_sigma) *)
    581543        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
    … …  
    593555              >prf >p1 >Hins >nth_append_second
    594556              [2,4,6: @(le_n (|prefix|))
    595               |1,3,5: <minus_n_n whd in match (nth ????);
    596              
    597 
    598 
    599         ]
    600       ]
    601     |4,5: cases daemon
    602     |1: cases daemon
    603     ] (* 4,5 and 1 are equal to 2,3,6, but cases-daemon'd for the moment because of
    604        * memory constraints *)
    605       (*#x #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus
     557              |1,3,5: <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1))
     558                 #H >H @plus_left_monotone @instruction_size_irrelevant @nmk / by /
     559              ]
     560            ]
     561          ]
     562        ]
     563      ]
     564    |4,5: #x #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus
    606565       #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi #Hi
    607566       [1,3: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    … …  
    611570               @plus_zero_zero
    612571             |2,4: @bitvector_of_nat_abs
    613                [1,4: @(transitive_lt ??? Hi)]
    614                [1,2,3,5: @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
    615                  @le_plus_n_r
    616                |4,6: @lt_to_not_eq @Hi
     572               [3,6: @lt_to_not_eq @Hi
     573               |1,4: @(transitive_lt ??? Hi)
    617574               ]
     575               @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
     576               >append_length @le_plus_n_r
    618577             ]
    619578           |2,4: @bitvector_of_nat_abs
    620              [1,4: @(transitive_lt ??? Hi) @le_S_to_le]
    621              [1,2,3,5: @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
    622                <plus_n_Sm @le_S_S @le_plus_n_r
    623              |4,6: @lt_to_not_eq @le_S @Hi
     579             [3,6: @lt_to_not_eq @le_S @Hi
     580             |1,4: @(transitive_lt ??? Hi) @le_S_to_le
    624581             ]
     582             @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
     583             >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    625584           ]
    626585         |2,4: >Hi >lookup_insert_miss
    627586           [1,3: >lookup_insert_hit >(Hold ? (|prefix|) (le_n (|prefix|)))
    628              [2,4: >commutative_plus in Hadded; @plus_zero_zero]
    629              @sym_eq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     587             [2,4: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
     588             (* USE: fst p = lookup |prefix| *)
     589             @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    630590           |2,4: @bitvector_of_nat_abs
    631              [1,4: @(transitive_lt ??? (le_S_S … (le_n (|prefix|))))]
    632              [1,2,3,5: @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
    633                <plus_n_Sm @le_S_S @le_plus_n_r
    634              |4,6: @lt_to_not_eq @le_n
     591             [3,6: @lt_to_not_eq @le_n
     592             |1,4: @(transitive_lt ??? (le_S_S … (le_n (|prefix|))))
    635593             ]
     594             @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
     595             >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    636596           ]
    637597         ]
    638        |2,4: >Hi >lookup_insert_hit
     598       |2,4: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1))
    639599         elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded)))
    640600         [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt <(proj2 ?? (pair_destruct ?????? Heq1))
    641            @etblorp / by I/
    642          |2,4: #H >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     601           @jump_length_le_max / by I/
     602         |2,4: #H (* USE: fst p = lookup |prefix| *)
     603           >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    643604           <(Hold ? (|prefix|) (le_n (|prefix|)))
    644            <(proj2 ?? (pair_destruct ?????? Heq1))
    645            (* USE: sigma_compact (from old_sigma) *)
    646            cases daemon (* XXX add policy_compact_unsafe to old_sigma *)
     605           [1,3: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H
     606             >(jump_length_equal_max … H)
     607             [1,3: (* USE: sigma_compact_unsafe (from old_sigma) *)
     608               lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
     609               [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     610               |2,4: lapply Holdeq lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
     611                 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
     612                 [1,3: normalize nodelta #_ #_ #ABS cases ABS
     613                 |2,4: normalize nodelta
     614                   lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
     615                   cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
     616                   [1,3: #_ #x cases x -x #pc #j normalize nodelta #_ #_ #ABS cases ABS
     617                   |2,4: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
     618                     normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     619                     >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair
     620                     >(proj2 ?? (pair_destruct ?????? EQpair)) >prf >nth_append_second
     621                     [1,3: <minus_n_n >p1 whd in match (nth ????); >Hins #H @H
     622                     |2,4: @le_n
     623                     ]
     624                   ]
     625                 ]
     626               ]
     627             |2,4: / by I/
     628             ]
     629           |2,4: @plus_zero_zero [2,4: >commutative_plus @Hadded]
     630           ]
    647631         ]
    648632       ]
    … …  
    656640          cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    657641          [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:
    658             <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    659           [1,3,5: >lookup_insert_miss
    660             [1,3,5: @(Hold Hadded i (le_S_to_le … Hi))
    661             |2,4,6: @bitvector_of_nat_abs
    662               [1,4,7: @(transitive_lt ??? Hi) ]
    663               [1,2,3,4,6,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length
    664                 @le_S_S @le_plus_n_r
    665               |5,7,9: @lt_to_not_eq @Hi
    666               ]
    667             ]
    668           |2,4,6: @bitvector_of_nat_abs
    669             [1,4,7: @(transitive_lt … Hi) @le_S_to_le]
    670             [1,2,3,4,6,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length
     642            <(proj2 ?? (pair_destruct ?????? Heq2))
     643            >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i))
     644            [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:
     645              >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc,new_length〉 16 (bitvector_of_nat 16 (|prefix|)) (bitvector_of_nat 16 i) inc_sigma)
     646              [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:
     647                @(Hold Hadded i (le_S_to_le … Hi))
     648              |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:
     649                @bitvector_of_nat_abs
     650                [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:
     651                  @lt_to_not_eq @Hi
     652                |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:
     653                  @(transitive_lt ??? Hi)
     654                ]
     655                @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
     656                @le_S_S <plus_n_Sm @le_S @le_plus_n_r
     657              ]
     658            |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:
     659              @bitvector_of_nat_abs
     660              [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:
     661                @lt_to_not_eq @le_S @Hi
     662              |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:
     663                @(transitive_lt … Hi) @le_S_to_le
     664              ]
     665              @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
    671666              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    672             |5,7,9: @lt_to_not_eq @le_S @Hi
    673             ]
    674           ]
    675         |2,4,6: >Hi >lookup_insert_miss
    676           [1,3,5: >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|)))
    677             @sym_eq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    678           |2,4,6: @bitvector_of_nat_abs
    679             [1,4,7: @(transitive_lt ??? (le_S_S … (le_n (|prefix|))))]
    680             [1,2,3,4,6,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length
    681               @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    682             |5,7,9: @lt_to_not_eq @le_n
    683             ]
    684           ]
    685         ]
    686       |2,4,6: >Hi >lookup_insert_hit
    687         >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    688         <(Hold Hadded (|prefix|) (le_n (|prefix|)))
    689         <(proj2 ?? (pair_destruct ?????? Heq1))
    690         (* USE: sigma_compact (from old_sigma) *)
    691         cases daemon (* XXX add policy_compact_unsafe to old_sigma *)
    692       ]*)
    693   ]
    694   | (* lookup p = lookup old_sigma + added *)
    695     cases daemon
    696   ]
    697   | (* sigma_safe *) (* cases daemon *)
    698     #i >append_length >commutative_plus #Hi normalize in Hi;
     667            ]
     668          |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:
     669            >Hi >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|)))
     670            [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:
     671              >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|))) @sym_eq
     672              (* USE: fst p = lookup |prefix| *)
     673              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     674            |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:
     675              @bitvector_of_nat_abs
     676              [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:
     677                @lt_to_not_eq @le_n
     678              |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:
     679                @le_S_to_le
     680              ]
     681              @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
     682                @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
     683            ]
     684          ]
     685        |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:
     686          >Hi >lookup_insert_hit
     687          (* USE fst p = lookup |prefix| *)
     688          >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     689          <(Hold Hadded (|prefix|) (le_n (|prefix|)))
     690          (* USE: sigma_compact (from old_sigma) *)
     691          lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
     692          [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:
     693            >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     694          |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:
     695            lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
     696            cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% -> %);
     697            [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:
     698              normalize nodelta #_ #ABS cases ABS
     699            |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:
     700              lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
     701              cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
     702              [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:
     703                normalize nodelta #Hl #x cases x -x #pc #j normalize nodelta #Hl2 #ABS cases ABS
     704              |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:
     705                normalize nodelta #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
     706                normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉)
     707                >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     708                >prf >p1 >Hins >nth_append_second
     709                [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:
     710                  @(le_n (|prefix|))
     711                |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:
     712                  <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1))
     713                  #H >H @plus_left_monotone @instruction_size_irrelevant @nmk #H @H
     714                ]
     715              ]
     716            ]
     717          ]
     718        ]
     719      |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Hold #Hadded
     720        #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
     721        -Hi #Hi
     722        [1,3,5,7,9,11,13,15,17: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     723          [1,3,5,7,9,11,13,15,17:
     724            >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i))
     725            [1,3,5,7,9,11,13,15,17:
     726              >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc,new_length〉 16 (bitvector_of_nat 16 (|prefix|)) (bitvector_of_nat 16 i) inc_sigma)
     727              [1,3,5,7,9,11,13,15,17: @(Hold ? i (le_S_to_le … Hi))
     728                >commutative_plus in Hadded; @plus_zero_zero
     729              |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
     730                [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi
     731                |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? Hi)
     732                ]
     733                @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
     734                >append_length @le_plus_n_r
     735              ]
     736            |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
     737              [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S @Hi
     738              |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? Hi) @le_S_to_le
     739              ]
     740              @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
     741              >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     742            ]
     743          |2,4,6,8,10,12,14,16,18: >Hi
     744            >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|)))
     745            [1,3,5,7,9,11,13,15,17: >lookup_insert_hit >(Hold ? (|prefix|) (le_n (|prefix|)))
     746              [2,4,6,8,10,12,14,16,18: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
     747              (* USE: fst p = lookup |prefix| *)
     748              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     749            |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
     750              [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n
     751              |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? (le_S_S … (le_n (|prefix|))))
     752              ]
     753              @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
     754              >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     755            ]
     756          ]
     757        |2,4,6,8,10,12,14,16,18: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1))
     758          elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded)))
     759          [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt
     760            <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max / by I/
     761          |2,4,6,8,10,12,14,16,18: #H (* USE: fst p = lookup |prefix| *)
     762            >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     763            <(Hold ? (|prefix|) (le_n (|prefix|)))
     764            [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H
     765              >(jump_length_equal_max … H)
     766              [1,3,5,7,9,11,13,15,17: (* USE: sigma_compact_unsafe (from old_sigma) *)
     767                lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
     768                [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     769                |2,4,6,8,10,12,14,16,18: lapply Holdeq
     770                  lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
     771                  cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
     772                  [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #ABS cases ABS
     773                  |2,4,6,8,10,12,14,16,18: normalize nodelta
     774                    lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
     775                    cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
     776                    [1,3,5,7,9,11,13,15,17: #_ #x cases x -x #pc #j normalize nodelta
     777                      #_ #_ #ABS cases ABS
     778                    |2,4,6,8,10,12,14,16,18: #x cases x -x #Spc #Sj #EQS #x cases x -x
     779                      #pc #j #EQ
     780                      normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     781                      >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair
     782                      >(proj2 ?? (pair_destruct ?????? EQpair)) >prf >nth_append_second
     783                      [1,3,5,7,9,11,13,15,17: <minus_n_n >p1 whd in match (nth ????); >Hins #H @H
     784                      |2,4,6,8,10,12,14,16,18: @le_n
     785                      ]
     786                    ]
     787                  ]
     788                ]
     789              |2,4,6,8,10,12,14,16,18: / by I/
     790              ]
     791            |2,4,6,8,10,12,14,16,18: @plus_zero_zero
     792              [2,4,6,8,10,12,14,16,18: >commutative_plus @Hadded]
     793            ]
     794          ]
     795        ]
     796      ]
     797    ] *)
     798  ]
     799  | (* out_of_program_none *) cases daemon
     800    (* #i #Hi2 >append_length <commutative_plus @conj
     801    [ (* → *) #Hi normalize in Hi;
     802      cases instr in Heq2; normalize nodelta
     803      #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss
     804      [1,3,5,7,9,11: >lookup_opt_insert_miss
     805        [1,3,5,7,9,11: (* USE[pass]: out_of_program_none → *)
     806          @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2))
     807          @le_S_to_le @Hi
     808        |2,4,6,8,10,12: @bitvector_of_nat_abs
     809          [1,4,7,10,13,16: @Hi2
     810          |2,5,8,11,14,17: @(transitive_lt … Hi2)
     811          |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
     812          ] @le_S_to_le @Hi
     813        ]
     814      |2,4,6,8,10,12: @bitvector_of_nat_abs
     815        [1,4,7,10,13,16: @Hi2
     816        |2,5,8,11,14,17: @(transitive_lt … Hi2)
     817        |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
     818        ] @Hi
     819      ]
     820    | (* ← *) <(proj2 ?? (pair_destruct ?????? Heq2)) #Hl
     821      elim (decidable_lt i (|prefix|))
     822      [ #Hi
     823        lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
     824        #Hl2 (* USE[pass]: out_of_program_none ← *)
     825        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2) Hl2)
     826        #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3
     827      | #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi))
     828        [ #Hi3 elim (le_to_or_lt_eq … Hi3)
     829          [ / by /
     830          | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? Hl)) >X >eq_bv_refl #H normalize in H; destruct (H)
     831          ]
     832        | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
     833          >X >eq_bv_refl #H normalize in H; destruct (H)
     834        ]
     835      ]
     836    ] *)
     837  ]
     838  | (* lookup p = lookup old_sigma + added *) cases daemon
     839    (* <(proj2 ?? (pair_destruct ?????? Heq2)) >append_length <plus_n_Sm <plus_n_O
     840    >lookup_insert_hit
     841    <(proj1 ?? (pair_destruct ?????? Heq2)) cases instr in p1 Heq1;
     842    [2,3,6: #x [3: #y] normalize nodelta #p1 #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
     843      (* USE: sigma_compact_unsafe (from old_sigma) *)
     844      lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
     845      [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     846      |2,4,6: lapply Holdeq -Holdeq
     847        lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
     848        cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
     849        [1,3,5: normalize nodelta #_ #_ #abs cases abs
     850        |2,4,6: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
     851          cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
     852          [1,3,5: normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs
     853          |2,4,6: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta
     854            #H (* USE: fst p = lookup |prefix| *)
     855            >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     856            (* USE[pass]: lookup p = lookup old_sigma + added *)
     857            >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
     858            -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
     859            >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second
     860            [1,3,5: <minus_n_n >p1 whd in match (nth ????); >associative_plus
     861              >(associative_plus pc) @plus_left_monotone >commutative_plus
     862              @plus_right_monotone @instruction_size_irrelevant @nmk #H @H
     863            |2,4,6: @le_n
     864            ]
     865          ]
     866        ]
     867      ]
     868    |4,5: #x normalize nodelta #p1 #Heq1
     869      (* USE: sigma_compact_unsafe (from old_sigma) *)
     870      lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
     871      [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     872      |2,4: lapply Holdeq -Holdeq
     873        lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
     874        cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
     875        [1,3: normalize nodelta #_ #_ #abs cases abs
     876        |2,4: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
     877          cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
     878          [1,3: normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs
     879          |2,4: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta
     880            #H (* USE: fst p = lookup |prefix| *)
     881            >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     882            (* USE[pass]: lookup p = lookup old_sigma + added *)
     883            >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
     884            -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
     885            >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >associative_plus
     886            >(associative_plus pc) @plus_left_monotone >assoc_plus1
     887            >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative
     888            [1,3: >(proj2 ?? (pair_destruct ?????? EQ)) >prf >nth_append_second
     889              [1,3: <minus_n_n whd in match (nth ????); >p1 >commutative_plus
     890                @minus_plus_m_m
     891              |2,4: @le_n
     892              ]
     893            |2,4: <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max @I
     894            ]
     895          ]
     896        ]
     897      ]
     898    |1: #pi cases pi
     899      [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:
     900        [1,2,3,6,7,24,25: #x #y
     901        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     902        normalize nodelta #p1 #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
     903        (* USE: sigma_compact_unsafe (from old_sigma) *)
     904        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
     905        [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:
     906          >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     907        |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:
     908          lapply Holdeq -Holdeq lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
     909          cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
     910          [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:
     911            normalize nodelta #_ #_ #abs cases abs
     912          |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:
     913            lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
     914            cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
     915            [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:
     916              normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs
     917            |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:
     918              #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta
     919              #H (* USE: fst p = lookup |prefix| *)
     920              >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     921              (* USE[pass]: lookup p = lookup old_sigma + added *)
     922              >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
     923              -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
     924              >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second
     925              [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:
     926                <minus_n_n >p1 whd in match (nth ????); >associative_plus
     927                >(associative_plus pc) @plus_left_monotone >commutative_plus
     928                @plus_right_monotone @instruction_size_irrelevant @nmk #H @H
     929              |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:
     930                @le_n
     931              ]
     932            ]
     933          ]
     934        ]
     935      |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta #p1 #Heq1
     936      (* USE: sigma_compact_unsafe (from old_sigma) *)
     937        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
     938        [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     939        |2,4,6,8,10,12,14,16,18: lapply Holdeq -Holdeq
     940          lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
     941          cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
     942          [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #abs cases abs
     943          |2,4,6,8,10,12,14,16,18: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
     944            cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
     945            [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #x cases x -x #Spc #Sj
     946              normalize nodelta #_ #_ #abs cases abs
     947            |2,4,6,8,10,12,14,16,18: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j
     948              #Holdeq #EQ normalize nodelta #H (* USE: fst p = lookup |prefix| *)
     949              >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     950              (* USE[pass]: lookup p = lookup old_sigma + added *)
     951              >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
     952              -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
     953              >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >associative_plus
     954              >(associative_plus pc) @plus_left_monotone >assoc_plus1
     955              >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative
     956              [1,3,5,7,9,11,13,15,17: >(proj2 ?? (pair_destruct ?????? EQ)) >prf
     957                >nth_append_second
     958                [1,3,5,7,9,11,13,15,17: <minus_n_n whd in match (nth ????); >p1
     959                  >commutative_plus @minus_plus_m_m
     960                |2,4,6,8,10,12,14,16,18: @le_n
     961                ]
     962              |2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq1))
     963                @jump_length_le_max @I
     964              ]
     965            ]
     966          ]
     967        ]
     968      ]
     969    ] *)
     970  ]
     971  | (* sigma_safe *) cases daemon
     972    (* #i >append_length >commutative_plus #Hi normalize in Hi;
    699973    elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    700974    [ >nth_append_first [2: @Hi]
    … …  
    704978          [ elim (le_to_or_lt_eq … Hi) -Hi #Hi
    705979            [ >lookup_insert_miss
    706               [ (* USE[pass]: sigma_safe *)
    707                 lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
    708                 cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
    709                 #pc #j cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉)
    710                 #pc_plus_jmp_length #_ cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins
    711                 normalize nodelta #Hind #dest #Hj lapply (Hind dest Hj) -Hind
    712                 lapply (refl ? (leb (lookup_def … labels dest 0) (S (|prefix|))))
    713                 cases (leb (lookup_def … labels dest 0) (S (|prefix|))) in ⊢ (???% → %);
    714                 normalize nodelta
    715                 [ #Hle elim (le_to_or_lt_eq … (leb_true_to_le … Hle)) -Hle #Hle
    716                   [ >(le_to_leb_true … (le_S_S_to_le … Hle)) normalize nodelta
    717                     >lookup_insert_miss
    718                     [ elim (le_to_or_lt_eq … (le_S_S_to_le … Hle)) -Hle #Hle
    719                       [ >lookup_insert_miss
    720                         [ cases j / by /
    721                         | @bitvector_of_nat_abs
    722                           [ @(transitive_lt ??? Hle) ]
    723                           [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program)))
    724                             >prf @le_S_S >append_length @le_plus_n_r
    725                           | @lt_to_not_eq @Hle
     980              [ lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
     981                lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le … Hi))
     982               lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma))
     983                cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) in ⊢ (???% → %);
     984                [ normalize nodelta #_ #abs cases abs
     985                | #x cases x -x #ipc #ij #EQi normalize nodelta
     986                  lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))
     987                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %);
     988                  [ normalize nodelta #_ #abs cases abs
     989                  | #x cases x -x #Sipc #Sij #EQSi normalize nodelta #Hcompact
     990                    >(lookup_opt_lookup_hit … EQi 〈0,short_jump〉)
     991                    >(lookup_opt_lookup_hit … EQSi 〈0,short_jump〉) >Hcompact
     992                    normalize nodelta (*cases ij*) normalize nodelta
     993                    lapply (refl ? (nth i ? prefix 〈None ?, Comment []〉))
     994                    cases (nth i ? prefix 〈None ?, Comment []〉) in ⊢ (???% → %);
     995                    #lbl #ins normalize nodelta #Hins #Hind #dest #Hi
     996                    lapply (Hind dest Hi) -Hind #Hind
     997                    elim (decidable_le (lookup_def … labels dest 0) (S (|prefix|)))
     998                    [ #Hle elim (le_to_or_lt_eq … Hle) -Hle #Hle
     999                      [ elim (le_to_or_lt_eq … (le_S_S_to_le … Hle)) -Hle #Hle
     1000                        [ >(le_to_leb_true ?? (le_S_to_le ?? Hle)) in Hind;
     1001                          >(le_to_leb_true ?? (le_S ?? (le_S_to_le ?? Hle)))
     1002                          normalize nodelta >lookup_insert_miss
     1003                          [ >lookup_insert_miss
     1004                            [ #H @H
     1005                            | @bitvector_of_nat_abs
     1006                              [3: @lt_to_not_eq @Hle
     1007                              |1: @(transitive_lt ??? Hle)
     1008                              ] @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
     1009                               >append_length @le_S_S @le_plus_n_r
     1010                            ]
     1011                          | @bitvector_of_nat_abs
     1012                            [3: @lt_to_not_eq @le_S_to_le @le_S_S @Hle
     1013                            |1: @(transitive_lt ??? Hle) @le_S_to_le
     1014                            ] @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
     1015                            >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
     1016                          ]
     1017                        | >Hle >Hle in Hind; >(le_to_leb_true ?? (le_n (|prefix|)))
     1018                          >(le_to_leb_true ?? (le_S ?? (le_n (|prefix|))))
     1019                          normalize nodelta >lookup_insert_miss
     1020                          [ >lookup_insert_hit
     1021                            >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     1022                            #H @H
     1023                          | @bitvector_of_nat_abs
     1024                            [3: @lt_to_not_eq @le_n
     1025                            |1: @le_S_to_le
     1026                            ] @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
     1027                            >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    7261028                          ]
    7271029                        ]
    728                       | >Hle >lookup_insert_hit
    729                         (* USE: inc_pc = fst policy *)
    730                         <(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    731                         cases j / by /
     1030                      | >Hle >Hle in Hind;
     1031                        >(not_le_to_leb_false (S (|prefix|)) (|prefix|))
     1032                        [2: @le_to_not_lt @le_n]
     1033                        >(le_to_leb_true ?? (le_n (S (|prefix|))))
     1034                        normalize nodelta >lookup_insert_hit
     1035                        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
     1036                        [ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     1037                        | lapply (proj2 ?? (proj1 ?? Hpolicy))
     1038                          lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
     1039                          cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
     1040                          [ normalize nodelta #_ #_ #abs cases abs
     1041                          | #x cases x -x #opc #oj #EQo
     1042                            lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
     1043                            cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
     1044                            [ normalize nodelta #_ #_ #abs cases abs
     1045                            | #x cases x -x #Sopc #Soj #EQSo normalize nodelta
     1046                              #Hadded #Hcommon
     1047                              >(lookup_opt_lookup_hit … EQSo 〈0,short_jump〉)
     1048                              >Hcommon >(lookup_opt_lookup_hit … EQo 〈0,short_jump〉) in Holdeq;
     1049                              #Holdeq >(proj1 ?? (pair_destruct ?????? Holdeq))
     1050                              >(commutative_plus old_pc ?) >associative_plus
     1051                              <Hadded
     1052                              <(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     1053                              >prf >nth_append_second
     1054                              [ <minus_n_n whd in match (nth ????); >p1 cases instr in Heq1;
     1055                                [2,3,6: #x [3: #y] normalize nodelta #Heq1
     1056                                  <(proj2 ?? (pair_destruct ?????? Heq1))
     1057                                  <(commutative_plus inc_pc)
     1058                                  >(instruction_size_irrelevant ?? oj short_jump)
     1059                                  [1,3,5: #H @H
     1060                                  |2,4,6: @nmk #H @H
     1061                                  ]
     1062                                |4,5: #x normalize nodelta #Heq1
     1063                                  <(proj2 ?? (pair_destruct ?????? Heq1)) #Hind
     1064                                  cases daemon (* axiomatise this *)
     1065                                |1: #pi cases pi
     1066                                  [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:
     1067                                    [1,2,3,6,7,24,25: #x #y
     1068                                    |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     1069                                    normalize nodelta #Heq1
     1070                                    <(proj2 ?? (pair_destruct ?????? Heq1))
     1071                                    <(commutative_plus inc_pc)
     1072                                    >(instruction_size_irrelevant ?? oj short_jump)
     1073                                    [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:
     1074                                      #H @H
     1075                                    |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:
     1076                                      @nmk #H @H
     1077                                    ]
     1078                                  |9,10,11,12,13,14,15,16,17:
     1079                                    #x [3,4,5,8,9: #y] normalize nodelta #Heq1
     1080                                    <(proj2 ?? (pair_destruct ?????? Heq1)) #Hind
     1081                                    cases daemon (* axiomatise this *)
     1082                                  ]
     1083                                ]
     1084                              | @le_n
     1085                              ]
     1086                            ]
     1087                          ]
     1088                        ]
    7321089                      ]
    733                     | @bitvector_of_nat_abs
    734                       [ @(transitive_lt ??? Hle) ]
    735                       [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program)))
    736                         @le_S_S >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    737                       | @lt_to_not_eq @Hle
     1090                    | #X >(not_le_to_leb_false … X)
     1091                      >(not_le_to_leb_false … (lt_to_not_le … (le_S_to_le … (not_le_to_lt … X)))) in Hind;
     1092                      normalize nodelta <(proj1 ?? (pair_destruct ?????? Heq2))
     1093                      cases instr in Heq1;
     1094                      [2,3,6: #x [3: #y] normalize nodelta #_ #H @H
     1095                      |4,5: #x normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) #Hind
     1096                        cases daemon (* axiomatise this *)
     1097                      |1: #pi cases pi
     1098                        [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:
     1099                          [1,2,3,6,7,24,25: #x #y
     1100                          |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     1101                          normalize nodelta #_ #H @H
     1102                        |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
     1103                          normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
     1104                          #Hind cases daemon (* axiomatise this *)
     1105                        ]
    7381106                      ]
    7391107                    ]
    740                   | >Hle >lookup_insert_hit >(not_le_to_leb_false (S (|prefix|)) (|prefix|))
    741                     [2: @le_to_not_lt @le_n ] normalize nodelta
    742                     (* USE: lookup p = lookup old_sigma + added *)
    743                     <(proj2 ?? (proj1 ?? Hpolicy)) cases daemon (* use compactness here *)
    7441108                  ]
    745                 | (* same, but with forward jump *) cases daemon
    7461109                ]
    747               | @bitvector_of_nat_abs cases daemon (* trivial, see above *)
    748               ]
    749             | >Hi >lookup_insert_hit cases daemon
    750             ]
    751           | @bitvector_of_nat_abs cases daemon (* see above *)
    752           ]
    753         | @bitvector_of_nat_abs cases daemon
    754         ]
    755       | @bitvector_of_nat_abs cases daemon
    756       ]
    757     | >Hi cases daemon
    758     ] *)
    759   ]
     1110              | @bitvector_of_nat_abs
     1111                [3: @lt_to_not_eq @Hi
     1112                |1: @(transitive_lt ??? Hi)
     1113                ]
     1114                @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
     1115                @le_S_S @le_plus_n_r
     1116              ]
     1117            | >Hi >lookup_insert_hit lapply ((proj2 ?? Hpolicy) i)
     1118            ] XXX to be continued *)
     1119  ]         
    7601120| normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
    7611121  [ #i cases i
     1122    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     1123    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
     1124    ]
     1125  | >lookup_insert_hit @refl
     1126  ]
     1127  | >lookup_insert_hit @refl
     1128  ]
     1129  | #i #Hi <(le_n_O_to_eq … Hi)
     1130    >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉)
     1131    #a #b normalize nodelta %2 @refl
     1132  ]
     1133  | #i cases i
     1134    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     1135    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     1136    ]
     1137  ]
     1138  | #_ %
     1139  ]
     1140  | #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit
     1141    (* USE: 0 ↦ 0 (from old_sigma) *)
     1142    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))))
     1143  ]
     1144  | #i cases i
    7621145    [ #Hi2 @conj
    7631146      [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /
    … …  
    7761159      ]
    7771160    ]
    778   | #i cases i
    779     [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    780     | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
    781     ]
    782   ]
    783   | >lookup_insert_hit @refl
    784   ]
    785   | >lookup_insert_hit @refl
    786   ]
    787   | #i #Hi <(le_n_O_to_eq … Hi)
    788     >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉)
    789     #a #b normalize nodelta %2 @refl
     1161  ]
     1162  | >lookup_insert_hit (* USE: 0 ↦ 0 (from old_sigma) *)
     1163    >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) <plus_n_O %
    7901164  ]
    7911165  | #i cases i
    … …  
    7941168    ]
    7951169  ]
    796   | #_ %
    797   ]
    798   | #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit
    799     (* USE: 0 ↦ 0 (from old_sigma) *)
    800     @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))))
    801   ]
    802   | cases daemon (* empty program here *)
    803   ]
    804   | #i cases i
    805     [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    806     | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    807     ]
    808   ]
    8091170]
    8101171qed.
     1172
Note: See TracChangeset for help on using the changeset viewer.