Changeset 2070


Ignore:
Timestamp:
Jun 14, 2012, 2:18:53 AM (5 years ago)
Author:
sacerdot
Message:

More daemons closed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2055 r2070  
    461461qed.
    462462
    463 (*definition rel_jump_length_ok ≝
    464  λlookup_address:Word.
    465  λpc:Word.
    466  Σjump_len:jump_length.
    467   (* CSC,JPB: Cheating here, use Jaap's better definition select_reljump_length *)
    468   ∀(*x,*)y. expand_relative_jump_internal_safe lookup_address jump_len (*x*) pc y ≠ None ?.
    469 
    470 lemma eject_rel_jump_length: ∀x,y. rel_jump_length_ok x y → jump_length.
    471  #x #y #p @(pi1 … p)
    472 qed.
    473 
    474 coercion eject_rel_jump_length nocomposites:
    475  ∀x,y.∀pol:rel_jump_length_ok x y. jump_length ≝
    476  eject_rel_jump_length on _pol:(rel_jump_length_ok ??) to jump_length.*)
    477 
    478 (*definition expand_relative_jump_internal:
    479  ∀lookup_address:Word. ∀pc:Word. ([[relative]] → preinstruction [[relative]]) →
    480  list instruction
    481 ≝ λlookup_address,pc,i.
    482    match expand_relative_jump_internal_safe lookup_address pc i
    483    return λres. res ≠ None ? → ?
    484    with
    485    [ None ⇒ λabs.⊥
    486    | Some res ⇒ λ_.res ] (pi2 … jump_len i).
    487  cases abs /2/
    488 qed.*)
    489 
    490463definition expand_relative_jump:
    491464  ∀lookup_labels.∀sigma.
     
    586559  %
    587560qed.
    588 
    589 (*
    590 (*X?
    591 definition jump_length_ok ≝
    592  λlookup_labels:Identifier → Word.
    593  λpc:Word.
    594  Σjump_len:jump_length.
    595   (* CSC,JPB: Cheating here, use Jaap's better definition select_reljump_length *)
    596   ∀x,y.expand_pseudo_instruction_safe lookup_labels pc jump_len x y ≠ None ?.
    597 *)
    598 
    599 lemma eject_jump_length: ∀x,y. jump_length_ok x y → jump_length.
    600  #x #y #p @(pi1 … p)
    601 qed.
    602 
    603 coercion eject_jump_length nocomposites:
    604  ∀x,y.∀pol:jump_length_ok x y. jump_length ≝
    605  eject_jump_length on _pol:(jump_length_ok ??) to jump_length.
    606 
    607 definition expand_pseudo_instruction:
    608  ∀lookup_labels:Identifier → Word. ∀pc:Word. jump_length_ok lookup_labels pc →
    609  ? → pseudo_instruction → list instruction ≝
    610  λlookup_labels,pc,jump_len,lookup_datalabels,i.
    611    match expand_pseudo_instruction_safe lookup_labels pc jump_len lookup_datalabels i
    612    return λres. res ≠ None ? → ?
    613    with
    614    [ None ⇒ λabs.⊥
    615    | Some res ⇒ λ_.res ] (pi2 … jump_len lookup_datalabels i).
    616  cases abs /2/
    617 qed.
    618 *)
    619 (*X?
    620 definition policy_type ≝
    621  λlookup_labels:Identifier → Word.
    622  ∀pc:Word. jump_length_ok lookup_labels pc.
    623 *)
    624 
    625 (*definition policy_type2 ≝
    626  λprogram.
    627   Σpol:Word → jump_length.
    628    let lookup_labels ≝
    629     (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) in
    630    ∀pc:Word. let jump_len ≝ pol pc in
    631     ∀x,y.expand_pseudo_instruction_safe lookup_labels pc jump_len x y ≠ None ?.*)
    632561 
    633562definition assembly_1_pseudoinstruction ≝
     
    652581    \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc (λx.zero …) i).
    653582
    654 (* Jaap: never used
    655 lemma fetch_pseudo_instruction_prefix:
    656   ∀prefix.∀x.∀ppc.ppc < (|prefix|) →
    657   fetch_pseudo_instruction prefix (bitvector_of_nat ? ppc) =
    658   fetch_pseudo_instruction (prefix@x) (bitvector_of_nat ? ppc).
    659  #prefix #x #ppc elim prefix
    660  [ #Hppc @⊥ @(absurd … Hppc) @le_to_not_lt @le_O_n
    661  | #h #t #Hind #Hppc whd in match (fetch_pseudo_instruction ??);
    662    whd in match (fetch_pseudo_instruction ((h::t)@x) ?);
    663    >nth_append_first
    664    [ //
    665    | >nat_of_bitvector_bitvector_of_nat
    666      [ @Hppc
    667      | cases daemon (* XXX invariant *)
    668      ]
    669    ]
    670  ]
    671 qed.
    672 *)
    673 
    674583(*CSC: move elsewhere *)
    675584lemma nth_safe_append:
     
    694603#EQ %{lbl0} @EQ
    695604qed.
    696 
    697 (*lemma sigma00_append:
    698  ∀jump_expansion,l1,l2.
    699  ∀acc:ℕ×ℕ×(BitVectorTrie Word 16).
    700   sigma00 jump_expansion (l1@l2) acc =
    701   sigma00 jump_expansion
    702     l2 (pi1 ?? (sigma00 jump_expansion l1 acc)).*)
    703 
    704 (* lemma sigma00_strict:
    705  ∀jump_expansion,l,acc. acc = None ? →
    706   sigma00 jump_expansion l acc = None ….
    707  #jump_expansion #l elim l
    708   [ #acc #H >H %
    709   | #hd #tl #IH #acc #H >H change with (sigma00 ? tl ? = ?) @IH % ]
    710 qed.
    711 
    712 lemma policy_ok_prefix_ok:
    713  ∀program.∀pol:policy program.∀suffix,prefix.
    714   prefix@suffix = \snd program →
    715    sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
    716  * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
    717  generalize in match (pi2 ?? pol); whd in prf:(???%); <prf in pol; #pol
    718  whd in match policy_ok; whd in match sigma_safe; whd in match sigma0;
    719  normalize nodelta >sigma00_append
    720  cases (sigma00 ?? prefix ?)
    721   [2: #x #_ % #abs destruct(abs)
    722   | * #abs @⊥ @abs >sigma00_strict % ]
    723 qed.
    724 
    725 lemma policy_ok_prefix_hd_ok:
    726  ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
    727   (prefix@[hd])@suffix = \snd program →
    728    Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
    729     let 〈ppc,pc_map〉 ≝ ppc_pc_map in
    730     let 〈program_counter, sigma_map〉 ≝ pc_map in
    731     let 〈label, i〉 ≝ hd in
    732      construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
    733  * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
    734  generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
    735   (prefix@[hd]) EQ1) in ⊢ ?; >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?);
    736  @pair_elim #ppc #pc_map #EQ3 normalize nodelta
    737  @pair_elim #pc #map #EQ4 normalize nodelta
    738  @pair_elim #l' #i' #EQ5 normalize nodelta
    739  cases (construct_costs_safe ??????) normalize
    740   [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
    741 qed. *)
    742 
    743 (* JPB,CSC: this definition is now replaced by the expand_pseudo_instruction higher up
    744 definition expand_pseudo_instruction:
    745  ∀program:pseudo_assembly_program.∀pol: policy program.
    746   ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc.
    747   lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
    748   lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
    749   let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
    750   pc = sigma program pol ppc →
    751   Σres:list instruction. Some … res = expand_pseudo_instruction_safe pc (lookup_labels pi) lookup_datalabels (pol ppc) pi
    752 ≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,prf1,prf2,prf3.
    753    match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) (\fst (fetch_pseudo_instruction (\snd program) ppc)) with
    754     [ None ⇒ let dummy ≝ [ ] in dummy
    755     | Some res ⇒ res ].
    756  [ @⊥ whd in p:(??%??);
    757    generalize in match (pi2 ?? pol); whd in ⊢ (% → ?);
    758    whd in ⊢ (?(??%?) → ?); change with (sigma00 ????) in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?);
    759    generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)));
    760    cases (sigma00 ????) in ⊢ (??%? → %); normalize nodelta [#_ * #abs @abs %]
    761    #res #K
    762    cases (fetch_pseudo_instruction_vsplit (\snd program) ppc) #pre * #suff * #lbl #EQ1
    763    generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?;
    764    cases daemon (* CSC: XXXXXXXX Ero qui
    765    
    766     [3: @policy_ok_prefix_ok ]
    767     | sigma00 program pol pre
    768 
    769 
    770 
    771    QUA USARE LEMMA policy_ok_prefix_hd_ok combinato a lemma da fare che
    772    fetch ppc = hd sse program = pre @ [hd] @ tl e |pre| = ppc
    773    per concludere construct_costs_safe ≠ None *)
    774  | >p %]
    775 qed. *)
    776 
    777 (* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
    778 (* definition assembly_1_pseudoinstruction':
    779  ∀program:pseudo_assembly_program.∀pol: policy program.
    780   ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
    781   lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
    782   lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
    783   \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
    784   Σres:(nat × (list Byte)).
    785    res = assembly_1_pseudoinstruction program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧
    786    let 〈len,code〉 ≝ res in
    787     sigma program pol (add ? ppc (bitvector_of_nat ? 1)) =
    788      bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)
    789 ≝ λprogram: pseudo_assembly_program.
    790   λpol: policy program.
    791   λppc: Word.
    792   λlookup_labels.
    793   λlookup_datalabels.
    794   λpi.
    795   λprf1,prf2,prf3.
    796    assembly_1_pseudoinstruction program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
    797  [ @⊥ elim pi in p; [*]
    798    try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs
    799    generalize in match (jmeq_to_eq ??? abs); -abs; #abs whd in abs:(??%?); try destruct(abs)
    800    whd in abs:(??match % with [_ ⇒ ? | _ ⇒ ?]?);
    801    (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
    802    cases daemon
    803  | % [ >p %]
    804    cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
    805    (* THIS SHOULD BE TRUE INSTEAD *)
    806    cases daemon]
    807 qed.
    808 
    809 definition assembly_1_pseudoinstruction:
    810  ∀program:pseudo_assembly_program.∀pol: policy program.
    811   ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
    812   lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
    813   lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
    814   \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
    815    nat × (list Byte)
    816 ≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3.
    817    assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1
    818     prf2 prf3.
    819 
    820 lemma assembly_1_pseudoinstruction_ok1:
    821  ∀program:pseudo_assembly_program.∀pol: policy program.
    822   ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
    823   ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
    824   ∀prf2:lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)).
    825   ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
    826      Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
    827    = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
    828  #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
    829  cases (pi2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
    830  #H1 #_ @H1
    831 qed. *)
    832 
    833 (* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
    834 (* definition construct_costs':
    835  ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.
    836   Σres:(nat × (BitVectorTrie costlabel 16)). Some … res = construct_costs_safe program pol ppc pc costs i
    837 
    838   λprogram.λpol: policy program.λppc,pc,costs,i.
    839    match construct_costs_safe program pol ppc pc costs i with
    840     [ None ⇒ let dummy ≝ 〈0, Stub costlabel 16〉 in dummy
    841     | Some res ⇒ res ].
    842  [ cases daemon
    843  | >p %]
    844 qed.
    845 
    846 definition construct_costs ≝
    847  λprogram,pol,ppc,pc,costs,i. pi1 … (construct_costs' program pol ppc pc costs i). *)
    848 
    849 (*
    850 axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A.
    851 axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l.
    852 
    853 axiom foldl_strong_step:
    854  ∀A:Type[0].
    855   ∀P: list A → Type[0].
    856    ∀l: list A.
    857     ∀H: ∀prefix,hd,tl. l =  prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
    858      ∀acc: P [ ].
    859       ∀Q: ∀prefix. P prefix → Prop.
    860        ∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl.
    861         ∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc).
    862        Q [ ] acc →
    863         Q l (foldl_strong A P l H acc).
    864 (*
    865  #A #P #l #H #acc #Q #HQ #Hacc normalize;
    866  generalize in match
    867   (foldl_strong ?
    868    (λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?))
    869    l ? Hacc)
    870  [3: >suffix_of_ok % | 2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ]
    871  [2: #prefix #hd #tl #prf #X whd in ⊢ (??%)
    872  #K
    873 
    874  generalize in match
    875   (foldl_strong ?
    876    (λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre))))
    877  [2: @H
    878 *)
    879 
    880 axiom foldl_elim:
    881  ∀A:Type[0].
    882   ∀B: Type[0].
    883    ∀H: A → B → A.
    884     ∀acc: A.
    885      ∀l: list B.
    886       ∀Q: A → Prop.
    887        (∀acc:A.∀b:B. Q acc → Q (H acc b)) →
    888          Q acc →
    889           Q (foldl A B H acc l).
    890 *)
    891 
    892 (*
    893 lemma tech_pc_sigma00_append_Some:
    894  ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
    895   tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
    896    tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
    897  #program #pol #prefix #costs #label #i #ppc #pc #H
    898   whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;
    899   whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;
    900   generalize in match (pi2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
    901   whd in match sigma0; normalize nodelta;
    902   >foldl_step
    903   change with (? → match match sigma00 program pol prefix with [None ⇒ ? | Some res ⇒ ?] with [ None ⇒ ? | Some res ⇒ ? ] = ?)
    904   whd in match tech_pc_sigma00 in H; normalize nodelta in H;
    905   cases (sigma00 program pol prefix) in H ⊢ %
    906    [ whd in ⊢ (??%% → ?) #abs destruct(abs)
    907    | * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H)
    908      
    909      normalize nodelta; -H;
    910      
    911  
    912    generalize in match H; -H;
    913   generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ? | _ ⇒ ?] with [_ ⇒ ? | _ ⇒ ?]?)
    914    [2: whd in ⊢ (??%%)
    915 XXX
    916 *)
    917 
    918 (* axiom construct_costs_sigma:
    919  ∀p.∀pol:policy p.∀ppc,pc,costs,i.
    920   bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
    921    bitvector_of_nat ? (\fst (construct_costs p pol ppc pc costs i)) = sigma p pol (bitvector_of_nat 16 (S ppc)).
    922 
    923 axiom tech_pc_sigma00_append_Some:
    924  ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
    925   tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
    926    tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉. *)
    927605
    928606axiom eq_identifier_eq:
     
    1070748
    1071749(*CSC: move elsewhere *)
     750axiom nat_of_bitvector_add:
     751 ∀n,v1,v2.
     752  nat_of_bitvector n v1 + nat_of_bitvector n v2 < 2^n →
     753   nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.
     754
     755(*CSC: move elsewhere *)
    1072756lemma fetch_pseudo_instruction_append:
    1073  ∀l1,l2,ppc,ppc_ok,ppc_ok'.
     757 ∀l1,l2. |l1@l2| < 2^16 → ∀ppc,ppc_ok,ppc_ok'.
    1074758  let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
    1075759  fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
    1076760  〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.
    1077  #l1 #l2 #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
    1078  (*CSC: FALSE, NEED INVARIANT? *)
    1079  > (?: nat_of_bitvector … (add 16 (bitvector_of_nat 16 (|l1|)) ppc)
    1080      = |l1| + nat_of_bitvector … ppc) [2: cases daemon]
     761 #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
     762 cut (|l1| + nat_of_bitvector … ppc < 2^16)
     763 [ @(transitive_lt … l1l2_ok) >length_append /2 by monotonic_lt_plus_r/ ]
     764 -l1l2_ok #l1ppc_ok >nat_of_bitvector_add
     765 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
     766 [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ]
    1081767 #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)
    1082768 #lbl #instr normalize nodelta >add_associative %
     
    1085771definition assembly:
    1086772    ∀p: pseudo_assembly_program.
     773    |\snd p| < 2^16 →
    1087774    ∀sigma: Word → Word.
    1088775    ∀policy: Word → bool.
     
    1103790            assembled K
    1104791
    1105   λp.
     792  λp. λinstr_list_ok.
    1106793  λsigma.
    1107794  λpolicy.
     
    1141828  | % // #ppc' #ppc_ok' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs) | skip]
    1142829  | cases ppc_code in p1; -ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; -EQppc_code
    1143     * #IH1 #IH2 % [ normalize nodelta >IH1 >length_append cases daemon (*CSC: TRUE, LEMMA NEEDED *)]
    1144     #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2
     830    * #IH1 #IH2 whd % [ normalize nodelta >IH1 >length_append cases daemon (*CSC: TRUE, LEMMA NEEDED *)]
     831    #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 #LTppc_ppc
    1145832    cases (le_to_or_lt_eq … LTppc')
    1146833    [2: #S_S_eq normalize nodelta in S_S_eq;
    1147834        (*CSC: FALSE, NEEDS INVARIANT *)
    1148         cut (ppc' = ppc) [cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc'  >prf
    1149         >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc #X lapply LTppc
     835        cut (ppc' = ppc) [ normalize nodelta in LTppc_ppc; >IH1 cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc'  >prf
     836        >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc lapply LTppc
    1150837        >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → match % with [_ ⇒ ?]);
    1151838        >fetch_pseudo_instruction_append
    1152         [3: @le_S_S @le_O_n |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H]
     839        [3: @le_S_S @le_O_n
     840        |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H
     841        |4: <prf <p_refl in instr_list_ok; #H @H ]
    1153842        #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2
    1154         #j #LTj
    1155         (* CSC: FALSE, NEEDS INVARIANT *)
    1156         >(?: nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … j)) =
    1157              nat_of_bitvector … (sigma ppc) + j) [2: cases daemon]
     843        #j #LTj >nat_of_bitvector_add
     844        >nat_of_bitvector_bitvector_of_nat_inverse
     845        [2,4: (* CSC: TRUE, NEEDS LEMMA, MAYBE ALREADY PROVED *) cases daemon
     846        |3: (* CSC: TRUE, NEEDS INVARIANT *) cases daemon ]
    1158847        >reverse_append >reverse_reverse
    1159         (* CSC: TRUE, NEEDS INVARIANT *)
     848        (* CSC: TRUE, NEEDS SAME INVARIANT *)
    1160849        >(? : nat_of_bitvector … (sigma ppc) = |reverse … code|) [2: cases daemon]
    1161850        @nth_safe_prepend
    1162     | #LTppc' #LT_ppc_ppc lapply (IH2 ppc' ?) [ (*CSC: EASY, FINISH*) cases daemon ]
     851    | #LTppc'' lapply (IH2 ppc' ?)
     852      [ @(transitive_le … LTppc'') @le_S_S // ]
    1163853      @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction
    1164854      @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH
     
    1166856      >eq_assembly_1_pseudoinstruction #j #LTj >reverse_append >reverse_reverse #K
    1167857      >IH
    1168       [2: (*CSC: FALSE, NEEDS INVARIANT? *) cases daemon
     858      [2: (*CSC: FALSE, NEEDS INVARIANT PPC'=PPC TO AVOID @PAIR_ELIM ABOVE? *) cases daemon
    1169859      | @shift_nth_prefix
    1170860      |3: >IH1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
Note: See TracChangeset for help on using the changeset viewer.