Changeset 2111 for src/ASM/Assembly.ma
 Timestamp:
 Jun 26, 2012, 5:30:41 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2110 r2111 581 581 \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc (λx.zero …) i). 582 582 583 (*CSC: move elsewhere *)584 lemma nth_safe_append:585 ∀A,l,n,n_ok.586 ∃pre,suff.587 (pre @ [nth_safe A n l n_ok]) @ suff = l.588 #A #l elim l normalize589 [ #n #abs cases (absurd ? abs (not_le_Sn_O ?))590  #hd #tl #IH #n cases n normalize591 [ #_ %{[]} /2/592  #m #m_ok cases (IH m ?)593 [ #pre * #suff #EQ %{(hd::pre)} %{suff} <EQ in ⊢ (???%); %  skip ]]594 qed.595 596 lemma fetch_pseudo_instruction_vsplit:597 ∀instr_list,ppc,ppc_ok.598 ∃pre,suff,lbl.599 (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list.600 #instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???);601 cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff}602 lapply EQ EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta603 #EQ %{lbl0} @EQ604 qed.605 606 axiom eqb_succ_injective_Pos:607 ∀l, r: Pos.608 eqb (succ l) (succ r) = true → eqb l r = true.609 610 lemma eqb_true_to_refl_Pos:611 ∀l, r: Pos.612 eqb l r = true → l = r.613 #l #r @(pos_elim2 … l r)614 [1:615 #r cases r616 [1:617 #_ %618 2,3:619 #l normalize in ⊢ (% → ?); #absurd destruct(absurd)620 ]621 2:622 #l cases l623 [1:624 normalize in ⊢ (% → ?); #absurd destruct(absurd)625 2,3:626 #l' normalize in ⊢ (% → ?); #absurd destruct(absurd)627 ]628 3:629 #l #r #inductive_hypothesis #relevant @eq_f630 @inductive_hypothesis @eqb_succ_injective_Pos631 assumption632 ]633 qed.634 635 lemma eq_identifier_eq:636 ∀tag: String.637 ∀l.638 ∀r.639 eq_identifier tag l r = true → l = r.640 #tag #l #r cases l cases r641 #pos_l #pos_r642 cases pos_l cases pos_r643 [1:644 #_ %645 2,3,4,7:646 #p1_l normalize in ⊢ (% → ?);647 #absurd destruct(absurd)648 5,9:649 #p1_l #p1_r normalize in ⊢ (% → ?);650 #relevant651 >(eqb_true_to_refl_Pos … relevant) %652 *:653 #p_l #p_r normalize in ⊢ (% → ?);654 #absurd destruct(absurd)655 ]656 qed.657 658 axiom neq_identifier_neq:659 ∀tag: String.660 ∀l, r: identifier tag.661 eq_identifier tag l r = false → (l = r → False).662 583 663 584 (* label_map: identifier ↦ pseudo program counter *) … … 772 693 qed. 773 694 774 775 (*CSC: move elsewhere; practically equal to shift_nth_safe but for commutation776 of addition. One of the two lemmas should disappear. *)777 lemma nth_safe_prepend:778 ∀A,l1,l2,j.∀H:j<l2.∀K:l1+j<(l1@l2).779 nth_safe A j l2 H =nth_safe A (l1+j) (l1@l2) K.780 #A #l1 #l2 #j #H >commutative_plus @shift_nth_safe781 qed.782 783 lemma nth_safe_cons:784 ∀A,hd,tl,l2,j,j_ok,Sj_ok.785 nth_safe A j (tl@l2) j_ok =nth_safe A (1+j) (hd::tl@l2) Sj_ok.786 //787 qed.788 789 lemma eq_nth_safe_proof_irrelevant:790 ∀A,l,i,i_ok,i_ok'.791 nth_safe A l i i_ok = nth_safe A l i i_ok'.792 #A #l #i #i_ok #i_ok' %793 qed.794 795 (*CSC: move elsewhere *)796 axiom nat_of_bitvector_add:797 ∀n,v1,v2.798 nat_of_bitvector n v1 + nat_of_bitvector n v2 < 2^n →799 nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.800 801 (*CSC: move elsewhere *)802 lemma fetch_pseudo_instruction_append:803 ∀l1,l2. l1@l2 ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'.804 let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in805 fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (l1)) (ppc)) ppc_ok' =806 〈\fst code_newppc, add … (bitvector_of_nat … (l1)) (\snd code_newppc)〉.807 #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta808 cut (l1 + nat_of_bitvector … ppc < 2^16)809 [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ]810 l1l2_ok #l1ppc_ok >nat_of_bitvector_add811 >nat_of_bitvector_bitvector_of_nat_inverse try assumption812 [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ]813 #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)814 #lbl #instr normalize nodelta >add_associative %815 qed.816 817 695 definition sigma_policy_specification ≝ 818 696 λprogram: pseudo_assembly_program. … … 832 710 ( (nat_of_bitvector … ppc < instr_list → nat_of_bitvector … pc < nat_of_bitvector … next_pc) 833 711 ∨ (nat_of_bitvector … ppc = instr_list → next_pc = (zero …))). 834 835 (*CSC: Move elsewhere *)836 axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n.837 712 838 713 definition assembly:
Note: See TracChangeset
for help on using the changeset viewer.