Changeset 2070 for src/ASM/Assembly.ma

Timestamp:

Jun 14, 2012, 2:18:53 AM (9 years ago)

Author:

sacerdot

Message:

More daemons closed.

File:

• src/ASM/Assembly.ma (modified) (9 diffs)

src/ASM/Assembly.ma

@@ -461 +461 @@
 qed.
 
-(*definition rel_jump_length_ok ≝
- λlookup_address:Word.
- λpc:Word.
- Σjump_len:jump_length.
-  (* CSC,JPB: Cheating here, use Jaap's better definition select_reljump_length *)
-  ∀(*x,*)y. expand_relative_jump_internal_safe lookup_address jump_len (*x*) pc y ≠ None ?.
-
-lemma eject_rel_jump_length: ∀x,y. rel_jump_length_ok x y → jump_length.
- #x #y #p @(pi1 … p)
-qed.
-
-coercion eject_rel_jump_length nocomposites:
- ∀x,y.∀pol:rel_jump_length_ok x y. jump_length ≝
- eject_rel_jump_length on _pol:(rel_jump_length_ok ??) to jump_length.*)
-
-(*definition expand_relative_jump_internal:
- ∀lookup_address:Word. ∀pc:Word. ([[relative]] → preinstruction [[relative]]) →
- list instruction
-≝ λlookup_address,pc,i.
-   match expand_relative_jump_internal_safe lookup_address pc i
-   return λres. res ≠ None ? → ?
-   with
-   [ None ⇒ λabs.⊥
-   | Some res ⇒ λ_.res ] (pi2 … jump_len i).
- cases abs /2/
-qed.*)
-
 definition expand_relative_jump: 
   ∀lookup_labels.∀sigma.
@@ -586 +559 @@
   %
 qed.
-
-(*
-(*X?
-definition jump_length_ok ≝
- λlookup_labels:Identifier → Word.
- λpc:Word.
- Σjump_len:jump_length.
-  (* CSC,JPB: Cheating here, use Jaap's better definition select_reljump_length *)
-  ∀x,y.expand_pseudo_instruction_safe lookup_labels pc jump_len x y ≠ None ?.
-*)
-
-lemma eject_jump_length: ∀x,y. jump_length_ok x y → jump_length.
- #x #y #p @(pi1 … p)
-qed.
-
-coercion eject_jump_length nocomposites:
- ∀x,y.∀pol:jump_length_ok x y. jump_length ≝
- eject_jump_length on _pol:(jump_length_ok ??) to jump_length.
-
-definition expand_pseudo_instruction:
- ∀lookup_labels:Identifier → Word. ∀pc:Word. jump_length_ok lookup_labels pc →
- ? → pseudo_instruction → list instruction ≝
- λlookup_labels,pc,jump_len,lookup_datalabels,i.
-   match expand_pseudo_instruction_safe lookup_labels pc jump_len lookup_datalabels i
-   return λres. res ≠ None ? → ?
-   with
-   [ None ⇒ λabs.⊥
-   | Some res ⇒ λ_.res ] (pi2 … jump_len lookup_datalabels i).
- cases abs /2/
-qed.
-*)
-(*X?
-definition policy_type ≝
- λlookup_labels:Identifier → Word.
- ∀pc:Word. jump_length_ok lookup_labels pc.
-*)
-
-(*definition policy_type2 ≝
- λprogram.
-  Σpol:Word → jump_length.
-   let lookup_labels ≝
-    (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) in
-   ∀pc:Word. let jump_len ≝ pol pc in
-    ∀x,y.expand_pseudo_instruction_safe lookup_labels pc jump_len x y ≠ None ?.*)
  
 definition assembly_1_pseudoinstruction ≝
@@ -652 +581 @@
     \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc (λx.zero …) i).
 
-(* Jaap: never used
-lemma fetch_pseudo_instruction_prefix:
-  ∀prefix.∀x.∀ppc.ppc < (|prefix|) → 
-  fetch_pseudo_instruction prefix (bitvector_of_nat ? ppc) =
-  fetch_pseudo_instruction (prefix@x) (bitvector_of_nat ? ppc).
- #prefix #x #ppc elim prefix
- [ #Hppc @⊥ @(absurd … Hppc) @le_to_not_lt @le_O_n
- | #h #t #Hind #Hppc whd in match (fetch_pseudo_instruction ??);
-   whd in match (fetch_pseudo_instruction ((h::t)@x) ?);
-   >nth_append_first
-   [ //
-   | >nat_of_bitvector_bitvector_of_nat
-     [ @Hppc
-     | cases daemon (* XXX invariant *)
-     ]
-   ]
- ]
-qed.
-*)
-
 (*CSC: move elsewhere *)
 lemma nth_safe_append:
@@ -694 +603 @@
 #EQ %{lbl0} @EQ
 qed.
-
-(*lemma sigma00_append:
- ∀jump_expansion,l1,l2.
- ∀acc:ℕ×ℕ×(BitVectorTrie Word 16).
-  sigma00 jump_expansion (l1@l2) acc =
-  sigma00 jump_expansion
-    l2 (pi1 ?? (sigma00 jump_expansion l1 acc)).*)
-
-(* lemma sigma00_strict:
- ∀jump_expansion,l,acc. acc = None ? →
-  sigma00 jump_expansion l acc = None ….
- #jump_expansion #l elim l
-  [ #acc #H >H %
-  | #hd #tl #IH #acc #H >H change with (sigma00 ? tl ? = ?) @IH % ]
-qed.
-
-lemma policy_ok_prefix_ok:
- ∀program.∀pol:policy program.∀suffix,prefix.
-  prefix@suffix = \snd program →
-   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
- * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
- generalize in match (pi2 ?? pol); whd in prf:(???%); <prf in pol; #pol
- whd in match policy_ok; whd in match sigma_safe; whd in match sigma0;
- normalize nodelta >sigma00_append
- cases (sigma00 ?? prefix ?)
-  [2: #x #_ % #abs destruct(abs)
-  | * #abs @⊥ @abs >sigma00_strict % ]
-qed. 
-
-lemma policy_ok_prefix_hd_ok:
- ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
-  (prefix@[hd])@suffix = \snd program →
-   Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
-    let 〈ppc,pc_map〉 ≝ ppc_pc_map in
-    let 〈program_counter, sigma_map〉 ≝ pc_map in
-    let 〈label, i〉 ≝ hd in
-     construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
- * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
- generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
-  (prefix@[hd]) EQ1) in ⊢ ?; >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?);
- @pair_elim #ppc #pc_map #EQ3 normalize nodelta
- @pair_elim #pc #map #EQ4 normalize nodelta
- @pair_elim #l' #i' #EQ5 normalize nodelta
- cases (construct_costs_safe ??????) normalize
-  [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
-qed. *)
-
-(* JPB,CSC: this definition is now replaced by the expand_pseudo_instruction higher up
-definition expand_pseudo_instruction:
- ∀program:pseudo_assembly_program.∀pol: policy program.
-  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc.
-  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
-  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
-  let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
-  pc = sigma program pol ppc →
-  Σres:list instruction. Some … res = expand_pseudo_instruction_safe pc (lookup_labels pi) lookup_datalabels (pol ppc) pi
-≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,prf1,prf2,prf3.
-   match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) (\fst (fetch_pseudo_instruction (\snd program) ppc)) with
-    [ None ⇒ let dummy ≝ [ ] in dummy
-    | Some res ⇒ res ].
- [ @⊥ whd in p:(??%??);
-   generalize in match (pi2 ?? pol); whd in ⊢ (% → ?);
-   whd in ⊢ (?(??%?) → ?); change with (sigma00 ????) in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?);
-   generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)));
-   cases (sigma00 ????) in ⊢ (??%? → %); normalize nodelta [#_ * #abs @abs %]
-   #res #K
-   cases (fetch_pseudo_instruction_vsplit (\snd program) ppc) #pre * #suff * #lbl #EQ1
-   generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?;
-   cases daemon (* CSC: XXXXXXXX Ero qui
-   
-    [3: @policy_ok_prefix_ok ]
-    | sigma00 program pol pre
-
-
-
-   QUA USARE LEMMA policy_ok_prefix_hd_ok combinato a lemma da fare che
-   fetch ppc = hd sse program = pre @ [hd] @ tl e |pre| = ppc
-   per concludere construct_costs_safe ≠ None *)
- | >p %]
-qed. *)
-
-(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
-(* definition assembly_1_pseudoinstruction':
- ∀program:pseudo_assembly_program.∀pol: policy program.
-  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
-  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
-  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
-  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
-  Σres:(nat × (list Byte)).
-   res = assembly_1_pseudoinstruction program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧
-   let 〈len,code〉 ≝ res in
-    sigma program pol (add ? ppc (bitvector_of_nat ? 1)) =
-     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)
-≝ λprogram: pseudo_assembly_program.
-  λpol: policy program.
-  λppc: Word.
-  λlookup_labels.
-  λlookup_datalabels.
-  λpi.
-  λprf1,prf2,prf3.
-   assembly_1_pseudoinstruction program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
- [ @⊥ elim pi in p; [*]
-   try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs
-   generalize in match (jmeq_to_eq ??? abs); -abs; #abs whd in abs:(??%?); try destruct(abs)
-   whd in abs:(??match % with [_ ⇒ ? | _ ⇒ ?]?);
-   (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
-   cases daemon
- | % [ >p %]
-   cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
-   (* THIS SHOULD BE TRUE INSTEAD *)
-   cases daemon]
-qed. 
-
-definition assembly_1_pseudoinstruction:
- ∀program:pseudo_assembly_program.∀pol: policy program.
-  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
-  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
-  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
-  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
-   nat × (list Byte)
-≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3.
-   assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1
-    prf2 prf3.
-
-lemma assembly_1_pseudoinstruction_ok1:
- ∀program:pseudo_assembly_program.∀pol: policy program.
-  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
-  ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
-  ∀prf2:lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)).
-  ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
-     Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
-   = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
- #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
- cases (pi2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
- #H1 #_ @H1
-qed. *)
-
-(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
-(* definition construct_costs':
- ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.
-  Σres:(nat × (BitVectorTrie costlabel 16)). Some … res = construct_costs_safe program pol ppc pc costs i
-≝
-  λprogram.λpol: policy program.λppc,pc,costs,i.
-   match construct_costs_safe program pol ppc pc costs i with
-    [ None ⇒ let dummy ≝ 〈0, Stub costlabel 16〉 in dummy
-    | Some res ⇒ res ].
- [ cases daemon
- | >p %]
-qed.
-
-definition construct_costs ≝
- λprogram,pol,ppc,pc,costs,i. pi1 … (construct_costs' program pol ppc pc costs i). *)
-
-(*
-axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A.
-axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l.
-
-axiom foldl_strong_step:
- ∀A:Type[0].
-  ∀P: list A → Type[0].
-   ∀l: list A.
-    ∀H: ∀prefix,hd,tl. l =  prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
-     ∀acc: P [ ].
-      ∀Q: ∀prefix. P prefix → Prop.
-       ∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl.
-        ∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc).
-       Q [ ] acc →
-        Q l (foldl_strong A P l H acc).
-(*
- #A #P #l #H #acc #Q #HQ #Hacc normalize;
- generalize in match
-  (foldl_strong ?
-   (λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?))
-   l ? Hacc)
- [3: >suffix_of_ok % | 2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ]
- [2: #prefix #hd #tl #prf #X whd in ⊢ (??%) 
- #K 
-
- generalize in match
-  (foldl_strong ?
-   (λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre))))
- [2: @H
-*)
-
-axiom foldl_elim:
- ∀A:Type[0].
-  ∀B: Type[0].
-   ∀H: A → B → A.
-    ∀acc: A.
-     ∀l: list B.
-      ∀Q: A → Prop.
-       (∀acc:A.∀b:B. Q acc → Q (H acc b)) →
-         Q acc →
-          Q (foldl A B H acc l).
-*)
-
-(*
-lemma tech_pc_sigma00_append_Some:
- ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
-  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
-   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
- #program #pol #prefix #costs #label #i #ppc #pc #H
-  whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;
-  whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;
-  generalize in match (pi2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
-  whd in match sigma0; normalize nodelta;
-  >foldl_step
-  change with (? → match match sigma00 program pol prefix with [None ⇒ ? | Some res ⇒ ?] with [ None ⇒ ? | Some res ⇒ ? ] = ?)
-  whd in match tech_pc_sigma00 in H; normalize nodelta in H;
-  cases (sigma00 program pol prefix) in H ⊢ %
-   [ whd in ⊢ (??%% → ?) #abs destruct(abs)
-   | * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H)
-     
-     normalize nodelta; -H;
-     
-  
-   generalize in match H; -H;
-  generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ? | _ ⇒ ?] with [_ ⇒ ? | _ ⇒ ?]?)
-   [2: whd in ⊢ (??%%)
-XXX
-*)
-
-(* axiom construct_costs_sigma:
- ∀p.∀pol:policy p.∀ppc,pc,costs,i.
-  bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
-   bitvector_of_nat ? (\fst (construct_costs p pol ppc pc costs i)) = sigma p pol (bitvector_of_nat 16 (S ppc)).
-
-axiom tech_pc_sigma00_append_Some:
- ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
-  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
-   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉. *)
 
 axiom eq_identifier_eq:
@@ -1070 +748 @@
 
 (*CSC: move elsewhere *)
+axiom nat_of_bitvector_add:
+ ∀n,v1,v2.
+  nat_of_bitvector n v1 + nat_of_bitvector n v2 < 2^n →
+   nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.
+
+(*CSC: move elsewhere *)
 lemma fetch_pseudo_instruction_append:
- ∀l1,l2,ppc,ppc_ok,ppc_ok'.
+ ∀l1,l2. |l1@l2| < 2^16 → ∀ppc,ppc_ok,ppc_ok'.
   let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
   fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
   〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.
- #l1 #l2 #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
- (*CSC: FALSE, NEED INVARIANT? *)
- > (?: nat_of_bitvector … (add 16 (bitvector_of_nat 16 (|l1|)) ppc)
-     = |l1| + nat_of_bitvector … ppc) [2: cases daemon]
+ #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
+ cut (|l1| + nat_of_bitvector … ppc < 2^16)
+ [ @(transitive_lt … l1l2_ok) >length_append /2 by monotonic_lt_plus_r/ ]
+ -l1l2_ok #l1ppc_ok >nat_of_bitvector_add
+ >nat_of_bitvector_bitvector_of_nat_inverse try assumption
+ [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ] 
  #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)
  #lbl #instr normalize nodelta >add_associative %
@@ -1085 +771 @@
 definition assembly:
     ∀p: pseudo_assembly_program.
+    |\snd p| < 2^16 →
     ∀sigma: Word → Word.
     ∀policy: Word → bool.
@@ -1103 +790 @@
             assembled K
 ≝
-  λp.
+  λp. λinstr_list_ok.
   λsigma.
   λpolicy.
@@ -1141 +828 @@
   | % // #ppc' #ppc_ok' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs) | skip]
   | cases ppc_code in p1; -ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; -EQppc_code
-    * #IH1 #IH2 % [ normalize nodelta >IH1 >length_append cases daemon (*CSC: TRUE, LEMMA NEEDED *)]
-    #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2
+    * #IH1 #IH2 whd % [ normalize nodelta >IH1 >length_append cases daemon (*CSC: TRUE, LEMMA NEEDED *)]
+    #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 #LTppc_ppc
     cases (le_to_or_lt_eq … LTppc')
     [2: #S_S_eq normalize nodelta in S_S_eq;
         (*CSC: FALSE, NEEDS INVARIANT *)
-        cut (ppc' = ppc) [cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc'  >prf
-        >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc #X lapply LTppc
+        cut (ppc' = ppc) [ normalize nodelta in LTppc_ppc; >IH1 cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc'  >prf
+        >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc lapply LTppc
         >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → match % with [_ ⇒ ?]);
         >fetch_pseudo_instruction_append
-        [3: @le_S_S @le_O_n |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H]
+        [3: @le_S_S @le_O_n
+        |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H
+        |4: <prf <p_refl in instr_list_ok; #H @H ]
         #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2
-        #j #LTj
-        (* CSC: FALSE, NEEDS INVARIANT *)
-        >(?: nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … j)) =
-             nat_of_bitvector … (sigma ppc) + j) [2: cases daemon]
+        #j #LTj >nat_of_bitvector_add
+        >nat_of_bitvector_bitvector_of_nat_inverse
+        [2,4: (* CSC: TRUE, NEEDS LEMMA, MAYBE ALREADY PROVED *) cases daemon
+        |3: (* CSC: TRUE, NEEDS INVARIANT *) cases daemon ]
         >reverse_append >reverse_reverse
-        (* CSC: TRUE, NEEDS INVARIANT *)
+        (* CSC: TRUE, NEEDS SAME INVARIANT *)
         >(? : nat_of_bitvector … (sigma ppc) = |reverse … code|) [2: cases daemon]
         @nth_safe_prepend
-    | #LTppc' #LT_ppc_ppc lapply (IH2 ppc' ?) [ (*CSC: EASY, FINISH*) cases daemon ]
+    | #LTppc'' lapply (IH2 ppc' ?)
+      [ @(transitive_le … LTppc'') @le_S_S // ]
       @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction
       @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH
@@ -1166 +856 @@
       >eq_assembly_1_pseudoinstruction #j #LTj >reverse_append >reverse_reverse #K
       >IH
-      [2: (*CSC: FALSE, NEEDS INVARIANT? *) cases daemon
+      [2: (*CSC: FALSE, NEEDS INVARIANT PPC'=PPC TO AVOID @PAIR_ELIM ABOVE? *) cases daemon
       | @shift_nth_prefix
       |3: >IH1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption