Ignore:
Timestamp:
Jun 16, 2011, 4:50:23 PM (9 years ago)
Author:
sacerdot
Message:

1) Major refactoring: proofs moved where they should be.
2) New build_map that never fails.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProof.ma

    r982 r985  
    11include "ASM/Assembly.ma".
    22include "ASM/Interpret.ma".
    3 
    43
    54definition bit_elim_prop: ∀P: bool → Prop. Prop ≝
    … …  
    3433qed.
    3534
    36 lemma eq_b_eq:
    37   ∀b, c.
    38     eq_b b c = true → b = c.
    39   #b #c
    40   cases b
    41   cases c
    42   normalize //
    43 qed.
    44 
    45 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
    46  #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
    47  #n #hd #tl #abs @⊥ //
    48 qed.
    49 
    50 lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
    51  ∃hd.∃tl.v ≃ VCons bool n hd tl.
    52  #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
    53  [ #abs @⊥ //
    54  | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
    55 qed.
    56 
    57 lemma eq_bv_eq:
    58   ∀n, v, q.
    59     eq_bv n v q = true → v = q.
    60   #n #v #q generalize in match v
    61   elim q
    62   [ #v #h @BitVector_O
    63   | #n #hd #tl #ih #v' #h
    64     cases (BitVector_Sn ? v')
    65     #hd' * #tl' #jmeq >jmeq in h;
    66     #new_h
    67     change in new_h with ((andb ? ?) = ?);
    68     cases(conjunction_true … new_h)
    69     #eq_heads #eq_tails
    70     whd in eq_heads:(??(??(%))?);
    71     cases(eq_b_eq … eq_heads)
    72     whd in eq_tails:(??(?????(%))?);
    73     change in eq_tails with (eq_bv ??? = ?);
    74     <(ih tl') //
    75   ]
    76 qed.
    77 
    7835lemma bool_eq_internal_eq:
    7936  ∀b, c.
    … …  
    8744    | normalize //
    8845    ]
    89   ]
    90 qed.
    91 
    92 lemma eq_bv_refl:
    93   ∀n,v. eq_bv n v v = true.
    94   #n #v
    95   elim v
    96   [ //
    97   | #n #hd #tl #ih
    98     normalize
    99     cases hd
    100     [ normalize
    101       @ ih
    102     | normalize
    103       @ ih
    104     ]
    105   ]
    106 qed.
    107 
    108 lemma eq_eq_bv:
    109   ∀n, v, q.
    110     v = q → eq_bv n v q = true.
    111   #n #v
    112   elim v
    113   [ #q #h <h normalize %
    114   | #n #hd #tl #ih #q #h >h //
    11546  ]
    11647qed.
    … …  
    623554qed.
    624555*)
    625 (*
    626 lemma test:
    627   let i ≝ SJMP (RELATIVE (bitvector_of_nat 8 255)) in
    628       (let assembled ≝ assembly1 i in
    629       let code_memory ≝ load_code_memory assembled in
    630       let fetched ≝ fetch code_memory ? in
    631       let 〈instr_pc, ticks〉 ≝ fetched in
    632         eq_instruction (\fst instr_pc)) i = true.
    633  [2: @ zero
    634  | normalize
    635  ]*)
    636 
    637 lemma BitVectorTrie_O:
    638  ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
    639  #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
    640   [ #w #_ %1 %[@w] %
    641   | #n #l #r #abs @⊥ //
    642   | #n #EQ %2 >EQ %]
    643 qed.
    644 
    645 lemma BitVectorTrie_Sn:
    646  ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
    647  #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
    648   [ #m #abs @⊥ //
    649   | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
    650   | #m #EQ %2 // ]
    651 qed.
    652 
    653 lemma lookup_prepare_trie_for_insertion_hit:
    654  ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
    655   lookup … b (prepare_trie_for_insertion … b v) a = v.
    656  #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
    657 qed.
    658  
    659 lemma lookup_insert_hit:
    660  ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
    661   lookup … b (insert … b v t) a = v.
    662  #A #a #v #n #b elim b -b -n //
    663  #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
    664   [ * #l * #r #JMEQ >JMEQ cases hd normalize //
    665   | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
    666 qed.
    667 
    668 coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
    669 
    670 lemma lookup_prepare_trie_for_insertion_miss:
    671  ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
    672   (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
    673  #A #a #v #n #c elim c
    674   [ #b >(BitVector_O … b) normalize #abs @⊥ //
    675   | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
    676     cases hd cases hd' normalize
    677     [2,3: #_ cases tl' //
    678     |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
    679 qed.
    680  
    681 lemma lookup_insert_miss:
    682  ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
    683   (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
    684  #A #a #v #n #c elim c -c -n
    685   [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
    686   | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
    687     #t cases(BitVectorTrie_Sn … t)
    688     [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
    689      [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
    690     | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
    691      [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
    692      [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
    693 qed.
    694556
    695557definition load_code_memory_aux ≝
    … …  
    702564  (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
    703565
    704 axiom half_add_SO:
     566example half_add_SO:
    705567 ∀pc.
    706568 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
     569 cases daemon.
     570qed.
    707571
    708572(*
    … …  
    724588qed.
    725589*)
    726 
    727 
    728 
    729590
    730591(*
    … …  
    817678qed.
    818679
    819 axiom eq_bv_to_eq: ∀n.∀v1,v2: BitVector n. eq_bv … v1 v2 = true → v1=v2.
    820 
    821680axiom eq_instruction_to_eq: ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2.
    822681
    … …  
    840699    cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %)
    841700    cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1
    842     cases (conjunction_true … K1) -K1; #K1 #K2 #K3 % try % //
    843     [ @eqb_true_to_eq <(eq_instruction_to_eq … K1) // | >(eq_bv_to_eq … K3) @IH @H2 ]
    844 qed.
    845 
    846 (* This establishes the correspondence between pseudo program counters and
    847    program counters. It is at the heart of the proof. *)
    848 (*CSC: code taken from build_maps *)
    849 definition sigma00: pseudo_assembly_program → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
    850  λinstr_list.λl:list labelled_instruction.
    851   foldl ??
    852    (λt,i.
    853        match t with
    854        [ None ⇒ None ?
    855        | Some ppc_pc_map ⇒
    856          let 〈ppc,pc_map〉 ≝ ppc_pc_map in
    857          let 〈program_counter, sigma_map〉 ≝ pc_map in
    858          let 〈label, i〉 ≝ i in
    859           match construct_costs instr_list ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
    860            [ None ⇒ None ?
    861            | Some pc_ignore ⇒
    862               let 〈pc,ignore〉 ≝ pc_ignore in
    863               Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
    864        ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l.
    865 
    866 definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16)))
    867  ≝ λprog.sigma00 prog (\snd prog).
    868 
    869 definition tech_pc_sigma00: pseudo_assembly_program → list labelled_instruction → option (nat × nat) ≝
    870  λprogram,instr_list.
    871   match sigma00 program instr_list with
    872    [ None ⇒ None …
    873    | Some result ⇒
    874       let 〈ppc,pc_sigma_map〉 ≝ result in
    875       let 〈pc,map〉 ≝ pc_sigma_map in
    876        Some … 〈ppc,pc〉 ].
    877 
    878 definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝       
    879  λinstr_list.
    880   match sigma0 instr_list with
    881   [ None ⇒ None ?
    882   | Some result ⇒
    883     let 〈ppc,pc_sigma_map〉 ≝ result in
    884     let 〈pc, sigma_map〉 ≝ pc_sigma_map in
    885       if gtb pc (2^16) then
    886         None ?
    887       else
    888         Some ? (λx.lookup ?? x sigma_map (zero …)) ].
    889 
    890 (* stuff about policy *)
    891 
    892 lemma policy_ok: ∀p. sigma_safe p ≠ None ….
    893  #instr_list whd in match (sigma_safe ?) whd in match (sigma0 ?)
    894  
    895 definition sigma: pseudo_assembly_program → Word → Word ≝
    896  λp.
    897   match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with
    898    [ None ⇒ λabs. ⊥
    899    | Some r ⇒ λ_.r] (policy_ok p).
    900  cases abs //
    901 qed.
    902 
    903 lemma length_append:
    904  ∀A.∀l1,l2:list A.
    905   |l1 @ l2| = |l1| + |l2|.
    906  #A #l1 elim l1
    907   [ //
    908   | #hd #tl #IH #l2 normalize <IH //]
    909 qed.
    910 
    911 let rec does_not_occur (id:Identifier) (l:list labelled_instruction) on l: bool ≝
    912  match l with
    913   [ nil ⇒ true
    914   | cons hd tl ⇒ notb (instruction_matches_identifier id hd) ∧ does_not_occur id tl].
    915 
    916 lemma does_not_occur_None:
    917  ∀id,i,list_instr.
    918   does_not_occur id (list_instr@[〈None …,i〉]) =
    919   does_not_occur id list_instr.
    920  #id #i #list_instr elim list_instr
    921   [ % | #hd #tl #IH whd in ⊢ (??%%) >IH %]
    922 qed.
    923 
    924 lemma does_not_occur_Some:
    925  ∀id,id',i,list_instr.
    926   eq_bv ? id' id = false →
    927    does_not_occur id (list_instr@[〈Some ? id',i〉]) =
    928     does_not_occur id list_instr.
    929  #id #id' #i #list_instr elim list_instr
    930   [ #H normalize in H ⊢ %; >H %
    931   | * #x #i' #tl #IH #H whd in ⊢ (??%%) >(IH H) %]
    932 qed.
    933 
    934 lemma does_not_occur_absurd:
    935  ∀id,i,list_instr.
    936   does_not_occur id (list_instr@[〈Some ? id,i〉]) = false.
    937  #id #i #list_instr elim list_instr
    938   [ normalize change with (if (if eq_bv ??? then ? else ?) then ? else ? = ?)
    939     >eq_bv_refl %
    940   | * #x #i' #tl #IH whd in ⊢ (??%%) >IH cases (notb ?) %]
    941 qed.
    942 
    943 let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝
    944  match l with
    945   [ nil ⇒ false
    946   | cons hd tl ⇒
    947      if instruction_matches_identifier id hd then
    948       does_not_occur id tl
    949      else
    950       occurs_exactly_once id tl ].
    951 
    952 lemma occurs_exactly_once_None:
    953  ∀id,i,list_instr.
    954   occurs_exactly_once id (list_instr@[〈None …,i〉]) =
    955   occurs_exactly_once id list_instr.
    956  #id #i #list_instr elim list_instr
    957   [ % | #hd #tl #IH whd in ⊢ (??%%) >IH >does_not_occur_None %]
    958 qed.
    959 
    960 lemma occurs_exactly_once_Some:
    961  ∀id,id',i,prefix.
    962   occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_bv ? id' id ∨ occurs_exactly_once id prefix.
    963  #id #id' #i #prefix elim prefix
    964   [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
    965     change with (? → eq_v ?? eq_b id' id ∨ ?) cases (eq_v ?????) normalize nodelta; /2/
    966   | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
    967     cases he; normalize nodelta
    968      [ #H @ (IH H)
    969      | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
    970        change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv ???) normalize nodelta;
    971        [generalize in match (refl … (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
    972         /2/ #H >does_not_occur_Some //
    973        | #H @IH @H]]]
    974 qed.
    975 
    976 lemma index_of_internal_None: ∀i,id,instr_list,n.
    977  occurs_exactly_once id (instr_list@[〈None …,i〉]) →
    978   index_of_internal ? (instruction_matches_identifier id) instr_list n =
    979    index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
    980  #i #id #instr_list elim instr_list
    981   [ #n #abs whd in abs; cases abs
    982   | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
    983     cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
    984     [ #H %
    985     | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %
    986       [ #_ % | #abs cases abs ]]]
    987 qed.
    988 
    989 lemma index_of_internal_Some_miss: ∀i,id,id'.
    990  eq_bv ? id' id = false →
    991  ∀instr_list,n.
    992  occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
    993   index_of_internal ? (instruction_matches_identifier id) instr_list n =
    994    index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id',i〉]) n.
    995  #i #id #id' #EQ #instr_list #n #H generalize in match (occurs_exactly_once_Some … H) in ⊢ ?; >EQ
    996  change with (occurs_exactly_once ?? → ?) generalize in match n; -n H; elim instr_list
    997   [ #n #abs cases abs
    998   | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
    999     [ // | #K @IH //]]
    1000 qed.
    1001 
    1002 lemma index_of_internal_Some_hit: ∀i,id.
    1003  ∀instr_list,n.
    1004   occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
    1005    index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id,i〉]) n
    1006   = |instr_list| + n.
    1007  #i #id #instr_list elim instr_list
    1008   [ #n #_ whd in ⊢ (??%%) change with (if eq_bv … id id then ? else ? = ?) >eq_bv_refl %
    1009   | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
    1010     [ >does_not_occur_absurd #abs cases abs | #H applyS (IH (S n)) //]]
    1011 qed.
    1012 
    1013 lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
    1014  occurs_exactly_once id (instr_list@[〈None …,i〉]) →
    1015   address_of_word_labels_code_mem instr_list id =
    1016   address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
    1017  #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
    1018  >(index_of_internal_None … H) %
    1019 qed.
    1020 
    1021 lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
    1022  eq_bv ? id' id = false →
    1023   occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
    1024    address_of_word_labels_code_mem instr_list id =
    1025    address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
    1026  #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
    1027  >(index_of_internal_Some_miss … H) //
    1028 qed.
    1029 
    1030 lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
    1031   occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
    1032    address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
    1033    = bitvector_of_nat … (|instr_list|).
    1034  #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)?)
    1035  >(index_of_internal_Some_hit … H) //
    1036 qed.
    1037 
    1038 axiom tech_pc_sigma00_append_Some:
    1039  ∀program,prefix,costs,label,i,pc',code,ppc,pc.
    1040   tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
    1041    construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
    1042     tech_pc_sigma00 program (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉.
    1043 
    1044 axiom tech_pc_sigma00_append_None:
    1045  ∀program,prefix,i,ppc,pc,costs.
    1046   tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
    1047    construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
    1048     → False.
    1049 
    1050 lemma eq_false_to_notb: ∀b. b = false → ¬ b.
    1051  *; //
    1052 qed.
    1053 
    1054 lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1.
    1055  #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/]
    1056 qed.
    1057 
    1058 example sigma_0: ∀p. sigma p (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
    1059  cases daemon.
    1060 qed.
    1061 
    1062 axiom construct_costs_sigma:
    1063  ∀p,ppc,pc,pc',costs,costs',i.
    1064   bitvector_of_nat ? pc = sigma p (bitvector_of_nat ? ppc) →
    1065    Some … 〈pc',costs'〉 = construct_costs p ppc pc (λx.zero 16) (λx.zero 16) costs i →
    1066     bitvector_of_nat ? pc' = sigma p (bitvector_of_nat 16 (S ppc)).
    1067 
    1068 definition build_maps' ≝
    1069   λpseudo_program.
    1070   let result ≝
    1071    foldl_strong
    1072     (option Identifier × pseudo_instruction)
    1073     (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))).
    1074       let 〈labels,ppc_pc_costs〉 ≝ res in
    1075       let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
    1076       let 〈pc',costs〉 ≝ pc_costs in
    1077        bitvector_of_nat ? pc' = sigma pseudo_program (bitvector_of_nat ? ppc') ∧
    1078        ppc' = length … pre ∧
    1079        tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧
    1080        ∀id. occurs_exactly_once id pre →
    1081         lookup ?? id labels (zero …) = sigma pseudo_program (address_of_word_labels_code_mem pre id))
    1082     (\snd pseudo_program)
    1083     (λprefix,i,tl,prf,t.
    1084       let 〈labels, ppc_pc_costs〉 ≝ t in
    1085       let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
    1086       let 〈pc,costs〉 ≝ pc_costs in
    1087        let 〈label, i'〉 ≝ i in
    1088        let labels ≝
    1089          match label with
    1090          [ None ⇒ labels
    1091          | Some label ⇒
    1092            let program_counter_bv ≝ bitvector_of_nat ? pc in
    1093              insert ? ? label program_counter_bv labels
    1094          ]
    1095        in
    1096          match construct_costs pseudo_program ppc pc (λx. zero ?) (λx. zero ?) costs i' with
    1097          [ None ⇒
    1098             let dummy ≝ 〈labels,ppc_pc_costs〉 in
    1099              dummy
    1100          | Some construct ⇒ 〈labels, 〈S ppc,construct〉〉
    1101          ]
    1102     ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉
    1103   in
    1104    let 〈labels, ppc_pc_costs〉 ≝ result in
    1105    let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
    1106    let 〈pc, costs〉 ≝ pc_costs in
    1107     〈labels, costs〉.
    1108  [3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
    1109  | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
    1110    cases construct in p4 #PC #CODE #JMEQ % [% [%]]
    1111    [ @(construct_costs_sigma … IHn1) [4: <JMEQ % |*: skip]
    1112    | >length_append <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
    1113    | @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ))
    1114    | #id normalize nodelta; -labels1; cases label; normalize nodelta
    1115      [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
    1116      | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
    1117        generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
    1118         [ #EQ #_ <(eq_bv_to_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
    1119           <IH0 [@IHn1 | <(eq_bv_to_eq … EQ) in H #H @H]
    1120         | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]
    1121           <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
    1122  | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2
    1123    @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]
    1124 qed.
    1125 
    1126 lemma build_maps_ok:
    1127  ∀p:pseudo_assembly_program.
    1128   let 〈labels,costs〉 ≝ build_maps' p in
    1129    ∀pc.
    1130     (nat_of_bitvector … pc) < length … (\snd p) →
    1131      lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)).
    1132  #p cases p #preamble #instr_list
    1133   elim instr_list
    1134    [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ]
    1135    | #hd #tl #IH
    1136     whd in ⊢ (match % with [ _ ⇒ ?])
    1137    ]
    1138 qed.
    1139 *)
     701    cases (conjunction_true … K1) -K1; #K1 #K2 #K3 % try %
     702    [ @K1 | @eqb_true_to_eq <(eq_instruction_to_eq … K1) @K2 | >(eq_bv_eq … K3) @IH @H2 ]
     703qed.
    1140704
    1141705(*
    … …  
    1211775lemma app_assoc: ∀A,l1,l2,l3. app A (app A l1 l2) l3 = app A l1 (l2@l3).
    1212776 #A * #l1 normalize //
    1213 qed.
    1214 
    1215 let rec foldli (A: Type[0]) (B: Propify (list A) → Type[0])
    1216  (f: ∀prefix. B prefix → ∀x.B (app … prefix [x]))
    1217  (prefix: Propify (list A)) (b: B prefix) (l: list A) on l :
    1218  B (app … prefix l) ≝
    1219   match l with
    1220   [ nil ⇒ ? (* b *)
    1221   | cons hd tl ⇒ ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
    1222   ].
    1223  [ applyS b
    1224  | <(app_assoc ?? [hd]) @(foldli A B f (app … prefix [hd]) (f prefix b hd) tl) ]
    1225 qed.
    1226 
    1227 (*
    1228 let rec foldli (A: Type[0]) (B: list A → Type[0]) (f: ∀prefix. B prefix → ∀x. B (prefix@[x]))
    1229  (prefix: list A) (b: B prefix) (l: list A) on l : B (prefix@l) ≝
    1230   match l with
    1231   [ nil ⇒ ? (* b *)
    1232   | cons hd tl ⇒
    1233      ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
    1234   ].
    1235  [ applyS b
    1236  | applyS (foldli A B f (prefix@[hd]) (f prefix b hd) tl) ]
    1237777qed.
    1238778*)
    1239779
    1240 definition foldll:
    1241  ∀A:Type[0].∀B: Propify (list A) → Type[0].
    1242   (∀prefix. B prefix → ∀x. B (app … prefix [x])) →
    1243    B (mk_Propify … []) → ∀l: list A. B (mk_Propify … l)
    1244  ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
    1245 
    1246 axiom is_pprefix: ∀A:Type[0]. Propify (list A) → list A → Prop.
    1247 axiom pprefix_of_append:
    1248  ∀A:Type[0].∀l,l1,l2.
    1249   is_pprefix A l l1 → is_pprefix A l (l1@l2).
    1250 axiom pprefix_reflexive: ∀A,l. is_pprefix A (mk_Propify … l) l.
    1251 axiom nil_pprefix: ∀A,l. is_pprefix A (mk_Propify … [ ]) l.
    1252 
    1253 
    1254 axiom foldll':
    1255  ∀A:Type[0].∀l: list A.
    1256   ∀B: ∀prefix:Propify (list A). is_pprefix ? prefix l → Type[0].
    1257   (∀prefix,proof. B prefix proof → ∀x,proof'. B (app … prefix [x]) proof') →
    1258    B (mk_Propify … [ ]) (nil_pprefix …) → B (mk_Propify … l) (pprefix_reflexive … l).
    1259  #A #l #B
    1260  generalize in match (foldll A (λprefix. is_pprefix ? prefix l)) #HH
    1261  
    1262  
    1263   #H #acc
    1264  @foldll
    1265   [
    1266   |
    1267   ]
    1268  
    1269  ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
    1270 
    1271 
    1272 (*
    1273 record subset (A:Type[0]) (P: A → Prop): Type[0] ≝
    1274  { subset_wit:> A;
    1275    subset_proof: P subset_wit
    1276  }.
    1277 *)
    1278 
    1279 definition build_maps' ≝
    1280   λpseudo_program.
    1281   let 〈preamble,instr_list〉 ≝ pseudo_program in
    1282   let result ≝
    1283    foldll
    1284     (option Identifier × pseudo_instruction)
    1285     (λprefix.
    1286       Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
    1287        match prefix return λ_.Prop with [mk_Propify prefix ⇒ tech_pc_sigma0 〈preamble,prefix〉 ≠ None ?])
    1288     (λprefix,t,i.
    1289       let 〈labels, pc_costs〉 ≝ t in
    1290       let 〈program_counter, costs〉 ≝ pc_costs in
    1291        let 〈label, i'〉 ≝ i in
    1292        let labels ≝
    1293          match label with
    1294          [ None ⇒ labels
    1295          | Some label ⇒
    1296            let program_counter_bv ≝ bitvector_of_nat ? program_counter in
    1297              insert ? ? label program_counter_bv labels
    1298          ]
    1299        in
    1300          match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
    1301          [ None ⇒
    1302             let dummy ≝ 〈labels,pc_costs〉 in
    1303               dummy
    1304          | Some construct ⇒ 〈labels, construct〉
    1305          ]
    1306     ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list
    1307   in
    1308    let 〈labels, pc_costs〉 ≝ result in
    1309    let 〈pc, costs〉 ≝ pc_costs in
    1310     〈labels, costs〉.
    1311  [
    1312  | @⊥
    1313  | normalize % //
    1314  ]
    1315 qed.
    1316 
    1317 definition build_maps' ≝
    1318   λpseudo_program.
    1319   let 〈preamble,instr_list〉 ≝ pseudo_program in
    1320   let result ≝
    1321    foldl
    1322     (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
    1323           ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
    1324            tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)))
    1325     (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
    1326           let instr_list_prefix' ≝ instr_list_prefix @ [i] in
    1327            is_prefix ? instr_list_prefix' instr_list →
    1328            tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)
    1329     (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
    1330           ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
    1331            tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)).
    1332      λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
    1333           let instr_list_prefix' ≝ instr_list_prefix @ [i] in
    1334            is_prefix ? instr_list_prefix' instr_list →
    1335            tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .
    1336       let 〈labels, pc_costs〉 ≝ t in
    1337       let 〈program_counter, costs〉 ≝ pc_costs in
    1338        let 〈label, i'〉 ≝ i in
    1339        let labels ≝
    1340          match label with
    1341          [ None ⇒ labels
    1342          | Some label ⇒
    1343            let program_counter_bv ≝ bitvector_of_nat ? program_counter in
    1344              insert ? ? label program_counter_bv labels
    1345          ]
    1346        in
    1347          match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
    1348          [ None ⇒
    1349             let dummy ≝ 〈labels,pc_costs〉 in
    1350               dummy
    1351          | Some construct ⇒ 〈labels, construct〉
    1352          ]
    1353     ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*)
    1354   in
    1355    let 〈labels, pc_costs〉 ≝ result in
    1356    let 〈pc, costs〉 ≝ pc_costs in
    1357     〈labels, costs〉.
    1358  [4: @(list_elim_rev ?
    1359        (λinstr_list. list (
    1360         (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
    1361           let instr_list_prefix' ≝ instr_list_prefix @ [i] in
    1362            is_prefix ? instr_list_prefix' instr_list →
    1363            tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)))
    1364        ?? instr_list) (* CSC: BAD ORDER FOR CODE EXTRACTION *)
    1365       [ @[ ]
    1366       | #l' #a #limage %2
    1367         [ %[@a] #PREFIX #PREFIX_OK
    1368         | (* CSC: EVEN WORST CODE FOR EXTRACTION: WE SHOULD STRENGTHEN
    1369              THE INDUCTION HYPOTHESIS INSTEAD *)
    1370           elim limage
    1371            [ %1
    1372            | #HD #TL #IH @(?::IH) cases HD #ELEM #K1 %[@ELEM] #K2 #K3
    1373              @K1 @(prefix_of_append ???? K3)
    1374            ] 
    1375         ]
    1376        
    1377        
    1378      
    1379  
    1380   cases t in c2 ⊢ % #t' * #LIST_PREFIX * #H1t' #H2t' #HJMt'
    1381      % [@ (LIST_PREFIX @ [i])] %
    1382       [ cases (sig2 … i LIST_PREFIX) #K1 #K2 @K1
    1383       | (* DOABLE IN PRINCIPLE *)
    1384       ]
    1385  | (* assert false case *)
    1386  |3: % [@ ([ ])] % [2: % | (* DOABLE *)]
    1387  |   
    1388 *)
    1389 
    1390780axiom assembly_ok:
    1391  ∀program,assembled,costs,labels.
    1392   Some … 〈labels,costs〉 = build_maps program →
     781 ∀program,assembled.
     782  let 〈labels,costs〉 ≝ build_maps program in
    1393783  Some … 〈assembled,costs〉 = assembly program →
    1394784  let code_memory ≝ load_code_memory assembled in
    … …  
    1421811      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi.
    1422812
     813axiom pair_elim':
     814  ∀A,B,C: Type[0].
     815  ∀T: A → B → C.
     816  ∀p.
     817  ∀P: A×B → C → Prop.
     818    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
     819      P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
     820
     821axiom pair_elim'':
     822  ∀A,B,C,C': Type[0].
     823  ∀T: A → B → C.
     824  ∀T': A → B → C'.
     825  ∀p.
     826  ∀P: A×B → C → C' → Prop.
     827    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
     828      P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
     829
     830axiom split_elim':
     831  ∀A: Type[0].
     832  ∀B: Type[1].
     833  ∀l, m, v.
     834  ∀T: Vector A l → Vector A m → B.
     835  ∀P: B → Prop.
     836    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
     837      P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt).
     838
     839axiom split_elim'':
     840  ∀A: Type[0].
     841  ∀B,B': Type[1].
     842  ∀l, m, v.
     843  ∀T: Vector A l → Vector A m → B.
     844  ∀T': Vector A l → Vector A m → B'.
     845  ∀P: B → B' → Prop.
     846    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
     847      P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt)
     848        (let 〈lft, rgt〉 ≝ split A l m v in T' lft rgt).
     849
    1423850lemma fetch_assembly_pseudo2:
    1424  ∀program,assembled,costs,labels.
    1425   Some … 〈labels,costs〉 = build_maps program →
     851 ∀program,assembled.
     852  let 〈labels,costs〉 ≝ build_maps program in
    1426853  Some … 〈assembled,costs〉 = assembly program →
    1427854   ∀ppc.
    … …  
    1436863      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi ∧
    1437864       fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions.
    1438  #program #assembled #costs #labels #BUILD_MAPS #ASSEMBLY #ppc
     865 #program #assembled @pair_elim' #labels #costs #BUILD_MAPS #ASSEMBLY #ppc
    1439866 generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program assembled costs ASSEMBLY ppc)
    1440867 letin code_memory ≝ (load_code_memory assembled)
    … …  
    1443870 letin lookup_labels ≝ (λx. sigma program (address_of_word_labels_code_mem (\snd program) x))
    1444871 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
    1445  whd in ⊢ (% → %)
    1446  generalize in match (assembly_ok … BUILD_MAPS ASSEMBLY ppc)
     872 whd in ⊢ (% → %) generalize in match (assembly_ok program assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX;
    1447873 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
    1448874 generalize in match (fetch_assembly_pseudo program ppc
    … …  
    22621688qed.
    22631689
    2264 axiom pair_elim':
    2265   ∀A,B,C: Type[0].
    2266   ∀T: A → B → C.
    2267   ∀p.
    2268   ∀P: A×B → C → Prop.
    2269     (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
    2270       P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
    2271 
    2272 axiom pair_elim'':
    2273   ∀A,B,C,C': Type[0].
    2274   ∀T: A → B → C.
    2275   ∀T': A → B → C'.
    2276   ∀p.
    2277   ∀P: A×B → C → C' → Prop.
    2278     (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
    2279       P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
    2280 
    2281 axiom split_elim':
    2282   ∀A: Type[0].
    2283   ∀B: Type[1].
    2284   ∀l, m, v.
    2285   ∀T: Vector A l → Vector A m → B.
    2286   ∀P: B → Prop.
    2287     (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
    2288       P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt).
    2289 
    2290 axiom split_elim'':
    2291   ∀A: Type[0].
    2292   ∀B,B': Type[1].
    2293   ∀l, m, v.
    2294   ∀T: Vector A l → Vector A m → B.
    2295   ∀T': Vector A l → Vector A m → B'.
    2296   ∀P: B → B' → Prop.
    2297     (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
    2298       P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt)
    2299         (let 〈lft, rgt〉 ≝ split A l m v in T' lft rgt).
    2300 
    23011690axiom split_append:
    23021691  ∀A: Type[0].
    … …  
    23171706    ((get_index_v A ? v 0 prf) ::: rest) = v.
    23181707
    2319 axiom sub_minus_one_seven_eight:
     1708example sub_minus_one_seven_eight:
    23201709  ∀v: BitVector 7.
    23211710  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
    23221711  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
     1712 cases daemon.
     1713qed.
    23231714
    23241715lemma pair_destruct_1:
    … …  
    24161807 generalize in match (assembly (code_memory … ps)) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?)
    24171808 cases (build_maps (code_memory … ps))
    2418   [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H #MAP
    2419     #abs @⊥ normalize in abs; destruct (abs) ]
    2420  * #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?)
     1809 #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?)
    24211810 generalize in match (refl … (code_memory … ps)) cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta;
    24221811 generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta;
    24231812  [ #EQ >EQ #_ #_ #abs @⊥ normalize in abs; destruct (abs) ]
    24241813 * #final_ppc * #final_pc #assembled #EQ >EQ -EQ ASS; normalize nodelta;
    2425  #H generalize in match (H ??? (refl …) (refl …)) -H; #H;
     1814 #H generalize in match (H ? (refl …)) -H; #H;
    24261815 #MAP
    24271816 #H1 generalize in match (option_destruct_Some ??? H1) -H1; #H1 <H1 -H1;
    … …  
    24621851    generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP M';
    24631852    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    2464     #H2 >(eq_bv_to_eq … H2) >EQ %
     1853    #H2 >(eq_bv_eq … H2) >EQ %
    24651854(*  |6: (* Mov *) #arg1 #arg2
    24661855       #H1 #H2 #EQ %[@1]
    … …  
    24761865       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
    24771866       #result #flags
    2478        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) % *)
     1867       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) % *)
    24791868  |5: (* Call *) #label #MAP
    24801869      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
    … …  
    24901879           whd in ⊢ (???% → ??%?);
    24911880           generalize in match (refl … (half_add 8 (get_8051_sfr ? ps SFR_SP) (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry #new_sp #EQ1 normalize nodelta;
    2492            >(eq_bv_to_eq … H2c)
     1881           >(eq_bv_eq … H2c)
    24931882           change with
    24941883            ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
    … …  
    24991888           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
    25001889           generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
    2501            #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
     1890           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
    25021891           @split_eq_status;
    25031892            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
    … …  
    25561945              >clock_write_at_stack_pointer whd in ⊢ (???%)
    25571946              >clock_write_at_stack_pointer %]
    2558        | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
     1947       (*| (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
    25591948         @pair_elim' #fst_5_addr #rest_addr #EQ1
    25601949         @pair_elim' #fst_5_pc #rest_pc #EQ2
    … …  
    25651954         @pair_elim' * #instr #newppc' #ticks #EQn
    25661955          * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
    2567           generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
     1956          generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_eq … H2c)
    25681957          @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
    25691958          @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
    … …  
    25731962          >get_8051_sfr_set_8051_sfr
    25741963         
    2575           whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?)
     1964          whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
    25761965           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
    25771966           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
    … …  
    25911980              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
    25921981            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
    2593               @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)
     1982              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)]
    25941983  |4: (* Jmp *) #label #MAP
    25951984      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
    … …  
    26021991           >H2b >(eq_instruction_to_eq … H2a)
    26031992           generalize in match EQ; -EQ;
    2604            #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
     1993           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
    26051994           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
    26061995       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
    … …  
    26222011           generalize in match EQ; -EQ;
    26232012           whd in ⊢ (???% → ?);
    2624            #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
     2013           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
    26252014           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ??) ? in ?) = ?)
    26262015           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 newppc) (sign_extension lower)))
    … …  
    26462035           generalize in match EQ; -EQ;
    26472036           whd in ⊢ (???% → ?);
    2648            #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?)
     2037           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
    26492038           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
    26502039           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
    … …  
    26832072             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
    26842073             false (DIRECT ARG2))
    2685            ? in ?) = ?)
     2074           ? in ?) = ?) //
    26862075       [1,2: cut (addressing_mode_ok M ps (DIRECT ARG2) = true) [2:
    26872076        [1,2:whd in MAP:(??(match % with [ _ ⇒ ? | _ ⇒ ?])?)]
    26882077       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
    26892078       #result #flags
    2690        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) %
    2691     | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
     2079       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
     2080    (*| (* INC *) #arg1 #H1 #H2 #EQ %[@1]
    26922081       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    26932082       change in ⊢ (? → ??%?) with (execute_1_0 ??)
    … …  
    27002089       | cases (half_add ???) #carry #bl normalize nodelta;
    27012090         cases (full_add ????) #carry' #bu normalize nodelta ]
    2702         #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) -newppc';
     2091        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) -newppc';
    27032092        [5: %
    27042093        |1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
    … …  
    27212110            [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
    27222111            |
    2723             ]
     2112            ] *)
Note: See TracChangeset for help on using the changeset viewer.