include "ASM/Assembly.ma". include "ASM/Interpret.ma". include "ASM/StatusProofs.ma". include alias "arithmetics/nat.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' …) ]. try applyS prefix try (@le_S_to_le assumption) letin res ≝ (bit ::: prefix) minus_Sn_m assumption qed. definition bitvector_elim_prop ≝ λn: nat. λP: BitVector n → Prop. bitvector_elim_prop_internal n P n ? ?. try @le_n reflex #H %) #m' #hd #tl #inductive_hypothesis normalize cases (eq ??) normalize nodelta try (#irrelevant %) @inductive_hypothesis 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 try (#r #assm assumption) #m' #hd #tl #inductive_hypothesis #r #assm normalize cases (eq ??) try % @inductive_hypothesis assumption 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 try (normalize #m #irrelevant @I) #m' #hd #tl #inductive_hypothesis #m #q change with (bool_to_Prop (andb ??)) cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true) [1: @mem_monotonic_wrt_append try assumption @mem_monotonic_wrt_append try assumption normalize >reflex % |2: #assm >assm >vector_cons_append change with (bool_to_Prop (subvector_with ??????)) @(dependent_rewrite_vectors … (vector_associative_append … q [[hd]] tl)) try @associative_plus @inductive_hypothesis ] qed. lemma vector_cons_empty: ∀A: Type[0]. ∀n: nat. ∀v: Vector A n. [[ ]] @@ v = v. #A #n #v cases v try % #n' #hd #tl % 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 … h v) <(vector_cons_empty … ([[h]] @@ v)) @(subvector_multiple_append … eq reflex [[ ]] v ? [[h]]) 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 #assm elim q try assumption #n' #hd #tl #inductive_hypothesis normalize cases (is_a ??) try @I >inductive_hypothesis @I 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 [1: #absurd normalize in absurd; cases absurd |2: #n' #hd' #tl #inductive_hypothesis #assm >vector_cons_append >(vector_cons_append … hd' tl) @(is_in_monotonic_wrt_append … ([[hd']]@@tl) [[hd]] to_search) assumption ] 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); assumption |1: generalize in match H; generalize in match tl; destruct #tl normalize in ⊢ (∀_: %. ?); #H whd normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?]); cases (is_a hd (subaddressing_modeel y tl H)) whd try @I normalize nodelta // ] 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 assumption 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 @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 [1: #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: @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 [*: #arg1 ] try @eq_addressing_mode_refl try @eq_preinstruction_refl #arg2 whd in ⊢ (??%?); >eq_addressing_mode_refl >eq_addressing_mode_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). lemma vsplit_zero: ∀A,m. ∀v: Vector A m. 〈[[]], v〉 = vsplit A 0 m v. #A #m #v cases v try % #n #hd #tl % qed. lemma Vector_O: ∀A: Type[0]. ∀v: Vector A 0. v ≃ VEmpty A. #A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); // #n #hd #tl #absurd destruct(absurd) qed. lemma Vector_Sn: ∀A: Type[0]. ∀n: nat. ∀v: Vector A (S n). ∃hd: A. ∃tl: Vector A n. v ≃ VCons A n hd tl. #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))); [1: #absurd destruct(absurd) |2: #m #hd #tl #eq <(injective_S … eq) %{hd} %{tl} % ] qed. lemma vector_append_zero: ∀A,m. ∀v: Vector A m. ∀q: Vector A 0. v = q@@v. #A #m #v #q >(Vector_O A q) % qed. lemma prod_eq_left: ∀A: Type[0]. ∀p, q, r: A. p = q → 〈p, r〉 = 〈q, r〉. #A #p #q #r #hyp destruct % qed. lemma prod_eq_right: ∀A: Type[0]. ∀p, q, r: A. p = q → 〈r, p〉 = 〈r, q〉. #A #p #q #r #hyp destruct % qed. corollary prod_vector_zero_eq_left: ∀A, n. ∀q: Vector A O. ∀r: Vector A n. 〈q, r〉 = 〈[[ ]], r〉. #A #n #q #r generalize in match (Vector_O A q …); #hyp destruct % qed. lemma tail_head: ∀a: Type[0]. ∀m, n: nat. ∀hd: a. ∀l: Vector a m. ∀r: Vector a n. tail a ? (hd:::(l@@r)) = l@@r. #a #m #n #hd #l #r cases l try % #m' #hd' #tl' % qed. lemma head_head': ∀a: Type[0]. ∀m: nat. ∀hd: a. ∀l: Vector a m. hd = head' … (hd:::l). #a #m #hd #l cases l try % #m' #hd' #tl % qed. lemma vsplit_succ: ∀A: Type[0]. ∀m, n: nat. ∀l: Vector A m. ∀r: Vector A n. ∀v: Vector A (m + n). ∀hd: A. v = l@@r → (〈l, r〉 = vsplit A m n v → 〈hd:::l, r〉 = vsplit A (S m) n (hd:::v)). #A #m elim m [1: #n #l #r #v #hd #eq #hyp destruct >(Vector_O … l) % |2: #m' #inductive_hypothesis #n #l #r #v #hd #equal #hyp destruct cases (Vector_Sn … l) #hd' #tl' whd in ⊢ (???%); >tail_head <(? : vsplit A (S m') n (l@@r) = vsplit' A (S m') n (l@@r)) try (hyp <(vector_append_zero A n q v) >(prod_vector_zero_eq_left A …) @vsplit_zero |2: #r #ih #n #p #v #q #hyp >hyp cases (Vector_Sn A r v) #hd #exists cases exists #tl #jmeq >jmeq @vsplit_succ try % @ih % ] qed. (* lemma vsplit_prod_exists: ∀A, m, n. ∀p: Vector A (m + n). ∃v: Vector A m. ∃q: Vector A n. 〈v, q〉 = vsplit A m n p. #A #m #n #p elim m @ex_intro [1: |2: @ex_intro [1: |2: ] ] *) definition vsplit_elim: ∀A: Type[0]. ∀l, m: nat. ∀v: Vector A (l + m). ∀P: (Vector A l) × (Vector A m) → Prop. (∀vl: Vector A l. ∀vm: Vector A m. v = vl@@vm → P 〈vl,vm〉) → P (vsplit A l m v) ≝ λa: Type[0]. λl, m: nat. λv: Vector a (l + m). λP. ?. 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 ]. axiom add_commutative: ∀n: nat. ∀l, r: BitVector n. add n l r = add n r l. axiom add_bitvector_of_nat_Sm: ∀n, m: nat. add … (bitvector_of_nat … 1) (bitvector_of_nat … m) = bitvector_of_nat n (S m). lemma encoding_check_append: ∀code_memory: BitVectorTrie Byte 16. ∀final_pc: Word. ∀l1: list Byte. ∀pc: Word. ∀l2: list Byte. encoding_check code_memory pc final_pc (l1@l2) → let pc_plus_len ≝ add … pc (bitvector_of_nat … (length … l1)) in encoding_check code_memory pc pc_plus_len l1 ∧ encoding_check code_memory pc_plus_len final_pc l2. #code_memory #final_pc #l1 elim l1 [1: #pc #l2 whd in ⊢ (????% → ?); #H add_SO in H2; #H2 *) cases (IH … H2) #E1 #E2 % [1: % try @H1 <(add_bitvector_of_nat_Sm 16 (|tl|)) in E1; absurd % |2: #n #hd #tl #_ #size_refl #hd_tl_refl %{hd} cut (n = 2) [1: @destruct_bug_fix_2 >size_refl % |2: #n_refl >n_refl in tl; #V @(Vector_inv_ind bool 2 V (λn: nat. λv: Vector bool n. ∃c:bool. ∃r:bool. hd:::v ≃ [[hd; c; r]])) [1: #absurd @⊥ -V @(destruct_bug_fix_1 1) >absurd % |2: #n' #hd' #tl' #_ #size_refl' #hd_tl_refl' %{hd'} cut (n' = 1) [1: @destruct_bug_fix_2 >size_refl' % |2: #n_refl' >n_refl' in tl'; #V' @(Vector_inv_ind bool 1 V' (λn: nat. λv: Vector bool n. ∃r: bool. hd:::hd':::v ≃ [[hd; hd'; r]])) [1: #absurd @⊥ -V' @(destruct_bug_fix_1 0) >absurd % |2: #n'' #hd'' #tl'' #_ #size_refl'' #hd_tl_refl'' %{hd''} cut (n'' = 0) [1: @destruct_bug_fix_2 >size_refl'' % |2: #n_refl'' >n_refl'' in tl''; #tl''' >(Vector_O … tl''') % ] ] ] ] ] ] qed. lemma 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. #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 cases (bitvector_3_cases … H9) #l #assm cases assm -assm #c #assm cases assm -assm #r #assm cases assm destruct cases l cases c cases r assumption qed. 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 ?)). lemma fetch_assembly: ∀pc: Word. ∀i: instruction. ∀code_memory: BitVectorTrie Byte 16. ∀assembled: list Byte. assembled = assembly1 i → let len ≝ length … assembled in let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in encoding_check code_memory pc pc_plus_len assembled → let 〈instr, pc', ticks〉 ≝ fetch code_memory pc in (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' pc_plus_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: @vsplit_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)] normalize in ⊢ (???% → ?);] #H >H * #H1 try (whd in ⊢ (% → ?); * #H2) try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4 [ whd in match fetch; normalize nodelta