include "ASM/Assembly.ma". include "ASM/Interpret.ma". include "ASM/StatusProofs.ma". 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 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. 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. 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 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 vector_cons_append2: ∀A: Type[0]. ∀n, m: nat. ∀v: Vector A n. ∀q: Vector A m. ∀hd: A. hd:::(v@@q) = (hd:::v)@@q. #A #n #m #v #q elim v [ #hd % | #n' #hd' #tl' #ih #hd' (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.*) definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝ λa, b: addressing_mode. match a with [ DIRECT d ⇒ match b with [ DIRECT e ⇒ eq_bv ? d e | _ ⇒ false ] | INDIRECT b' ⇒ match b with [ INDIRECT e ⇒ eq_b b' e | _ ⇒ false ] | EXT_INDIRECT b' ⇒ match b with [ EXT_INDIRECT e ⇒ eq_b b' e | _ ⇒ false ] | REGISTER bv ⇒ match b with [ REGISTER bv' ⇒ eq_bv ? bv bv' | _ ⇒ false ] | ACC_A ⇒ match b with [ ACC_A ⇒ true | _ ⇒ false ] | ACC_B ⇒ match b with [ ACC_B ⇒ true | _ ⇒ false ] | DPTR ⇒ match b with [ DPTR ⇒ true | _ ⇒ false ] | DATA b' ⇒ match b with [ DATA e ⇒ eq_bv ? b' e | _ ⇒ false ] | DATA16 w ⇒ match b with [ DATA16 e ⇒ eq_bv ? w e | _ ⇒ false ] | ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true | _ ⇒ false ] | ACC_PC ⇒ match b with [ ACC_PC ⇒ true | _ ⇒ false ] | EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ] | INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ] | CARRY ⇒ match b with [ CARRY ⇒ true | _ ⇒ false ] | BIT_ADDR b' ⇒ match b with [ BIT_ADDR e ⇒ eq_bv ? b' e | _ ⇒ false ] | N_BIT_ADDR b' ⇒ match b with [ N_BIT_ADDR e ⇒ eq_bv ? b' e | _ ⇒ false ] | RELATIVE n ⇒ match b with [ RELATIVE e ⇒ eq_bv ? n e | _ ⇒ false ] | ADDR11 w ⇒ match b with [ ADDR11 e ⇒ eq_bv ? w e | _ ⇒ false ] | ADDR16 w ⇒ match b with [ ADDR16 e ⇒ eq_bv ? w e | _ ⇒ false ] ]. lemma eq_bv_refl: ∀n, b. eq_bv n b b = true. #n #b cases b // qed. lemma eq_b_refl: ∀b. eq_b b b = true. #b cases b // qed. lemma eq_addressing_mode_refl: ∀a. eq_addressing_mode a a = true. #a cases a try #arg1 try #arg2 try @eq_bv_refl try @eq_b_refl try normalize % qed. definition eq_sum: ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝ λlt, rt, leq, req, left, right. match left with [ inl l ⇒ match right with [ inl l' ⇒ leq l l' | _ ⇒ false ] | inr r ⇒ match right with [ inr r' ⇒ req r r' | _ ⇒ false ] ]. definition eq_prod: ∀A, B. (A → A → bool) → (B → B → bool) → (A × B) → (A × B) → bool ≝ λlt, rt, leq, req, left, right. let 〈l, r〉 ≝ left in let 〈l', r'〉 ≝ right in leq l l' ∧ req r r'. definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝ λi, j. match i with [ ADD arg1 arg2 ⇒ match j with [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | ADDC arg1 arg2 ⇒ match j with [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | SUBB arg1 arg2 ⇒ match j with [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | INC arg ⇒ match j with [ INC arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | DEC arg ⇒ match j with [ DEC arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | MUL arg1 arg2 ⇒ match j with [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | DIV arg1 arg2 ⇒ match j with [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | DA arg ⇒ match j with [ DA arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | JC arg ⇒ match j with [ JC arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | JNC arg ⇒ match j with [ JNC arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | JB arg1 arg2 ⇒ match j with [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | JNB arg1 arg2 ⇒ match j with [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | JBC arg1 arg2 ⇒ match j with [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | JZ arg ⇒ match j with [ JZ arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | JNZ arg ⇒ match j with [ JNZ arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | CJNE arg1 arg2 ⇒ match j with [ CJNE arg1' arg2' ⇒ let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | DJNZ arg1 arg2 ⇒ match j with [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | CLR arg ⇒ match j with [ CLR arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | CPL arg ⇒ match j with [ CPL arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | RL arg ⇒ match j with [ RL arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | RLC arg ⇒ match j with [ RLC arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | RR arg ⇒ match j with [ RR arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | RRC arg ⇒ match j with [ RRC arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | SWAP arg ⇒ match j with [ SWAP arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | SETB arg ⇒ match j with [ SETB arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | PUSH arg ⇒ match j with [ PUSH arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | POP arg ⇒ match j with [ POP arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | XCH arg1 arg2 ⇒ match j with [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | XCHD arg1 arg2 ⇒ match j with [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ] | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ] | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ] | MOVX arg ⇒ match j with [ MOVX arg' ⇒ let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in sum_eq arg arg' | _ ⇒ false ] | XRL arg ⇒ match j with [ XRL arg' ⇒ let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in sum_eq arg arg' | _ ⇒ false ] | ORL arg ⇒ match j with [ ORL arg' ⇒ let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in sum_eq arg arg' | _ ⇒ false ] | ANL arg ⇒ match j with [ ANL arg' ⇒ let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in sum_eq arg arg' | _ ⇒ false ] | MOV arg ⇒ match j with [ MOV arg' ⇒ let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in sum_eq_5 arg arg' | _ ⇒ false ] ]. lemma eq_sum_refl: ∀A, B: Type[0]. ∀leq, req. ∀s. ∀leq_refl: (∀t. leq t t = true). ∀req_refl: (∀u. req u u = true). eq_sum A B leq req s s = true. #A #B #leq #req #s #leq_refl #req_refl cases s whd in ⊢ (? → ??%?) // qed. lemma eq_prod_refl: ∀A, B: Type[0]. ∀leq, req. ∀s. ∀leq_refl: (∀t. leq t t = true). ∀req_refl: (∀u. req u u = true). eq_prod A B leq req s s = true. #A #B #leq #req #s #leq_refl #req_refl cases s whd in ⊢ (? → ? → ??%?) #l #r >leq_refl normalize @req_refl qed. lemma eq_preinstruction_refl: ∀i. eq_preinstruction i i = true. #i cases i try #arg1 try #arg2 try @eq_addressing_mode_refl [1,2,3,4,5,6,7,8,10,16,17,18,19,20: whd in ⊢ (??%?) try % >eq_addressing_mode_refl >eq_addressing_mode_refl % |13,15: whd in ⊢ (??%?) cases arg1 [*: #arg1_left normalize nodelta >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl] ] |11,12: whd in ⊢ (??%?) cases arg1 [1: #arg1_left normalize nodelta >(eq_sum_refl …) [1: % | 2,3: #arg @eq_prod_refl ] @eq_addressing_mode_refl |2: #arg1_left normalize nodelta @eq_prod_refl [*: @eq_addressing_mode_refl ] |3: #arg1_left normalize nodelta >(eq_sum_refl …) [1: % |2,3: #arg @eq_prod_refl #arg @eq_addressing_mode_refl ] |4: #arg1_left normalize nodelta @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] ] |14: whd in ⊢ (??%?) cases arg1 [ #arg1_left normalize nodelta @eq_sum_refl [1: #arg @eq_sum_refl [1: #arg @eq_sum_refl [1: #arg @eq_sum_refl [1: #arg @eq_prod_refl [*: @eq_addressing_mode_refl ] |2: #arg @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] ] |2: #arg @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] ] |2: #arg @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] ] |2: #arg @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] ] |2: #arg1_right normalize nodelta @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] ] |*: whd in ⊢ (??%?) cases arg1 [*: #arg1 >eq_sum_refl [1,4: normalize @eq_addressing_mode_refl |2,3,5,6: #arg @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] ] ] ] qed. definition eq_instruction: instruction → instruction → bool ≝ λi, j. match i with [ ACALL arg ⇒ match j with [ ACALL arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | LCALL arg ⇒ match j with [ LCALL arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | AJMP arg ⇒ match j with [ AJMP arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | LJMP arg ⇒ match j with [ LJMP arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | SJMP arg ⇒ match j with [ SJMP arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | JMP arg ⇒ match j with [ JMP arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | MOVC arg1 arg2 ⇒ match j with [ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | RealInstruction instr ⇒ match j with [ RealInstruction instr' ⇒ eq_preinstruction instr instr' | _ ⇒ false ] ]. lemma eq_instruction_refl: ∀i. eq_instruction i i = true. #i cases i [1,2,3,4,5,6: #arg1 @eq_addressing_mode_refl |7: #arg1 #arg2 whd in ⊢ (??%?) >eq_addressing_mode_refl >eq_addressing_mode_refl % |8: #arg @eq_preinstruction_refl ] qed. 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. *) 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). example half_add_SO: ∀pc. \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc). cases daemon. qed. (* 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. definition ticks_of_instruction ≝ λi. let trivial_code_memory ≝ assembly1 i in let trivial_status ≝ load_code_memory trivial_code_memory in \snd (fetch trivial_status (zero ?)). 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 ∧ eqb ticks (ticks_of_instruction instr) ∧ 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 ?)