Changeset 2055
 Timestamp:
 Jun 13, 2012, 12:11:21 PM (5 years ago)
 Location:
 src/ASM
 Files:

 5 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2051 r2055 672 672 *) 673 673 674 (* 675 (* This establishes the correspondence between pseudo program counters and 676 program counters. It is at the heart of the proof. *) 677 (*CSC: code taken from build_maps *) 678 definition sigma00: 679 ∀jump_expansion:policy_type2.∀l:list labelled_instruction.? → 680 (Σppc_pc_map:ℕ×(ℕ×(BitVectorTrie Word 16)). 681 let 〈ppc,pc_map〉 ≝ ppc_pc_map in 682 let 〈program_counter, sigma_map〉 ≝ pc_map in 683 ppc = l ∧ 684 (ppc = l → 685 (bvt_lookup ?? (bitvector_of_nat ? ppc) sigma_map (zero ?) = (bitvector_of_nat ? program_counter)) ∧ 686 (∀x.x < l → 687 ∀pi.\fst (fetch_pseudo_instruction l (bitvector_of_nat ? x)) = pi → 688 let pc_x ≝ bvt_lookup ?? (bitvector_of_nat 16 x) sigma_map (zero ?) in 689 bvt_lookup ?? (bitvector_of_nat 16 (S x)) sigma_map (zero ?) = 690 bitvector_of_nat 16 ((nat_of_bitvector ? pc_x) + 691 (\fst (assembly_1_pseudoinstruction lookup_labels(*X?(λx.pc_x)*) (jump_expansion (*?(λx.pc_x)*)) pc_x 692 (λx.zero ?) pi))))) 693 ) ≝ 694 (*?*)λlookup_labels. 695 λjump_expansion(*X?: policy_type2*). 696 λl:list labelled_instruction. 697 λacc. 698 foldl_strong ? 699 (λprefix.(Σppc_pc_map:ℕ×(ℕ×(BitVectorTrie Word 16)). 700 let 〈ppc,pc_map〉 ≝ ppc_pc_map in 701 let 〈program_counter, sigma_map〉 ≝ pc_map in 702 (ppc = prefix) ∧ 703 (ppc = prefix → 704 (bvt_lookup ?? (bitvector_of_nat ? ppc) sigma_map (zero ?) = (bitvector_of_nat ? program_counter)) ∧ 705 (∀x.x < prefix → 706 ∀pi.\fst (fetch_pseudo_instruction l (bitvector_of_nat ? x)) = pi → 707 let pc_x ≝ bvt_lookup ?? (bitvector_of_nat 16 x) sigma_map (zero ?) in 708 bvt_lookup ?? (bitvector_of_nat 16 (S x)) sigma_map (zero ?) = 709 bitvector_of_nat 16 ((nat_of_bitvector ? pc_x) + 710 (\fst (assembly_1_pseudoinstruction (*X?(λx.pc_x)*)lookup_labels (jump_expansion (*X?(λx.pc_x)*)) pc_x 711 (λx.zero ?) pi)))))) 712 ) 713 l 714 (λhd.λi.λtl.λp.λppc_pc_map. 715 let 〈ppc,pc_map〉 ≝ ppc_pc_map in 716 let 〈program_counter, sigma_map〉 ≝ pc_map in 717 let 〈label, i〉 ≝ i in 718 let 〈pc,ignore〉 ≝ construct_costs lookup_labels program_counter (jump_expansion (*X?(λx.bitvector_of_nat ? program_counter)*)) ppc (Stub …) i in 719 〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 (S ppc)) (bitvector_of_nat 16 pc) sigma_map〉〉 720 ) acc. 721 cases i in p; #label #ins #p @pair_elim #new_ppc #x normalize nodelta cases x x #old_pc #old_map 722 @pair_elim #new_pc #ignore #Hc #Heq normalize nodelta @conj 723 [ lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta #Hind 724 <(pair_eq1 ?????? Heq) >(proj1 ?? Hind) >append_length <commutative_plus normalize @refl 725  #Hnew <(pair_eq2 ?????? (pair_eq2 ?????? Heq)) <(pair_eq1 ?????? Heq) @conj 726 [ >lookup_insert_hit >(pair_eq1 ?????? (pair_eq2 ?????? Heq)) @refl 727  #x <(pair_eq1 ?????? Heq) >append_length <commutative_plus #Hx normalize in Hx; 728 #pi #Hpi <(pair_eq2 ?????? (pair_eq2 ?????? Heq)) <(pair_eq1 ?????? Heq) in Hnew; 729 >append_length <commutative_plus #Hnew normalize in Hnew; >(injective_S … Hnew) 730 elim (le_to_or_lt_eq … Hx) Hx #Hx 731 [ lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta #Hind 732 lapply (proj2 ?? ((proj2 ?? Hind) (proj1 ?? Hind)) x (le_S_S_to_le … Hx) pi Hpi) 733 Hind #Hind >lookup_insert_miss 734 [2: @bitvector_of_nat_abs 735 [3: @lt_to_not_eq @Hx 736 1: @(transitive_le … Hx) 737 ] 738 cases daemon (* XXX invariant *) 739 ] 740 >lookup_insert_miss 741 [2: @bitvector_of_nat_abs 742 [3: @lt_to_not_eq @(transitive_le … (le_S_S_to_le … Hx)) @le_S @le_n 743 1: @(transitive_le … (le_S_S_to_le … Hx)) 744 ] 745 cases daemon (* XXX invariant *) 746 ] 747 @Hind 748  lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta 749 #Hind lapply (proj1 ?? ((proj2 ?? Hind) (proj1 ?? Hind))) Hind 750 >(injective_S … Hnew) #Hind <(injective_S … Hx) >lookup_insert_hit >lookup_insert_miss 751 [2: @bitvector_of_nat_abs 752 [3: @lt_to_not_eq @le_n 753 1: @(transitive_le ??? (le_n (S x))) 754 ] 755 cases daemon (* XXX invariant *) 756 ] 757 >p in Hpi; whd in match (fetch_pseudo_instruction ??); >nth_append_second 758 >nat_of_bitvector_bitvector_of_nat >(injective_S … Hx) 759 [3: @le_n] 760 [2,3: cases daemon (* XXX invariant *)] 761 <minus_n_n cases (half_add ???) #x #y normalize nodelta x y #Heq <Heq 762 whd in match (construct_costs ?????) in Hc; whd in match (assembly_1_pseudoinstruction ?????); 763 cases ins in p Hc; normalize nodelta 764 [1,2,4,5: #x #p >Hind #H <(pair_eq1 ?????? H) >commutative_plus >nat_of_bitvector_bitvector_of_nat 765 [1,3,5,7: @refl 766 2,4,6,8: cases daemon (* XXX invariant *) 767 ] 768 3: #c #p >Hind #H <(pair_eq1 ?????? H) >nat_of_bitvector_bitvector_of_nat 769 [2: cases daemon (* XXX invariant *) ] 770 whd in match (expand_pseudo_instruction ?????); normalize <plus_n_O @refl 771 6: #x #y #p >Hind #H <(pair_eq1 ?????? H) >commutative_plus >nat_of_bitvector_bitvector_of_nat 772 [ @refl 773  cases daemon (* XXX invariant *) 774 ] 775 ] 776 ] 777 ] 778 ] 779 qed. 780 781 definition sigma0: pseudo_assembly_program → policy_type2 → (nat × (nat × (BitVectorTrie Word 16))) ≝ 782 λprog. 783 λjump_expansion. 784 sigma00 jump_expansion (\snd prog) 785 〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub …))〉〉. 786 normalize nodelta @conj 787 [ / by refl/ 788  #H @conj 789 [ >lookup_insert_hit @refl 790  #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n 791 ] 792 ] 793 qed. 794 795 definition tech_pc_sigma00: pseudo_assembly_program → policy_type2 → 796 list labelled_instruction → (nat × nat) ≝ 797 λprogram,jump_expansion,instr_list. 798 let 〈ppc,pc_sigma_map〉 ≝ sigma00 jump_expansion instr_list 799 〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub ? ?))〉〉 in 800 (* acc copied from sigma0 *) 801 let 〈pc,map〉 ≝ pc_sigma_map in 802 〈ppc,pc〉. 803 normalize nodelta @conj 804 [ / by refl/ 805  #H @conj 806 [ >lookup_insert_hit @refl 807  #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n 808 ] 809 ] 810 qed. 811 812 definition sigma_safe: pseudo_assembly_program → policy_type2 → 813 option (Word → Word) ≝ 814 λinstr_list,jump_expansion. 815 let 〈ppc,pc_sigma_map〉 ≝ sigma0 instr_list jump_expansion in 816 let 〈pc, sigma_map〉 ≝ pc_sigma_map in 817 if gtb pc (2^16) then 818 None ? 819 else 820 Some ? (λx. lookup … x sigma_map (zero …)). *) 821 822 (* stuff about policy *) 823 824 (*definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….*) 825 826 (*definition policy ≝ λp. Σjump_expansion:policy_type2. policy_ok jump_expansion p.*) 827 828 (*lemma eject_policy: ∀p. policy p → policy_type2. 829 #p #pol @(pi1 … pol) 830 qed. 831 832 coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type2 ≝ eject_policy on _pol:(policy ?) to policy_type2. 833 834 definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝ 835 λp,policy. 836 match sigma_safe p (pi1 … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with 837 [ None ⇒ λabs. ⊥ 838  Some r ⇒ λ_.r] (pi2 … policy). 839 cases abs /2 by / 840 qed.*) 841 842 (*CSC: Main axiom here, needs to be proved soon! *) 843 (*lemma snd_assembly_1_pseudoinstruction_ok: 844 ∀program:pseudo_assembly_program.∀pol: policy program. 845 ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels. 846 lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) → 847 lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) → 848 (nat_of_bitvector 16 ppc) < \snd program → 849 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi → 850 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) (sigma program pol ppc) lookup_datalabels pi) in 851 sigma program pol (add ? ppc (bitvector_of_nat ? 1)) = 852 bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len). 853 #program #pol #ppc #pi #lookup_labels #lookup_datalabels #Hll #Hldl #Hppc 854 lapply (refl … (sigma0 program pol)) whd in match (sigma0 ??) in ⊢ (??%? → ?); 855 cases (sigma00 ???) #x #Hpmap #EQ 856 whd in match (sigma ???); 857 whd in match (sigma program pol (add ???)); 858 whd in match sigma_safe; normalize nodelta 859 (*Problem1: backtracking cases (sigma0 program pol)*) 860 generalize in match (pi2 ???); whd in match policy_ok; normalize nodelta 861 whd in match sigma_safe; normalize nodelta <EQ cases x in Hpmap EQ; x #final_ppc #x 862 cases x x #final_pc #smap normalize nodelta #Hpmap #EQ #Heq #Hfetch cases (gtb final_pc (2^16)) in Heq; 863 normalize nodelta 864 [ #abs @⊥ @(absurd ?? abs) @refl 865  #_ lapply (proj1 ?? ((proj2 ?? Hpmap) (proj1 ?? Hpmap))) #Hpmap1 866 lapply ((proj2 ?? ((proj2 ?? Hpmap) (proj1 ?? Hpmap))) (nat_of_bitvector 16 ppc) Hppc) #Hpmap2 Hpmap 867 <(bitvector_of_nat_nat_of_bitvector 16 ppc) >add_SO 868 869 >(Hpmap2 ? (refl …)) @eq_f @eq_f2 [%] 870 >bitvector_of_nat_nat_of_bitvector 871 >Hfetch lapply Hfetch lapply pi 872 873 874 whd in match assembly_1_pseudoinstruction; normalize nodelta 875 876 qed.*) 877 878 879 (*example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0. 880 cases daemon. 881 qed.*) 882 883 (*CSC: FALSE!!!*) 884 axiom fetch_pseudo_instruction_vsplit: 885 ∀instr_list,ppc. 674 (*CSC: move elsewhere *) 675 lemma nth_safe_append: 676 ∀A,l,n,n_ok. 677 ∃pre,suff. 678 (pre @ [nth_safe A n l n_ok]) @ suff = l. 679 #A #l elim l normalize 680 [ #n #abs cases (absurd ? abs (not_le_Sn_O ?)) 681  #hd #tl #IH #n cases n normalize 682 [ #_ %{[]} /2/ 683  #m #m_ok cases (IH m ?) 684 [ #pre * #suff #EQ %{(hd::pre)} %{suff} <EQ in ⊢ (???%); %  skip ]] 685 qed. 686 687 lemma fetch_pseudo_instruction_vsplit: 688 ∀instr_list,ppc,ppc_ok. 886 689 ∃pre,suff,lbl. 887 (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc)〉]) @ suff = instr_list. 690 (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list. 691 #instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???); 692 cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff} 693 lapply EQ EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta 694 #EQ %{lbl0} @EQ 695 qed. 888 696 889 697 (*lemma sigma00_append: … … 1240 1048 qed. 1241 1049 1242 (*CSC: move elsewhere; also proved in CostProofs as shift_nth_safe *) 1050 1051 (*CSC: move elsewhere; practically equal to shift_nth_safe but for commutation 1052 of addition. One of the two lemmas should disappear. *) 1243 1053 lemma nth_safe_prepend: 1244 1054 ∀A,l1,l2,j.∀H:j<l2.∀K:l1+j<(l1@l2). 1245 1055 nth_safe A j l2 H =nth_safe A (l1+j) (l1@l2) K. 1246 #A #l1 elim l1 normalize // 1247 qed. 1248 1249 (*CSC: move elsewhere; also proved in CostProofs as shift_nth_prefix *) 1250 lemma shift_nth_prefix: 1251 ∀T,l1,i,l2,K1,K2. 1252 nth_safe T i l1 K1 = nth_safe T i (l1@l2) K2. 1253 #T #l1 elim l1 normalize 1254 [ 1255 #i #l1 #K1 cases(lt_to_not_zero … K1) 1256  1257 #hd #tl #IH #i #l2 1258 cases i 1259 [ 1260 // 1261  1262 #i' #K1 #K2 whd in ⊢ (??%%); 1263 @IH 1264 ] 1265 ] 1266 qed. 1267 1268 lemma nth_cons: 1269 ∀A,hd,tl,l2,j,d. 1270 nth j A (tl@l2) d =nth (1+j) A (hd::tl@l2) d. 1056 #A #l1 #l2 #j #H >commutative_plus @shift_nth_safe 1057 qed. 1058 1059 lemma nth_safe_cons: 1060 ∀A,hd,tl,l2,j,j_ok,Sj_ok. 1061 nth_safe A j (tl@l2) j_ok =nth_safe A (1+j) (hd::tl@l2) Sj_ok. 1271 1062 // 1063 qed. 1064 1065 lemma eq_nth_safe_proof_irrelevant: 1066 ∀A,l,i,i_ok,i_ok'. 1067 nth_safe A l i i_ok = nth_safe A l i i_ok'. 1068 #A #l #i #i_ok #i_ok' % 1272 1069 qed. 1273 1070 1274 1071 (*CSC: move elsewhere *) 1275 1072 lemma fetch_pseudo_instruction_append: 1276 ∀l1,l2,ppc .1277 let code_newppc ≝ fetch_pseudo_instruction l2 ppc in1278 fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (l1)) (ppc)) =1073 ∀l1,l2,ppc,ppc_ok,ppc_ok'. 1074 let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in 1075 fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (l1)) (ppc)) ppc_ok' = 1279 1076 〈\fst code_newppc, add … (bitvector_of_nat … (l1)) (\snd code_newppc)〉. 1280 #l1 elim l1 1281 [ #l2 #ppc >add_commutative <add_zero >add_commutative <add_zero // 1282  #hd #tl #IH #l2 #ppc whd whd in match fetch_pseudo_instruction in ⊢ (??%?); normalize nodelta 1283 (*CSC: FALSE, NEED INVARIANT? *) 1284 > (?: nat_of_bitvector … (add 16 (bitvector_of_nat 16 (hd::tl)) ppc) 1285 = 1 + nat_of_bitvector … (add … (bitvector_of_nat … (tl)) ppc)) [2: cases daemon] 1286 <nth_cons lapply (IH l2 ppc) IH normalize nodelta cases (fetch_pseudo_instruction l2 ppc) 1287 #i #newppc whd in match fetch_pseudo_instruction; normalize nodelta 1288 cases (nth ? labelled_instruction ??) #i' #newppc' normalize nodelta #EQ 1289 destruct EQ change with (add ??? = ?) in e0; 1290 (*CSC: TRUE, NEEDS TRIVIAL ARITHMETICS *) cases daemon 1291 ] 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] 1081 #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???) 1082 #lbl #instr normalize nodelta >add_associative % 1292 1083 qed. 1293 1084 … … 1303 1094 let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in 1304 1095 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in 1305 ∀ppc. 1306 nat_of_bitvector … ppc < instr_list → 1307 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc in 1096 ∀ppc. ∀ppc_ok:nat_of_bitvector … ppc < instr_list. 1097 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc ppc_ok in 1308 1098 let 〈len,assembledi〉 ≝ 1309 1099 assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in … … 1327 1117 let 〈ppc,code〉 ≝ ppc_code in 1328 1118 ppc = bitvector_of_nat … (pre) ∧ 1329 ∀ppc'. 1119 ∀ppc'.∀ppc_ok'. 1330 1120 nat_of_bitvector … ppc' < nat_of_bitvector … ppc → 1331 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in1121 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' ppc_ok' in 1332 1122 let 〈len,assembledi〉 ≝ 1333 1123 assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in … … 1346 1136 fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉. 1347 1137 [ cases (foldl_strong ? (λx.Σy.?) ???) in p2; #ignore_revcode #Hfold #EQignore_revcode 1348 >EQignore_revcode in Hfold; * #_ #Hfold whd >p1 whd #ppc #LTppc @Hfold 1349 (* CSC: ??? *) cases daemon 1350  % // #ppc' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs)  skip] 1138 >EQignore_revcode in Hfold; * #Hfold1 #Hfold2 whd >p1 whd #ppc #LTppc @Hfold2 1139 >Hfold1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption 1140 (* CSC: FALSE, NEEDS ADDITIONAL ASSUMPTION *) cases daemon 1141  % // #ppc' #ppc_ok' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs)  skip] 1351 1142  cases ppc_code in p1; ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; EQppc_code 1352 1143 * #IH1 #IH2 % [ normalize nodelta >IH1 >length_append cases daemon (*CSC: TRUE, LEMMA NEEDED *)] 1353 whd#ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p21144 #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 1354 1145 cases (le_to_or_lt_eq … LTppc') 1355 1146 [2: #S_S_eq normalize nodelta in S_S_eq; 1356 1147 (*CSC: FALSE, NEEDS INVARIANT *) 1357 cut (ppc' = ppc) [cases daemon] S_S_eq #EQppc' >EQppc' in LTppc'; ppc' #LTppc 1358 >prf >IH1 in ⊢ match % with [_ ⇒ ?]; >(add_zero … (bitvector_of_nat 16 (prefix))) in ⊢ match % with [_ ⇒ ?]; 1359 @pair_elim #pi' #newppc' >fetch_pseudo_instruction_append #EQpair destruct(EQpair) 1360 >p2 1148 cut (ppc' = ppc) [cases daemon] S_S_eq #EQppc' >EQppc' in LTppc'; ppc' >prf 1149 >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc #X lapply LTppc 1150 >(add_zero … (bitvector_of_nat 16 (prefix))) in ⊢ (% → match % with [_ ⇒ ?]); 1151 >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] 1153 #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2 1361 1154 #j #LTj 1362 1155 (* CSC: FALSE, NEEDS INVARIANT *) … … 1367 1160 >(? : nat_of_bitvector … (sigma ppc) = reverse … code) [2: cases daemon] 1368 1161 @nth_safe_prepend 1369  #LTppc' lapply (IH2 ppc' ?) [ (*CSC: EASY, FINISH*) cases daemon ]1162  #LTppc' #LT_ppc_ppc lapply (IH2 ppc' ?) [ (*CSC: EASY, FINISH*) cases daemon ] 1370 1163 @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction 1371 1164 @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH … … 1374 1167 >IH 1375 1168 [2: (*CSC: FALSE, NEEDS INVARIANT? *) cases daemon 1376  @shift_nth_prefix 1169  @shift_nth_prefix 1170 3: >IH1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption 1171 (*CSC: ALSO FALSE, NEEDS INVARIANT? *) cases daemon 1377 1172 ] 1378 1173 ] 
