# Changeset 2108 for src/ASM

Ignore:
Timestamp:
Jun 25, 2012, 2:39:06 PM (9 years ago)
Message:

Various axioms closed and others moved around. Uncommented main lemma and found that it no longer compiles due to changing how we expand jumps. Problem in proof highlighted with XXX for Claudio.

Location:
src/ASM
Files:
5 edited

Unmodified
Added
Removed
• ## src/ASM/Arithmetic.ma

 r2032 \snd (half_add n l r). axiom add_zero: lemma half_add_carry_Sn: ∀n: nat. ∀l: BitVector n. ∀hd: bool. \fst (half_add (S n) (hd:::l) (false:::(zero n))) = andb hd (\fst (half_add n l (zero n))). #n #l elim l [1: #hd normalize cases hd % |2: #n' #hd #tl #inductive_hypothesis #hd' whd in match half_add; normalize nodelta whd in match full_add; normalize nodelta normalize in ⊢ (??%%); cases hd' normalize @pair_elim #c1 #r #c1_r_refl cases c1 % ] qed. lemma half_add_zero_carry_false: ∀m: nat. ∀b: BitVector m. \fst (half_add m b (zero m)) = false. #m #b elim b try % #n #hd #tl #inductive_hypothesis change with (false:::(zero ?)) in match (zero ?); >half_add_carry_Sn >inductive_hypothesis cases hd % qed. axiom half_add_true_true_carry_true: ∀n: nat. ∀hd, hd': bool. ∀l, r: BitVector n. \fst (half_add (S n) (true:::l) (true:::r)) = true. lemma add_Sn_carry_add: ∀n: nat. ∀hd, hd': bool. ∀l, r: BitVector n. add (S n) (hd:::l) (hd':::r) = xorb (xorb hd hd') (\fst (half_add n l r)):::add n l r. #n #hd #hd' #l elim l [1: #r cases hd cases hd' >(BitVector_O … r) normalize % |2: #n' #hd'' #tl #inductive_hypothesis #r cases (BitVector_Sn … r) #hd''' * #tl' #r_refl destruct cases hd cases hd' cases hd'' cases hd''' whd in match (xorb ??); cases daemon ] qed. lemma add_zero: ∀n: nat. ∀l: BitVector n. l = add n l (zero …). #n #l elim l try % #n' #hd #tl #inductive_hypothesis change with (false:::zero ?) in match (zero ?); >add_Sn_carry_add >half_add_zero_carry_false cases hd zero_add_head % qed. axiom bitvector_of_nat_one_Sm: ∀m: nat. ∃b: BitVector m. bitvector_of_nat (S m) 1 ≃ b @@ [[true]]. axiom increment_zero_bitvector_of_nat_1: ∀m: nat. ∀b: BitVector m. increment m b = add m (bitvector_of_nat m 1) b. axiom add_associative: ∀n: nat. ∀l, c, r: BitVector n. add … l (add … c r) = add … (add … l c) r. ∀m: nat. ∀l, c, r: BitVector m. add m l (add m c r) = add m (add m l c) r. lemma bitvector_of_nat_aux_buffer: ∀m, n: nat. ∀b: BitVector m. bitvector_of_nat_aux m n b = add m (bitvector_of_nat m n) b. #m #n elim n [1: #b change with (? = add ? (zero …) b) >zero_add % |2: #n' #inductive_hypothesis #b whd in match (bitvector_of_nat_aux ???); >inductive_hypothesis whd in match (bitvector_of_nat ??) in ⊢ (???%); >inductive_hypothesis >increment_zero_bitvector_of_nat_1 >increment_zero_bitvector_of_nat_1 <(add_zero m (bitvector_of_nat m 1)) most_significant_bit_zero [1: elim m [1: % |2: #n' #inductive_hypothesis whd in match bitvector_of_nat; normalize nodelta whd in match (bitvector_of_nat_aux ???); whd in match (bitvector_of_nat_aux ???) in ⊢ (???%); >(bitvector_of_nat_aux_buffer 16 n') cases daemon ] |2: assumption ] qed. axiom add_commutative:
• ## src/ASM/Assembly.ma

 r2101 qed. axiom eq_identifier_eq: axiom eqb_succ_injective_Pos: ∀l, r: Pos. eqb (succ l) (succ r) = true → eqb l r = true. lemma eqb_true_to_refl_Pos: ∀l, r: Pos. eqb l r = true → l = r. #l #r @(pos_elim2 … l r) [1: #r cases r [1: #_ % |2,3: #l normalize in ⊢ (% → ?); #absurd destruct(absurd) ] |2: #l cases l [1: normalize in ⊢ (% → ?); #absurd destruct(absurd) |2,3: #l' normalize in ⊢ (% → ?); #absurd destruct(absurd) ] |3: #l #r #inductive_hypothesis #relevant @eq_f @inductive_hypothesis @eqb_succ_injective_Pos assumption ] qed. lemma eq_identifier_eq: ∀tag: String. ∀l. ∀r. eq_identifier tag l r = true → l = r. #tag #l #r cases l cases r #pos_l #pos_r cases pos_l cases pos_r [1: #_ % |2,3,4,7: #p1_l normalize in ⊢ (% → ?); #absurd destruct(absurd) |5,9: #p1_l #p1_r normalize in ⊢ (% → ?); #relevant >(eqb_true_to_refl_Pos … relevant) % |*: #p_l #p_r normalize in ⊢ (% → ?); #absurd destruct(absurd) ] qed. axiom neq_identifier_neq: ∀l, r: identifier tag. eq_identifier tag l r = false → (l = r → False). (* label_map: identifier ↦ pseudo program counter *) definition label_map ≝ identifier_map ASMTag ℕ.
• ## src/ASM/AssemblyProof.ma

 r2078 let datalabels ≝ construct_datalabels preamble in let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in 〈assembled,costs'〉 = assembly program length_proof sigma policy → 〈assembled,costs'〉 = assembly program sigma policy → (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *) let code_memory ≝ load_code_memory assembled in sigma newppc = add … pc (bitvector_of_nat … len). #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs' cases (assembly program length_proof sigma policy) * #assembled' #costs'' @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %); @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %); @pair_elim #preamble #instr_list #EQprogram cases (assembly program sigma policy) * #assembled' #costs'' >EQprogram normalize nodelta @pair_elim #labels #costs #EQcreate_label_cost_refl normalize nodelta #assembly_ok #Pair_eq destruct(Pair_eq) whd #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd lapply (assembly_ok ppc ?) [(*CSC: ????? WRONG HERE?*) cases daemon] -assembly_ok >eq_fetch_pseudo_instruction #ppc #ppc_ok @pair_elim #pi #newppc #EQfetch_pseudo_instruction >EQprogram in sigma_policy_witness; #sigma_policy_witness lapply (assembly_ok sigma_policy_witness ? ppc ?) [2: >EQprogram in length_proof; #length_proof; assumption ] try assumption >EQfetch_pseudo_instruction normalize nodelta change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<|assembledi|.?) → ?) >(? : assembly_1_pseudoinstruction ????? pi = 〈len,assembled〉) [2: (*CSC: Provable, isn't it?*) cases daemon | whd in ⊢ (% → ?); #assembly_ok % @pair_elim #len #assembledi #EQassembly_1_pseudo_instruction letin lookup_labels ≝ (λx.sigma (bitvector_of_nat 16 (lookup_def ASMTag ℕ labels x O))) letin lookup_datalabels ≝ (λx. lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)) >(? : assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi = 〈len,assembledi〉) [2: EQlen -len elim assembled [ #pc #_ whd EQlen -len elim assembledi [1: #pc #_ whd (* most_significant_bit_zero [1: cases daemon |2: assumption |3: // #i cases i try (#assm1 #assm2) try #assm1 [8: cases assm1 try (#assm1 #assm2) try #assm1 whd in match assembly1; normalize nodelta whd in match assembly_preinstruction; normalize nodelta try @(subaddressing_mode_elim … assm2) try @(subaddressing_mode_elim … assm1) try #w try #w' normalize nodelta [32: cases assm1 -assm1 #assm1 normalize nodelta cases assm1 #addr1 #addr2 normalize nodelta [1: @(subaddressing_mode_elim … addr2) |2: @(subaddressing_mode_elim … addr1) ] #w |35,36,37: cases assm1 -assm1 #assm1 normalize nodelta [1,3: cases assm1 -assm1 #assm1 normalize nodelta ] cases assm1 #addr1 #addr2 normalize nodelta @(subaddressing_mode_elim … addr2) try #w |49: cases assm1 -assm1 #assm1 normalize nodelta [1: cases assm1 -assm1 #assm1 normalize nodelta [1: cases assm1 -assm1 #assm1 normalize nodelta [1: cases assm1 -assm1 #assm1 normalize nodelta [1: cases assm1 -assm1 #assm1 normalize nodelta ] ] ] ] cases assm1 #addr1 #addr2 normalize nodelta [1,3,4,5: @(subaddressing_mode_elim … addr2) try #w |*: @(subaddressing_mode_elim … addr1) try #w normalize nodelta [1,2: @(subaddressing_mode_elim … addr2) try #w ] ] |50: cases assm1 -assm1 #assm1 normalize nodelta cases assm1 #addr1 #addr2 normalize nodelta [1: @(subaddressing_mode_elim … addr2) try #w |2: @(subaddressing_mode_elim … addr1) try #w ] ] normalize repeat @le_S_S @le_O_n ] qed. whd in match assembly1; normalize nodelta [6: normalize repeat @le_S_S @le_O_n |7: @(subaddressing_mode_elim … assm2) normalize repeat @le_S_S @le_O_n |*: @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n ] qed.
