Changeset 985 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 16, 2011, 4:50:23 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r982 r985 1 1 include "ASM/Assembly.ma". 2 2 include "ASM/Interpret.ma". 3 4 3 5 4 definition bit_elim_prop: ∀P: bool → Prop. Prop ≝ … … 34 33 qed. 35 34 36 lemma eq_b_eq:37 ∀b, c.38 eq_b b c = true → b = c.39 #b #c40 cases b41 cases c42 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 v61 elim q62 [ #v #h @BitVector_O63  #n #hd #tl #ih #v' #h64 cases (BitVector_Sn ? v')65 #hd' * #tl' #jmeq >jmeq in h;66 #new_h67 change in new_h with ((andb ? ?) = ?);68 cases(conjunction_true … new_h)69 #eq_heads #eq_tails70 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 78 35 lemma bool_eq_internal_eq: 79 36 ∀b, c. … … 87 44  normalize // 88 45 ] 89 ]90 qed.91 92 lemma eq_bv_refl:93 ∀n,v. eq_bv n v v = true.94 #n #v95 elim v96 [ //97  #n #hd #tl #ih98 normalize99 cases hd100 [ normalize101 @ ih102  normalize103 @ ih104 ]105 ]106 qed.107 108 lemma eq_eq_bv:109 ∀n, v, q.110 v = q → eq_bv n v q = true.111 #n #v112 elim v113 [ #q #h <h normalize %114  #n #hd #tl #ih #q #h >h //115 46 ] 116 47 qed. … … 623 554 qed. 624 555 *) 625 (*626 lemma test:627 let i ≝ SJMP (RELATIVE (bitvector_of_nat 8 255)) in628 (let assembled ≝ assembly1 i in629 let code_memory ≝ load_code_memory assembled in630 let fetched ≝ fetch code_memory ? in631 let 〈instr_pc, ticks〉 ≝ fetched in632 eq_instruction (\fst instr_pc)) i = true.633 [2: @ zero634  normalize635 ]*)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 c674 [ #b >(BitVector_O … b) normalize #abs @⊥ //675  #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ676 cases hd cases hd' normalize677 [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 n685 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //686  #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ687 #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 ???))) ] normalize692 [3,4: cases tl' //  *: @lookup_prepare_trie_for_insertion_miss //]]]693 qed.694 556 695 557 definition load_code_memory_aux ≝ … … 702 564 (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v). 703 565 704 axiomhalf_add_SO:566 example half_add_SO: 705 567 ∀pc. 706 568 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc). 569 cases daemon. 570 qed. 707 571 708 572 (* … … 724 588 qed. 725 589 *) 726 727 728 729 590 730 591 (* … … 817 678 qed. 818 679 819 axiom eq_bv_to_eq: ∀n.∀v1,v2: BitVector n. eq_bv … v1 v2 = true → v1=v2.820 821 680 axiom eq_instruction_to_eq: ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2. 822 681 … … 840 699 cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %) 841 700 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 ] 703 qed. 1140 704 1141 705 (* … … 1211 775 lemma app_assoc: ∀A,l1,l2,l3. app A (app A l1 l2) l3 = app A l1 (l2@l3). 1212 776 #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 with1220 [ nil ⇒ ? (* b *)1221  cons hd tl ⇒ ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)1222 ].1223 [ applyS b1224  <(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 with1231 [ nil ⇒ ? (* b *)1232  cons hd tl ⇒1233 ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)1234 ].1235 [ applyS b1236  applyS (foldli A B f (prefix@[hd]) (f prefix b hd) tl) ]1237 777 qed. 1238 778 *) 1239 779 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 #B1260 generalize in match (foldll A (λprefix. is_pprefix ? prefix l)) #HH1261 1262 1263 #H #acc1264 @foldll1265 [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_wit1276 }.1277 *)1278 1279 definition build_maps' ≝1280 λpseudo_program.1281 let 〈preamble,instr_list〉 ≝ pseudo_program in1282 let result ≝1283 foldll1284 (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 in1290 let 〈program_counter, costs〉 ≝ pc_costs in1291 let 〈label, i'〉 ≝ i in1292 let labels ≝1293 match label with1294 [ None ⇒ labels1295  Some label ⇒1296 let program_counter_bv ≝ bitvector_of_nat ? program_counter in1297 insert ? ? label program_counter_bv labels1298 ]1299 in1300 match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with1301 [ None ⇒1302 let dummy ≝ 〈labels,pc_costs〉 in1303 dummy1304  Some construct ⇒ 〈labels, construct〉1305 ]1306 ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list1307 in1308 let 〈labels, pc_costs〉 ≝ result in1309 let 〈pc, costs〉 ≝ pc_costs in1310 〈labels, costs〉.1311 [1312  @⊥1313  normalize % //1314 ]1315 qed.1316 1317 definition build_maps' ≝1318 λpseudo_program.1319 let 〈preamble,instr_list〉 ≝ pseudo_program in1320 let result ≝1321 foldl1322 (Σ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] in1327 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] in1334 is_prefix ? instr_list_prefix' instr_list →1335 tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .1336 let 〈labels, pc_costs〉 ≝ t in1337 let 〈program_counter, costs〉 ≝ pc_costs in1338 let 〈label, i'〉 ≝ i in1339 let labels ≝1340 match label with1341 [ None ⇒ labels1342  Some label ⇒1343 let program_counter_bv ≝ bitvector_of_nat ? program_counter in1344 insert ? ? label program_counter_bv labels1345 ]1346 in1347 match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with1348 [ None ⇒1349 let dummy ≝ 〈labels,pc_costs〉 in1350 dummy1351  Some construct ⇒ 〈labels, construct〉1352 ]1353 ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*)1354 in1355 let 〈labels, pc_costs〉 ≝ result in1356 let 〈pc, costs〉 ≝ pc_costs in1357 〈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] in1362 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 %21367 [ %[@a] #PREFIX #PREFIX_OK1368  (* CSC: EVEN WORST CODE FOR EXTRACTION: WE SHOULD STRENGTHEN1369 THE INDUCTION HYPOTHESIS INSTEAD *)1370 elim limage1371 [ %11372  #HD #TL #IH @(?::IH) cases HD #ELEM #K1 %[@ELEM] #K2 #K31373 @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 @K11383  (* DOABLE IN PRINCIPLE *)1384 ]1385  (* assert false case *)1386 3: % [@ ([ ])] % [2: %  (* DOABLE *)]1387 1388 *)1389 1390 780 axiom 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 1393 783 Some … 〈assembled,costs〉 = assembly program → 1394 784 let code_memory ≝ load_code_memory assembled in … … 1421 811 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi. 1422 812 813 axiom 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 821 axiom 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 830 axiom 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 839 axiom 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 1423 850 lemma 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 1426 853 Some … 〈assembled,costs〉 = assembly program → 1427 854 ∀ppc. … … 1436 863 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi ∧ 1437 864 fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions. 1438 #program #assembled #costs #labels #BUILD_MAPS #ASSEMBLY #ppc865 #program #assembled @pair_elim' #labels #costs #BUILD_MAPS #ASSEMBLY #ppc 1439 866 generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program assembled costs ASSEMBLY ppc) 1440 867 letin code_memory ≝ (load_code_memory assembled) … … 1443 870 letin lookup_labels ≝ (λx. sigma program (address_of_word_labels_code_mem (\snd program) x)) 1444 871 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; 1447 873 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc 1448 874 generalize in match (fetch_assembly_pseudo program ppc … … 2262 1688 qed. 2263 1689 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 2301 1690 axiom split_append: 2302 1691 ∀A: Type[0]. … … 2317 1706 ((get_index_v A ? v 0 prf) ::: rest) = v. 2318 1707 2319 axiomsub_minus_one_seven_eight:1708 example sub_minus_one_seven_eight: 2320 1709 ∀v: BitVector 7. 2321 1710 false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) = 2322 1711 \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false). 1712 cases daemon. 1713 qed. 2323 1714 2324 1715 lemma pair_destruct_1: … … 2416 1807 generalize in match (assembly (code_memory … ps)) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?) 2417 1808 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 ? ? ? ?) 2421 1810 generalize in match (refl … (code_memory … ps)) cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta; 2422 1811 generalize in ⊢ (???(match % with [_ ⇒ ?  _ ⇒ ?]) → ?) *; normalize nodelta; 2423 1812 [ #EQ >EQ #_ #_ #abs @⊥ normalize in abs; destruct (abs) ] 2424 1813 * #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; 2426 1815 #MAP 2427 1816 #H1 generalize in match (option_destruct_Some ??? H1) H1; #H1 <H1 H1; … … 2462 1851 generalize in match (option_destruct_Some ??? MAP) MAP; #MAP <MAP MAP M'; 2463 1852 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 % 2465 1854 (* 6: (* Mov *) #arg1 #arg2 2466 1855 #H1 #H2 #EQ %[@1] … … 2476 1865 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) *: cases (sub_8_with_carry ???)] 2477 1866 #result #flags 2478 #EQ >EQ EQ; normalize nodelta; >(eq_bv_ to_eq … H2c) % *)1867 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c) % *) 2479 1868 5: (* Call *) #label #MAP 2480 1869 generalize in match (option_destruct_Some ??? MAP) MAP; #MAP <MAP MAP; … … 2490 1879 whd in ⊢ (???% → ??%?); 2491 1880 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) 2493 1882 change with 2494 1883 ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) → … … 2499 1888 >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr 2500 1889 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) 2502 1891 @split_eq_status; 2503 1892 [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?) … … 2556 1945 >clock_write_at_stack_pointer whd in ⊢ (???%) 2557 1946 >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; 2559 1948 @pair_elim' #fst_5_addr #rest_addr #EQ1 2560 1949 @pair_elim' #fst_5_pc #rest_pc #EQ2 … … 2565 1954 @pair_elim' * #instr #newppc' #ticks #EQn 2566 1955 * * #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) 2568 1957 @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4 2569 1958 @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5 … … 2573 1962 >get_8051_sfr_set_8051_sfr 2574 1963 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 ⊢ (??%?) 2576 1965 change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?) 2577 1966 generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc))) … … 2591 1980 (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *) 2592 1981  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))) %]] *)] 2594 1983 4: (* Jmp *) #label #MAP 2595 1984 generalize in match (option_destruct_Some ??? MAP) MAP; #MAP >MAP MAP; … … 2602 1991 >H2b >(eq_instruction_to_eq … H2a) 2603 1992 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) 2605 1994 cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX % 2606 1995 1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; H1; … … 2622 2011 generalize in match EQ; EQ; 2623 2012 whd in ⊢ (???% → ?); 2624 #EQ >EQ EQ; normalize nodelta; >(eq_bv_ to_eq … H2c)2013 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c) 2625 2014 change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ??) ? in ?) = ?) 2626 2015 generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 newppc) (sign_extension lower))) … … 2646 2035 generalize in match EQ; EQ; 2647 2036 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 ⊢ (??%?) 2649 2038 change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?) 2650 2039 generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc))) … … 2683 2072 (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps))) 2684 2073 false (DIRECT ARG2)) 2685 ? in ?) = ?) 2074 ? in ?) = ?) // 2686 2075 [1,2: cut (addressing_mode_ok M ps (DIRECT ARG2) = true) [2: 2687 2076 [1,2:whd in MAP:(??(match % with [ _ ⇒ ?  _ ⇒ ?])?)] 2688 2077 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) *: cases (sub_8_with_carry ???)] 2689 2078 #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] 2692 2081 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 2693 2082 change in ⊢ (? → ??%?) with (execute_1_0 ??) … … 2700 2089  cases (half_add ???) #carry #bl normalize nodelta; 2701 2090 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'; 2703 2092 [5: % 2704 2093 1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program … … 2721 2110 [ normalize nodelta (* HERE *) whd in ⊢ (??%%) % 2722 2111  2723 ] 2112 ] *)
Note: See TracChangeset
for help on using the changeset viewer.