src/ASM/CostsProof.ma
r2001 r2055 457 457 (λ_.0). 458 458 @tech_cost_of_label0 @codom_dom 459 qed.460 461 lemma shift_nth_safe:462 ∀T,i,l2,l1,K1,K2.463 nth_safe T i l1 K1 = nth_safe T (i+l2) (l2@l1) K2.464 #T #i #l2 elim l2 normalize465 [ #l1 #K1 <plus_n_O #K2 %466  #hd #tl #IH #l1 #K1 <plus_n_Sm #K2 change with (? < ?) in K1; change with (? < ?) in K2;467 whd in ⊢ (???%); @IH ]468 qed.469 470 lemma shift_nth_prefix:471 ∀T,l1,i,l2,K1,K2.472 nth_safe T i l1 K1 = nth_safe T i (l1@l2) K2.473 #T #l1 elim l1 normalize474 [475 #i #l1 #K1 cases(lt_to_not_zero … K1)476 477 #hd #tl #IH #i #l2478 cases i479 [480 //481 482 #i' #K1 #K2 whd in ⊢ (??%%);483 @IH484 ]485 ]486 459 qed. 487 460 
src/ASM/Policy.ma
r2034 r2055 625 625 ∀program:preamble × (Σl:list labelled_instruction.S (l) < 2^16). 626 626 option (Σsigma:Word → Word × bool. 627 ∀ppc: Word. 627 ∀ppc: Word. ∀ppc_ok. 628 628 let pc ≝ \fst (sigma ppc) in 629 629 let labels ≝ \fst (create_label_cost_map (\snd program)) in 630 630 let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def ?? labels x 0) in 631 let instruction ≝ \fst (fetch_pseudo_instruction (\snd program) ppc ) in631 let instruction ≝ \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in 632 632 let next_pc ≝ \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in 633 633 And (nat_of_bitvector … ppc ≤ \snd program → 
src/ASM/Status.ma
r2032 r2055 1114 1114 set_code_memory (BitVectorTrie Word 16) ? cm status (load_code_memory l). 1115 1115 1116 definition fetch_pseudo_instruction: list labelled_instruction → Word → (pseudo_instruction × Word) ≝ 1116 definition fetch_pseudo_instruction: 1117 ∀code_mem:list labelled_instruction. ∀pc:Word. 1118 nat_of_bitvector … pc < code_mem → (pseudo_instruction × Word) ≝ 1117 1119 λcode_mem. 1118 1120 λpc: Word. 1119 let 〈lbl, instr〉 ≝ nth (nat_of_bitvector ? pc) … code_mem ? in 1120 let new_pc ≝ add ? pc (bitvector_of_nat ? 1) in 1121 λpc_ok. 1122 let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? pc) … code_mem pc_ok in 1123 let new_pc ≝ add ? pc (bitvector_of_nat … 1) in 1121 1124 〈instr, new_pc〉. 1122 cases not_implemented.1123 qed.1124 1125 1125 1126 lemma snd_fetch_pseudo_instruction: 1126 ∀l,ppc . \snd (fetch_pseudo_instruction l ppc) = add ? ppc (bitvector_of_nat ? 1).1127 #l #ppc whd in ⊢ (??(???%)?); @pair_elim1127 ∀l,ppc,ppc_ok. \snd (fetch_pseudo_instruction l ppc ppc_ok) = add ? ppc (bitvector_of_nat ? 1). 1128 #l #ppc #ppc_ok whd in ⊢ (??(???%)?); @pair_elim 1128 1129 #lft #rgt #_ % 1129 1130 qed. 
src/ASM/Util.ma
r2037 r2055 225 225 ] 226 226 qed. 227 228 lemma shift_nth_safe: 229 ∀T,i,l2,l1,K1,K2. 230 nth_safe T i l1 K1 = nth_safe T (i+l2) (l2@l1) K2. 231 #T #i #l2 elim l2 normalize 232 [ #l1 #K1 <plus_n_O #K2 % 233  #hd #tl #IH #l1 #K1 <plus_n_Sm #K2 change with (? < ?) in K1; change with (? < ?) in K2; 234 whd in ⊢ (???%); @IH ] 235 qed. 236 237 lemma shift_nth_prefix: 238 ∀T,l1,i,l2,K1,K2. 239 nth_safe T i l1 K1 = nth_safe T i (l1@l2) K2. 240 #T #l1 elim l1 normalize 241 [ 242 #i #l1 #K1 cases(lt_to_not_zero … K1) 243  244 #hd #tl #IH #i #l2 245 cases i 246 [ 247 // 248  249 #i' #K1 #K2 whd in ⊢ (??%%); 250 @IH 251 ] 252 ] 253 qed. 254 227 255 228 256 definition last_safe ≝
Note: See TracChangeset
for help on using the changeset viewer.