Changeset 2059 for src


Ignore:
Timestamp:
Jun 13, 2012, 3:44:20 PM (9 years ago)
Author:
boender
Message:
  • updated Policy to work better
Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Policy.ma

    r2055 r2059  
    77let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (S (|l|)) 2^16) (n: ℕ)
    88  on n:(Σx:bool × (option ppc_pc_map).
    9     let 〈c,pol〉 ≝ x in
     9    let 〈no_ch,pol〉 ≝ x in
    1010    And
    1111    (match pol with
    1212    [ None ⇒ True
    1313    | Some x ⇒
    14       And (And (And (And
     14      And (And (And (And (And
    1515        (out_of_program_none program x)
    1616        (jump_not_in_policy program x))
    17         (n > 0 → policy_compact program (create_label_map program) x))
     17        (no_ch = true → policy_compact program (create_label_map program) x))
    1818        (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd x) 〈0,short_jump〉) = 0))
     19        (\fst x = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd x) 〈0,short_jump〉)))
    1920        (\fst x < 2^16)
    20     ]) (n = 0 → c = true)) ≝
     21    ]) (n = 0 → no_ch = false)) ≝
    2122  let labels ≝ create_label_map program in
    2223  match n return λx.n = x → Σa:bool × (option ppc_pc_map).? with
    23   [ O   ⇒ λp.〈true,pi1 ?? (jump_expansion_start program labels)〉
    24   | S m ⇒ λp.let 〈ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
     24  [ O   ⇒ λp.〈false,pi1 ?? (jump_expansion_start program labels)〉
     25  | S m ⇒ λp.let 〈no_ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
    2526          match z return λx. z=x → Σa:bool × (option ppc_pc_map).? with
    2627          [ None    ⇒ λp2.〈false,None ?〉
    27           | Some op ⇒ λp2.if ch
    28             then pi1 ?? (jump_expansion_step program labels «op,?»)
    29             else pi1 ?? (jump_expansion_internal program m)
     28          | Some op ⇒ λp2.if no_ch
     29            then pi1 ?? (jump_expansion_internal program m)
     30            else pi1 ?? (jump_expansion_step program labels «op,?»)
    3031          ] (refl … z)
    3132  ] (refl … n).
    … …  
    3334  #x cases x -x
    3435  [ #H @conj / by I/
    35   | #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj
     36  | #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj [ @conj
    3637    [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    37     | >p #H @⊥ @(absurd ? H) @le_to_not_lt @le_n
     38    | >p #H destruct (H)
    3839    ]
    3940    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
    4041    ]
     42    | cases daemon (* XXX add this to jump_expansion_start *)
     43    ]
    4144    | @(proj2 ?? H)
    4245    ]
    … …  
    4548  ]
    4649| normalize nodelta @conj [ / by I/ | >p #H destruct (H) ]
    47 | cases ch in p1; #p1
    48   [ normalize nodelta
    49     cases (jump_expansion_step program (create_label_map program) «op,?»)
     50| cases no_ch in p1; #p1
     51  [ normalize nodelta lapply (pi2 ?? (jump_expansion_internal program m))
     52    <p1 >p2 normalize nodelta #H @conj
     53    [ @(proj1 ?? H)
     54    | >p #H2 destruct (H2)
     55    ]
     56  | cases (jump_expansion_step program (create_label_map program) «op,?»)
    5057    #x cases x -x #ch2 #z2 cases z2 normalize nodelta
    5158    [ #_ @conj [ / by I/ | >p #H2 destruct (H2) ]
    52     | #j2 #H2 @conj [ @conj [ @conj [ @conj
    53       [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))
    54       | #_ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))
     59    | #j2 #H2 @conj [ @conj [ @conj [ @conj [ @conj
     60      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))))
     61      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))
     62      ]
     63      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))
    5564      ]
    5665      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
    … …  
    6069      | >p #H3 destruct (H3)
    6170      ]
    62     ]
    63   | normalize nodelta lapply (pi2 ?? (jump_expansion_internal program m))
    64     <p1 >p2 normalize nodelta #H @conj [ @conj [ @conj [ @conj
    65     [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
    66     | >p #Hm cases (le_to_or_lt_eq … Hm) -Hm #Hm
    67       [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @(le_S_S_to_le … Hm)
    68       | lapply ((proj2 ?? H) (sym_eq … (injective_S … Hm))) #H2 destruct (H2)
    69       ]
    70     ]
    71     | @(proj2 ?? (proj1 ?? (proj1 ?? H)))
    72     ]
    73     | @(proj2 ?? (proj1 ?? H))
    74     ]
    75     | >p #H2 destruct (H2)
    7671    ]
    7772  ]
    … …  
    8075  [ #_ >p2 #ABS destruct (ABS)
    8176  | #map >p2 normalize nodelta
    82     #H #eq destruct (eq) @conj [ @conj
    83     [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     77    #H #eq destruct (eq) @conj [ @conj [ @conj
     78    [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
     79    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     80    ]
    8481    | @(proj2 ?? (proj1 ?? (proj1 ?? H)))
    8582    ]
    … …  
    9087qed.
    9188
    92 lemma pe_int_refl: ∀program.reflexive ? (policy_equal program).
     89lemma pe_int_refl: ∀program.reflexive ? (policy_jump_equal program).
    9390#program whd #x whd #n #Hn
    9491cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,short_jump〉)
    … …  
    9693qed.
    9794
    98 lemma pe_int_sym: ∀program.symmetric ? (policy_equal program).
     95lemma pe_int_sym: ∀program.symmetric ? (policy_jump_equal program).
    9996#program whd #x #y #Hxy whd #n #Hn
    10097lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉)
    … …  
    104101qed.
    105102 
    106 lemma pe_int_trans: ∀program.transitive ? (policy_equal program).
    107 #program whd #x #y #z whd in match (policy_equal ???); whd in match (policy_equal ?y ?);
    108 whd in match (policy_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
     103lemma pe_int_trans: ∀program.transitive ? (policy_jump_equal program).
     104#program whd #x #y #z whd in match (policy_jump_equal ???); whd in match (policy_jump_equal ?y ?);
     105whd in match (policy_jump_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
    109106lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉)
    110107#x1 #x2
    … …  
    118115  match p1 with
    119116  [ Some x1 ⇒ match p2 with
    120               [ Some x2 ⇒ policy_equal program x1 x2
     117              [ Some x2 ⇒ policy_jump_equal program x1 x2
    121118              | _       ⇒ False
    122119              ]
    … …  
    252249    jump_not_in_policy program p ∧
    253250    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
     251    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
    254252    \fst p < 2^16.
    255253  ∀l.|l| ≤ |program| → ∀acc:ℕ.
    … …  
    265263  [ / by I/
    266264  | #x normalize nodelta #Hx #Hjeq
    267     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx))))) (|t|) Hp)
     265    lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))))) (|t|) (le_S_to_le … Hp))
    268266    whd in match (measure_int ???); whd in match (measure_int ? x ?);
    269267    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd (pi1 ?? policy)) 〈0,short_jump〉)
    … …  
    336334    out_of_program_none program p ∧ jump_not_in_policy program p ∧
    337335    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
     336    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
    338337    \fst p < 2^16.
    339338  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with
    340339  [ None ⇒ True
    341   | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_equal program policy p ].
     340  | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_jump_equal program policy p ].
    342341#program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program) policy)))
    343342cases (jump_expansion_step program (create_label_map program) policy) in ⊢ (???% → %);
    … …  
    347346  @(list_ind ?  (λx.|x| ≤ |pi1 ?? program| →
    348347      measure_int x policy 0 = measure_int x p 0 →
    349       policy_equal x policy p) ?? (pi1 ?? program))
     348      policy_jump_equal x policy p) ?? (pi1 ?? program))
    350349 [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @le_to_not_lt @le_O_n
    351350 | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … (le_S_S_to_le …  Hi)) -Hi #Hi
    … …  
    353352     [ @(transitive_le … Hp) / by /
    354353     | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
    355        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))))) (|t|) Hp) #Hinc
    356        cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm Hinc; #x1 #x2
    357        cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉); #y1 #y2
    358        #Hm #Hinc lapply Hm -Hm; lapply Hinc -Hinc; normalize nodelta
     354       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) (|t|) (le_S_to_le … Hp))
     355       #Hinc cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm Hinc;
     356       #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉);
     357       #y1 #y2 #Hm #Hinc lapply Hm -Hm; lapply Hinc -Hinc; normalize nodelta
    359358       cases x2 cases y2 normalize nodelta
    360359       [1: / by /
    … …  
    376375     ]
    377376   | >Hi whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
    378      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))))) (|t|) Hp)
     377     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) (|t|) (le_S_to_le … Hp))
    379378     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm;
    380379     #x1 #x2
    … …  
    436435      [ None ⇒ True
    437436      | Some pol ⇒ And (out_of_program_none program pol)
    438       ((pi1 ?? program) ≠ [] → policy_compact program (create_label_map program) pol)
     437      (policy_compact program (create_label_map program) pol)
    439438      ])
    440439    (∃n.∀k.n < k →
    … …  
    442441#program @(\snd (pi1 ?? (jump_expansion_internal program (2*|program|)))) @conj
    443442[ lapply (pi2 ?? (jump_expansion_internal program (2*|program|)))
    444     cases (jump_expansion_internal program (2*|program|)) #p cases p -p
    445     #c #pol #Hp cases pol
    446     [ normalize nodelta //
    447     | #x normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    448     | #Hneq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) cases (pi1 ?? program) in Hneq;
    449       [ #H cases H #H @⊥ @H @refl
    450       | #h #t #_ / by /
    451       ] ]
    452     ]
     443  cases (jump_expansion_internal program (2*|program|)) #p cases p -p
     444  #c #pol #Hp cases pol
     445  [ normalize nodelta //
     446  | #x normalize nodelta #H @conj
     447    [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))
     448    | #Hneq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
     449      cases daemon (* XXX add invariant here *)
     450    ]
     451  ]
    453452| cases (dec_bounded_exists (λk.policy_equal_opt (pi1 ?? program)
    454453   (\snd (pi1 ?? (jump_expansion_internal program k)))
    … …  
    477476      >EQ normalize nodelta
    478477      lapply (refl ? (jump_expansion_step program (create_label_map program) «Fp,?»))
    479       [ @conj [ @conj
    480       [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))
    481       | @(proj2 ?? (proj1 ?? (proj1 ?? HFp))) ]
    482       | @(proj2 ?? (proj1 ?? HFp)) ]
     478      [ @conj [ @conj [ @conj
     479      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))))
     480      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))
     481      ]
     482      | @(proj2 ?? (proj1 ?? (proj1 ?? HFp)))
     483      ]
     484      | @(proj2 ?? (proj1 ?? HFp))
     485      ]
    483486      | lapply (measure_full program Fp ?)
    484487        [ @le_to_le_to_eq
    … …  
    517520                    [ cases (jump_expansion_internal program x) in Hxpol;
    518521                      #z cases z -z #xch #xpol normalize nodelta #H #H2 >(proj1 ?? H2) in H;
    519                       normalize nodelta #H @conj [ @conj
    520                       [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     522                      normalize nodelta #H @conj [ @conj [ @conj
     523                      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
     524                      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) ]
    521525                      | @(proj2 ?? (proj1 ?? (proj1 ?? H))) ]
    522526                      | @(proj2 ?? (proj1 ?? H)) ]
    … …  
    524528                      lapply (refl ? (jump_expansion_internal program x))
    525529                      lapply Hxpol -Hxpol
    526                       whd in match (jump_expansion_internal program (S x));
     530                      cases daemon (* this whd takes an enormous amount of time *)
     531                      (* whd in match (pi1 ?? (jump_expansion_internal program (S x)));
    527532                      cases (jump_expansion_internal program x) in ⊢ (% → ???% → %);
    528533                      #z cases z -z #xch #b normalize nodelta #H #Heq >(proj1 ?? Heq) in H;
    529534                      #H #Heq2 cases xch in H Heq2; #H #Heq2 normalize nodelta
    530535                      [ lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»))
    531                         [ @conj [ @conj
    532                           [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     536                        [ @conj [ @conj [ @conj
     537                          [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     538                          | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) ]
    533539                          | @(proj2 ?? (proj1 ?? (proj1 ?? H))) ]
    534540                          | @(proj2 ?? (proj1 ?? H)) ]
    … …  
    559565                          ]
    560566                        ]
    561                       ]
     567                      ] *)
    562568                    ]
    563569                  ]
    … …  
    572578          [ #H #EQ2 @⊥ @(absurd ?? H) @Hfull
    573579          | #Gp #HGp #EQ2 cases Fch
    574             [ normalize nodelta #i #Hi
     580            [ normalize nodelta /2 by pe_int_refl/
     581            | normalize nodelta #i #Hi
    575582              cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) #Hj
    576               [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))) i Hi)
     583              [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))))) i (le_S_to_le … Hi))
    577584                lapply (Hfull i Hi Hj)
    578585                cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
    … …  
    583590                |3: #_ @refl
    584591                ]
    585               | >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))))) i Hi Hj)
    586                 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) i Hi Hj) @refl
     592              | >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))))) i Hi Hj)
     593                >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))) i Hi Hj) @refl
    587594              ]
    588             | normalize nodelta /2 by pe_int_refl/
    589595            ]
    590596          ]
    … …  
    599605  cases npol in Hnpol; cases Spol in HSpol;
    600606  [ #Hnpol #HSpol %1 //
    601   |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal ???); //
     607  |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); //
    602608    #H destruct (H)
    603   |4: #np #Hnp #Sp #HSp whd in match (policy_equal ???); cases program #p #_ cases p
     609  |4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); cases program #p #_ cases p
    604610    [ %1 #m #Hm @⊥ @(absurd ? Hm) @le_to_not_lt @le_O_n
    605611    | #h #t elim (dec_bounded_forall ?? (|t|))

  • src/ASM/PolicyFront.ma

    r2048 r2059  
    128128  ppc_pc_map → Prop ≝
    129129 λprogram.λop.λp.
    130  ∀i.i < |program| →
     130 ∀i.i ≤ |program| →
    131131   let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,short_jump〉 in
    132132   let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉 in
    133133     (*opc ≤ pc ∧*) jmpleq oj j.
    134 
     134     
    135135(* this is the instruction size as determined by the jump length given *)
    136136definition expand_relative_jump_internal_unsafe:
    … …  
    639639qed.
    640640
    641 definition policy_equal ≝
     641(* NOTE: we only compare the first elements here because otherwise the
     642 * added = 0 → policy_equal property of jump_expansion_step doesn't hold:
     643 * if we have not added anything to the pc, we only know the PC hasn't changed,
     644 * there might still have been a short/medium jump change *)
     645definition policy_pc_equal ≝
    642646  λprogram:list labelled_instruction.λp1,p2:ppc_pc_map.
    643647  (∀n:ℕ.n ≤ |program| →
    644     bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 =
    645     bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉).
     648    \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) =
     649    \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)).
     650
     651definition policy_jump_equal ≝
     652  λprogram:list labelled_instruction.λp1,p2:ppc_pc_map.
     653  (∀n:ℕ.n < |program| →
     654    \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) =
     655    \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)).
    646656   
    647657definition nec_plus_ultra ≝

  • src/ASM/PolicyStep.ma

    r2038 r2059  
    11include "ASM/PolicyFront.ma".
    2 
    32include alias "basics/lists/list.ma".
    43include alias "arithmetics/nat.ma".
    … …  
    1211    address_of_word_labels_code_mem program l).
    1312  ∀old_policy:(Σpolicy:ppc_pc_map.
    14     And (And (And (out_of_program_none program policy)
     13    And (And (And (And (out_of_program_none program policy)
    1514    (jump_not_in_policy program policy))
    1615    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
     16    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd policy) 〈0,short_jump〉)))
    1717    (\fst policy < 2^16)).
    1818  (Σx:bool × (option ppc_pc_map).
    … …  
    2020    match y with
    2121    [ None ⇒ nec_plus_ultra program old_policy
    22     | Some p ⇒ And (And (And (And (And (And (And (out_of_program_none program p)
     22    | Some p ⇒ And (And (And (And (And (And (And (And (out_of_program_none program p)
    2323       (jump_not_in_policy program p))
    2424       (policy_increase program old_policy p))
    25        (policy_compact program labels p))
     25       (no_ch = true → policy_compact program labels 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〉)))
    28        (no_ch = true → policy_equal program old_policy p))
     28       (no_ch = true → policy_pc_equal program old_policy p))
     29       (policy_jump_equal program old_policy p → no_ch = true))
    2930       (\fst p < 2^16)
    3031    ])
    … …  
    3536    (λprefix.Σx:ℕ × ppc_pc_map.
    3637      let 〈added,policy〉 ≝ x in
    37       And (And (And (And (And (And (And (out_of_program_none prefix policy)
     38      And (And (And (And (And (And (And (And (out_of_program_none prefix policy)
    3839      (jump_not_in_policy prefix policy))
    3940      (policy_increase prefix old_sigma policy))
    4041      (policy_compact_unsafe prefix labels policy))
    41       (policy_safe prefix labels policy))
     42      (policy_safe prefix labels added old_sigma policy))
    4243      (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
    4344      (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
    44       (added = 0 → policy_equal prefix old_sigma policy))
     45      (added = 0 → policy_pc_equal prefix old_sigma policy))
     46      (policy_jump_equal prefix old_sigma policy → added = 0))
    4547    program
    4648    (λprefix.λx.λtl.λprf.λacc.
    … …  
    7476      | Some x ⇒ plus inc_added (minus isize old_size)
    7577      ] in
     78      let old_Slength ≝
     79        \snd (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
    7680      let updated_sigma ≝
    7781        (* we add the new PC to the next position and the new jump length to this one *)
    78         bvt_insert … (bitvector_of_nat ? (S (|prefix|))) 〈inc_pc + isize, short_jump〉
     82        bvt_insert … (bitvector_of_nat ? (S (|prefix|))) 〈inc_pc + isize, old_Slength〉
    7983        (bvt_insert … (bitvector_of_nat ? (|prefix|)) 〈inc_pc, new_length〉 inc_sigma) in
    8084      〈new_added, 〈plus inc_pc isize, updated_sigma〉〉
    81     ) 〈0, 〈0, bvt_insert … (bitvector_of_nat 16 0) 〈0, short_jump〉 (Stub ??)〉〉) in
     85    ) 〈0, 〈0,
     86      bvt_insert …
     87        (bitvector_of_nat ? 0)
     88        〈0, \snd (bvt_lookup … (bitvector_of_nat ? 0) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)〉
     89        (Stub ??)〉〉
     90    ) in
    8291    if geb (\fst final_policy) 2^16 then
    8392      〈eqb final_added 0, None ?〉
    8493    else
    8594      〈eqb final_added 0, Some ? final_policy〉.
    86 [ normalize nodelta cases daemon (* XXX nec_plus_ultra *)
     95[ normalize nodelta @nmk #Habs lapply p generalize in match (foldl_strong ?????); *
     96  #x #H #Heq >Heq in H; normalize nodelta -Heq -x #Hind
     97  (* USE: inc_pc = fst of policy (from fold) *)
     98  >(proj2 ?? (proj1 ?? (proj1 ?? Hind))) in p1;
     99  (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *)
     100  lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (pi2 ?? old_sigma)))
     101  #Hsig #Hge
     102  (* USE: added = 0 → policy_pc_equal (from fold) *)
     103  lapply ((proj2 ?? (proj1 ?? Hind)) ? (|program|) (le_n (|program|)))
     104  [ @(proj2 ?? Hind) #i #Hi
     105    cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
     106    [ #Hj
     107      (* USE: policy_increase (from fold) *)
     108      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi))
     109      lapply (Habs i Hi Hj)
     110      cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉)
     111      #opc #oj
     112      cases (bvt_lookup … (bitvector_of_nat ? i) (\snd final_policy) 〈0,short_jump〉)
     113      #pc #j normalize nodelta #Heq >Heq cases j
     114      [1,2: #abs cases abs #abs2 try (cases abs2) @refl
     115      |3: #_ @refl
     116      ]
     117    | #Hnj
     118      (* USE: jump_not_in_policy (from fold and old_sigma) *)
     119      >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))))) i Hi Hnj)
     120      >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi Hnj)
     121      @refl
     122    ]
     123  | #abs >abs in Hsig; #Hsig
     124    @(absurd ? Hsig) @le_to_not_lt @leb_true_to_le <geb_to_leb @Hge
     125  ]
    87126| normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2
    88127  >H2 in H; normalize nodelta -H2 -x #H @conj
    89   [ @conj
    90     [ @conj
    91       [ @conj
    92         [ @conj
    93           [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    94           | (* policy_compact_unsafe → policy_compact (in the end) *)
    95             #i #Hi
    96             lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) i Hi)
    97             lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))) i Hi)
    98             lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd final_policy)))
    99             cases (lookup_opt … (bitvector_of_nat ? i) (\snd final_policy)) in ⊢ (???% → %);
    100             [ / by /
    101             | #x cases x -x #x1 #x2 #EQ
    102               cases (lookup_opt … (bitvector_of_nat ? (S i)) (\snd final_policy))
    103               [ / by /
    104               | #y cases y -y #y1 #y2 normalize nodelta #H #H2
    105                 cut (
    106                   instruction_size_jmplen x2
    107                   (\snd (nth i ? (pi1 ?? program) 〈None ?, Comment []〉)) =
    108                   instruction_size … (bitvector_of_nat ? i)
    109                   (\snd (nth i ? (pi1 ?? program) 〈None ?, Comment []〉))
    110                  )
    111                 [5: #H3 <H3 @H2
    112                 |4: whd in match (instruction_size_jmplen ??);
    113                     whd in match (instruction_size …);
    114                     whd in match (assembly_1_pseudoinstruction …);
    115                     whd in match (expand_pseudo_instruction …);
    116                     normalize nodelta whd in match (append …) in H;
    117                     cases (nth i ? (pi1 ?? program) 〈None ?,Comment []〉) in H;
    118                     #lbl #instr cases instr
    119                     [2,3,6: #x [3: #y] normalize nodelta #H @refl
    120                     |4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    121                       #Hj lapply (Hj x (refl ? x)) -Hj
    122                       normalize nodelta >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O
    123                       cases x2 normalize nodelta
    124                       [1,4:
    125                         whd in match short_jump_cond; normalize nodelta
    126                         cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    127                         #result #flags normalize nodelta
    128                         cases (vsplit bool 8 8 result)
    129                         #upper #lower normalize nodelta
    130                         cases (eq_bv 8 upper (zero 8))
    131                         [2,4: #H lapply (proj1 ?? H) #H3 destruct (H3)
    132                         |1: #_ normalize @refl
    133                         |3: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/
    134                         ]
    135                       |2,5: whd in match short_jump_cond; whd in match medium_jump_cond;
    136                         normalize nodelta
    137                         cases (vsplit bool 5 11 ?) #addr1 #addr2
    138                         cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
    139                         cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    140                         #result #flags normalize nodelta
    141                         cases (vsplit bool 8 8 result)
    142                         #upper #lower normalize nodelta
    143                         #H >(not_true_is_false ? (proj2 ?? (proj1 ?? H)))
    144                         >(proj1 ?? (proj1 ?? H)) normalize @refl
    145                       |3,6: whd in match short_jump_cond; whd in match medium_jump_cond;
    146                         normalize nodelta
    147                         cases (vsplit bool 5 11 ?) #addr1 #addr2
    148                         cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
    149                         cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    150                         #result #flags normalize nodelta
    151                         cases (vsplit bool 8 8 result)
    152                         #upper #lower normalize nodelta
    153                         #H >(not_true_is_false ? (proj1 ?? H)) >(not_true_is_false ? (proj2 ?? H))
    154                         normalize nodelta normalize @refl
    155                       ]
    156                     |1: #pi cases pi
    157                       [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:
    158                         [1,2,3,6,7,24,25: #x #y
    159                         |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    160                         normalize nodelta #H @refl
    161                       |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta
    162                         >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj
    163                         [1,2,3,4,5: lapply (Hj y (refl ? y)) | 6,7,8,9: lapply (Hj x (refl ? x))] -Hj
    164                         whd in match expand_relative_jump; normalize nodelta
    165                         whd in match expand_relative_jump_internal; normalize nodelta
    166                         whd in match expand_relative_jump_unsafe; normalize nodelta
    167                         whd in match expand_relative_jump_internal_unsafe;
    168                         normalize nodelta >(add_bitvector_of_nat_plus ? i 1)
    169                         <(plus_n_Sm i 0) <plus_n_O cases x2 normalize nodelta
    170                         [1,4,7,10,13,16,19,22,25:
    171                           whd in match short_jump_cond; normalize nodelta
    172                           cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    173                           #result #flags normalize nodelta
    174                           cases (vsplit bool 8 8 result)
    175                           #upper #lower normalize nodelta
    176                           cases (eq_bv 8 upper (zero 8))
    177                           [2,4,6,8,10,12,14,16,18: #H lapply (proj1 ?? H) #H3 destruct (H3)
    178                           |1,3,5,7,9,11,13,15,17: #_ normalize nodelta
    179                             [6,7,8,9: normalize @refl]
    180                             whd in match (map ????);
    181                             whd in match (map ??? []);
    182                             whd in match (map ????);
    183                             whd in match (map ??? []);
    184                             normalize cases x
    185                             [1,2,3,6: #am cases am normalize nodelta
    186                               [1,2,3,4,8,9,16,17,18,19: #z #Ham cases Ham
    187                               |5,6,7,10,11,12,13,14: #Ham cases Ham
    188                               |15: #z #Ham normalize @refl
    189                               |20,21,22,23,27,28,35,36,37,38: #z #Ham cases Ham
    190                               |24,25,26,29,30,31,32,33: #Ham cases Ham
    191                               |34: #z #Ham normalize @refl
    192                               |39,40,41,42,46,47,54,55,56,57: #z #Ham cases Ham
    193                               |43,44,45,48,49,50,51,52: #Ham cases Ham
    194                               |53: #z #Ham normalize @refl
    195                               |59,60,65,66,72,73,74,75,76: #z #Ham cases Ham
    196                               |62,63,64,67,68,69,70,71: #Ham cases Ham
    197                               |58,61: #z #Ham normalize @refl
    198                               ]
    199                             ]
    200                             #w cases w #w1 #w2 cases w2 #am cases am normalize nodelta
    201                             [1,2,3,4,8,9,15,16,17,18,19: #z #Ham @refl
    202                             |5,6,7,10,11,12,13,14: #Ham @refl
    203                             |20,21,22,23,28: #z #Ham cases Ham
    204                             |24,25,26: #Ham cases Ham
    205                             |27: #z #Ham cases w1 #am cases am normalize nodelta
    206                                [1,2,3,4,8,9,15,16,17,18,19: #z #Ham @refl
    207                                |5,6,7,10,11,12,13,14: #Ham @refl
    208                                ]
    209                             |34,35,36,37,38: #z #Ham cases Ham
    210                             |29,30,31,32,33: #Ham cases Ham
    211                             ]
    212                           ]
    213                         |2,5,8,11,14,17,20,23,26:
    214                           whd in match short_jump_cond; whd in match medium_jump_cond;
    215                           normalize nodelta
    216                           cases (vsplit bool 5 11 ?) #addr1 #addr2
    217                           cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
    218                           cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    219                           #result #flags normalize nodelta
    220                           cases (vsplit bool 8 8 result)
    221                           #upper #lower normalize nodelta
    222                           #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/
    223                         |3,6,9,12,15,18,21,24,27:
    224                           whd in match short_jump_cond; whd in match medium_jump_cond;
    225                           normalize nodelta
    226                           cases (vsplit bool 5 11 ?) #addr1 #addr2
    227                           cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
    228                           cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    229                           #result #flags normalize nodelta
    230                           cases (vsplit bool 8 8 result)
    231                           #upper #lower normalize nodelta
    232                           #H >(not_true_is_false ? (proj1 ?? H)) >(not_true_is_false ? (proj2 ?? H))
    233                           [6,7,8,9: normalize @refl]
    234                           cases x normalize nodelta
    235                           [1,2,3,6: #am cases am normalize nodelta
    236                             [1,2,3,4,8,9,16,17,18,19: #z #Ham cases Ham
    237                             |5,6,7,10,11,12,13,14: #Ham cases Ham
    238                             |15: #z #Ham @refl
    239                             |20,21,22,23,27,28,35,36,37,38: #z #Ham cases Ham
    240                             |24,25,26,29,30,31,32,33: #Ham cases Ham
    241                             |34: #z #Ham @refl
    242                             |39,40,41,42,46,47,54,55,56,57: #z #Ham cases Ham
    243                             |43,44,45,48,49,50,51,52: #Ham cases Ham
    244                             |53: #z #Ham @refl
    245                             |59,60,65,66,72,73,74,75,76: #z #Ham cases Ham
    246                             |62,63,64,67,68,69,70,71: #Ham cases Ham
    247                             |58,61: #z #Ham @refl
    248                             ]
    249                           ]
    250                           #w cases w normalize nodelta #w1 #w2 cases w2 normalize nodelta
    251                           #am cases am normalize nodelta
    252                           [2,3,4,9,15,16,17,18,19: #z #Ham cases Ham
    253                           |5,6,7,10,11,12,13,14: #Ham cases Ham
    254                           |1,8: #z #Ham @refl
    255                           |20,21,22,23,28: #z #Ham cases Ham
    256                           |24,25,26: #Ham cases Ham
    257                           |27: #z #Ham cases w1 normalize nodelta #am cases am normalize nodelta
    258                             [1,3,8,9,15,16,17,18,19: #z #Ham cases Ham
    259                             |5,6,7,10,11,12,13,14: #Ham cases Ham
    260                             |2,4: #z #Ham @refl
    261                             ]
    262                           |34,35,36,37,38: #z #Ham cases Ham
    263                           |29,30,31,32,33: #Ham cases Ham
    264                           ]
    265                         ]
    266                       ]
    267                     ]
    268                   ]
     128  [ @conj [ @conj [ @conj [ @conj [ @conj
     129  [ (* USE[pass]: out_of_program_none, jump_not_in_policy, policy_increase (from fold) *)
     130    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))
     131  | (* policy_compact_unsafe → policy_compact (in the end) *)
     132    #Hch #i #Hi
     133    (* USE: policy_compact_unsafe (from fold) *)
     134    lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) i Hi)
     135    (* USE: policy_safe (from fold) *)
     136    lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) i Hi)
     137    lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd final_policy)))
     138    cases (lookup_opt … (bitvector_of_nat ? i) (\snd final_policy)) in ⊢ (???% → %);
     139    [ / by /
     140    | #x cases x -x #x1 #x2 #EQ
     141      cases (lookup_opt … (bitvector_of_nat ? (S i)) (\snd final_policy))
     142      [ / by /
     143      | #y cases y -y #y1 #y2 normalize nodelta #H #H2
     144        cut (instruction_size_jmplen x2
     145         (\snd (nth i ? (pi1 ?? program) 〈None ?, Comment []〉)) =
     146         instruction_size … (bitvector_of_nat ? i)
     147         (\snd (nth i ? (pi1 ?? program) 〈None ?, Comment []〉)))
     148        [5: #H3 <H3 @H2
     149        |4: whd in match (instruction_size_jmplen ??);
     150            whd in match (instruction_size …);
     151            whd in match (assembly_1_pseudoinstruction …);
     152            whd in match (expand_pseudo_instruction …);
     153            normalize nodelta whd in match (append …) in H;
     154            cases (nth i ? (pi1 ?? program) 〈None ?,Comment []〉) in H;
     155            #lbl #instr cases instr
     156            [2,3,6: #x [3: #y] normalize nodelta #H @refl
     157            |4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj
     158              lapply (Hj x (refl ? x)) -Hj normalize nodelta
     159              >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O
     160              cases x2 normalize nodelta
     161              [1,4: whd in match short_jump_cond; normalize nodelta
     162                lapply (refl ? (leb i (lookup_def ?? labels x 0)))
     163                cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab
     164                normalize nodelta
     165                (* USE: added = 0 → policy_pc_equal *)
     166                >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?)
     167                [2,4,6,8: cases daemon (* XXX *) ]
     168                [1,5: >(eqb_true_to_eq … Hch) <plus_n_O]
     169                cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
     170                #result #flags normalize nodelta
     171                cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
     172                cases (get_index' bool 2 0 flags) normalize nodelta
     173                [1,3,5,7: cases (eq_bv 9 upper ?)
     174                |2,4,6,8: cases (eq_bv 9 upper (zero 9))]
     175                [2,4,6,8,10,12,14,16: #H lapply (proj1 ?? H) #H3 destruct (H3)
     176                |5,7,13,15: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/
     177                |1,3,9,11: #_ normalize nodelta @refl
    269178                ]
    270               ]
    271             ]
    272             | @(proj2 ?? (proj1 ?? (proj1 ?? H)))
    273           ]
    274         | @(proj2 ?? (proj1 ?? H))
    275         ]
    276       | #H2 @(proj2 ?? H) @eqb_true_to_eq @H2
    277       ]
    278     | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1
    279     ]
     179             |2,5: whd in match short_jump_cond; whd in match medium_jump_cond;
     180                lapply (refl ? (leb i (lookup_def ?? labels x 0)))
     181                cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab
     182                normalize nodelta
     183                (* USE: added = 0 → policy_pc_equal *)
     184                >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?)
     185                [2,4,6,8: cases daemon (* XXX *)]
     186                [1,3: >(eqb_true_to_eq … Hch) <plus_n_O]
     187                normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2
     188                cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
     189                cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
     190                #result #flags normalize nodelta
     191                cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
     192                cases (get_index' bool 2 0 flags) normalize nodelta
     193                #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl
     194             |3,6: whd in match short_jump_cond; whd in match medium_jump_cond;
     195                lapply (refl ? (leb i (lookup_def ?? labels x 0)))
     196                cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab
     197                normalize nodelta
     198                >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?)
     199                [2,4,6,8: cases daemon (* XXX *)]
     200                [1,3: >(eqb_true_to_eq … Hch) <plus_n_O]
     201                normalize nodelta
     202                cases (vsplit bool 5 11 ?) #addr1 #addr2
     203                cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
     204                cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
     205                #result #flags normalize nodelta
     206                cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
     207                cases (get_index' bool 2 0 flags) normalize nodelta
     208                #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl
     209             ]
     210           |1: #pi cases pi
     211             [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:
     212               [1,2,3,6,7,24,25: #x #y
     213               |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     214               normalize nodelta #H @refl
     215             |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x]
     216               normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     217               #Hj lapply (Hj x (refl ? x)) -Hj
     218               whd in match expand_relative_jump; normalize nodelta
     219               whd in match expand_relative_jump_internal; normalize nodelta
     220               whd in match expand_relative_jump_unsafe; normalize nodelta
     221               whd in match expand_relative_jump_internal_unsafe;
     222               normalize nodelta >(add_bitvector_of_nat_plus ? i 1)
     223               <(plus_n_Sm i 0) <plus_n_O
     224               cases daemon (* XXX *)
     225             ]
     226           ]
     227         ]
     228       ]
     229     ]
     230   ]
     231   | (* USE: 0 ↦ 0 (from fold) *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     232   ]
     233   | (* USE: inc_pc = fst of policy (from fold) *) @(proj2 ?? (proj1 ?? (proj1 ?? H)))
     234   ]
     235   | #H2 (* USE: added = 0 → policy_pc_equal (from fold) *)
     236     @(proj2 ?? (proj1 ?? H)) @eqb_true_to_eq @H2
     237   ]
     238   | #H2 (* USE: policy_jump_equal → added = 0 (from fold *)
     239     @eq_to_eqb_true @(proj2 ?? H) @H2
     240   ]
     241   | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1
     242   ]
    280243|4: lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma
    281244  lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉))
    … …  
    283246  #old_pc #old_length #Holdeq #Hpolicy @pair_elim #added #policy normalize nodelta
    284247  @pair_elim #new_length #isize normalize nodelta #Heq1 #Heq2
    285   @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
     248  @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
    286249  [ (* out_of_program_none *) #i #Hi2 >append_length <commutative_plus @conj
    287250    [ (* → *) #Hi normalize in Hi;
    … …  
    289252      #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss
    290253      [1,3,5,7,9,11: >lookup_opt_insert_miss
    291         [1,3,5,7,9,11: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i Hi2))
     254        [1,3,5,7,9,11: (* USE: out_of_program_none → *)
     255          @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi2))
    292256          @le_S_to_le @Hi
    293257        |2,4,6,8,10,12: @bitvector_of_nat_abs
    … …  
    307271      [ #Hi
    308272        lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
    309         #Hl2
    310         lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i Hi2) Hl2)
     273        #Hl2 (* USE: out_of_program_none ← *)
     274        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi2) Hl2)
    311275        #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3
    312276      | #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi))
    … …  
    325289      [ >lookup_insert_miss
    326290        [ >(nth_append_first ? i prefix ?? Hi)
    327           @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i Hi)
     291          (* USE: jump_not_in_policy *)
     292          @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi)
    328293        | @bitvector_of_nat_abs
    329294          [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm
    … …  
    368333  ]
    369334  | (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi;
    370     cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi; #Hi
    371     [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i Hi)
    372       <(proj2 ?? (pair_destruct ?????? Heq2))     
    373       @pair_elim #opc #oj #EQ1 >lookup_insert_miss
    374       [ >lookup_insert_miss
    375         [ @pair_elim #pc #j #EQ2 / by /
     335    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
     336    [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     337      [ (* USE: policy_increase *)
     338        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i (le_S_to_le … Hi))
     339        <(proj2 ?? (pair_destruct ?????? Heq2))
     340        @pair_elim #opc #oj #EQ1 >lookup_insert_miss
     341        [ >lookup_insert_miss
     342          [ @pair_elim #pc #j #EQ2 / by /
     343          | @bitvector_of_nat_abs
     344            [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S
     345              >commutative_plus @le_plus_a @Hi
     346            | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
     347            | @lt_to_not_eq @Hi
     348            ]
     349          ]
    376350        | @bitvector_of_nat_abs
    377           [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S <commutative_plus
     351          [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S >commutative_plus
    378352            @le_plus_a @Hi
    379           | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
    380           | @lt_to_not_eq @Hi
    381           ]
    382         ]
    383       | @bitvector_of_nat_abs
    384         [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S >commutative_plus
    385           @le_plus_a @Hi
    386         | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm @le_plus_n_r
    387         | @lt_to_not_eq @le_S @Hi
    388         ]
    389       ]
    390     | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    391       [ >lookup_insert_hit
    392         cases (dec_is_jump instr)
    393         [ cases instr in Heq1; normalize nodelta
    394           [ #pi cases pi
    395             [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:
    396               [1,2,3,6,7,24,25: #x #y
    397               |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj
    398             |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    399               whd in match jump_expansion_step_instruction; normalize nodelta #Heq1
    400               <(proj1 ?? (pair_destruct ?????? Heq1)) #_ >Holdeq normalize nodelta
    401               @jmpleq_max_length
     353          | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm @le_plus_n_r
     354          | @lt_to_not_eq @le_S @Hi
     355          ]
     356        ]
     357      | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) @pair_elim #opc #oj #EQ1
     358        >lookup_insert_miss
     359        [ >lookup_insert_hit cases (dec_is_jump instr)
     360          [ cases instr in Heq1; normalize nodelta
     361            [ #pi cases pi
     362              [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:
     363                [1,2,3,6,7,24,25: #x #y
     364                |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj
     365              |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
     366                whd in match jump_expansion_step_instruction; normalize nodelta #Heq1
     367                #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq in EQ1; normalize nodelta
     368                #H42 >(proj2 ?? (pair_destruct ?????? H42)) @jmpleq_max_length
     369              ]
     370            |2,3,6: #x [3: #y] #_ #Hj cases Hj
     371            |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq in EQ1;
     372              normalize nodelta #H42 >(proj2 ?? (pair_destruct ?????? H42)) @jmpleq_max_length
    402373            ]
    403           |2,3,6: #x [3: #y] #_ #Hj cases Hj
    404           |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq normalize nodelta
    405             @jmpleq_max_length
    406           ]
    407         | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta
    408           [ #pi cases pi
    409             [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:
    410               [1,2,3,6,7,24,25: #x #y
    411               |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    412               whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1
    413               #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
    414               lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
    415               [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:
    416                 >prf >nth_append_second
    417                 [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:
    418                   <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
    419                 |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:
    420                   @le_n
     374          | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta
     375            [ #pi cases pi
     376              [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:
     377                [1,2,3,6,7,24,25: #x #y
     378                |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     379                whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1
     380                #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
     381                (* USE: jump_not_in_policy (from old_sigma) *)
     382                lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
     383                [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:
     384                  >prf >nth_append_second
     385                  [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:
     386                    <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
     387                  |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:
     388                    @le_n
     389                  ]
     390                |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:
     391                  >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     392                |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:
     393                  cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in EQ1;
     394                  #a #b #EQ1 >(proj2 ?? (pair_destruct ?????? EQ1)) #EQ2 >EQ2
     395                  %2 @refl
    421396                ]
    422               |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:
    423                 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    424               |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:
    425                 cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
    426                 #a #b #H >H normalize nodelta %2 @refl
     397              |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
     398                #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
    427399              ]
    428             |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    429               #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
     400            |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
     401              (* USE: jump_not_in_policy (from old_sigma) *)
     402              lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
     403              [1,4,7: >prf >nth_append_second
     404                [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
     405                |2,4,6: @le_n
     406                ]
     407              |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     408              |3,6,9:
     409                cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in EQ1;
     410                #a #b #EQ1 >(proj2 ?? (pair_destruct ?????? EQ1)) #EQ2 >EQ2 %2 @refl
     411              ]
     412            |4,5: #x #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
    430413            ]
    431           |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
    432             lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
    433             [1,4,7: >prf >nth_append_second
    434               [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
    435               |2,4,6: @le_n
    436               ]
    437             |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    438             |3,6,9: cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
    439               #a #b #H >H normalize nodelta %2 @refl
    440             ]
    441           |4,5: #x #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
    442           ]
    443         ]
    444       | @bitvector_of_nat_abs
    445         [ @(transitive_lt … (pi2 … program)) >prf @le_S_S >append_length @le_plus_n_r
    446         | @(transitive_lt … (pi2 … program)) @le_S_S >prf >append_length <plus_n_Sm
    447           @le_S_S @le_plus_n_r
    448         | @lt_to_not_eq @le_n
    449         ]
    450       ]
     414          ]
     415        | @bitvector_of_nat_abs
     416          [ @(transitive_lt … (pi2 … program)) >prf @le_S_S >append_length @le_plus_n_r
     417          | @(transitive_lt … (pi2 … program)) @le_S_S >prf >append_length <plus_n_Sm
     418            @le_S_S @le_plus_n_r
     419          | @lt_to_not_eq @le_n
     420          ]
     421        ]
     422      ]
     423    | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
     424      normalize nodelta
     425      cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉)
     426      #a #b normalize nodelta %2 @refl
    451427    ]
    452428  ]
    … …  
    459435          [ cases (le_to_or_lt_eq … Hi) -Hi #Hi
    460436            [ >lookup_opt_insert_miss
    461               [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?)
     437              [ (* USE: policy_compact_unsafe *)
     438                lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)
    462439                [ @le_S_to_le @Hi ]
    463440                cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
    … …  
    477454              ]
    478455            | >Hi >lookup_opt_insert_hit normalize nodelta
    479               lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?)
     456              (* USE: policy_compact_unsafe *)
     457              lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)
    480458              [ <Hi @le_n
    481459              | cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
    482460                [ normalize nodelta / by /
    483461                | #x cases x -x #x1 #x2
    484                   lapply (proj2 ?? (proj1 ?? Hpolicy)) <Hi
     462                  (* USE: inc_pc = fst inc_sigma *)
     463                  lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) <Hi
    485464                  lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))
    486465                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %);
    … …  
    522501      ]
    523502      >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta
    524       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i ?))
     503      (* USE: out_of_program_none ← *)
     504      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i ?))
    525505      [ >Hi @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
    526506      | >Hi
    527         lapply (proj2 ?? (proj1 ?? Hpolicy))
     507        (* USE: inc_pc = fst policy *)
     508        lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
    528509        lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma))
    529510        cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma) in ⊢ (???% → %);
    … …  
    556537    ]
    557538  ]
    558   | (* policy_safe *) cases daemon (*#i >append_length >commutative_plus #Hi normalize in Hi;
     539  | (* policy_safe *) cases daemon
     540    (* #i >append_length >commutative_plus #Hi normalize in Hi;
    559541    elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    560542    [ >nth_append_first
    561543      [2: @Hi]
    562       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi)
    563544      <(proj2 ?? (pair_destruct ?????? Heq2))
    564545      >lookup_insert_miss
    565       [
     546      [ >lookup_insert_miss
     547        [ >lookup_insert_miss
     548          [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi)
     549            cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
     550            #pc #j cases (nth i ? prefix 〈None ?, Comment []〉) #label #instr cases j
     551            normalize nodelta
     552            [ #H cases (le_to_or_lt_eq … Hi) -Hi #Hi
     553              [ >lookup_insert_miss
     554                [ #dest #Hjmp <(proj1 ?? (pair_destruct ?????? Heq2))
     555
    566556      |
    567557      ]
    … …  
    572562    [ cases (decidable_eq_nat 0 (|prefix|))
    573563      [ #Heq <Heq >lookup_insert_hit
    574         lapply (proj2 ?? (proj1 ?? Hpolicy))
    575         lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) <Heq
     564        (* USE: inc_pc = fst policy *)
     565        lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
     566        (* USE: 0 ↦ 0 *)
     567        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) <Heq
    576568        #ONE #TWO >TWO >ONE @refl
    577569      | #Hneq >lookup_insert_miss
    578         [ @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
     570        [ (* USE: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
    579571        | @bitvector_of_nat_abs
    580572          [3: @Hneq]
    … …  
    593585    >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
    594586  ]
    595   | (* added = 0 → policy_equal *) lapply (proj2 ?? Hpolicy)
     587  | (* added = 0 → policy_pc_equal *)
     588    (* USE: added = 0 → policy_pc_equal *)
     589    lapply (proj2 ?? (proj1 ?? Hpolicy))
    596590    lapply Heq2 -Heq2 lapply Heq1 -Heq1 lapply (refl ? instr)
    597     cases instr in ⊢ (???% → % → % → %); normalize nodelta
     591    cases daemon
     592    (*cases instr in ⊢ (???% → % → % → %); normalize nodelta
    598593    [ #pi cases pi normalize nodelta
    599594      [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:
    … …  
    609604            (bitvector_of_nat 16 i))
    610605          [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:
     606            (* le_to_or_lt_eq, part 2 *)
    611607            >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc,new_length〉 16
    612608              (bitvector_of_nat 16 (|prefix|)) (bitvector_of_nat 16 i))
    … …  
    617613              [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:
    618614                @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
    619                 @le_S_S @le_plus_a @le_S_to_le @(le_S_S_to_le … Hi)
     615                @le_S_S @le_plus_a @(le_S_S_to_le … Hi)
    620616              |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:
    621617                @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S
    622618                @le_plus_n_r
    623619              |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:
    624                 @lt_to_not_eq @(le_S_S_to_le … Hi)
     620                @lt_to_not_eq  @(le_S_to_le … Hi)
    625621              ]
    626622            ]
    … …  
    807803         ]
    808804       ]
    809      ]
     805     ]*)
    810806   ]
    811 | normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
     807 | (* policy_jump_equal → added = 0 *)
     808   cases daemon
     809 ]
     810| normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
    812811  [ #i cases i
    813812    [ #Hi2 @conj
    … …  
    832831    ]
    833832  ]
     833  | #i #Hi <(le_n_O_to_eq … Hi)
     834    >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉)
     835    #a #b normalize nodelta %2 @refl
     836  ]
    834837  | #i cases i
    835838    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    … …  
    842845    ]
    843846  ]
    844   | #i cases i
    845     [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    846     | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    847     ]
    848   ]
    849847  | >lookup_insert_hit @refl
    850848  ]
    851849  | >lookup_insert_hit @refl
    852850  ]
    853   | #_ #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     851  | #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit
     852    (* USE: 0 ↦ 0 (from old_sigma *)
     853    @(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))
     854  ]
     855  | #_ @refl
    854856  ]
    855857]
Note: See TracChangeset for help on using the changeset viewer.