Changeset 2141


Ignore:
Timestamp:
Jun 28, 2012, 8:08:58 PM (5 years ago)
Author:
boender
Message:
  • committed working version
Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2101 r2141  
    55include alias "basics/logic.ma".
    66
    7 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (S (|l|)) 2^16) (n: ℕ)
     7let rec jump_expansion_internal (program: Σl:list labelled_instruction.
     8  lt (S (|l|)) 2^16 ∧ is_well_labelled_p l) (n: ℕ)
    89  on n:(Σx:bool × (option ppc_pc_map).
    910    let 〈no_ch,pol〉 ≝ x in
     
    3435  [ #H / by I/
    3536  | #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj
    36     [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))
     37    [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    3738    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    3839    ]
     
    5253    | #j2 #H2 @conj [ @conj [ @conj [ @conj
    5354      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))))
    54       | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))
    55       ]
    56       | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
     55      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))))
     56      ]
     57      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))
    5758      ]     
    5859      | @(proj2 ?? H2)
    5960      ]
    60       | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))
    61       ]
     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      ]
    6267    ]
    6368  ]
     
    6671  [ #_ >p2 #ABS destruct (ABS)
    6772  | #map >p2 normalize nodelta
    68     #H #eq destruct (eq) @(proj1 ?? H)
     73    #H #eq destruct (eq) cases daemon (* change order *)
    6974  ]
    7075]
     
    157162qed.
    158163
    159 lemma pe_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).
     164lemma pe_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
    160165  ∀n.policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program n)))
    161166   (\snd (pi1 ?? (jump_expansion_internal program (S n)))) →
     
    166171qed.
    167172
    168 (* this is in the stdlib, but commented out, why? *)
    169 theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.
    170   #n (elim n) normalize /2 by S_pred/ qed.
    171  
    172 lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).∀n:ℕ.
     173lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.
     174  S (|l|) < 2^16 ∧ is_well_labelled_p l).∀n:ℕ.
    173175  policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n)))
    174176   (\snd (pi1 … (jump_expansion_internal program (S n)))) →
     
    228230
    229231(* uses the second part of policy_increase *)
    230 lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.S (|l|) <2^16.
     232lemma measure_incr_or_equal: ∀program:(Σl:list labelled_instruction.
     233  S (|l|) <2^16 ∧ is_well_labelled_p l).
    231234  ∀policy:Σp:ppc_pc_map.
    232     out_of_program_none program p ∧
     235    (*out_of_program_none program p ∧*)
    233236    not_jump_default program p ∧
    234237    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
    235238    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
     239    sigma_compact_unsafe program (create_label_map program) p ∧
    236240    \fst p < 2^16.
    237241  ∀l.|l| ≤ |program| → ∀acc:ℕ.
     
    247251  [ / by I/
    248252  | #x normalize nodelta #Hx #Hjeq
    249     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))))) (|t|) (le_S_to_le … Hp))
     253    lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (|t|) (le_S_to_le … Hp))
    250254    whd in match (measure_int ???); whd in match (measure_int ? x ?);
    251255    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd (pi1 ?? policy)) 〈0,short_jump〉)
     
    266270qed.
    267271
    268 (* these lemmas seem superfluous, but not sure how *)
    269 lemma bla: ∀a,b:ℕ.a + a = b + b → a = b.
    270  #a elim a
    271  [ normalize #b //
    272  | -a #a #Hind #b cases b [ /2 by le_n_O_to_eq/ | -b #b normalize
    273    <plus_n_Sm <plus_n_Sm #H
    274    >(Hind b (injective_S ?? (injective_S ?? H))) // ]
    275  ]
    276 qed.
    277 
    278 lemma sth_not_s: ∀x.x ≠ S x.
    279  #x cases x
    280  [ // | #y // ]
    281 qed.
    282  
    283272lemma measure_full: ∀program.∀policy.
    284273  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
     
    314303
    315304(* uses second part of policy_increase *)
    316 lemma measure_special: ∀program:(Σl:list labelled_instruction.(S (|l|)) < 2^16).
     305lemma measure_special: ∀program:(Σl:list labelled_instruction.
     306    (S (|l|)) < 2^16 ∧ is_well_labelled_p l).
    317307  ∀policy:Σp:ppc_pc_map.
    318     out_of_program_none program p ∧ not_jump_default program p ∧
     308    not_jump_default program p ∧
    319309    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧
    320310    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
     311    sigma_compact_unsafe program (create_label_map program) p ∧
    321312    \fst p < 2^16.
    322313  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with
     
    336327     [ @(transitive_le … Hp) / by /
    337328     | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
    338        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) (|t|) (le_S_to_le … Hp))
     329       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) (le_S_to_le … Hp))
    339330       #Hinc cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm Hinc;
    340331       #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉);
     
    359350     ]
    360351   | >Hi whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
    361      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) (|t|) (le_S_to_le … Hp))
     352     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) (le_S_to_le … Hp))
    362353     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm;
    363354     #x1 #x2
     
    379370qed.
    380371
    381 lemma le_to_eq_plus: ∀n,z.
    382   n ≤ z → ∃k.z = n + k.
    383  #n #z elim z
    384  [ #H cases (le_to_or_lt_eq … H)
    385    [ #H2 @⊥ @(absurd … H2) @not_le_Sn_O
    386    | #H2 @(ex_intro … 0) >H2 //
    387    ]
    388  | #z' #Hind #H cases (le_to_or_lt_eq … H)
    389    [ #H' elim (Hind (le_S_S_to_le … H')) #k' #H2 @(ex_intro … (S k'))
    390      >H2 >plus_n_Sm //
    391    | #H' @(ex_intro … 0) >H' //
    392    ]
    393  ]
    394 qed.
    395 
    396 lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.S (|l|) < 2^16.
     372lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.
     373  S (|l|) < 2^16 ∧ is_well_labelled_p l.
    397374  match jump_expansion_start program (create_label_map program) with
    398375  [ None ⇒ True
     
    406383   [ / by refl/
    407384   | #h #t #Hind #Hp whd in match (measure_int ???);
    408      elim (proj2 ?? (proj1 ?? (proj1 ?? Hpl)) (|t|) (le_S_to_le … Hp))
     385     elim (proj2 ?? (proj1 ?? Hpl) (|t|) (le_S_to_le … Hp))
    409386     #pc #Hpc >(lookup_opt_lookup_hit … Hpc 〈0,short_jump〉) normalize nodelta @Hind
    410387     @(transitive_le … Hp) @le_n_Sn
     
    414391
    415392(* the actual computation of the fixpoint *)
    416 definition je_fixpoint: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).
     393definition je_fixpoint: ∀program:(Σl:list labelled_instruction.
     394  S (|l|) < 2^16 ∧ is_well_labelled_p l).
    417395  Σp:option ppc_pc_map.
    418396    match p with
     
    513491                  normalize nodelta #Hpe
    514492                  lapply (measure_incr_or_equal program Xp program (le_n (|program|)) 0)
    515                   [ @(proj1 ?? HXp)
     493                  [ cases daemon (* reorder *)
    516494                  | lapply (Hfa x Hx) >Xeq >Seq
    517495                    lapply (measure_special program «Xp,?»)
    518                     [ @(proj1 ?? HXp)
     496                    [ cases daemon (* reorder *)
    519497                    | lapply Seq whd in match (jump_expansion_internal program (S x)); (*340s*)
    520498                      >Xeq normalize nodelta cases Xno_ch in HXp Xeq; #HXp #Xeq
     
    556534        | -sto #stp normalize nodelta #Hstp @conj [ @conj
    557535          [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))))
    558           | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))
    559             @(proj2 ?? (proj1 ?? Hstp)) #i #Hi
    560             cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
    561             [ #Hj
    562               lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))) i (le_S_to_le … Hi))
    563               lapply (Hfull i Hi Hj)
    564               cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
    565               #fp #fj #Hfj >Hfj normalize nodelta
    566               cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉)
    567               #stp #stj cases stj normalize nodelta
    568               [1,2: #H cases H #H2 cases H2 destruct (H2)
    569               |3: #_ @refl
     536          | @(equal_compact_unsafe_compact ?? Fp)
     537            [ @(proj2 ?? (proj1 ?? (proj1 ?? Hstp))) @(proj2 ?? (proj1 ?? Hstp))
     538              #i #Hi
     539              cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
     540              [ #Hj
     541                lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))) i (le_S_to_le … Hi))
     542                lapply (Hfull i Hi Hj)
     543                cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
     544                #fp #fj #Hfj >Hfj normalize nodelta
     545                cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉)
     546                #stp #stj cases stj normalize nodelta
     547                [1,2: #H cases H #H2 cases H2 destruct (H2)
     548                |3: #_ @refl
     549                ]
     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
    570552              ]
    571             | #Hj >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))) i Hi Hj)
    572               >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) i Hi Hj) @refl
     553            | cases daemon 
     554            | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))
    573555            ]
    574556          ]
     
    597579include alias "arithmetics/nat.ma".
    598580include alias "basics/logic.ma".
    599 
    600 lemma nth_safe_nth:
    601   ∀A:Type[0].∀l:list A.∀i.∀proof:i < |l|.∀x.nth_safe A i l proof = nth i A l x.
    602 #A #l elim l
    603 [ #i #prf @⊥ @(absurd ? prf) @le_to_not_lt @le_O_n
    604 | -l #h #t #Hind #i elim i
    605   [ #prf #x normalize @refl
    606   | -i #i #Hind2 #prf #x whd in match (nth ????); whd in match (tail ??);
    607     whd in match (nth_safe ????); @Hind
    608   ]
    609 ]
    610 qed.
    611581
    612582(* The glue between Policy and Assembly. *)
     
    686656]
    687657qed.           
    688      
    689 
    690        
    691 
    692     >(add_bitvector_of_nat_plus ?? ppc)
    693      
    694 qed.
  • src/ASM/PolicyFront.ma

    r2102 r2141  
    253253 ∀dest.is_jump_to instr dest →
    254254   let paddr ≝ lookup_def … labels dest 0 in
    255    let addr ≝ bitvector_of_nat ? (if leb i paddr (* forward jump *)
    256    then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) + added
    257    else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)) in
     255   let addr ≝ bitvector_of_nat ? (if leb paddr (|prefix|) (* jump to address already known *)
     256   then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)
     257   else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
    258258   match j with
    259259   [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧
     
    265265       \fst (absolute_jump_cond pc_plus_jmp_length addr) = false
    266266   ].
    267 
    268267 
    269268(* Definitions and theorems for the jump_length type (itself defined in Assembly) *)
     
    324323  let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in
    325324  let paddr ≝ lookup_def … labels lbl 0 in
    326   let addr ≝ bitvector_of_nat ? (if leb ppc paddr (* forward jump *)
    327   then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added
    328   else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in
     325  let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *)
     326  then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)
     327  else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
    329328  let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in
    330329  if sj_possible
     
    339338  let paddr ≝ lookup_def ? ? labels lbl 0 in
    340339  let addr ≝ bitvector_of_nat ?
    341     (if leb ppc paddr (* forward jump *)
    342     then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)
    343             + added
    344     else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉)) in
     340    (if leb paddr ppc (* jump to address already known *)
     341    then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉)
     342    else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
    345343  let 〈aj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length addr in   
    346344  if aj_possible
     
    354352  let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in
    355353  let paddr ≝ lookup_def … labels lbl 0 in
    356   let addr ≝ bitvector_of_nat ? (if leb ppc paddr (* forward jump *)
    357   then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added
    358   else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in
     354  let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *)
     355  then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)
     356  else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
    359357  let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in
    360358  if sj_possible
     
    395393qed.
    396394
    397 lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a.
    398   #a #b / by refl/
    399 qed.
    400 
    401 lemma nth_last: ∀A,a,l.
    402   nth (|l|) A l a = a.
    403  #A #a #l elim l
    404  [ / by /
    405  | #h #t #Hind whd in match (nth ????); whd in match (tail ??); @Hind
    406  ]
    407 qed.
    408 
    409395(* The first step of the jump expansion: everything to short. *)
    410396definition jump_expansion_start:
    411   ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).
     397  ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
    412398  ∀labels:label_map.
    413399  Σpolicy:option ppc_pc_map.
    414400    match policy with
    415401    [ None ⇒ True
    416     | Some p ⇒ And (And (And (And (And (And (And
     402    | Some p ⇒ And (And (And (And (And (And
    417403       (out_of_program_none (pi1 ?? program) p)
    418404       (not_jump_default (pi1 ?? program) p))
    419        (sigma_compact_unsafe program labels p))
    420405       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
    421406       (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
     407       (sigma_compact_unsafe program labels p))
    422408       (∀i.i ≤ |program| → ∃pc.
    423409         bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉))
    424        (bvt_lookup_opt … (bitvector_of_nat ? (|program|)) (\snd p) = Some ? 〈\fst p,short_jump〉))
    425        (\fst p < 2^16)
     410       (\fst p < 2^16)         
    426411    ] ≝
    427412  λprogram.λlabels.
    428413  let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction)
    429   (λprefix.Σpolicy:ppc_pc_map.And (And (And (And (And (And
     414  (λprefix.Σpolicy:ppc_pc_map.And (And (And (And (And
    430415    (out_of_program_none prefix policy)
    431416    (not_jump_default prefix policy))
    432     (sigma_compact_unsafe prefix labels policy))
    433417    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
    434418    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
     419    (sigma_compact_unsafe prefix labels policy))
    435420    (∀i.i ≤ |prefix| → ∃pc.
    436421      bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉))
    437     (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd policy) =
    438       Some ? 〈\fst policy,short_jump〉))
    439422  program
    440423  (λprefix.λx.λtl.λprf.λp.
     
    451434| lapply p -p generalize in match (foldl_strong ?????); * #p #Hp #hg
    452435  @conj [ @Hp | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ]
    453 | @conj [ @conj [ @conj [ @conj [ @conj [ @conj
     436| @conj [ @conj [ @conj [ @conj [ @conj
    454437  [ (* out_of_program_none *)
    455438    #i #Hi2 >append_length <commutative_plus @conj
     
    457440      cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi
    458441      [ >lookup_opt_insert_miss
    459         [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi2))
     442        [ (* USE[pass]: out_of_program_none → *)
     443          @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2))
    460444          @le_S_to_le @le_S_to_le @Hi
    461445        | @bitvector_of_nat_abs
     
    467451      | >lookup_opt_insert_miss
    468452        [ <Hi
    469           @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) (S (S (|prefix|))) ?))
     453          (* USE[pass]: out_of_program_none → *)
     454          @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) (S (S (|prefix|))) ?))
    470455          [ >Hi @Hi2
    471456          | @le_S @le_n
     
    483468      | #Hi >lookup_opt_insert_miss
    484469        [ #Hl
    485           elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi2) Hl))
     470          (* USE[pass]: out_of_program_none ← *)
     471          elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2) Hl))
    486472          [ #Hi3 @Hi3
    487473          | #Hi3 @⊥ @(absurd ? Hi3) @sym_neq @Hi
     
    489475        | @bitvector_of_nat_abs
    490476          [ @Hi2
    491           | @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length
     477          | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length
    492478            <plus_n_Sm @le_S_S @le_plus_n_r
    493479          | @Hi
     
    500486    normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    501487    [ >lookup_insert_miss
    502       [ lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))))) i Hi)
     488      [ (* USE[pass]: not_jump_default *)
     489        lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi)
    503490        >nth_append_first
    504491        [ #H #H2 @H @H2
     
    506493        ]
    507494      | @bitvector_of_nat_abs
    508         [ @(transitive_lt … (pi2 ?? program)) >prf >append_length <commutative_plus >plus_n_Sm
    509           @le_plus_a @le_S @Hi
    510         | @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <plus_n_Sm @le_S_S
    511           @le_plus_n_r
     495        [ @(transitive_lt ??? Hi) @le_S_to_le]
     496        [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
     497          <plus_n_Sm @le_S_S @le_plus_n_r
    512498        | @lt_to_not_eq @le_S @Hi
    513499        ]
    514500      ]
    515501    | >Hi >lookup_insert_miss
    516       [ #_ elim (proj2 ?? (proj1 ?? Hp) (|prefix|) (le_n (|prefix|))) #pc #Hl
     502      [ #_ (* USE: everything is short *)
     503        elim ((proj2 ?? Hp) (|prefix|) (le_n (|prefix|))) #pc #Hl
    517504        >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) @refl
    518505      | @bitvector_of_nat_abs
    519         [ @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length @le_plus_n_r
    520         | @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm @le_S_S
     506        [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length @le_plus_n_r
     507        | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm @le_S_S
    521508          @le_plus_n_r
    522509        | @lt_to_not_eq @le_n
     
    524511      ]
    525512    ]
     513  ]
     514  | (* 0 ↦ 0 *)
     515    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
     516    >lookup_insert_miss
     517    [ (* USE[pass]: 0 ↦ 0 *)
     518      @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))
     519    | @bitvector_of_nat_abs
     520      [ / by /
     521      | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S <plus_n_Sm
     522        @le_S_S @le_plus_n_r
     523      | @lt_to_not_eq / by /
     524      ]
     525    ]
     526  ]
     527  | (* fst p = pc *)
     528    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
     529    >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
    526530  ]
    527531  | (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi;
     
    530534    [ >lookup_opt_insert_miss
    531535      [ >lookup_opt_insert_miss
    532         [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi)
     536        [ (* USE[pass]: policy_compact_unsafe *)
     537          lapply (proj2 ?? (proj1 ?? Hp) i Hi)
    533538          lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) sigma))
    534539          cases (bvt_lookup_opt … (bitvector_of_nat ? i) sigma) in ⊢ (???% → %);
     
    548553      [2: lapply (le_S_to_le … Hi) -Hi #Hi]
    549554      @bitvector_of_nat_abs
    550       [1,4: @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <commutative_plus
     555      [1,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <commutative_plus
    551556        @le_plus_a @Hi
    552       |2,5: @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm
     557      |2,5: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm
    553558        @le_S_S @le_plus_n_r
    554559      |3,6: @lt_to_not_eq @le_S_S @Hi
     
    556561    | >lookup_opt_insert_miss
    557562      [ >Hi >lookup_opt_insert_hit normalize nodelta
    558         >(proj2 ?? Hp) normalize nodelta >nth_append_second
    559         [ <minus_n_n whd in match (nth ????); @refl
     563        (* USE: everything is short, fst p = pc *)
     564        elim ((proj2 ?? Hp) (|prefix|) (le_n ?)) #pc #Hl
     565        lapply (proj2 ?? (proj1 ?? (proj1 ?? Hp))) >Hl
     566        >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #EQ normalize nodelta >nth_append_second
     567        [ <minus_n_n whd in match (nth ????); >EQ @refl
    560568        | @le_n
    561569        ]
    562570      | @bitvector_of_nat_abs
    563         [ @(transitive_lt … (pi2 ?? program)) >Hi >prf @le_S_S >append_length <commutative_plus
     571        [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >Hi >prf @le_S_S >append_length <commutative_plus
    564572          @le_plus_a @le_n
    565         | @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm
     573        | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm
    566574          @le_S_S @le_plus_n_r
    567575        | @lt_to_not_eq @le_S_S >Hi @le_n
     
    570578    ]
    571579  ]
    572   | (* 0 ↦ 0 *)
    573     cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
    574     >lookup_insert_miss
    575     [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))
    576     | @bitvector_of_nat_abs
    577       [ / by /
    578       | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
    579         @le_S_S @le_plus_n_r
    580       | @lt_to_not_eq / by /
    581       ]
    582     ]
    583   ]
    584   | (* fst p = pc *)
    585     cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
    586     >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
    587   ]
    588   | (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi;
     580  | (* everything is short *) #i >append_length <commutative_plus #Hi normalize in Hi;
    589581    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
    590582    cases (le_to_or_lt_eq … Hi) -Hi #Hi
    591583    [ >lookup_opt_insert_miss
    592       [ @(proj2 ?? (proj1 ?? Hp) i (le_S_S_to_le … Hi))
     584      [ (* USE[pass]: everything is short *)
     585        @((proj2 ?? Hp) i (le_S_S_to_le … Hi))
    593586      | @bitvector_of_nat_abs
    594         [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S >commutative_plus
    595           @le_plus_a @le_S_S_to_le @Hi
    596         | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
    597           @le_S_S @le_plus_n_r
     587        [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
     588          >commutative_plus @le_plus_a @le_S_S_to_le @Hi
     589        | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length <plus_n_Sm
     590          @le_S_S @le_S_S @le_plus_n_r
    598591        | @lt_to_not_eq @Hi
    599592        ]
     
    603596    ]
    604597  ]
    605   | (* lookup at the end *) cases p -p #p cases p -p #pc #sigma #Hp cases x
    606     #lbl #instr >append_length <plus_n_Sm <plus_n_O >lookup_opt_insert_hit
    607     / by refl/
    608   ]
    609 | @conj [ @conj [ @conj [ @conj [ @conj [ @conj
     598| @conj [ @conj [ @conj [ @conj [ @conj
    610599  [ #i cases i
    611600    [ #Hi2 @conj
     
    629618    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
    630619    ]
    631   ]
     620  ] ] ]
     621  >lookup_insert_hit @refl
    632622  | #i cases i
    633623    [ #Hi @⊥ @(absurd … Hi) @le_to_not_lt @le_n
    634624    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    635625    ]
    636   ]
    637   | >lookup_insert_hit @refl
    638   ]
    639   | >lookup_insert_hit @refl
    640626  ]
    641627  | #i cases i
     
    643629    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    644630    ]
    645   ]
    646   | >lookup_opt_insert_hit @refl
    647631  ]
    648632]
     
    676660include alias "basics/logic.ma".
    677661
    678 lemma blerpque: ∀a,b,i.
     662lemma jump_length_equal_max: ∀a,b,i.
    679663  is_jump i → instruction_size_jmplen (max_length a b) i = instruction_size_jmplen a i →
    680664  (max_length a b) = a.
     
    699683qed.
    700684
    701 lemma etblorp: ∀a,b,i.is_jump i →
     685lemma jump_length_le_max: ∀a,b,i.is_jump i →
    702686  instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i.
    703687 #a #b #i cases i
     
    706690 |1: #pi cases pi
    707691   [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:
    708      [1,2,3,6,7,24,25: #x #y
    709      |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    710      #H cases H
     692     try (#x #y #H) try (#x #H) try (#H) cases H
    711693   |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    712694     #_ cases a cases b
    713      [2,3: cases x #ad cases ad
    714        [15,34: #b #Hb / by le_n/
    715        |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb
    716      |1,4,5,6,7,8,9: / by le_n/
    717      |11,12: cases x #ad cases ad
    718        [15,34: #b #Hb / by le_n/
    719        |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb
     695     [1,4,5,6,7,8,9: / by le_n/
    720696     |10,13,14,15,16,17,18: / by le_n/
    721      |20,21: cases x #ad cases ad
    722        [15,34: #b #Hb / by le_n/
    723        |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb
    724697     |19,22,23,24,25,26,27: / by le_n/
    725      |29,30: cases x #ad cases ad #a1 #a2
    726        [1,3: cases a2 #ad2 cases ad2
    727          [1,8,20,27: #b #Hb / by le_n/
    728          |2,3,4,9,15,16,17,18,19,21,22,23,28,34,35,36,37,38: #b] #Hb cases Hb
    729        |2,4: cases a1 #ad1 cases ad1
    730          [2,4,21,23: #b #Hb / by le_n/
    731          |1,3,8,9,15,16,17,18,19,20,22,27,28,34,35,36,37,38: #b] #Hb cases Hb
    732        ]
    733698     |28,31,32,33,34,35,36: / by le_n/
    734      |38,39: cases x #ad cases ad
    735        [1,4,20,23: #b #Hb / by le_n/
    736        |2,3,8,9,15,16,17,18,19,21,22,27,28,34,35,36,37,38: #b] #Hb cases Hb
    737699     |37,40,41,42,43,44,45: / by le_n/
    738700     |46,47,48,49,50,51,52,53,54: / by le_n/
     
    741703     |73,74,75,76,77,78,79,80,81: / by le_n/
    742704     ]
     705     try (@(subaddressing_mode_elim … x) #w normalize @le_S @le_S @le_S @le_S @le_S @le_n)
     706     cases x * #ad   
     707     try (@(subaddressing_mode_elim … ad) #w #z normalize @le_S @le_S @le_S @le_S @le_S @le_n)
     708     #z @(subaddressing_mode_elim … z) #w normalize / by /
    743709   ]
    744710 ]
    745711qed.
    746712
    747 lemma minus_zero_to_le: ∀n,m:ℕ.n - m = 0 → n ≤ m.
    748  #n
    749  elim n
    750  [ #m #_ @le_O_n
    751  | #n' #Hind #m cases m
    752    [ #H -n whd in match (minus ??) in H; >H @le_n
    753    | #m' -m #H whd in match (minus ??) in H; @le_S_S @Hind @H
    754    ]
    755  ]
    756 qed.
    757 
    758 lemma plus_zero_zero: ∀n,m:ℕ.n + m = 0 → m = 0.
    759  #n #m #Hn @sym_eq @le_n_O_to_eq <Hn >commutative_plus @le_plus_n_r
    760 qed.
    761 
    762 lemma not_true_is_false:
    763   ∀b:bool.b ≠ true → b = false.
    764  #b cases b
    765  [ #H @⊥ @(absurd ?? H) @refl
    766  | #H @refl
    767  ]
    768 qed.
    769 
    770 lemma occurs_does_not: ∀tag,A,id,list_instr.
    771   does_not_occur tag A id list_instr = true →
    772   occurs_exactly_once tag A id list_instr = true →
    773   False.
    774  #tag #A #id #list_instr elim list_instr
    775  [ #_ whd in match (occurs_exactly_once ????); #ABS destruct (ABS)
    776  | #h #t #Hind whd in match (does_not_occur ????);
    777    whd in match (occurs_exactly_once ????);
    778    cases (instruction_matches_identifier ?? id h) normalize nodelta
    779    [ #ABS destruct (ABS)
    780    | @Hind
    781    ]
    782  ]
    783 qed.
    784  
    785 lemma label_in_program: ∀program:(Σl.S (|l|) < 2^16).∀labels:(Σlm.
     713lemma label_in_program: ∀program:(Σl.S (|l|) < 2^16 ∧ is_well_labelled_p l).∀labels:(Σlm.
    786714   ∀l.occurs_exactly_once ?? l program →
    787715    bitvector_of_nat ? (lookup_def ?? lm l 0) =
     
    789717 occurs_exactly_once ?? x program →   
    790718 lookup_def ASMTag ℕ labels x O≤|program|.
    791  #program cases program -program #program #Hprogram #labels #x cases labels
    792  -labels #labels #H lapply (H x) -H
    793  generalize in match (lookup_def … labels x 0);
    794  whd in match address_of_word_labels_code_mem;
    795  whd in match index_of; normalize nodelta elim program in Hprogram;
    796  [ #Hprogram #n cases not_implemented
    797  | #h #t #Hind #Hprogram #n #Hlm #Hocc lapply (Hlm Hocc) -Hlm #Hbv
    798    whd in match (occurs_exactly_once ????) in Hocc;
    799    whd in match (index_of_internal ????) in Hbv;
    800    lapply (refl ? (instruction_matches_identifier … x h))
    801    lapply Hocc; lapply Hbv; -Hocc -Hbv
    802    cases (instruction_matches_identifier … x h) in ⊢ (% → % → ???% → %);
    803    normalize nodelta #Hbv #Hocc #EQ
    804    [ >(bitvector_of_nat_ok 16 n 0)
    805      [ @le_O_n
    806      | >(eq_eq_bv … Hbv) @I
    807      | / by /
    808      | cases daemon
    809      ]
    810    | cases n in Hbv;
    811      [ #_ @le_O_n
    812      | -n #n #Hbv @le_S_S @(Hind … Hocc)
    813        [ @(transitive_lt … Hprogram) @le_n
    814        | #_ lapply (bitvector_of_nat_ok 16 (S n) (index_of_internal ? (instruction_matches_identifier ?? x) t 1) ???)
    815          [ >Hbv >eq_bv_refl @I
    816          | @(transitive_lt … Hprogram) cases daemon
    817          | cases daemon
    818          | #H >(index_of_label_from_internal … Hocc)
    819            <plus_O_n >(index_of_label_from_internal … Hocc) in H;
    820            #H >(injective_S … H) <plus_O_n @refl
    821          ]
    822        ]
    823      ]
    824    ]
    825  ]
    826 qed.
     719#program cases program -program #program #Hprogram #labels #x cases labels
     720-labels #labels #H lapply (H x) -H
     721generalize in match (lookup_def … labels x 0);
     722whd in match address_of_word_labels_code_mem;
     723whd in match index_of; normalize nodelta elim program in Hprogram;
     724[ #Hprogram #n cases not_implemented
     725| #h #t #Hind #Hprogram #n #Hlm #Hocc lapply (Hlm Hocc) -Hlm #Hbv
     726  whd in match (occurs_exactly_once ????) in Hocc;
     727  whd in match (index_of_internal ????) in Hbv;
     728  lapply (refl ? (instruction_matches_identifier … x h))
     729  lapply Hocc; lapply Hbv; -Hocc -Hbv
     730  cases (instruction_matches_identifier … x h) in ⊢ (% → % → ???% → %);
     731  normalize nodelta #Hbv #Hocc #EQ
     732  [ >(bitvector_of_nat_ok 16 n 0)
     733    [ @le_O_n
     734    | >(eq_eq_bv … Hbv) @I
     735    | / by /
     736    | cases daemon
     737    ]
     738  | cases n in Hbv;
     739    [ #_ @le_O_n
     740    | -n #n #Hbv @le_S_S @(Hind … Hocc)
     741      [ @conj
     742        [ @(transitive_lt … (proj1 ?? Hprogram)) @le_n
     743        | cases daemon (* axiomatize this *)
     744        ]
     745      | #_ lapply (bitvector_of_nat_ok 16 (S n) (index_of_internal ? (instruction_matches_identifier ?? x) t 1) ???)
     746        [ >Hbv >eq_bv_refl @I
     747        | @(transitive_lt … (proj1 ?? Hprogram)) cases daemon
     748        | cases daemon
     749        | #H >(index_of_label_from_internal … Hocc)
     750          <plus_O_n >(index_of_label_from_internal … Hocc) in H;
     751          #H >(injective_S … H) <plus_O_n @refl
     752        ]
     753      ]
     754    ]
     755  ]
     756]
     757qed.
     758
     759lemma equal_compact_unsafe_compact: ∀program:(Σl.(S (|l|)) < 2^16 ∧ is_well_labelled_p l).
     760  ∀labels.∀old_sigma.∀sigma.
     761  sigma_pc_equal program old_sigma sigma →
     762  sigma_safe program labels 0 old_sigma sigma →
     763  sigma_compact_unsafe program labels sigma →
     764  sigma_compact program labels sigma.
     765  #program #labels #old_sigma #sigma #Hequal #Hsafe #Hcp_unsafe #i #Hi
     766  lapply (Hcp_unsafe i Hi) lapply (Hsafe i Hi)
     767  lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)))
     768  cases (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)) in ⊢ (???% → %);
     769  [ / by /
     770  | #x cases x -x #x1 #x2 #EQ
     771    cases (lookup_opt … (bitvector_of_nat ? (S i)) (\snd sigma))
     772    [ / by /
     773    | #y cases y -y #y1 #y2 normalize nodelta #H #H2
     774      cut (instruction_size_jmplen x2
     775       (\snd (nth i ? program 〈None ?, Comment []〉)) =
     776       instruction_size … (bitvector_of_nat ? i)
     777       (\snd (nth i ? program 〈None ?, Comment []〉)))
     778      [5: #H3 <H3 @H2
     779      |4: whd in match (instruction_size_jmplen ??);
     780          whd in match (instruction_size …);
     781          whd in match (assembly_1_pseudoinstruction …);
     782          whd in match (expand_pseudo_instruction …);
     783          normalize nodelta whd in match (append …) in H;
     784          cases (nth i ? program 〈None ?,Comment []〉) in H;
     785          #lbl #instr cases instr
     786          [2,3,6: #x [3: #y] normalize nodelta #H @refl
     787          |4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj
     788            lapply (Hj x (refl ? x)) -Hj normalize nodelta
     789            >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O
     790            cases x2 normalize nodelta
     791            [1,4: whd in match short_jump_cond; normalize nodelta
     792              lapply (refl ? (leb (lookup_def ?? labels x 0) (|[]@program|)))
     793              cases (leb (lookup_def ?? labels x 0) (|[]@program|)) in ⊢ (???% → %); #Hlab
     794              normalize nodelta
     795              >(Hequal (lookup_def ?? labels x 0) ?)
     796              [2,4,6,8: @(label_in_program program labels x)
     797                cases daemon (* XXX this has to come from somewhere else *)
     798              ]
     799              <plus_n_O
     800              cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
     801              #result #flags normalize nodelta
     802              cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
     803              cases (get_index' bool 2 0 flags) normalize nodelta
     804              [5,6,7,8: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/
     805              |1,2,3,4: cases (eq_bv 9 upper ?)
     806                [2,4,6,8: #H lapply (proj1 ?? H) #H3 destruct (H3)
     807                |1,3,5,7: #_ normalize nodelta @refl
     808                ]
     809              ]
     810            |2,5: whd in match short_jump_cond; whd in match absolute_jump_cond;
     811              lapply (refl ? (leb (lookup_def ?? labels x 0) (|[]@program|)))
     812              cases (leb (lookup_def ?? labels x 0) (|[]@program|)) in ⊢ (???% → %); #Hlab
     813              normalize nodelta
     814              (* USE: added = 0 → policy_pc_equal (from fold) *)
     815              >(Hequal (lookup_def ?? labels x 0) ?)
     816              [2,4,6,8: @(label_in_program program labels x)
     817                cases daemon (* XXX this has to come from somewhere else *)]
     818              <plus_n_O
     819              normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2
     820              cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
     821              cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
     822              #result #flags normalize nodelta
     823              cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
     824              cases (get_index' bool 2 0 flags) normalize nodelta
     825              #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl
     826            |3,6: whd in match short_jump_cond; whd in match absolute_jump_cond;
     827              lapply (refl ? (leb (lookup_def ?? labels x 0) (|[]@program|)))
     828              cases (leb (lookup_def ?? labels x 0) (|[]@program|)) in ⊢ (???% → %); #Hlab
     829              normalize nodelta
     830              (* USE: added = 0 → policy_pc_equal (from fold) *)
     831              >(Hequal (lookup_def ?? labels x 0) ?)
     832              [2,4,6,8: @(label_in_program program labels x)
     833                cases daemon (* XXX this has to come from somewhere else *)]
     834              <plus_n_O normalize nodelta
     835              cases (vsplit bool 5 11 ?) #addr1 #addr2
     836              cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
     837              cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
     838              #result #flags normalize nodelta
     839              cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
     840              cases (get_index' bool 2 0 flags) normalize nodelta
     841              #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl
     842            ]
     843          |1: #pi cases pi
     844            [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:
     845              [1,2,3,6,7,24,25: #x #y
     846              |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     847              normalize nodelta #H @refl
     848            |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x]
     849              normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     850              #Hj lapply (Hj x (refl ? x)) -Hj
     851              whd in match expand_relative_jump; normalize nodelta
     852              whd in match expand_relative_jump_internal; normalize nodelta
     853              whd in match expand_relative_jump_unsafe; normalize nodelta
     854              whd in match expand_relative_jump_internal_unsafe;
     855              normalize nodelta >(add_bitvector_of_nat_plus ? i 1)
     856              <(plus_n_Sm i 0) <plus_n_O
     857              cases daemon (* XXX this needs subadressing mode magic, see above *)
     858            ]
     859          ]
     860        ]
     861      ]
     862    ]
     863qed.
  • src/ASM/PolicyStep.ma

    r2102 r2141  
    55
    66(* One step in the search for a jump expansion fixpoint. *)
    7 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).
     7definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.
     8  S (|l|) < 2^16 ∧ is_well_labelled_p l).
    89  ∀labels:(Σlm:label_map.∀l.
    910    occurs_exactly_once ?? l program →
     
    1112    address_of_word_labels_code_mem program l).
    1213  ∀old_policy:(Σpolicy:ppc_pc_map.
    13     And (And (And (And (out_of_program_none program policy)
    14     (not_jump_default program policy))
     14    (* out_of_program_none program policy *)
     15    And (And (And (And (not_jump_default program policy)
    1516    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
    1617    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd policy) 〈0,short_jump〉)))
     18    (sigma_compact_unsafe program labels policy))
    1719    (\fst policy < 2^16)).
    1820  (Σx:bool × (option ppc_pc_map).
     
    2224    | Some p ⇒ And (And (And (And (And (And (And (And (out_of_program_none program p)
    2325       (not_jump_default program p))
    24        (jump_increase program old_policy p))
    25        (no_ch = true → sigma_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       (jump_increase program old_policy p))
     29       (sigma_compact_unsafe program labels p))
    2830       (no_ch = true → sigma_pc_equal program old_policy p))
    2931       (sigma_jump_equal program old_policy p → no_ch = true))
     
    3638    (λprefix.Σx:ℕ × ppc_pc_map.
    3739      let 〈added,policy〉 ≝ x in
    38       And (And (And (And (And (And (And (And (out_of_program_none prefix policy)
     40      And (And (And (And (And (And (And (And (And (out_of_program_none prefix policy)
    3941      (not_jump_default prefix policy))
     42      (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
     43      (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
    4044      (jump_increase prefix old_sigma policy))
    4145      (sigma_compact_unsafe prefix labels policy))
     46      (sigma_jump_equal prefix old_sigma policy → added = 0))
     47      (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))
    4250      (sigma_safe prefix labels added old_sigma policy))
    43       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
    44       (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
    45       (added = 0 → sigma_pc_equal prefix old_sigma policy))
    46       (sigma_jump_equal prefix old_sigma policy → added = 0))
    4751    program
    4852    (λprefix.λx.λtl.λprf.λacc.
     
    96100  #x #H #Heq >Heq in H; normalize nodelta -Heq -x #Hind
    97101  (* USE: inc_pc = fst of policy (from fold) *)
    98   >(proj2 ?? (proj1 ?? (proj1 ?? Hind))) in p1;
     102  >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))))) in p1;
    99103  (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *)
    100   lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (pi2 ?? old_sigma)))
     104  lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))
    101105  #Hsig #Hge
    102106  (* USE: added = 0 → policy_pc_equal (from fold) *)
    103   lapply ((proj2 ?? (proj1 ?? Hind)) ? (|program|) (le_n (|program|)))
    104   [ @(proj2 ?? Hind) #i #Hi
     107  lapply ((proj2 ?? (proj1 ?? (proj1 ?? Hind))) ? (|program|) (le_n (|program|)))
     108  [ (* USE: policy_jump_equal → added = 0 (from fold) *)
     109    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))) #i #Hi
    105110    cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
    106111    [ #Hj
    107112      (* USE: policy_increase (from fold) *)
    108       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi))
     113      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) i (le_S_to_le … Hi))
    109114      lapply (Habs i Hi Hj)
    110115      cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉)
     
    117122    | #Hnj
    118123      (* USE: not_jump_default (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)
     124      >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi Hnj)
     125      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi Hnj)
    121126      @refl
    122127    ]
     
    126131| normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2
    127132  >H2 in H; normalize nodelta -H2 -x #H @conj
    128   [ @conj [ @conj [ @conj [ @conj [ @conj
    129   [ (* USE[pass]: out_of_program_none, not_jump_default, 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: @(label_in_program program labels x)
    168                   cases daemon (* XXX this has to come from somewhere else *)
    169                 ]
    170                 [1,5: >(eqb_true_to_eq … Hch) <plus_n_O]
    171                 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    172                 #result #flags normalize nodelta
    173                 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
    174                 cases (get_index' bool 2 0 flags) normalize nodelta
    175                 [1,3,5,7: cases (eq_bv 9 upper ?)
    176                 |2,4,6,8: cases (eq_bv 9 upper (zero 9))]
    177                 [2,4,6,8,10,12,14,16: #H lapply (proj1 ?? H) #H3 destruct (H3)
    178                 |5,7,13,15: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/
    179                 |1,3,9,11: #_ normalize nodelta @refl
    180                 ]
    181              |2,5: whd in match short_jump_cond; whd in match absolute_jump_cond;
    182                 lapply (refl ? (leb i (lookup_def ?? labels x 0)))
    183                 cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab
    184                 normalize nodelta
    185                 (* USE: added = 0 → policy_pc_equal *)
    186                 >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?)
    187                 [2,4,6,8: @(label_in_program program labels x)
    188                   cases daemon (* XXX this has to come from somewhere else *)]
    189                 [1,3: >(eqb_true_to_eq … Hch) <plus_n_O]
    190                 normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2
    191                 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
    192                 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    193                 #result #flags normalize nodelta
    194                 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
    195                 cases (get_index' bool 2 0 flags) normalize nodelta
    196                 #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl
    197              |3,6: whd in match short_jump_cond; whd in match absolute_jump_cond;
    198                 lapply (refl ? (leb i (lookup_def ?? labels x 0)))
    199                 cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab
    200                 normalize nodelta
    201                 >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?)
    202                 [2,4,6,8: @(label_in_program program labels x)
    203                   cases daemon (* XXX this has to come from somewhere else *)]
    204                 [1,3: >(eqb_true_to_eq … Hch) <plus_n_O]
    205                 normalize nodelta
    206                 cases (vsplit bool 5 11 ?) #addr1 #addr2
    207                 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
    208                 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    209                 #result #flags normalize nodelta
    210                 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
    211                 cases (get_index' bool 2 0 flags) normalize nodelta
    212                 #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl
    213              ]
    214            |1: #pi cases pi
    215              [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:
    216                [1,2,3,6,7,24,25: #x #y
    217                |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    218                normalize nodelta #H @refl
    219              |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x]
    220                normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    221                #Hj lapply (Hj x (refl ? x)) -Hj
    222                whd in match expand_relative_jump; normalize nodelta
    223                whd in match expand_relative_jump_internal; normalize nodelta
    224                whd in match expand_relative_jump_unsafe; normalize nodelta
    225                whd in match expand_relative_jump_internal_unsafe;
    226                normalize nodelta >(add_bitvector_of_nat_plus ? i 1)
    227                <(plus_n_Sm i 0) <plus_n_O
    228                cases daemon (* XXX this needs subadressing mode magic, see above *)
    229              ]
    230            ]
    231          ]
    232        ]
    233      ]
    234    ]
    235    | (* USE: 0 ↦ 0 (from fold) *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
    236    ]
    237    | (* USE: inc_pc = fst of policy (from fold) *) @(proj2 ?? (proj1 ?? (proj1 ?? H)))
    238    ]
    239    | #H2 (* USE: added = 0 → policy_pc_equal (from fold) *)
    240      @(proj2 ?? (proj1 ?? H)) @eqb_true_to_eq @H2
    241    ]
    242    | #H2 (* USE: policy_jump_equal → added = 0 (from fold *)
    243      @eq_to_eqb_true @(proj2 ?? H) @H2
    244    ]
    245    | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1
    246    ]
    247 |4: lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma
     133  [ @conj [ @conj
     134  [ (* USE[pass]: out_of_program_none, not_jump_default, 0 ↦ 0, inc_pc = fst policy,
     135     * jump_increase, sigma_compact_unsafe (from fold) *)
     136    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     137  | (* 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
     142  ]
     143  | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1
     144  ]
     145|4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %);
     146  #inc_pc #inc_sigma #Hips
    248147  lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉))
    249148  cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in ⊢ (???% → %);
    250   #old_pc #old_length #Holdeq #Hpolicy @pair_elim #added #policy normalize nodelta
    251   @pair_elim #new_length #isize normalize nodelta #Heq1 #Heq2
    252   @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
    253   [ (* out_of_program_none *) #i #Hi2 >append_length <commutative_plus @conj
     149  #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim
     150  #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta
     151  #Heq1 #Heq2
     152  @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
     153  (* NOTE: to save memory and speed up work, there's cases daemon here. They can be
     154   * 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
    254157    [ (* → *) #Hi normalize in Hi;
    255158      cases instr in Heq2; normalize nodelta
    256159      #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss
    257160      [1,3,5,7,9,11: >lookup_opt_insert_miss
    258         [1,3,5,7,9,11: (* USE: out_of_program_none → *)
    259           @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi2))
     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))
    260163          @le_S_to_le @Hi
    261164        |2,4,6,8,10,12: @bitvector_of_nat_abs
     
    275178      [ #Hi
    276179        lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
    277         #Hl2 (* USE: out_of_program_none ← *)
    278         lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi2) Hl2)
     180        #Hl2 (* USE[pass]: out_of_program_none ← *)
     181        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2) Hl2)
    279182        #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3
    280183      | #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi))
     
    287190        ]
    288191      ]
    289     ]
    290   | (* not_jump_default *) #i >append_length <commutative_plus #Hi normalize in Hi;
     192    ]
     193  | (* not_jump_default *) (* cases daemon *)
     194    #i >append_length <commutative_plus #Hi normalize in Hi;
    291195    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    292196    [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    293197      [ >lookup_insert_miss
    294198        [ >(nth_append_first ? i prefix ?? Hi)
    295           (* USE: not_jump_default *)
    296           @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi)
     199          (* USE[pass]: not_jump_default *)
     200          @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi)
    297201        | @bitvector_of_nat_abs
    298           [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm
    299             >commutative_plus @le_plus_a @Hi
    300           | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S
     202          [ @(transitive_lt ??? Hi) ]
     203          [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
    301204            @le_plus_n_r
    302205          | @lt_to_not_eq @Hi
     
    304207        ]
    305208      | @bitvector_of_nat_abs
    306         [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm
    307           >commutative_plus @le_plus_a @Hi
    308         | @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <plus_n_Sm
    309           @le_S_S @le_plus_n_r
     209        [ @(transitive_lt ??? Hi) @le_S_to_le ]
     210        [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
     211          <plus_n_Sm @le_S_S @le_plus_n_r
    310212        | @lt_to_not_eq @le_S @Hi
    311213        ]
     
    328230        ]
    329231      | @bitvector_of_nat_abs
    330         [ @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length @le_plus_n_r
    331         | @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm
    332           @le_S_S @le_plus_n_r
     232        [ @le_S_to_le ]
     233        [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S
     234          >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    333235        | @lt_to_not_eq @le_n
    334         ]
    335       ]
    336     ]
    337   ]
    338   | (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi;
     236        ]
     237      ]
     238    ]
     239  ]
     240  | (* 0 ↦ 0 *) (* cases daemon *)
     241    <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
     242    [ cases (decidable_eq_nat 0 (|prefix|))
     243      [ #Heq <Heq >lookup_insert_hit
     244        (* USE: inc_pc = fst policy *)
     245        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     246        (* USE[pass]: 0 ↦ 0 *)
     247        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     248        <Heq #ONE #TWO >TWO >ONE @refl
     249      | #Hneq >lookup_insert_miss
     250        [ (* USE[pass]: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     251        | @bitvector_of_nat_abs
     252          [3: @Hneq]
     253        ]
     254      ]
     255    | @bitvector_of_nat_abs
     256      [3: @lt_to_not_eq / by / ]
     257    ]     
     258    [1,3: / by /
     259    |2,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
     260      [2: <plus_n_Sm @le_S_S]
     261      @le_plus_n_r
     262    ]
     263  ]
     264  | (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2))
     265    >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
     266  ]
     267  | (* jump_increase *) (* cases daemon *)
     268    #i >append_length >commutative_plus #Hi normalize in Hi;
    339269    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    340270    [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    341       [ (* USE: policy_increase *)
    342         lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i (le_S_to_le … Hi))
     271      [ (* USE[pass]: jump_increase *)
     272        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i (le_S_to_le … Hi))
    343273        <(proj2 ?? (pair_destruct ?????? Heq2))
    344274        @pair_elim #opc #oj #EQ1 >lookup_insert_miss
     
    346276          [ @pair_elim #pc #j #EQ2 / by /
    347277          | @bitvector_of_nat_abs
    348             [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S
    349               >commutative_plus @le_plus_a @Hi
    350             | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
     278            [ @(transitive_lt ??? Hi) ]
     279            [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
     280              @le_S_S @le_plus_n_r
    351281            | @lt_to_not_eq @Hi
    352282            ]
    353283          ]
    354284        | @bitvector_of_nat_abs
    355           [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S >commutative_plus
    356             @le_plus_a @Hi
    357           | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm @le_plus_n_r
     285          [ @(transitive_lt ??? Hi) @le_S_to_le ]
     286          [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
     287            >append_length @le_S_S <plus_n_Sm @le_plus_n_r
    358288          | @lt_to_not_eq @le_S @Hi
    359289          ]
     
    384314                #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
    385315                (* USE: not_jump_default (from old_sigma) *)
    386                 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
     316                lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
    387317                [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:
    388318                  >prf >nth_append_second
     
    404334            |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
    405335              (* USE: not_jump_default (from old_sigma) *)
    406               lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
     336              lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
    407337              [1,4,7: >prf >nth_append_second
    408338                [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
     
    418348          ]
    419349        | @bitvector_of_nat_abs
    420           [ @(transitive_lt … (pi2 … program)) >prf @le_S_S >append_length @le_plus_n_r
    421           | @(transitive_lt … (pi2 … program)) @le_S_S >prf >append_length <plus_n_Sm
    422             @le_S_S @le_plus_n_r
     350          [ @le_S_to_le ]
     351          [1,2: @(transitive_lt … (proj1 ?? (pi2 … program))) @le_S_S >prf
     352            >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    423353          | @lt_to_not_eq @le_n
    424354          ]
     
    431361    ]
    432362  ]
    433   | (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi;
     363  | (* sigma_compact_unsafe *) (* cases daemon *)
     364    #i >append_length <commutative_plus #Hi normalize in Hi;
    434365    <(proj2 ?? (pair_destruct ?????? Heq2))
    435366    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     
    439370          [ cases (le_to_or_lt_eq … Hi) -Hi #Hi
    440371            [ >lookup_opt_insert_miss
    441               [ (* USE: policy_compact_unsafe *)
    442                 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)
     372              [ (* USE[pass]: sigma_compact_unsafe *)
     373                lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?)
    443374                [ @le_S_to_le @Hi ]
    444375                cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
     
    458389              ]
    459390            | >Hi >lookup_opt_insert_hit normalize nodelta
    460               (* USE: policy_compact_unsafe *)
    461               lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)
     391              (* USE[pass]: sigma_compact_unsafe *)
     392              lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?)
    462393              [ <Hi @le_n
    463394              | cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
     
    465396                | #x cases x -x #x1 #x2
    466397                  (* USE: inc_pc = fst inc_sigma *)
    467                   lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) <Hi
    468                   lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))
     398                  lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     399                  <Hi lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))
    469400                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %);
    470401                  [ normalize nodelta #_  #_ #H cases H
     
    482413      ]
    483414      [3,4,5: @bitvector_of_nat_abs]
    484       [1: (* Si < 2^16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
    485         >commutative_plus @le_plus_a @Hi
    486       |2,8: (* Spref < 2*16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
     415      [ @(transitive_lt ??? (le_S_S … Hi))
     416      |3: @lt_to_not_eq @le_S_S @Hi
     417      |4,7,10: @(transitive_lt ??? Hi) @le_S_to_le
     418      |5,11: @le_S_to_le
     419      |6: @lt_to_not_eq @Hi
     420      |9: @lt_to_not_eq @le_S @Hi
     421      ]
     422      @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
    487423        <plus_n_Sm @le_S_S @le_plus_n_r
    488       | (* Si ≠ Spref *) @lt_to_not_eq @le_S_S @Hi
    489       |4,7: (* i < 2^16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
    490         >commutative_plus @le_plus_a @le_S_to_le @Hi
    491       |5,11: (* pref < 2^16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
    492         @le_plus_n_r
    493       | @lt_to_not_eq @Hi
    494       | @lt_to_not_eq @le_S_to_le @le_S_S @Hi
    495       | @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm
    496         >commutative_plus @le_plus_a @Hi
    497       ]
    498424    | >Hi >lookup_opt_insert_miss
    499425      [2: @bitvector_of_nat_abs
    500         [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
    501         | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S
     426        [ @le_S_to_le ]
     427        [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
    502428          <plus_n_Sm @le_S_S @le_plus_n_r
    503429        | @lt_to_not_eq @le_n
     
    506432      >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta
    507433      (* USE: out_of_program_none ← *)
    508       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i ?))
    509       [ >Hi @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
     434      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i ?))
     435      [ >Hi @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S @le_plus_n_r
    510436      | >Hi
    511437        (* USE: inc_pc = fst policy *)
    512         lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
     438        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    513439        lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma))
    514440        cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma) in ⊢ (???% → %);
     
    522448          cases instr in Heq1;
    523449          [2,3,6: #x [3: #y] #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
    524             / by refl/
     450            <(proj1 ?? (pair_destruct ?????? Heq1)) %
    525451          |4,5: #x #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
    526             <(proj1 ?? (pair_destruct ?????? Heq1)) @refl
     452            <(proj1 ?? (pair_destruct ?????? Heq1)) %
    527453          |1: #pi cases pi normalize nodelta
    528454            [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:
     
    530456              |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    531457              #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
    532               / by /
     458              <(proj1 ?? (pair_destruct ?????? Heq1)) %
    533459            |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Heq1
    534460              <(proj2 ?? (pair_destruct ?????? Heq1))
    535               <(proj1 ?? (pair_destruct ?????? Heq1))
    536               / by /
    537             ]
    538           ]
    539         ]   
     461              <(proj1 ?? (pair_destruct ?????? Heq1)) %
     462            ]
     463          ]
     464        ]
    540465      ]
    541466    ]
    542467  ]
    543   | (* policy_safe *) cases daemon
    544     (* #i >append_length >commutative_plus #Hi normalize in Hi;
    545     elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    546     [ >nth_append_first
    547       [2: @Hi]
    548       <(proj2 ?? (pair_destruct ?????? Heq2))
    549       >lookup_insert_miss
    550       [ >lookup_insert_miss
     468  | (* policy_jump_equal → added = 0 *) (* cases daemon *)
     469    <(proj2 ?? (pair_destruct ?????? Heq2))
     470    #Heq <(proj1 ?? (pair_destruct ?????? Heq2))
     471    (* USE[pass]: policy_jump_equal → added = 0 *)
     472    >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) ?)
     473    [ cases instr in Heq1 Heq;
     474      [2,3,6: #x [3: #y] normalize nodelta #_ #_ %
     475      |4,5: #x normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
     476        #Heq lapply Holdeq -Holdeq
     477        (* USE: inc_pc = fst inc_sigma *)
     478        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     479        lapply (Heq (|prefix|) ?)
     480        [1,3: >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
     481        -Heq >lookup_insert_miss
     482        [1,3: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
     483          #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
     484          #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n / by /
     485        |2,4: @bitvector_of_nat_abs
     486          [1,4: @le_S_to_le]
     487          [1,2,3,5: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
     488            <plus_n_Sm @le_S_S @le_plus_n_r
     489          |4,6: @lt_to_not_eq @le_n
     490          ]
     491        ]
     492      |1: #pi cases pi normalize nodelta
     493        [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:
     494          [1,2,3,6,7,24,25: #x #y
     495          |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #_ @refl
     496        |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Heq1
     497          <(proj2 ?? (pair_destruct ?????? Heq1)) #Heq lapply Holdeq -Holdeq
     498          (* USE: inc_pc = fst inc_sigma *)
     499          >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     500          lapply (Heq (|prefix|) ?)
     501          [1,3,5,7,9,11,13,15,17: >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
     502          -Heq >lookup_insert_miss
     503          [1,3,5,7,9,11,13,15,17: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
     504            #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
     505            #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n / by /
     506          |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
     507            [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n
     508            |1,4,7,10,13,16,19,22,25: @le_S_to_le
     509            ]
     510            @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S
     511              >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     512          ]
     513        ]
     514      ]
     515    | #i #Hi lapply (Heq i ?)
     516      [ >append_length <plus_n_Sm @le_S <plus_n_O @Hi
     517      | >lookup_insert_miss
    551518        [ >lookup_insert_miss
    552           [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi)
    553             cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
    554             #pc #j cases (nth i ? prefix 〈None ?, Comment []〉) #label #instr cases j
    555             normalize nodelta
    556             [ #H cases (le_to_or_lt_eq … Hi) -Hi #Hi
    557               [ >lookup_insert_miss
    558                 [ #dest #Hjmp <(proj1 ?? (pair_destruct ?????? Heq2))
     519          [ / by /
     520          | @bitvector_of_nat_abs
     521            [ @(transitive_lt ??? Hi) ]
     522            [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
     523              @le_plus_n_r
     524            | @lt_to_not_eq @Hi
     525            ]
     526          ]
     527        | @bitvector_of_nat_abs
     528          [ @(transitive_lt ??? Hi) @le_S_to_le ]
     529          [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
     530            <plus_n_Sm @le_S_S @le_plus_n_r
     531          | @lt_to_not_eq @le_S @Hi
     532          ]
     533        ]
     534      ]
     535    ] *)
     536  ]
     537  | (* added = 0 → policy_pc_equal *) (* cases daemon *)
     538    (* USE: added = 0 → policy_pc_equal *)
     539    lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
     540    <(proj2 ?? (pair_destruct ?????? Heq2))
     541    <(proj1 ?? (pair_destruct ?????? Heq2))
     542    lapply Heq1 -Heq1 lapply (refl ? instr)
     543    cases instr in ⊢ (???% → % → %); normalize nodelta
     544    [2,3,6: #x [3: #y] #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus
     545      #Hi normalize in Hi;
     546      cases (le_to_or_lt_eq … Hi) -Hi #Hi
     547      [1,3,5: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     548        [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
     549          [1,3,5: >lookup_insert_miss
     550            [1,3,5: @(Hold Hadded i (le_S_to_le … Hi))
     551            |2,4,6: @bitvector_of_nat_abs
     552              [3,6,9: @lt_to_not_eq @Hi
     553              |1,4,7: @(transitive_lt ??? Hi)
     554              ]
     555              @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
     556              @le_S_S <plus_n_Sm @le_S @le_plus_n_r
     557            ]
     558          |2,4,6: @bitvector_of_nat_abs
     559            [3,6,9: @lt_to_not_eq @le_S @Hi
     560            |1,4,7: @(transitive_lt … Hi) @le_S_to_le
     561            ]
     562            @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
     563              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
     564          ]
     565        |2,4,6: >Hi >lookup_insert_miss
     566          [1,3,5: >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|)))
     567            @sym_eq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     568          |2,4,6: @bitvector_of_nat_abs
     569            [3,6,9: @lt_to_not_eq @le_n
     570            |1,4,7: @le_S_to_le
     571            ]
     572            @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
     573              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
     574          ]
     575        ]
     576      |2,4,6: >Hi >lookup_insert_hit
     577        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     578        <(Hold Hadded (|prefix|) (le_n (|prefix|)))
     579        (*<(proj2 ?? (pair_destruct ?????? Heq1))*)
     580        (* USE: sigma_compact (from old_sigma) *)
     581        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
     582        [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     583        |2,4,6:
     584          lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
     585          cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% -> %);
     586          [1,3,5: normalize nodelta #_ #ABS cases ABS
     587          |2,4,6: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
     588            cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
     589            [1,3,5: normalize nodelta #Hl #x cases x -x #pc #j normalize nodelta #Hl2 #ABS cases ABS
     590            |2,4,6: normalize nodelta #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
     591              normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉)
     592              >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     593              >prf >p1 >Hins >nth_append_second
     594              [2,4,6: @(le_n (|prefix|))
     595              |1,3,5: <minus_n_n whd in match (nth ????);
     596             
    559597
    560       |
    561       ]
    562     |
    563     ] *)
    564   ]
    565   | (* 0 ↦ 0 *) <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    566     [ cases (decidable_eq_nat 0 (|prefix|))
    567       [ #Heq <Heq >lookup_insert_hit
    568         (* USE: inc_pc = fst policy *)
    569         lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
    570         (* USE: 0 ↦ 0 *)
    571         lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) <Heq
    572         #ONE #TWO >TWO >ONE @refl
    573       | #Hneq >lookup_insert_miss
    574         [ (* USE: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
    575         | @bitvector_of_nat_abs
    576           [3: @Hneq]
    577         ]
    578       ]
    579     | @bitvector_of_nat_abs
    580       [3: @lt_to_not_eq / by / ]
    581     ]     
    582     [1,3: / by /
    583     |2,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S
    584       [2: <plus_n_Sm @le_S_S]
    585       @le_plus_n_r
    586     ]
    587   ]
    588   | (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2))
    589     >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
    590   ]
    591   | (* added = 0 → policy_pc_equal *)
    592     (* USE: added = 0 → policy_pc_equal *)
    593     lapply (proj2 ?? (proj1 ?? Hpolicy))
    594     lapply Heq2 -Heq2 lapply Heq1 -Heq1 lapply (refl ? instr)
    595     cases daemon
    596     (*cases instr in ⊢ (???% → % → % → %); normalize nodelta
    597     [ #pi cases pi normalize nodelta
     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
     606       #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi #Hi
     607       [1,3: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     608         [1,3: >lookup_insert_miss
     609           [1,3: >lookup_insert_miss
     610             [1,3: @(Hold ? i (le_S_to_le … Hi)) >commutative_plus in Hadded;
     611               @plus_zero_zero
     612             |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
     617               ]
     618             ]
     619           |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
     624             ]
     625           ]
     626         |2,4: >Hi >lookup_insert_miss
     627           [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)))))))
     630           |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
     635             ]
     636           ]
     637         ]
     638       |2,4: >Hi >lookup_insert_hit
     639         elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded)))
     640         [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)))))))
     643           <(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 *)
     647         ]
     648       ]
     649     |1: #pi cases pi normalize nodelta
    598650      [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:
    599651        [1,2,3,6,7,24,25: #x #y
    600652        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    601         #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) #Hadded
    602         #i >append_length >commutative_plus #Hi normalize in Hi;
     653        #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus #Hi normalize in Hi;
    603654        cases (le_to_or_lt_eq … Hi) -Hi #Hi
    604655        [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:
    605           <(proj2 ?? (pair_destruct ?????? Heq2))
    606           >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16
    607             (bitvector_of_nat 16 (S (|prefix|)))
    608             (bitvector_of_nat 16 i))
     656          cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    609657          [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:
    610             (* le_to_or_lt_eq, part 2 *)
    611             >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc,new_length〉 16
    612               (bitvector_of_nat 16 (|prefix|)) (bitvector_of_nat 16 i))
    613             [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:
    614               @(Hold Hadded i (le_S_S_to_le … Hi))
    615             |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:
    616               @bitvector_of_nat_abs
    617               [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:
    618                 @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
    619                 @le_S_S @le_plus_a @(le_S_S_to_le … Hi)
    620               |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:
    621                 @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S
    622                 @le_plus_n_r
    623               |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_to_le … Hi)
     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
    625666              ]
    626667            ]
    627           |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:
    628             @bitvector_of_nat_abs
    629             [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:
    630               @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
    631               @le_S_S @le_plus_a @le_S_to_le @(le_S_S_to_le … Hi)
    632             |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:
    633               @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
    634               @le_S_S @le_plus_n_r
    635             |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:
    636               @lt_to_not_eq @le_S_to_le @Hi
    637             ]
    638           ]
    639         |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:
    640            <(proj2 ?? (pair_destruct ?????? Heq2)) >(injective_S … Hi)
    641            >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16
    642              (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat ? (|prefix|)))
    643            [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:
    644              >lookup_insert_hit
    645              lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
    646              [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:
    647                >prf >nth_append_second
    648                [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:
    649                  <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H
    650                |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:
    651                  @le_n
    652                ]
    653              |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:
    654                >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    655              |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:
    656                cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
    657                #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl
    658              ]
    659            |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:
    660              @bitvector_of_nat_abs
    661              [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:
    662                @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
    663              |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:
    664                @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
    665                @le_S_S @le_plus_n_r
    666              |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:
    667                @lt_to_not_eq @le_n
    668              ]
    669            ]
    670          ]
    671        |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Heq2 #Hold
    672          <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1))
    673          #H #i >append_length >commutative_plus #Hi normalize in Hi;
    674          cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    675          [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq2))
    676            >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16
    677               (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i))
    678            [1,3,5,7,9,11,13,15,17:
    679              >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc,new_length〉 16
    680                (bitvector_of_nat 16 (|prefix|)) (bitvector_of_nat 16 i))
    681              [1,3,5,7,9,11,13,15,17: @(Hold ? i Hi)
    682              [1,2,3,4,5,6,7,8,9: @sym_eq @le_n_O_to_eq <H @le_plus_n_r]
    683              ]
    684              @bitvector_of_nat_abs
    685              [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
    686                >append_length >commutative_plus @le_S @le_plus_a @Hi
    687              |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
    688                >append_length @le_S <plus_n_Sm @le_S_S @le_plus_n_r
    689              |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi
    690              ]
    691            |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
    692              [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
    693                >append_length >commutative_plus @le_S @le_plus_a @Hi
    694              |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
    695                >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    696              |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S @Hi
    697              ]
    698            ]
    699          |2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi
    700            >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16
    701               (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|)))
    702            [1,3,5,7,9,11,13,15,17: >lookup_insert_hit
    703              <(proj1 ?? (pair_destruct ?????? Heq1))
    704              >Holdeq normalize nodelta @sym_eq @blerpque
    705              [3,6,9,12,15,18,21,24,27:
    706                elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H)))
    707                [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp
    708                |2,4,6,8,10,12,14,16,18: #H @H
    709                ]
    710                / by I/
    711              |2,5,8,11,14,17,20,23,26: / by I/
    712              ]
    713            |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
    714              [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
    715                >append_length @le_S_S @le_plus_n_r
    716              |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
    717                >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    718              |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S_S @le_n
    719              ]
    720            ]
    721          ]
    722        ]
    723      |2,3,6: #x [3: #y] #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2))
    724        #Hadded #i >append_length >commutative_plus #Hi normalize in Hi;
    725        cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    726        [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    727          [1,3,5: >lookup_insert_miss
    728            [1,3,5: @(Hold Hadded i Hi)
    729            |2,4,6: @bitvector_of_nat_abs
    730              [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length
    731                >commutative_plus @le_S @le_plus_a @Hi
    732              |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length
    733                @le_S <plus_n_Sm @le_S_S @le_plus_n_r
    734              |3,6,9: @lt_to_not_eq @Hi
    735              ]
    736            ]
    737          |2,4,6: @bitvector_of_nat_abs
    738            [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length
    739              >commutative_plus @le_S @le_plus_a @Hi
    740            |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length
    741              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    742            |3,6,9: @lt_to_not_eq @le_S @Hi
    743            ]
    744          ]
    745        |2,4,6: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_miss
    746          [1,3,5: >lookup_insert_hit
    747            lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
    748            [1,4,7: >prf >nth_append_second
    749              [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H
    750              |2,4,6: @le_n
    751              ]
    752            |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    753            |3,6,9:
    754              cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
    755              #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl
    756            ]
    757          |2,4,6: @bitvector_of_nat_abs
    758            [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf
    759              >append_length @le_S_S @le_plus_n_r
    760            |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf
    761              >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    762            |3,6,9: @lt_to_not_eq @le_S_S @le_n
    763            ]
    764          ]
    765        ]
    766      |4,5: #x #Hins #Heq1 #Heq2 #Hold
    767        <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1))
    768        #H #i >append_length >commutative_plus #Hi normalize in Hi;
    769        cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    770        [1,3: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    771          [1,3: >lookup_insert_miss
    772            [1,3: @(Hold ? i Hi)
    773            [1,2: @sym_eq @le_n_O_to_eq <H @le_plus_n_r]
    774            ]
    775            @bitvector_of_nat_abs
    776            [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length
    777              >commutative_plus @le_S @le_plus_a @Hi
    778            |2,5: @(transitive_lt … (pi2 ?? program)) >prf >append_length
    779              @le_S_S @le_plus_n_r
    780            |3,6: @lt_to_not_eq @Hi
    781            ]
    782          |2,4: @bitvector_of_nat_abs
    783            [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length
    784              >commutative_plus @le_S @le_plus_a @Hi
    785            |2,5: @(transitive_lt … (pi2 ?? program)) >prf >append_length
    786              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    787            |3,6: @lt_to_not_eq @le_S @Hi
    788            ]
    789          ]
    790        |2,4: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_miss
    791          [1,3: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
    792            >Holdeq normalize nodelta @sym_eq @blerpque
    793            [3,6: elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H)))
    794              [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp
    795              |2,4: #H @H
    796              ]
    797              / by I/
    798            |2,5: / by I/
    799            ]
    800          |2,4: @bitvector_of_nat_abs
    801            [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length
    802              @le_S_S @le_plus_n_r
    803            |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length
    804              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    805            |3,6,9: @lt_to_not_eq @le_S_S @le_n
    806            ]
    807          ]
    808        ]
    809      ]*)
    810    ]
    811  | (* policy_jump_equal → added = 0 *)
    812    cases daemon
    813  ]
    814 | normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
     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
     671              @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;
     699    elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     700    [ >nth_append_first [2: @Hi]
     701      <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
     702      [ >lookup_insert_miss
     703        [ >lookup_insert_miss
     704          [ elim (le_to_or_lt_eq … Hi) -Hi #Hi
     705            [ >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
     726                          ]
     727                        ]
     728                      | >Hle >lookup_insert_hit
     729                        (* USE: inc_pc = fst policy *)
     730                        <(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     731                        cases j / by /
     732                      ]
     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
     738                      ]
     739                    ]
     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 *)
     744                  ]
     745                | (* same, but with forward jump *) cases daemon
     746                ]
     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  ]
     760| normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
    815761  [ #i cases i
    816762    [ #Hi2 @conj
     
    829775      | #_ @le_S_S @le_O_n
    830776      ]
    831     ] 
     777    ]
    832778  | #i cases i
    833779    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     
    835781    ]
    836782  ]
     783  | >lookup_insert_hit @refl
     784  ]
     785  | >lookup_insert_hit @refl
     786  ]
    837787  | #i #Hi <(le_n_O_to_eq … Hi)
    838788    >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉)
     
    844794    ]
    845795  ]
     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  ]
    846804  | #i cases i
    847805    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     
    849807    ]
    850808  ]
    851   | >lookup_insert_hit @refl
    852   ]
    853   | >lookup_insert_hit @refl
    854   ]
    855   | #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit
    856     (* USE: 0 ↦ 0 (from old_sigma *)
    857     @(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))
    858   ]
    859   | #_ @refl
    860   ]
    861809]
    862810qed.
Note: See TracChangeset for help on using the changeset viewer.