include "ASM/Assembly.ma". include "ASM/Interpret.ma". (* RUSSEL **) include "basics/jmeq.ma". notation > "hvbox(a break ≃ b)" non associative with precedence 45 for @{ 'jmeq ? \$a ? \$b }. notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)" non associative with precedence 45 for @{ 'jmeq \$t \$a \$u \$b }. interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y). lemma eq_to_jmeq: ∀A: Type[0]. ∀x, y: A. x = y → x ≃ y. // qed. definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p. definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w]. coercion inject nocomposites: ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?. coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?. axiom VOID: Type[0]. axiom assert_false: VOID. definition bigbang: ∀A:Type[0].False → VOID → A. #A #abs cases abs qed. coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?. lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p). #A #P #p cases p #w #q @q qed. lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y. #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) % qed. coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?. (* END RUSSELL **) definition bit_elim_prop: ∀P: bool → Prop. Prop ≝ λP. P true ∧ P false. let rec bitvector_elim_prop_internal (n: nat) (P: BitVector n → Prop) (m: nat) on m: m ≤ n → BitVector (n - m) → Prop ≝ match m return λm. m ≤ n → BitVector (n - m) → Prop with [ O ⇒ λprf1. λprefix. P ? | S n' ⇒ λprf2. λprefix. bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' ? ?) ]. [ applyS prefix | letin res ≝ (bit ::: prefix) < (minus_S_S ? ?) > (minus_Sn_m ? ?) [ @ res | @ prf2 ] | /2/ ]. qed. definition bitvector_elim_prop ≝ λn: nat. λP: BitVector n → Prop. bitvector_elim_prop_internal n P n ? ?. [ @ (le_n ?) | < (minus_n_n ?) @ [[ ]] ] qed. lemma eq_b_eq: ∀b, c. eq_b b c = true → b = c. #b #c cases b cases c normalize // qed. lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool. #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) // #n #hd #tl #abs @⊥ // qed. lemma BitVector_Sn: ∀n.∀v:BitVector (S n). ∃hd.∃tl.v ≃ VCons bool n hd tl. #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))) [ #abs @⊥ // | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] qed. lemma eq_bv_eq: ∀n, v, q. eq_bv n v q = true → v = q. #n #v #q generalize in match v elim q [ #v #h @BitVector_O | #n #hd #tl #ih #v' #h cases (BitVector_Sn ? v') #hd' * #tl' #jmeq >jmeq in h; #new_h change in new_h with ((andb ? ?) = ?); cases(conjunction_true … new_h) #eq_heads #eq_tails whd in eq_heads:(??(??(%))?); cases(eq_b_eq … eq_heads) whd in eq_tails:(??(?????(%))?); change in eq_tails with (eq_bv ??? = ?); <(ih tl') // ] qed. lemma bool_eq_internal_eq: ∀b, c. (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c. #b #c cases b [ normalize // | normalize cases c [ normalize // | normalize // ] ] qed. lemma eq_bv_refl: ∀n,v. eq_bv n v v = true. #n #v elim v [ // | #n #hd #tl #ih normalize cases hd [ normalize @ ih | normalize @ ih ] ] qed. lemma eq_eq_bv: ∀n, v, q. v = q → eq_bv n v q = true. #n #v elim v [ #q #h h // ] qed. let rec foldl_strong_internal (A: Type[0]) (P: list A → Type[0]) (l: list A) (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd])) (prefix: list A) (suffix: list A) (acc: P prefix) on suffix: l = prefix @ suffix → P(prefix @ suffix) ≝ match suffix return λl'. l = prefix @ l' → P (prefix @ l') with [ nil ⇒ λprf. ? | cons hd tl ⇒ λprf. ? ]. [ > (append_nil ?) @ acc | applyS (foldl_strong_internal A P l H (prefix @ [hd]) tl ? ?) [ @ (H prefix hd tl prf acc) | applyS prf ] ] qed. definition foldl_strong ≝ λA: Type[0]. λP: list A → Type[0]. λl: list A. λH: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]). λacc: P [ ]. foldl_strong_internal A P l H [ ] l acc (refl …). definition bit_elim: ∀P: bool → bool. bool ≝ λP. P true ∧ P false. let rec bitvector_elim_internal (n: nat) (P: BitVector n → bool) (m: nat) on m: m ≤ n → BitVector (n - m) → bool ≝ match m return λm. m ≤ n → BitVector (n - m) → bool with [ O ⇒ λprf1. λprefix. P ? | S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?) ]. [ applyS prefix | letin res ≝ (bit ::: prefix) < (minus_S_S ? ?) > (minus_Sn_m ? ?) [ @ res | @ prf2 ] | /2/ ]. qed. definition bitvector_elim ≝ λn: nat. λP: BitVector n → bool. bitvector_elim_internal n P n ? ?. [ @ (le_n ?) | < (minus_n_n ?) @ [[ ]] ] qed. axiom vector_associative_append: ∀A: Type[0]. ∀n, m, o: nat. ∀v: Vector A n. ∀q: Vector A m. ∀r: Vector A o. ((v @@ q) @@ r) ≃ (v @@ (q @@ r)). lemma vector_cons_append: ∀A: Type[0]. ∀n: nat. ∀e: A. ∀v: Vector A n. e ::: v = [[ e ]] @@ v. # A # N # E # V elim V [ normalize % | # NN # AA # VV # IH normalize % ] qed. lemma super_rewrite2: ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m. ∀P: ∀m. Vector A m → Prop. n=m → v1 ≃ v2 → P n v1 → P m v2. #A #n #m #v1 #v2 #P #EQ JMEQ // qed. lemma mem_middle_vector: ∀A: Type[0]. ∀m, o: nat. ∀eq: A → A → bool. ∀reflex: ∀a. eq a a = true. ∀p: Vector A m. ∀a: A. ∀r: Vector A o. mem A eq ? (p@@(a:::r)) a = true. # A # M # O # EQ # REFLEX # P # A elim P [ normalize > (REFLEX A) normalize # H % | # NN # AA # PP # IH normalize cases (EQ A AA) // @ IH ] qed. lemma mem_monotonic_wrt_append: ∀A: Type[0]. ∀m, o: nat. ∀eq: A → A → bool. ∀reflex: ∀a. eq a a = true. ∀p: Vector A m. ∀a: A. ∀r: Vector A o. mem A eq ? r a = true → mem A eq ? (p @@ r) a = true. # A # M # O # EQ # REFLEX # P # A elim P [ #R #H @H | #NN #AA # PP # IH #R #H normalize cases (EQ A AA) [ normalize % | @ IH @ H ] ] qed. lemma subvector_multiple_append: ∀A: Type[0]. ∀o, n: nat. ∀eq: A → A → bool. ∀refl: ∀a. eq a a = true. ∀h: Vector A o. ∀v: Vector A n. ∀m: nat. ∀q: Vector A m. bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)). # A # O # N # EQ # REFLEX # H # V elim V [ normalize # M # V % | # NN # AA # VV # IH # MM # QQ change with (bool_to_Prop (andb ??)) cut ((mem A EQ (O + (MM + S NN)) (H@@QQ@@AA:::VV) AA) = true) [ | # HH > HH > (vector_cons_append ? ? AA VV) change with (bool_to_Prop (subvector_with ??????)) @(super_rewrite2 A ((MM + 1)+ NN) (MM+S NN) ?? (λSS.λVS.bool_to_Prop (subvector_with ?? (O+SS) ?? (H@@VS))) ? (vector_associative_append A ? ? ? QQ [[AA]] VV)) [ >associative_plus // | @IH ] ] @(mem_monotonic_wrt_append) [ @ REFLEX | @(mem_monotonic_wrt_append) [ @ REFLEX | normalize > REFLEX normalize % ] ] qed. lemma vector_cons_empty: ∀A: Type[0]. ∀n: nat. ∀v: Vector A n. [[ ]] @@ v = v. # A # N # V elim V [ normalize % | # NN # HH # VV #H % ] qed. corollary subvector_hd_tl: ∀A: Type[0]. ∀o: nat. ∀eq: A → A → bool. ∀refl: ∀a. eq a a = true. ∀h: A. ∀v: Vector A o. bool_to_Prop (subvector_with A ? ? eq v (h ::: v)). # A # O # EQ # REFLEX # H # V > (vector_cons_append A ? H V) < (vector_cons_empty A ? ([[H]] @@ V)) @ (subvector_multiple_append A ? ? EQ REFLEX [[]] V ? [[ H ]]) qed. lemma eq_a_reflexive: ∀a. eq_a a a = true. # A cases A % qed. lemma is_in_monotonic_wrt_append: ∀m, n: nat. ∀p: Vector addressing_mode_tag m. ∀q: Vector addressing_mode_tag n. ∀to_search: addressing_mode. bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search). # M # N # P # Q # TO_SEARCH # H elim Q [ normalize @ H | # NN # PP # QQ # IH normalize cases (is_a PP TO_SEARCH) [ normalize % | normalize normalize in IH @ IH ] ] qed. corollary is_in_hd_tl: ∀to_search: addressing_mode. ∀hd: addressing_mode_tag. ∀n: nat. ∀v: Vector addressing_mode_tag n. bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search). # TO_SEARCH # HD # N # V elim V [ # H normalize in H; cases H | # NN # HHD # VV # IH # HH > vector_cons_append > (vector_cons_append ? ? HHD VV) @ (is_in_monotonic_wrt_append ? 1 ([[HHD]]@@VV) [[HD]] TO_SEARCH) @ HH ] qed. let rec list_addressing_mode_tags_elim (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝ match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x'). (l → bool) → bool ] with [ VEmpty ⇒ true | VCons len hd tl ⇒ λP. let process_hd ≝ match hd return λhd. ∀P: hd:::tl → bool. bool with [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x)) | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x)) | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x)) | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x)) | acc_a ⇒ λP.P ACC_A | acc_b ⇒ λP.P ACC_B | dptr ⇒ λP.P DPTR | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x)) | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x)) | acc_dptr ⇒ λP.P ACC_DPTR | acc_pc ⇒ λP.P ACC_PC | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR | indirect_dptr ⇒ λP.P INDIRECT_DPTR | carry ⇒ λP.P CARRY | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x)) | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x)) | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x)) | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x)) | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x)) ] in andb (process_hd P) (match len return λx. x = len → bool with [ O ⇒ λprf. true | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len)) ]. try % [ 2: cases (sym_eq ??? prf); @tl | generalize in match H; generalize in match tl; cases prf; (* cases prf in tl H; : ??? WAS WORKING BEFORE *) #tl normalize in ⊢ (∀_: %. ?) # H whd normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?]) cases (is_a hd (subaddressing_modeel y tl H)) whd // ] qed. definition product_elim ≝ λm, n: nat. λv: Vector addressing_mode_tag (S m). λq: Vector addressing_mode_tag (S n). λP: (v × q) → bool. list_addressing_mode_tags_elim ? v (λx. list_addressing_mode_tags_elim ? q (λy. P 〈x, y〉)). definition union_elim ≝ λA, B: Type[0]. λelimA: (A → bool) → bool. λelimB: (B → bool) → bool. λelimU: A ⊎ B → bool. elimA (λa. elimB (λb. elimU (inl ? ? a) ∧ elimU (inr ? ? b))). (* definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝ λP. list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADD ? ACC_A addr)) ∧ list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADDC ? ACC_A addr)) ∧ list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (SUBB ? ACC_A addr)) ∧ list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ; dptr ]] (λaddr. P (INC ? addr)) ∧ list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (DEC ? addr)) ∧ list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (MUL ? ACC_A addr)) ∧ list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (DIV ? ACC_A addr)) ∧ list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧ list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CLR ? addr)) ∧ list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧ P (DA ? ACC_A) ∧ bitvector_elim 8 (λr. P (JC ? (RELATIVE r))) ∧ bitvector_elim 8 (λr. P (JNC ? (RELATIVE r))) ∧ bitvector_elim 8 (λr. P (JZ ? (RELATIVE r))) ∧ bitvector_elim 8 (λr. P (JNZ ? (RELATIVE r))) ∧ bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JB ? (BIT_ADDR b) (RELATIVE r))))) ∧ bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JNB ? (BIT_ADDR b) (RELATIVE r))))) ∧ bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JBC ? (BIT_ADDR b) (RELATIVE r))))) ∧ list_addressing_mode_tags_elim ? [[ registr; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧ P (RL ? ACC_A) ∧ P (RLC ? ACC_A) ∧ P (RR ? ACC_A) ∧ P (RRC ? ACC_A) ∧ P (SWAP ? ACC_A) ∧ P (RET ?) ∧ P (RETI ?) ∧ P (NOP ?) ∧ bit_elim (λb. P (XCHD ? ACC_A (INDIRECT b))) ∧ list_addressing_mode_tags_elim ? [[ carry; bit_addr ]] (λaddr. P (SETB ? addr)) ∧ bitvector_elim 8 (λaddr. P (PUSH ? (DIRECT addr))) ∧ bitvector_elim 8 (λaddr. P (POP ? (DIRECT addr))) ∧ union_elim ? ? (product_elim ? ? [[ acc_a ]] [[ direct; data ]]) (product_elim ? ? [[ registr; indirect ]] [[ data ]]) (λd. bitvector_elim 8 (λb. P (CJNE ? d (RELATIVE b)))) ∧ list_addressing_mode_tags_elim ? [[ registr; direct; indirect ]] (λaddr. P (XCH ? ACC_A addr)) ∧ union_elim ? ? (product_elim ? ? [[acc_a]] [[ data ; registr ; direct ; indirect ]]) (product_elim ? ? [[direct]] [[ acc_a ; data ]]) (λd. P (XRL ? d)) ∧ union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]]) (product_elim ? ? [[direct]] [[ acc_a ; data ]])) (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]]) (λd. P (ANL ? d)) ∧ union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; data ; direct ; indirect ]]) (product_elim ? ? [[direct]] [[ acc_a ; data ]])) (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]]) (λd. P (ORL ? d)) ∧ union_elim ? ? (product_elim ? ? [[acc_a]] [[ ext_indirect ; ext_indirect_dptr ]]) (product_elim ? ? [[ ext_indirect ; ext_indirect_dptr ]] [[acc_a]]) (λd. P (MOVX ? d)) ∧ union_elim ? ? ( union_elim ? ? ( union_elim ? ? ( union_elim ? ? ( union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]]) (product_elim ? ? [[ registr ; indirect ]] [[ acc_a ; direct ; data ]])) (product_elim ? ? [[direct]] [[ acc_a ; registr ; direct ; indirect ; data ]])) (product_elim ? ? [[dptr]] [[data16]])) (product_elim ? ? [[carry]] [[bit_addr]])) (product_elim ? ? [[bit_addr]] [[carry]]) (λd. P (MOV ? d)). % qed. definition instruction_elim: ∀P: instruction → bool. bool ≝ λP. (* bitvector_elim 11 (λx. P (ACALL (ADDR11 x))) ∧ bitvector_elim 16 (λx. P (LCALL (ADDR16 x))) ∧ bitvector_elim 11 (λx. P (AJMP (ADDR11 x))) ∧ bitvector_elim 16 (λx. P (LJMP (ADDR16 x))) ∧ *) bitvector_elim 8 (λx. P (SJMP (RELATIVE x))). (* ∧ P (JMP INDIRECT_DPTR) ∧ list_addressing_mode_tags_elim ? [[ acc_dptr; acc_pc ]] (λa. P (MOVC ACC_A a)) ∧ preinstruction_elim (λp. P (RealInstruction p)). *) % qed. axiom instruction_elim_complete: ∀P. instruction_elim P = true → ∀i. P i = true. *) (*definition eq_instruction ≝ λi, j: instruction. true.*) axiom eq_instruction: instruction → instruction → bool. axiom eq_instruction_refl: ∀i. eq_instruction i i = true. let rec vect_member (A: Type[0]) (n: nat) (eq: A → A → bool) (v: Vector A n) (a: A) on v: bool ≝ match v with [ VEmpty ⇒ false | VCons len hd tl ⇒ eq hd a ∨ (vect_member A ? eq tl a) ]. let rec list_addressing_mode_tags_elim_prop (n: nat) (l: Vector addressing_mode_tag (S n)) on l: ∀P: l → Prop. ∀direct_a. ∀indirect_a. ∀ext_indirect_a. ∀register_a. ∀acc_a_a. ∀acc_b_a. ∀dptr_a. ∀data_a. ∀data16_a. ∀acc_dptr_a. ∀acc_pc_a. ∀ext_indirect_dptr_a. ∀indirect_dptr_a. ∀carry_a. ∀bit_addr_a. ∀n_bit_addr_a. ∀relative_a. ∀addr11_a. ∀addr16_a. ∀x: l. P x ≝ match l return λy. match y with [ O ⇒ λm: Vector addressing_mode_tag O. ∀prf: 0 = S n. True | S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n.∀P:l → Prop. ∀direct_a: if vect_member … eq_a l direct then ∀x. P (DIRECT x) else True. ∀indirect_a: if vect_member … eq_a l indirect then ∀x. P (INDIRECT x) else True. ∀ext_indirect_a: if vect_member … eq_a l ext_indirect then ∀x. P (EXT_INDIRECT x) else True. ∀register_a: if vect_member … eq_a l registr then ∀x. P (REGISTER x) else True. ∀acc_a_a: if vect_member … eq_a l acc_a then P (ACC_A) else True. ∀acc_b_a: if vect_member … eq_a l acc_b then P (ACC_B) else True. ∀dptr_a: if vect_member … eq_a l dptr then P DPTR else True. ∀data_a: if vect_member … eq_a l data then ∀x. P (DATA x) else True. ∀data16_a: if vect_member … eq_a l data16 then ∀x. P (DATA16 x) else True. ∀acc_dptr_a: if vect_member … eq_a l acc_dptr then P ACC_DPTR else True. ∀acc_pc_a: if vect_member … eq_a l acc_pc then P ACC_PC else True. ∀ext_indirect_dptr_a: if vect_member … eq_a l ext_indirect_dptr then P EXT_INDIRECT_DPTR else True. ∀indirect_dptr_a: if vect_member … eq_a l indirect_dptr then P INDIRECT_DPTR else True. ∀carry_a: if vect_member … eq_a l carry then P CARRY else True. ∀bit_addr_a: if vect_member … eq_a l bit_addr then ∀x. P (BIT_ADDR x) else True. ∀n_bit_addr_a: if vect_member … eq_a l n_bit_addr then ∀x. P (N_BIT_ADDR x) else True. ∀relative_a: if vect_member … eq_a l relative then ∀x. P (RELATIVE x) else True. ∀addr11_a: if vect_member … eq_a l addr11 then ∀x. P (ADDR11 x) else True. ∀addr_16_a: if vect_member … eq_a l addr16 then ∀x. P (ADDR16 x) else True. ∀x:l. P x ] with [ VEmpty ⇒ λAbsurd. ⊥ | VCons len hd tl ⇒ λProof. ? ] (refl ? (S n)). cases daemon. qed. (* [ destruct(Absurd) | # A1 # A2 # A3 # A4 # A5 # A6 # A7 # A8 # A9 # A10 # A11 # A12 # A13 # A14 # A15 # A16 # A17 # A18 # A19 # X cases X # SUB cases daemon ] qed. cases SUB [ # BYTE normalize ]. (* let prepare_hd ≝ match hd with [ direct ⇒ λdirect_prf. ? | indirect ⇒ λindirect_prf. ? | ext_indirect ⇒ λext_indirect_prf. ? | registr ⇒ λregistr_prf. ? | acc_a ⇒ λacc_a_prf. ? | acc_b ⇒ λacc_b_prf. ? | dptr ⇒ λdptr_prf. ? | data ⇒ λdata_prf. ? | data16 ⇒ λdata16_prf. ? | acc_dptr ⇒ λacc_dptr_prf. ? | acc_pc ⇒ λacc_pc_prf. ? | ext_indirect_dptr ⇒ λext_indirect_prf. ? | indirect_dptr ⇒ λindirect_prf. ? | carry ⇒ λcarry_prf. ? | bit_addr ⇒ λbit_addr_prf. ? | n_bit_addr ⇒ λn_bit_addr_prf. ? | relative ⇒ λrelative_prf. ? | addr11 ⇒ λaddr11_prf. ? | addr16 ⇒ λaddr16_prf. ? ] in ? *) ]. [ 1: destruct(absd) | 2: # A1 # A2 # A3 # A4 # A5 # A6 # A7 # A8 # A9 # A10 # A11 # A12 # A13 # A14 # A15 # A16 # A17 # A18 # A19 * ]. match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x'). (l → bool) → bool ] with [ VEmpty ⇒ true | VCons len hd tl ⇒ λP. let process_hd ≝ match hd return λhd. ∀P: hd:::tl → bool. bool with [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x)) | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x)) | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x)) | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x)) | acc_a ⇒ λP.P ACC_A | acc_b ⇒ λP.P ACC_B | dptr ⇒ λP.P DPTR | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x)) | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x)) | acc_dptr ⇒ λP.P ACC_DPTR | acc_pc ⇒ λP.P ACC_PC | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR | indirect_dptr ⇒ λP.P INDIRECT_DPTR | carry ⇒ λP.P CARRY | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x)) | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x)) | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x)) | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x)) | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x)) ] in andb (process_hd P) (match len return λx. x = len → bool with [ O ⇒ λprf. true | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len)) ]. try % [ 2: cases (sym_eq ??? prf); @tl | generalize in match H; generalize in match tl; cases prf; (* cases prf in tl H; : ??? WAS WORKING BEFORE *) #tl normalize in ⊢ (∀_: %. ?) # H whd normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?]) cases (is_a hd (subaddressing_modeel y tl H)) whd // ] qed. *) (* lemma test: let i ≝ SJMP (RELATIVE (bitvector_of_nat 8 255)) in (let assembled ≝ assembly1 i in let code_memory ≝ load_code_memory assembled in let fetched ≝ fetch code_memory ? in let 〈instr_pc, ticks〉 ≝ fetched in eq_instruction (\fst instr_pc)) i = true. [2: @ zero | normalize ]*) lemma BitVectorTrie_O: ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0. #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??)) [ #w #_ %1 %[@w] % | #n #l #r #abs @⊥ // | #n #EQ %2 >EQ %] qed. lemma BitVectorTrie_Sn: ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n). #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%) [ #m #abs @⊥ // | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] // | #m #EQ %2 // ] qed. lemma lookup_prepare_trie_for_insertion_hit: ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n. lookup … b (prepare_trie_for_insertion … b v) a = v. #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize // qed. lemma lookup_insert_hit: ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n. lookup … b (insert … b v t) a = v. #A #a #v #n #b elim b -b -n // #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t) [ * #l * #r #JMEQ >JMEQ cases hd normalize // | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ] qed. coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. lemma lookup_prepare_trie_for_insertion_miss: ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n. (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a. #A #a #v #n #c elim c [ #b >(BitVector_O … b) normalize #abs @⊥ // | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ cases hd cases hd' normalize [2,3: #_ cases tl' // |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]] qed. lemma lookup_insert_miss: ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n. (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a. #A #a #v #n #c elim c -c -n [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF // | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ #t cases(BitVectorTrie_Sn … t) [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H; [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH // | #JMEQ >JMEQ cases hd cases hd' #H normalize in H; [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]] qed. definition load_code_memory_aux ≝ fold_left_i_aux … ( λi, mem, v. insert … (bitvector_of_nat … i) v mem) (Stub Byte 16). axiom split_elim: ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop. (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v). axiom half_add_SO: ∀pc. \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc). (* axiom not_eqvb_S: ∀pc. (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S pc))). axiom not_eqvb_SS: ∀pc. (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))). axiom bitvector_elim_complete: ∀n,P. bitvector_elim n P = true → ∀bv. P bv. lemma bitvector_elim_complete': ∀n,P. bitvector_elim n P = true → ∀bv. P bv = true. #n #P #H generalize in match (bitvector_elim_complete … H) #K #bv generalize in match (K bv) normalize cases (P bv) normalize // #abs @⊥ // qed. *) (* lemma andb_elim': ∀b1,b2. (b1 = true) → (b2 = true) → (b1 ∧ b2) = true. #b1 #b2 #H1 #H2 @andb_elim cases b1 in H1; normalize // qed. *) let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word) (encoding: list Byte) on encoding: Prop ≝ match encoding with [ nil ⇒ final_pc = pc | cons hd tl ⇒ let 〈new_pc, byte〉 ≝ next code_memory pc in hd = byte ∧ encoding_check code_memory new_pc final_pc tl ]. lemma encoding_check_append: ∀code_memory,final_pc,l1,pc,l2. encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc) (l1@l2) → let intermediate_pc ≝ pc + length … l1 in encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc) l1 ∧ encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2. #code_memory #final_pc #l1 elim l1 [ #pc #l2 whd in ⊢ (????% → ?) #H half_add_SO in H2; #H2 cases (IH … H2) half_add_SO @K1 ] qed. axiom bitvector_3_elim_prop: ∀P: BitVector 3 → Prop. P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] → P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] → P [[true;true;false]] → P [[true;true;true]] → ∀v. P v. axiom fetch_assembly: ∀pc,i,code_memory,assembled. assembled = assembly1 i → let len ≝ length … assembled in encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled → let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in let 〈instr_pc, ticks〉 ≝ fetched in let 〈instr,pc'〉 ≝ instr_pc in (eq_instruction instr i ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true. (* #pc #i #code_memory #assembled cases i [8: *] [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]] [47,48,49: |*: #arg @(list_addressing_mode_tags_elim_prop … arg) whd try % -arg [2,3,5,7,10,12,16,17,18,21,25,26,27,30,31,32,37,38,39,40,41,42,43,44,45,48,51,58, 59,60,63,64,65,66,67: #ARG]] [4,5,6,7,8,9,10,11,12,13,22,23,24,27,28,39,40,41,42,43,44,45,46,47,48,49,50,51,52, 56,57,69,70,72,73,75: #arg2 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2 [1,2,4,7,9,10,12,13,15,16,17,18,20,22,23,24,25,26,27,28,29,30,31,32,33,36,37,38, 39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65, 68,69,70,71: #ARG2]] [1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3] normalize in ⊢ (???% → ?) [92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)] normalize in ⊢ (???% → ?)] #H >H * #H1 try (change in ⊢ (% → ?) with (? ∧ ?) * #H2) try (change in ⊢ (% → ?) with (? ∧ ?) * #H3) whd in ⊢ (% → ?) #H4 change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??) whd in ⊢ (let fetched ≝ ??% in ?)