• ## src/ASM/AssemblyProofSplit.ma

 r2047 include alias "ASM/Vector.ma". axiom main_lemma_preinstruction: ∀M, M': internal_pseudo_address_map. ∀preamble: preamble. ∀instr_list: list labelled_instruction. ∀cm: pseudo_assembly_program. ∀EQcm: cm = 〈preamble, instr_list〉. ∀sigma: Word → Word. ∀policy: Word → bool. ∀sigma_policy_witness: sigma_policy_specification cm sigma policy. ∀ps: PseudoStatus cm. ∀ppc: Word. ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps. ∀labels: label_map. ∀costs: BitVectorTrie costlabel 16. ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉. ∀newppc: Word. ∀lookup_labels: Identifier → Word. ∀EQlookup_labels: lookup_labels = (λx:Identifier. address_of_word_labels_code_mem instr_list x). ∀lookup_datalabels: Identifier → Word. ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)). ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1). ∀instr: preinstruction Identifier. ∀ticks: nat × nat. ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr). ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16. ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x). ∀s: PreStatus pseudo_assembly_program cm. ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))). ∀P: preinstruction Identifier → PseudoStatus cm → Prop. ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc) (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels (Instruction instr)))) → next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr) M cm ps = Some internal_pseudo_address_map M' → fetch_many (load_code_memory (\fst (pi1 … (assembly cm sigma policy)))) (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma (program_counter pseudo_assembly_program cm ps)) (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) → ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) = status_of_pseudo_status M' cm s sigma policy). P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s). (* axiom sub16_with_carry_overflow: ∀left, right, result: BitVector 16. ∀flags: BitVector 3. ∀upper: BitVector 9. ∀lower: BitVector 7. sub_16_with_carry left right false = 〈result, flags〉 → vsplit bool 9 7 result = 〈upper, lower〉 → get_index_v bool 3 flags 2 ? = true → upper = [[true; true; true; true; true; true; true; true; true]]. // qed. lemma main_lemma_preinstruction: ∀M, M': internal_pseudo_address_map. (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels (Instruction instr)))) → next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr) M cm ps = Some internal_pseudo_address_map M' → next_internal_pseudo_address_map0 ? cm addr_of (Instruction instr) M ps = Some internal_pseudo_address_map M' → fetch_many (load_code_memory (\fst (pi1 … (assembly cm sigma policy)))) (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma (program_counter pseudo_assembly_program cm ps)) (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) → [31,32: (* DJNZ *) (* XXX: work on the right hand side *) >p normalize nodelta >p normalize nodelta >p1 normalize nodelta (* XXX: switch to the left hand side *) -instr_refl >EQP -P normalize nodelta #sigma_increment_commutation #maps_assm #fetch_many_assm whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; whd in match (expand_relative_jump ????); p1 normalize nodelta [1,3: >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} whd in ⊢ (??%?); >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm; normalize nodelta in ⊢ (% → ?); #fetch_many_assm <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); (* XXX: work on the left hand side *) cases daemon |2,4: XXX: here >EQppc * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
• ## src/ASM/Interpret.ma

 r2062 include "ASM/Fetch.ma". include "ASM/AbstractStatus.ma". definition sign_extension: Byte → Word ≝ λc. let b ≝ get_index_v ? 8 c 1 ? in [[ b; b; b; b; b; b; b; b ]] @@ c. normalize repeat (@le_S_S) @le_O_n qed. lemma execute_1_technical:
Note: See TracChangeset for help on using the changeset viewer.