set "baseuri" "cic:/matita/assembly/".
include "nat/div_and_mod.ma".
-(*include "nat/compare.ma".*)
include "list/list.ma".
inductive exadecimal : Type ≝
definition eqbyte ≝
λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
+inductive cartesian_product (A,B: Type) : Type ≝
+ couple: ∀a:A.∀b:B. cartesian_product A B.
+
+definition plusex ≝
+ λb1,b2,c.
+ match c with
+ [ true ⇒
+ match b1 with
+ [ x0 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x1 false
+ | x1 ⇒ couple exadecimal bool x2 false
+ | x2 ⇒ couple exadecimal bool x3 false
+ | x3 ⇒ couple exadecimal bool x4 false
+ | x4 ⇒ couple exadecimal bool x5 false
+ | x5 ⇒ couple exadecimal bool x6 false
+ | x6 ⇒ couple exadecimal bool x7 false
+ | x7 ⇒ couple exadecimal bool x8 false
+ | x8 ⇒ couple exadecimal bool x9 false
+ | x9 ⇒ couple exadecimal bool xA false
+ | xA ⇒ couple exadecimal bool xB false
+ | xB ⇒ couple exadecimal bool xC false
+ | xC ⇒ couple exadecimal bool xD false
+ | xD ⇒ couple exadecimal bool xE false
+ | xE ⇒ couple exadecimal bool xF false
+ | xF ⇒ couple exadecimal bool x0 true ]
+ | x1 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x2 false
+ | x1 ⇒ couple exadecimal bool x3 false
+ | x2 ⇒ couple exadecimal bool x4 false
+ | x3 ⇒ couple exadecimal bool x5 false
+ | x4 ⇒ couple exadecimal bool x6 false
+ | x5 ⇒ couple exadecimal bool x7 false
+ | x6 ⇒ couple exadecimal bool x8 false
+ | x7 ⇒ couple exadecimal bool x9 false
+ | x8 ⇒ couple exadecimal bool xA false
+ | x9 ⇒ couple exadecimal bool xB false
+ | xA ⇒ couple exadecimal bool xC false
+ | xB ⇒ couple exadecimal bool xD false
+ | xC ⇒ couple exadecimal bool xE false
+ | xD ⇒ couple exadecimal bool xF false
+ | xE ⇒ couple exadecimal bool x0 true
+ | xF ⇒ couple exadecimal bool x1 true ]
+ | x2 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x3 false
+ | x1 ⇒ couple exadecimal bool x4 false
+ | x2 ⇒ couple exadecimal bool x5 false
+ | x3 ⇒ couple exadecimal bool x6 false
+ | x4 ⇒ couple exadecimal bool x7 false
+ | x5 ⇒ couple exadecimal bool x8 false
+ | x6 ⇒ couple exadecimal bool x9 false
+ | x7 ⇒ couple exadecimal bool xA false
+ | x8 ⇒ couple exadecimal bool xB false
+ | x9 ⇒ couple exadecimal bool xC false
+ | xA ⇒ couple exadecimal bool xD false
+ | xB ⇒ couple exadecimal bool xE false
+ | xC ⇒ couple exadecimal bool xF false
+ | xD ⇒ couple exadecimal bool x0 true
+ | xE ⇒ couple exadecimal bool x1 true
+ | xF ⇒ couple exadecimal bool x2 true ]
+ | x3 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x4 false
+ | x1 ⇒ couple exadecimal bool x5 false
+ | x2 ⇒ couple exadecimal bool x6 false
+ | x3 ⇒ couple exadecimal bool x7 false
+ | x4 ⇒ couple exadecimal bool x8 false
+ | x5 ⇒ couple exadecimal bool x9 false
+ | x6 ⇒ couple exadecimal bool xA false
+ | x7 ⇒ couple exadecimal bool xB false
+ | x8 ⇒ couple exadecimal bool xC false
+ | x9 ⇒ couple exadecimal bool xD false
+ | xA ⇒ couple exadecimal bool xE false
+ | xB ⇒ couple exadecimal bool xF false
+ | xC ⇒ couple exadecimal bool x0 true
+ | xD ⇒ couple exadecimal bool x1 true
+ | xE ⇒ couple exadecimal bool x2 true
+ | xF ⇒ couple exadecimal bool x3 true ]
+ | x4 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x5 false
+ | x1 ⇒ couple exadecimal bool x6 false
+ | x2 ⇒ couple exadecimal bool x7 false
+ | x3 ⇒ couple exadecimal bool x8 false
+ | x4 ⇒ couple exadecimal bool x9 false
+ | x5 ⇒ couple exadecimal bool xA false
+ | x6 ⇒ couple exadecimal bool xB false
+ | x7 ⇒ couple exadecimal bool xC false
+ | x8 ⇒ couple exadecimal bool xD false
+ | x9 ⇒ couple exadecimal bool xE false
+ | xA ⇒ couple exadecimal bool xF false
+ | xB ⇒ couple exadecimal bool x0 true
+ | xC ⇒ couple exadecimal bool x1 true
+ | xD ⇒ couple exadecimal bool x2 true
+ | xE ⇒ couple exadecimal bool x3 true
+ | xF ⇒ couple exadecimal bool x4 true ]
+ | x5 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x6 false
+ | x1 ⇒ couple exadecimal bool x7 false
+ | x2 ⇒ couple exadecimal bool x8 false
+ | x3 ⇒ couple exadecimal bool x9 false
+ | x4 ⇒ couple exadecimal bool xA false
+ | x5 ⇒ couple exadecimal bool xB false
+ | x6 ⇒ couple exadecimal bool xC false
+ | x7 ⇒ couple exadecimal bool xD false
+ | x8 ⇒ couple exadecimal bool xE false
+ | x9 ⇒ couple exadecimal bool xF false
+ | xA ⇒ couple exadecimal bool x0 true
+ | xB ⇒ couple exadecimal bool x1 true
+ | xC ⇒ couple exadecimal bool x2 true
+ | xD ⇒ couple exadecimal bool x3 true
+ | xE ⇒ couple exadecimal bool x4 true
+ | xF ⇒ couple exadecimal bool x5 true ]
+ | x6 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x7 false
+ | x1 ⇒ couple exadecimal bool x8 false
+ | x2 ⇒ couple exadecimal bool x9 false
+ | x3 ⇒ couple exadecimal bool xA false
+ | x4 ⇒ couple exadecimal bool xB false
+ | x5 ⇒ couple exadecimal bool xC false
+ | x6 ⇒ couple exadecimal bool xD false
+ | x7 ⇒ couple exadecimal bool xE false
+ | x8 ⇒ couple exadecimal bool xF false
+ | x9 ⇒ couple exadecimal bool x0 true
+ | xA ⇒ couple exadecimal bool x1 true
+ | xB ⇒ couple exadecimal bool x2 true
+ | xC ⇒ couple exadecimal bool x3 true
+ | xD ⇒ couple exadecimal bool x4 true
+ | xE ⇒ couple exadecimal bool x5 true
+ | xF ⇒ couple exadecimal bool x6 true ]
+ | x7 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x8 false
+ | x1 ⇒ couple exadecimal bool x9 false
+ | x2 ⇒ couple exadecimal bool xA false
+ | x3 ⇒ couple exadecimal bool xB false
+ | x4 ⇒ couple exadecimal bool xC false
+ | x5 ⇒ couple exadecimal bool xD false
+ | x6 ⇒ couple exadecimal bool xE false
+ | x7 ⇒ couple exadecimal bool xF false
+ | x8 ⇒ couple exadecimal bool x0 true
+ | x9 ⇒ couple exadecimal bool x1 true
+ | xA ⇒ couple exadecimal bool x2 true
+ | xB ⇒ couple exadecimal bool x3 true
+ | xC ⇒ couple exadecimal bool x4 true
+ | xD ⇒ couple exadecimal bool x5 true
+ | xE ⇒ couple exadecimal bool x6 true
+ | xF ⇒ couple exadecimal bool x7 true ]
+ | x8 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x9 false
+ | x1 ⇒ couple exadecimal bool xA false
+ | x2 ⇒ couple exadecimal bool xB false
+ | x3 ⇒ couple exadecimal bool xC false
+ | x4 ⇒ couple exadecimal bool xD false
+ | x5 ⇒ couple exadecimal bool xE false
+ | x6 ⇒ couple exadecimal bool xF false
+ | x7 ⇒ couple exadecimal bool x0 true
+ | x8 ⇒ couple exadecimal bool x1 true
+ | x9 ⇒ couple exadecimal bool x2 true
+ | xA ⇒ couple exadecimal bool x3 true
+ | xB ⇒ couple exadecimal bool x4 true
+ | xC ⇒ couple exadecimal bool x5 true
+ | xD ⇒ couple exadecimal bool x6 true
+ | xE ⇒ couple exadecimal bool x7 true
+ | xF ⇒ couple exadecimal bool x8 true ]
+ | x9 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xA false
+ | x1 ⇒ couple exadecimal bool xB false
+ | x2 ⇒ couple exadecimal bool xC false
+ | x3 ⇒ couple exadecimal bool xD false
+ | x4 ⇒ couple exadecimal bool xE false
+ | x5 ⇒ couple exadecimal bool xF false
+ | x6 ⇒ couple exadecimal bool x0 true
+ | x7 ⇒ couple exadecimal bool x1 true
+ | x8 ⇒ couple exadecimal bool x2 true
+ | x9 ⇒ couple exadecimal bool x3 true
+ | xA ⇒ couple exadecimal bool x4 true
+ | xB ⇒ couple exadecimal bool x5 true
+ | xC ⇒ couple exadecimal bool x6 true
+ | xD ⇒ couple exadecimal bool x7 true
+ | xE ⇒ couple exadecimal bool x8 true
+ | xF ⇒ couple exadecimal bool x9 true ]
+ | xA ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xB false
+ | x1 ⇒ couple exadecimal bool xC false
+ | x2 ⇒ couple exadecimal bool xD false
+ | x3 ⇒ couple exadecimal bool xE false
+ | x4 ⇒ couple exadecimal bool xF false
+ | x5 ⇒ couple exadecimal bool x0 true
+ | x6 ⇒ couple exadecimal bool x1 true
+ | x7 ⇒ couple exadecimal bool x2 true
+ | x8 ⇒ couple exadecimal bool x3 true
+ | x9 ⇒ couple exadecimal bool x4 true
+ | xA ⇒ couple exadecimal bool x5 true
+ | xB ⇒ couple exadecimal bool x6 true
+ | xC ⇒ couple exadecimal bool x7 true
+ | xD ⇒ couple exadecimal bool x8 true
+ | xE ⇒ couple exadecimal bool x9 true
+ | xF ⇒ couple exadecimal bool xA true ]
+ | xB ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xC false
+ | x1 ⇒ couple exadecimal bool xD false
+ | x2 ⇒ couple exadecimal bool xE false
+ | x3 ⇒ couple exadecimal bool xF false
+ | x4 ⇒ couple exadecimal bool x0 true
+ | x5 ⇒ couple exadecimal bool x1 true
+ | x6 ⇒ couple exadecimal bool x2 true
+ | x7 ⇒ couple exadecimal bool x3 true
+ | x8 ⇒ couple exadecimal bool x4 true
+ | x9 ⇒ couple exadecimal bool x5 true
+ | xA ⇒ couple exadecimal bool x6 true
+ | xB ⇒ couple exadecimal bool x7 true
+ | xC ⇒ couple exadecimal bool x8 true
+ | xD ⇒ couple exadecimal bool x9 true
+ | xE ⇒ couple exadecimal bool xA true
+ | xF ⇒ couple exadecimal bool xB true ]
+ | xC ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xD false
+ | x1 ⇒ couple exadecimal bool xE false
+ | x2 ⇒ couple exadecimal bool xF false
+ | x3 ⇒ couple exadecimal bool x0 true
+ | x4 ⇒ couple exadecimal bool x1 true
+ | x5 ⇒ couple exadecimal bool x2 true
+ | x6 ⇒ couple exadecimal bool x3 true
+ | x7 ⇒ couple exadecimal bool x4 true
+ | x8 ⇒ couple exadecimal bool x5 true
+ | x9 ⇒ couple exadecimal bool x6 true
+ | xA ⇒ couple exadecimal bool x7 true
+ | xB ⇒ couple exadecimal bool x8 true
+ | xC ⇒ couple exadecimal bool x9 true
+ | xD ⇒ couple exadecimal bool xA true
+ | xE ⇒ couple exadecimal bool xB true
+ | xF ⇒ couple exadecimal bool xC true ]
+ | xD ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xE false
+ | x1 ⇒ couple exadecimal bool xF false
+ | x2 ⇒ couple exadecimal bool x0 true
+ | x3 ⇒ couple exadecimal bool x1 true
+ | x4 ⇒ couple exadecimal bool x2 true
+ | x5 ⇒ couple exadecimal bool x3 true
+ | x6 ⇒ couple exadecimal bool x4 true
+ | x7 ⇒ couple exadecimal bool x5 true
+ | x8 ⇒ couple exadecimal bool x6 true
+ | x9 ⇒ couple exadecimal bool x7 true
+ | xA ⇒ couple exadecimal bool x8 true
+ | xB ⇒ couple exadecimal bool x9 true
+ | xC ⇒ couple exadecimal bool xA true
+ | xD ⇒ couple exadecimal bool xB true
+ | xE ⇒ couple exadecimal bool xC true
+ | xF ⇒ couple exadecimal bool xD true ]
+ | xE ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xF false
+ | x1 ⇒ couple exadecimal bool x0 true
+ | x2 ⇒ couple exadecimal bool x1 true
+ | x3 ⇒ couple exadecimal bool x2 true
+ | x4 ⇒ couple exadecimal bool x3 true
+ | x5 ⇒ couple exadecimal bool x4 true
+ | x6 ⇒ couple exadecimal bool x5 true
+ | x7 ⇒ couple exadecimal bool x6 true
+ | x8 ⇒ couple exadecimal bool x7 true
+ | x9 ⇒ couple exadecimal bool x8 true
+ | xA ⇒ couple exadecimal bool x9 true
+ | xB ⇒ couple exadecimal bool xA true
+ | xC ⇒ couple exadecimal bool xB true
+ | xD ⇒ couple exadecimal bool xC true
+ | xE ⇒ couple exadecimal bool xD true
+ | xF ⇒ couple exadecimal bool xE true ]
+ | xF ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x0 true
+ | x1 ⇒ couple exadecimal bool x1 true
+ | x2 ⇒ couple exadecimal bool x2 true
+ | x3 ⇒ couple exadecimal bool x3 true
+ | x4 ⇒ couple exadecimal bool x4 true
+ | x5 ⇒ couple exadecimal bool x5 true
+ | x6 ⇒ couple exadecimal bool x6 true
+ | x7 ⇒ couple exadecimal bool x7 true
+ | x8 ⇒ couple exadecimal bool x8 true
+ | x9 ⇒ couple exadecimal bool x9 true
+ | xA ⇒ couple exadecimal bool xA true
+ | xB ⇒ couple exadecimal bool xB true
+ | xC ⇒ couple exadecimal bool xC true
+ | xD ⇒ couple exadecimal bool xD true
+ | xE ⇒ couple exadecimal bool xE true
+ | xF ⇒ couple exadecimal bool xF true ]
+ ]
+ | false ⇒
+ match b1 with
+ [ x0 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x0 false
+ | x1 ⇒ couple exadecimal bool x1 false
+ | x2 ⇒ couple exadecimal bool x2 false
+ | x3 ⇒ couple exadecimal bool x3 false
+ | x4 ⇒ couple exadecimal bool x4 false
+ | x5 ⇒ couple exadecimal bool x5 false
+ | x6 ⇒ couple exadecimal bool x6 false
+ | x7 ⇒ couple exadecimal bool x7 false
+ | x8 ⇒ couple exadecimal bool x8 false
+ | x9 ⇒ couple exadecimal bool x9 false
+ | xA ⇒ couple exadecimal bool xA false
+ | xB ⇒ couple exadecimal bool xB false
+ | xC ⇒ couple exadecimal bool xC false
+ | xD ⇒ couple exadecimal bool xD false
+ | xE ⇒ couple exadecimal bool xE false
+ | xF ⇒ couple exadecimal bool xF false ]
+ | x1 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x1 false
+ | x1 ⇒ couple exadecimal bool x2 false
+ | x2 ⇒ couple exadecimal bool x3 false
+ | x3 ⇒ couple exadecimal bool x4 false
+ | x4 ⇒ couple exadecimal bool x5 false
+ | x5 ⇒ couple exadecimal bool x6 false
+ | x6 ⇒ couple exadecimal bool x7 false
+ | x7 ⇒ couple exadecimal bool x8 false
+ | x8 ⇒ couple exadecimal bool x9 false
+ | x9 ⇒ couple exadecimal bool xA false
+ | xA ⇒ couple exadecimal bool xB false
+ | xB ⇒ couple exadecimal bool xC false
+ | xC ⇒ couple exadecimal bool xD false
+ | xD ⇒ couple exadecimal bool xE false
+ | xE ⇒ couple exadecimal bool xF false
+ | xF ⇒ couple exadecimal bool x0 true ]
+ | x2 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x2 false
+ | x1 ⇒ couple exadecimal bool x3 false
+ | x2 ⇒ couple exadecimal bool x4 false
+ | x3 ⇒ couple exadecimal bool x5 false
+ | x4 ⇒ couple exadecimal bool x6 false
+ | x5 ⇒ couple exadecimal bool x7 false
+ | x6 ⇒ couple exadecimal bool x8 false
+ | x7 ⇒ couple exadecimal bool x9 false
+ | x8 ⇒ couple exadecimal bool xA false
+ | x9 ⇒ couple exadecimal bool xB false
+ | xA ⇒ couple exadecimal bool xC false
+ | xB ⇒ couple exadecimal bool xD false
+ | xC ⇒ couple exadecimal bool xE false
+ | xD ⇒ couple exadecimal bool xF false
+ | xE ⇒ couple exadecimal bool x0 true
+ | xF ⇒ couple exadecimal bool x1 true ]
+ | x3 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x3 false
+ | x1 ⇒ couple exadecimal bool x4 false
+ | x2 ⇒ couple exadecimal bool x5 false
+ | x3 ⇒ couple exadecimal bool x6 false
+ | x4 ⇒ couple exadecimal bool x7 false
+ | x5 ⇒ couple exadecimal bool x8 false
+ | x6 ⇒ couple exadecimal bool x9 false
+ | x7 ⇒ couple exadecimal bool xA false
+ | x8 ⇒ couple exadecimal bool xB false
+ | x9 ⇒ couple exadecimal bool xC false
+ | xA ⇒ couple exadecimal bool xD false
+ | xB ⇒ couple exadecimal bool xE false
+ | xC ⇒ couple exadecimal bool xF false
+ | xD ⇒ couple exadecimal bool x0 true
+ | xE ⇒ couple exadecimal bool x1 true
+ | xF ⇒ couple exadecimal bool x2 true ]
+ | x4 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x4 false
+ | x1 ⇒ couple exadecimal bool x5 false
+ | x2 ⇒ couple exadecimal bool x6 false
+ | x3 ⇒ couple exadecimal bool x7 false
+ | x4 ⇒ couple exadecimal bool x8 false
+ | x5 ⇒ couple exadecimal bool x9 false
+ | x6 ⇒ couple exadecimal bool xA false
+ | x7 ⇒ couple exadecimal bool xB false
+ | x8 ⇒ couple exadecimal bool xC false
+ | x9 ⇒ couple exadecimal bool xD false
+ | xA ⇒ couple exadecimal bool xE false
+ | xB ⇒ couple exadecimal bool xF false
+ | xC ⇒ couple exadecimal bool x0 true
+ | xD ⇒ couple exadecimal bool x1 true
+ | xE ⇒ couple exadecimal bool x2 true
+ | xF ⇒ couple exadecimal bool x3 true ]
+ | x5 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x5 false
+ | x1 ⇒ couple exadecimal bool x6 false
+ | x2 ⇒ couple exadecimal bool x7 false
+ | x3 ⇒ couple exadecimal bool x8 false
+ | x4 ⇒ couple exadecimal bool x9 false
+ | x5 ⇒ couple exadecimal bool xA false
+ | x6 ⇒ couple exadecimal bool xB false
+ | x7 ⇒ couple exadecimal bool xC false
+ | x8 ⇒ couple exadecimal bool xD false
+ | x9 ⇒ couple exadecimal bool xE false
+ | xA ⇒ couple exadecimal bool xF false
+ | xB ⇒ couple exadecimal bool x0 true
+ | xC ⇒ couple exadecimal bool x1 true
+ | xD ⇒ couple exadecimal bool x2 true
+ | xE ⇒ couple exadecimal bool x3 true
+ | xF ⇒ couple exadecimal bool x4 true ]
+ | x6 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x6 false
+ | x1 ⇒ couple exadecimal bool x7 false
+ | x2 ⇒ couple exadecimal bool x8 false
+ | x3 ⇒ couple exadecimal bool x9 false
+ | x4 ⇒ couple exadecimal bool xA false
+ | x5 ⇒ couple exadecimal bool xB false
+ | x6 ⇒ couple exadecimal bool xC false
+ | x7 ⇒ couple exadecimal bool xD false
+ | x8 ⇒ couple exadecimal bool xE false
+ | x9 ⇒ couple exadecimal bool xF false
+ | xA ⇒ couple exadecimal bool x0 true
+ | xB ⇒ couple exadecimal bool x1 true
+ | xC ⇒ couple exadecimal bool x2 true
+ | xD ⇒ couple exadecimal bool x3 true
+ | xE ⇒ couple exadecimal bool x4 true
+ | xF ⇒ couple exadecimal bool x5 true ]
+ | x7 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x7 false
+ | x1 ⇒ couple exadecimal bool x8 false
+ | x2 ⇒ couple exadecimal bool x9 false
+ | x3 ⇒ couple exadecimal bool xA false
+ | x4 ⇒ couple exadecimal bool xB false
+ | x5 ⇒ couple exadecimal bool xC false
+ | x6 ⇒ couple exadecimal bool xD false
+ | x7 ⇒ couple exadecimal bool xE false
+ | x8 ⇒ couple exadecimal bool xF false
+ | x9 ⇒ couple exadecimal bool x0 true
+ | xA ⇒ couple exadecimal bool x1 true
+ | xB ⇒ couple exadecimal bool x2 true
+ | xC ⇒ couple exadecimal bool x3 true
+ | xD ⇒ couple exadecimal bool x4 true
+ | xE ⇒ couple exadecimal bool x5 true
+ | xF ⇒ couple exadecimal bool x6 true ]
+ | x8 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x8 false
+ | x1 ⇒ couple exadecimal bool x9 false
+ | x2 ⇒ couple exadecimal bool xA false
+ | x3 ⇒ couple exadecimal bool xB false
+ | x4 ⇒ couple exadecimal bool xC false
+ | x5 ⇒ couple exadecimal bool xD false
+ | x6 ⇒ couple exadecimal bool xE false
+ | x7 ⇒ couple exadecimal bool xF false
+ | x8 ⇒ couple exadecimal bool x0 true
+ | x9 ⇒ couple exadecimal bool x1 true
+ | xA ⇒ couple exadecimal bool x2 true
+ | xB ⇒ couple exadecimal bool x3 true
+ | xC ⇒ couple exadecimal bool x4 true
+ | xD ⇒ couple exadecimal bool x5 true
+ | xE ⇒ couple exadecimal bool x6 true
+ | xF ⇒ couple exadecimal bool x7 true ]
+ | x9 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x9 false
+ | x1 ⇒ couple exadecimal bool xA false
+ | x2 ⇒ couple exadecimal bool xB false
+ | x3 ⇒ couple exadecimal bool xC false
+ | x4 ⇒ couple exadecimal bool xD false
+ | x5 ⇒ couple exadecimal bool xE false
+ | x6 ⇒ couple exadecimal bool xF false
+ | x7 ⇒ couple exadecimal bool x0 true
+ | x8 ⇒ couple exadecimal bool x1 true
+ | x9 ⇒ couple exadecimal bool x2 true
+ | xA ⇒ couple exadecimal bool x3 true
+ | xB ⇒ couple exadecimal bool x4 true
+ | xC ⇒ couple exadecimal bool x5 true
+ | xD ⇒ couple exadecimal bool x6 true
+ | xE ⇒ couple exadecimal bool x7 true
+ | xF ⇒ couple exadecimal bool x8 true ]
+ | xA ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xA false
+ | x1 ⇒ couple exadecimal bool xB false
+ | x2 ⇒ couple exadecimal bool xC false
+ | x3 ⇒ couple exadecimal bool xD false
+ | x4 ⇒ couple exadecimal bool xE false
+ | x5 ⇒ couple exadecimal bool xF false
+ | x6 ⇒ couple exadecimal bool x0 true
+ | x7 ⇒ couple exadecimal bool x1 true
+ | x8 ⇒ couple exadecimal bool x2 true
+ | x9 ⇒ couple exadecimal bool x3 true
+ | xA ⇒ couple exadecimal bool x4 true
+ | xB ⇒ couple exadecimal bool x5 true
+ | xC ⇒ couple exadecimal bool x6 true
+ | xD ⇒ couple exadecimal bool x7 true
+ | xE ⇒ couple exadecimal bool x8 true
+ | xF ⇒ couple exadecimal bool x9 true ]
+ | xB ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xB false
+ | x1 ⇒ couple exadecimal bool xC false
+ | x2 ⇒ couple exadecimal bool xD false
+ | x3 ⇒ couple exadecimal bool xE false
+ | x4 ⇒ couple exadecimal bool xF false
+ | x5 ⇒ couple exadecimal bool x0 true
+ | x6 ⇒ couple exadecimal bool x1 true
+ | x7 ⇒ couple exadecimal bool x2 true
+ | x8 ⇒ couple exadecimal bool x3 true
+ | x9 ⇒ couple exadecimal bool x4 true
+ | xA ⇒ couple exadecimal bool x5 true
+ | xB ⇒ couple exadecimal bool x6 true
+ | xC ⇒ couple exadecimal bool x7 true
+ | xD ⇒ couple exadecimal bool x8 true
+ | xE ⇒ couple exadecimal bool x9 true
+ | xF ⇒ couple exadecimal bool xA true ]
+ | xC ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xC false
+ | x1 ⇒ couple exadecimal bool xD false
+ | x2 ⇒ couple exadecimal bool xE false
+ | x3 ⇒ couple exadecimal bool xF false
+ | x4 ⇒ couple exadecimal bool x0 true
+ | x5 ⇒ couple exadecimal bool x1 true
+ | x6 ⇒ couple exadecimal bool x2 true
+ | x7 ⇒ couple exadecimal bool x3 true
+ | x8 ⇒ couple exadecimal bool x4 true
+ | x9 ⇒ couple exadecimal bool x5 true
+ | xA ⇒ couple exadecimal bool x6 true
+ | xB ⇒ couple exadecimal bool x7 true
+ | xC ⇒ couple exadecimal bool x8 true
+ | xD ⇒ couple exadecimal bool x9 true
+ | xE ⇒ couple exadecimal bool xA true
+ | xF ⇒ couple exadecimal bool xB true ]
+ | xD ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xD false
+ | x1 ⇒ couple exadecimal bool xE false
+ | x2 ⇒ couple exadecimal bool xF false
+ | x3 ⇒ couple exadecimal bool x0 true
+ | x4 ⇒ couple exadecimal bool x1 true
+ | x5 ⇒ couple exadecimal bool x2 true
+ | x6 ⇒ couple exadecimal bool x3 true
+ | x7 ⇒ couple exadecimal bool x4 true
+ | x8 ⇒ couple exadecimal bool x5 true
+ | x9 ⇒ couple exadecimal bool x6 true
+ | xA ⇒ couple exadecimal bool x7 true
+ | xB ⇒ couple exadecimal bool x8 true
+ | xC ⇒ couple exadecimal bool x9 true
+ | xD ⇒ couple exadecimal bool xA true
+ | xE ⇒ couple exadecimal bool xB true
+ | xF ⇒ couple exadecimal bool xC true ]
+ | xE ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xE false
+ | x1 ⇒ couple exadecimal bool xF false
+ | x2 ⇒ couple exadecimal bool x0 true
+ | x3 ⇒ couple exadecimal bool x1 true
+ | x4 ⇒ couple exadecimal bool x2 true
+ | x5 ⇒ couple exadecimal bool x3 true
+ | x6 ⇒ couple exadecimal bool x4 true
+ | x7 ⇒ couple exadecimal bool x5 true
+ | x8 ⇒ couple exadecimal bool x6 true
+ | x9 ⇒ couple exadecimal bool x7 true
+ | xA ⇒ couple exadecimal bool x8 true
+ | xB ⇒ couple exadecimal bool x9 true
+ | xC ⇒ couple exadecimal bool xA true
+ | xD ⇒ couple exadecimal bool xB true
+ | xE ⇒ couple exadecimal bool xC true
+ | xF ⇒ couple exadecimal bool xD true ]
+ | xF ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xF false
+ | x1 ⇒ couple exadecimal bool x0 true
+ | x2 ⇒ couple exadecimal bool x1 true
+ | x3 ⇒ couple exadecimal bool x2 true
+ | x4 ⇒ couple exadecimal bool x3 true
+ | x5 ⇒ couple exadecimal bool x4 true
+ | x6 ⇒ couple exadecimal bool x5 true
+ | x7 ⇒ couple exadecimal bool x6 true
+ | x8 ⇒ couple exadecimal bool x7 true
+ | x9 ⇒ couple exadecimal bool x8 true
+ | xA ⇒ couple exadecimal bool x9 true
+ | xB ⇒ couple exadecimal bool xA true
+ | xC ⇒ couple exadecimal bool xB true
+ | xD ⇒ couple exadecimal bool xC true
+ | xE ⇒ couple exadecimal bool xD true
+ | xF ⇒ couple exadecimal bool xE true ]
+ ]
+ ]
+.
+
+definition plusbyte ≝
+ λb1,b2,c.
+ match plusex (bl b1) (bl b2) c with
+ [ couple l c' ⇒
+ match plusex (bh b1) (bh b2) c' with
+ [ couple h c'' ⇒ couple ? ? (mk_byte h l) c'' ]].
+
alias num (instance 0) = "natural number".
definition nat_of_exadecimal ≝
λb.
| x7 ⇒ 7
| x8 ⇒ 8
| x9 ⇒ 9
- | x10 ⇒ 10
- | x11 ⇒ 11
- | x12 ⇒ 12
- | x13 ⇒ 13
- | x14 ⇒ 14
- | x15 ⇒ 15
+ | xA ⇒ 10
+ | xB ⇒ 11
+ | xC ⇒ 12
+ | xD ⇒ 13
+ | xE ⇒ 14
+ | xF ⇒ 15
].
coercion cic:/matita/assembly/nat_of_exadecimal.con.
coercion cic:/matita/assembly/nat_of_byte.con.
-definition exadecimal_of_nat ≝
- λb.
+let rec exadecimal_of_nat b ≝
match b with [ O ⇒ x0 | S b ⇒
match b with [ O ⇒ x1 | S b ⇒
match b with [ O ⇒ x2 | S b ⇒
match b with [ O ⇒ xC | S b ⇒
match b with [ O ⇒ xD | S b ⇒
match b with [ O ⇒ xE | S b ⇒
- match b with [ O ⇒ xF | S b ⇒ x0]]]]]]]]]]]]]]]].
+ match b with [ O ⇒ xF | S b ⇒ exadecimal_of_nat b ]]]]]]]]]]]]]]]].
definition byte_of_nat ≝
- λn. mk_byte (exadecimal_of_nat ((n / 16) \mod 16)) (exadecimal_of_nat (n \mod 16)).
-
+ λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n).
+
lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
intros;
elim b;
reflexivity.
qed.
-lemma sign_ok: byte_of_nat 257 = mk_byte x0 x1.
+lemma lt_nat_of_exadecimal_16: ∀b. nat_of_exadecimal b < 16.
+ intro;
+ elim b;
+ simplify;
+ autobatch.
+qed.
+
+lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256.
+ intro;
+ unfold nat_of_byte;
+ letin H ≝ (lt_nat_of_exadecimal_16 (bh b)); clearbody H;
+ letin K ≝ (lt_nat_of_exadecimal_16 (bl b)); clearbody K;
+ unfold lt in H K ⊢ %;
+ letin H' ≝ (le_S_S_to_le ? ? H); clearbody H'; clear H;
+ letin K' ≝ (le_S_S_to_le ? ? K); clearbody K'; clear K;
+ apply le_S_S;
+ cut (16*bh b ≤ 16*15);
+ [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
+ simplify in Hf:(? ? %);
+ assumption
+ | autobatch
+ ]
+qed.
+
+lemma le_to_lt: ∀n,m. n ≤ m → n < S m.
+ intros;
+ autobatch.
+qed.
+
+axiom daemon: False.
+
+lemma exadecimal_of_nat_mod:
+ ∀n.exadecimal_of_nat n = exadecimal_of_nat (n \mod 16).
+ elim daemon.
+(*
+ intros;
+ cases n; [ reflexivity | ];
+ cases n1; [ reflexivity | ];
+ cases n2; [ reflexivity | ];
+ cases n3; [ reflexivity | ];
+ cases n4; [ reflexivity | ];
+ cases n5; [ reflexivity | ];
+ cases n6; [ reflexivity | ];
+ cases n7; [ reflexivity | ];
+ cases n8; [ reflexivity | ];
+ cases n9; [ reflexivity | ];
+ cases n10; [ reflexivity | ];
+ cases n11; [ reflexivity | ];
+ cases n12; [ reflexivity | ];
+ cases n13; [ reflexivity | ];
+ cases n14; [ reflexivity | ];
+ cases n15; [ reflexivity | ];
+ change in ⊢ (? ? ? (? (? % ?))) with (16 + n16);
+ cut ((16 + n16) \mod 16 = n16 \mod 16);
+ [ rewrite > Hcut;
+ simplify in ⊢ (? ? % ?);
+
+ | unfold mod;
+ change with (mod_aux (16+n16) (16+n16) 15 = n16);
+ unfold mod_aux;
+ change with
+ (match leb (16+n16) 15 with
+ [true ⇒ 16+n16
+ | false ⇒ mod_aux (15+n16) ((16+n16) - 16) 15
+ ] = n16);
+ cut (leb (16+n16) 15 = false);
+ [ rewrite > Hcut;
+ change with (mod_aux (15+n16) (16+n16-16) 15 = n16);
+ cut (16+n16-16 = n16);
+ [ rewrite > Hcut1; clear Hcut1;
+
+ |
+ ]
+ |
+ ]
+ ]*)
+qed.
+
+(*lemma exadecimal_of_nat_elim:
+ ∀P:exadecimal → Prop.
+ (∀m. m < 16 → P (exadecimal_of_nat m)) →
+ ∀n. P (exadecimal_of_nat n).
+ intros;
+ cases n; [ apply H; autobatch | ]; clear n;
+ cases n1; [ apply H; autobatch | ]; clear n1;
+ cases n; [ apply H; autobatch | ]; clear n;
+ cases n1; [ apply H; autobatch | ]; clear n1;
+ cases n; [ apply H; autobatch | ]; clear n;
+ cases n1; [ apply H; autobatch | ]; clear n1;
+ cases n; [ apply H; autobatch | ]; clear n;
+ cases n1; [ apply H; autobatch | ]; clear n1;
+ cases n; [ apply H; autobatch | ]; clear n;
+ cases n1; [ apply H; autobatch | ]; clear n1;
+ cases n; [ apply H; autobatch | ]; clear n;
+ cases n1; [ apply H; autobatch | ]; clear n1;
+ cases n; [ apply H; autobatch | ]; clear n;
+ cases n1; [ apply H; autobatch | ]; clear n1;
+ cases n; [ apply H; autobatch | ]; clear n;
+ cases n1; [ apply H; autobatch | ]; clear n1;
+ simplify;
+ elim daemon.
+qed.
+*)
+
+axiom nat_of_exadecimal_exadecimal_of_nat:
+ ∀n. nat_of_exadecimal (exadecimal_of_nat n) = n \mod 16.
+(*
+ intro;
+ apply (exadecimal_of_nat_elim (λn.;
+
+
+
+ elim n 0; [ reflexivity | intro ];
+ elim n1 0; [ intros; reflexivity | intros 2 ];
+ elim n2 0; [ intros; reflexivity | intros 2 ];
+ elim n3 0; [ intros; reflexivity | intros 2 ];
+ elim n4 0; [ intros; reflexivity | intros 2 ];
+ elim n5 0; [ intros; reflexivity | intros 2 ];
+ elim n6 0; [ intros; reflexivity | intros 2 ];
+ elim n7 0; [ intros; reflexivity | intros 2 ];
+ elim n8 0; [ intros; reflexivity | intros 2 ];
+ elim n9 0; [ intros; reflexivity | intros 2 ];
+ elim n10 0; [ intros; reflexivity | intros 2 ];
+ elim n11 0; [ intros; reflexivity | intros 2 ];
+ elim n12 0; [ intros; reflexivity | intros 2 ];
+ elim n13 0; [ intros; reflexivity | intros 2 ];
+ elim n14 0; [ intros; reflexivity | intros 2 ];
+ elim n15 0; [ intros; reflexivity | intros 2 ];
+ intro;
+ simplify;
+ rewrite < H15;
+ change in ⊢ (? ? % ?) with (nat_of_exadecimal (exadecimal_of_nat n16));
+qed.
+*)
+
+lemma nat_of_byte_byte_of_nat: ∀n. nat_of_byte (byte_of_nat n) = n \mod 256.
+ intro;
+ unfold byte_of_nat;
+ unfold nat_of_byte;
+ change with (16*(exadecimal_of_nat (n/16)) + exadecimal_of_nat n = n \mod 256);
+ rewrite > nat_of_exadecimal_exadecimal_of_nat in ⊢ (? ? (? (? ? %) ?) ?);
+ rewrite > nat_of_exadecimal_exadecimal_of_nat;
+ elim daemon.
+qed.
+
+definition nat_of_bool ≝
+ λb. match b with [ true ⇒ 1 | false ⇒ 0 ].
+
+lemma plusex_ok:
+ ∀b1,b2,c.
+ match plusex b1 b2 c with
+ [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecimal r + nat_of_bool c' * 16 ].
+ intros;
+ elim c;
+ elim b1;
+ elim b2;
+ normalize;
reflexivity.
qed.
-
+
+lemma plusbyte_ok:
+ ∀b1,b2,c.
+ match plusbyte b1 b2 c with
+ [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c' * 256
+ ].
+ intros;
+ unfold plusbyte;
+ generalize in match (plusex_ok (bl b1) (bl b2) c);
+ elim (plusex (bl b1) (bl b2) c);
+ simplify in H ⊢ %;
+ generalize in match (plusex_ok (bh b1) (bh b2) t1);
+ elim (plusex (bh b1) (bh b2) t1);
+ simplify in H1 ⊢ %;
+ change in ⊢ (? ? ? (? (? % ?) ?)) with (16 * t2);
+ unfold nat_of_byte;
+ letin K ≝ (eq_f ? ? (λy.16*y) ? ? H1); clearbody K; clear H1;
+ rewrite > distr_times_plus in K:(? ? ? %);
+ rewrite > symmetric_times in K:(? ? ? (? ? (? ? %)));
+ rewrite < associative_times in K:(? ? ? (? ? %));
+ normalize in K:(? ? ? (? ? (? % ?)));
+ rewrite > symmetric_times in K:(? ? ? (? ? %));
+ rewrite > sym_plus in ⊢ (? ? ? (? % ?));
+ rewrite > associative_plus in ⊢ (? ? ? %);
+ letin K' ≝ (eq_f ? ? (plus t) ? ? K); clearbody K'; clear K;
+ apply transitive_eq; [3: apply K' | skip | ];
+ clear K';
+ rewrite > sym_plus in ⊢ (? ? (? (? ? %) ?) ?);
+ rewrite > associative_plus in ⊢ (? ? (? % ?) ?);
+ rewrite > associative_plus in ⊢ (? ? % ?);
+ rewrite > associative_plus in ⊢ (? ? (? ? %) ?);
+ rewrite > associative_plus in ⊢ (? ? (? ? (? ? %)) ?);
+ rewrite > sym_plus in ⊢ (? ? (? ? (? ? (? ? %))) ?);
+ rewrite < associative_plus in ⊢ (? ? (? ? (? ? %)) ?);
+ rewrite < associative_plus in ⊢ (? ? (? ? %) ?);
+ rewrite < associative_plus in ⊢ (? ? (? ? (? % ?)) ?);
+ rewrite > H; clear H;
+ autobatch paramodulation.
+qed.
+
+(*
+lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256.
+ intros; elim n; [ reflexivity | unfold byte_of_nat.
+qed.
+*)
+
definition addr ≝ nat.
definition xpred ≝
| false ⇒ mk_byte (bh b) (xpred (bl b))
].
-(* way too slow!
+(* Way too slow and subsumed by previous theorem
lemma bpred_pred:
∀b.
match eqbyte b (mk_byte x0 x0) with
elim b;
elim e;
elim e1;
- whd;
reflexivity.
qed.
*)
| STAd ⇒ 3
].
-inductive cartesian_product (A,B: Type) : Type ≝
- couple: ∀a:A.∀b:B. cartesian_product A B.
-
definition opcodemap ≝
[ couple ? ? ADDd (mk_byte xA xB);
couple ? ? BEQ (mk_byte x3 x7);
[ true ⇒ v
| false ⇒ f x ].
+lemma update_update_a_a:
+ ∀s,a,v1,v2,b.
+ update (update s a v1) a v2 b = update s a v2 b.
+ intros;
+ unfold update;
+ unfold update;
+ elim (eqb b a);
+ reflexivity.
+qed.
+
+lemma update_update_a_b:
+ ∀s,a1,v1,a2,v2,b.
+ a1 ≠ a2 →
+ update (update s a1 v1) a2 v2 b = update (update s a2 v2) a1 v1 b.
+ intros;
+ unfold update;
+ unfold update;
+ apply (bool_elim ? (eqb b a1)); intros;
+ apply (bool_elim ? (eqb b a2)); intros;
+ simplify;
+ [ elim H;
+ rewrite < (eqb_true_to_eq ? ? H1);
+ apply eqb_true_to_eq;
+ assumption
+ |*: reflexivity
+ ].
+qed.
+
+definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
+
definition tick ≝
- λs:status.
- (* fetch *)
- let opc ≝ opcode_of_byte (mem s (pc s)) in
- let op1 ≝ mem s (S (pc s)) in
+ λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒
+ let opc ≝ opcode_of_byte (mem pc) in
+ let op1 ≝ mem (S pc) in
let clk' ≝ cycles_of_opcode opc in
- match eqb (S (clk s)) clk' with
+ match eqb (S clk) clk' with
[ true ⇒
match opc with
[ ADDd ⇒
- let x ≝ nat_of_byte (mem s op1) in
- let acc' ≝ x + acc s in (* signed!!! *)
- mk_status (byte_of_nat acc') (2 + pc s) (spc s)
- (eqb O acc') (cf s) (mem s) 0
+ let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *)
+ let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in
+ let c' ≝ match res with [ couple _ c' ⇒ c'] in
+ mk_status acc' (2 + pc) spc
+ (eqbyte (mk_byte x0 x0) acc') c' mem 0 (* verify carrier! *)
| BEQ ⇒
mk_status
- (acc s)
- (match zf s with
- [ true ⇒ 2 + op1 + pc s (* signed!!! *)
- | false ⇒ 2 + pc s
+ acc
+ (match zf with
+ [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*) (* signed!!! *)
+ | false ⇒ 2 + pc
])
- (spc s)
- (zf s)
- (cf s)
- (mem s)
+ spc
+ zf
+ cf
+ mem
0
| BRA ⇒
mk_status
- (acc s) (2 + op1 + pc s) (* signed!!! *)
- (spc s)
- (zf s)
- (cf s)
- (mem s)
+ acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
+ spc
+ zf
+ cf
+ mem
0
| DECd ⇒
- let x ≝ bpred (mem s op1) in (* signed!!! *)
- let mem' ≝ update (mem s) op1 x in
- mk_status (acc s) (2 + pc s) (spc s)
- (eqb O x) (cf s) mem' 0 (* check zb!!! *)
+ let x ≝ bpred (mem op1) in (* signed!!! *)
+ let mem' ≝ update mem op1 x in
+ mk_status acc (2 + pc) spc
+ (eqbyte (mk_byte x0 x0) x) cf mem' 0 (* check zb!!! *)
| LDAi ⇒
- mk_status op1 (2 + pc s) (spc s) (eqb O op1) (cf s) (mem s) 0
+ mk_status op1 (2 + pc) spc (eqbyte (mk_byte x0 x0) op1) cf mem 0
| LDAd ⇒
- let x ≝ bpred (mem s op1) in
- mk_status x (2 + pc s) (spc s) (eqb O x) (cf s) (mem s) 0
+ let x ≝ mem op1 in
+ mk_status x (2 + pc) spc (eqbyte (mk_byte x0 x0) x) cf mem 0
| STAd ⇒
- mk_status (acc s) (2 + pc s) (spc s) (zf s) (cf s)
- (update (mem s) op1 (acc s)) 0
+ mk_status acc (2 + pc) spc zf cf
+ (update mem op1 acc) 0
]
| false ⇒
mk_status
- (acc s) (pc s) (spc s) (zf s) (cf s) (mem s) (S (clk s))
- ].
+ acc pc spc zf cf mem (S clk)
+ ]].
let rec execute s n on n ≝
match n with
| S n' ⇒ execute (tick s) n'
].
-lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
- intros; reflexivity.
+lemma breakpoint:
+ ∀s,n1,n2. execute s (n1 + n2) = execute (execute s n1) n2.
+ intros;
+ generalize in match s; clear s;
+ elim n1;
+ [ reflexivity
+ | simplify;
+ apply H;
+ ]
qed.
notation "hvbox(# break a)"
(cic:/matita/assembly/byte_of_opcode.con a).
definition mult_source : list byte ≝
- [#LDAi; mk_byte x0 x0;
- #STAd; mk_byte x2 x0; (* 18 = locazione $12 *)
- #LDAd; mk_byte x1 xF; (* 17 = locazione $11 *)
- #BEQ; mk_byte x0 xC;
- #LDAd; mk_byte x1 x2;
- #DECd; mk_byte x1 xF;
- #ADDd; mk_byte x1 xE; (* 16 = locazione $10 *)
- #STAd; mk_byte x2 x0;
- #LDAd; mk_byte x1 xF;
- #BRA; mk_byte xF x2; (* 242 = -14 *)
- #LDAd; mk_byte x2 x0].
+ [#LDAi; mk_byte x0 x0; (* A := 0 *)
+ #STAd; mk_byte x2 x0; (* Z := A *)
+ #LDAd; mk_byte x1 xF; (* (l1) A := Y *)
+ #BEQ; mk_byte x0 xA; (* if A == 0 then goto l2 *)
+ #LDAd; mk_byte x2 x0; (* A := Z *)
+ #DECd; mk_byte x1 xF; (* Y := Y - 1 *)
+ #ADDd; mk_byte x1 xE; (* A += X *)
+ #STAd; mk_byte x2 x0; (* Z := A *)
+ #BRA; mk_byte xF x2; (* goto l1 *)
+ #LDAd; mk_byte x2 x0].(* (l2) *)
-definition mult_status ≝
- λx,y.
- mk_status (mk_byte x0 x0) 0 0 false false
- (λa:addr.
+definition mult_memory ≝
+ λx,y.λa:addr.
match leb a 29 with
[ true ⇒ nth ? mult_source (mk_byte x0 x0) a
| false ⇒
[ true ⇒ x
| false ⇒ y
]
- ]) 0.
+ ].
-lemma goo1:
- ∀x.
- (λi.
- let s ≝ execute (mult_status x (mk_byte x0 x0)) i in
- pc s = 22 ∧ mem s 32 = byte_of_nat 0) 14.
+definition mult_status ≝
+ λx,y.
+ mk_status (mk_byte x0 x0) 0 0 false false (mult_memory x y) 0.
+
+lemma plusbyte_O_x:
+ ∀b. plusbyte (mk_byte x0 x0) b false = couple ? ? b false.
+ intros;
+ elim b;
+ elim e;
+ elim e1;
+ reflexivity.
+qed.
+
+definition plusbytenc ≝
+ λx,y.
+ match plusbyte x y false with
+ [couple res _ ⇒ res].
+
+definition plusbytec ≝
+ λx,y.
+ match plusbyte x y false with
+ [couple _ c ⇒ c].
+
+lemma plusbytenc_O_x:
+ ∀x. plusbytenc (mk_byte x0 x0) x = x.
+ intros;
+ unfold plusbytenc;
+ rewrite > plusbyte_O_x;
+ reflexivity.
+qed.
+
+axiom mod_plus: ∀a,b,m. (a + b) \mod m = a \mod m + b \mod m.
+axiom eq_mod_times_n_m_m_O: ∀n,m. O < m → n * m \mod m = O.
+
+axiom eq_nat_of_byte_mod: ∀b. nat_of_byte b = nat_of_byte b \mod 256.
+
+theorem plusbytenc_ok:
+ ∀b1,b2:byte. nat_of_byte (plusbytenc b1 b2) = (b1 + b2) \mod 256.
intros;
- whd;
+ unfold plusbytenc;
+ generalize in match (plusbyte_ok b1 b2 false);
+ elim (plusbyte b1 b2 false);
+ simplify in H ⊢ %;
+ change with (nat_of_byte t = (b1 + b2) \mod 256);
+ rewrite < plus_n_O in H;
+ rewrite > H; clear H;
+ rewrite > mod_plus;
+ letin K ≝ (eq_nat_of_byte_mod t); clearbody K;
+ letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool t1) 256 ?); clearbody K';
+ [ autobatch | ];
+ autobatch paramodulation.
+qed.
+
+lemma test_O_O:
+ let i ≝ 14 in
+ let s ≝ execute (mult_status (mk_byte x0 x0) (mk_byte x0 x0)) i in
+ pc s = 20 ∧ mem s 32 = byte_of_nat 0.
+ normalize;
split;
- [ reduce;
- reflexivity
- | reduce;
- reflexivity
- ].
+ reflexivity.
+qed.
+
+lemma test_0_2:
+ let x ≝ mk_byte x0 x0 in
+ let y ≝ mk_byte x0 x2 in
+ let i ≝ 14 + 23 * nat_of_byte y in
+ let s ≝ execute (mult_status x y) i in
+ pc s = 20 ∧ mem s 32 = plusbytenc x x.
+ intros;
+ split;
+ reflexivity.
+qed.
-lemma goo1:
+lemma test_x_1:
∀x.
- let i ≝ 14 in
- let s ≝ execute (mult_status x (mk_byte x0 x0)) i in
- pc s = 22 ∧ mem s 32 = byte_of_nat 0.
+ let y ≝ mk_byte x0 x1 in
+ let i ≝ 14 + 23 * nat_of_byte y in
+ let s ≝ execute (mult_status x y) i in
+ pc s = 20 ∧ mem s 32 = x.
intros;
split;
- [ reduce;
-
- |
+ [ reflexivity
+ | change in ⊢ (? ? % ?) with (plusbytenc (mk_byte x0 x0) x);
+ rewrite > plusbytenc_O_x;
+ reflexivity
].
qed.
-lemma goo1:
- ∀x,y.
+lemma test_x_2:
+ ∀x.
+ let y ≝ mk_byte x0 x2 in
let i ≝ 14 + 23 * nat_of_byte y in
let s ≝ execute (mult_status x y) i in
- pc s = 22 ∧ mem s 32 = byte_of_nat (nat_of_byte x * nat_of_byte y).
+ pc s = 20 ∧ mem s 32 = plusbytenc x x.
+ intros;
+ split;
+ [ reflexivity
+ | change in ⊢ (? ? % ?) with
+ (plusbytenc (plusbytenc (mk_byte x0 x0) x) x);
+ rewrite > plusbytenc_O_x;
+ reflexivity
+ ].
+qed.
+
+theorem lt_trans: ∀x,y,z. x < y → y < z → x < z.
+ unfold lt;
intros;
+ autobatch.
qed.
-lemma goo: True.
- letin s0 ≝ mult_status;
- letin pc0 ≝ (pc s0);
- reduce in pc0;
- letin i0 ≝ (opcode_of_byte (mem s0 pc0));
- reduce in i0;
-
- letin s1 ≝ (execute s0 (cycles_of_opcode i0));
- letin pc1 ≝ (pc s1);
- reduce in pc1;
- letin i1 ≝ (opcode_of_byte (mem s1 pc1));
- reduce in i1;
-
- letin s2 ≝ (execute s1 (cycles_of_opcode i1));
- letin pc2 ≝ (pc s2);
- reduce in pc2;
- letin i2 ≝ (opcode_of_byte (mem s2 pc2));
- reduce in i2;
-
- letin s3 ≝ (execute s2 (cycles_of_opcode i2));
- letin pc3 ≝ (pc s3);
- reduce in pc3;
- letin i3 ≝ (opcode_of_byte (mem s3 pc3));
- reduce in i3;
- letin zf3 ≝ (zf s3);
- reduce in zf3;
-
- letin s4 ≝ (execute s3 (cycles_of_opcode i3));
- letin pc4 ≝ (pc s4);
- reduce in pc4;
- letin i4 ≝ (opcode_of_byte (mem s4 pc4));
- reduce in i4;
-
- letin s5 ≝ (execute s4 (cycles_of_opcode i4));
- letin pc5 ≝ (pc s5);
- reduce in pc5;
- letin i5 ≝ (opcode_of_byte (mem s5 pc5));
- reduce in i5;
-
- letin s6 ≝ (execute s5 (cycles_of_opcode i5));
- letin pc6 ≝ (pc s6);
- reduce in pc6;
- letin i6 ≝ (opcode_of_byte (mem s6 pc6));
- reduce in i6;
-
- letin s7 ≝ (execute s6 (cycles_of_opcode i6));
- letin pc7 ≝ (pc s7);
- reduce in pc7;
- letin i7 ≝ (opcode_of_byte (mem s7 pc7));
- reduce in i7;
+axiom status_eq:
+ ∀s,s'.
+ acc s = acc s' →
+ pc s = pc s' →
+ spc s = spc s' →
+ zf s = zf s' →
+ cf s = cf s' →
+ (∀a. mem s a = mem s' a) →
+ clk s = clk s' →
+ s=s'.
+
+lemma eq_eqex_S_x0_false:
+ ∀n. n < 15 → eqex x0 (exadecimal_of_nat (S n)) = false.
+ intro;
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ intro;
+ unfold lt in H;
+ cut (S n1 ≤ 0);
+ [ elim (not_le_Sn_O ? Hcut)
+ | do 15 (apply le_S_S_to_le);
+ assumption
+ ]
+qed.
+
+lemma leq_m_n_to_eq_div_n_m_S: ∀n,m:nat. 0 < m → m ≤ n → ∃z. n/m = S z.
+ intros;
+ unfold div;
+ apply (ex_intro ? ? (div_aux (pred n) (n-m) (pred m)));
+ cut (∃w.m = S w);
+ [ elim Hcut;
+ rewrite > H2;
+ rewrite > H2 in H1;
+ clear Hcut; clear H2; clear H; (*clear m;*)
+ simplify;
+ unfold in ⊢ (? ? % ?);
+ cut (∃z.n = S z);
+ [ elim Hcut; clear Hcut;
+ rewrite > H in H1;
+ rewrite > H; clear m;
+ change in ⊢ (? ? % ?) with
+ (match leb (S a1) a with
+ [ true ⇒ O
+ | false ⇒ S (div_aux a1 ((S a1) - S a) a)]);
+ cut (S a1 ≰ a);
+ [ apply (leb_elim (S a1) a);
+ [ intro;
+ elim (Hcut H2)
+ | intro;
+ simplify;
+ reflexivity
+ ]
+ | intro;
+ autobatch
+ ]
+ | elim H1; autobatch
+ ]
+ | autobatch
+ ].
+qed.
+
+lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
+ ∀b. b < 255 → eqbyte (mk_byte x0 x0) (byte_of_nat (S b)) = false.
+ intros;
+ unfold byte_of_nat;
+ cut (b < 15 ∨ b ≥ 15);
+ [ elim Hcut;
+ [ unfold eqbyte;
+ change in ⊢ (? ? (? ? %) ?) with (eqex x0 (exadecimal_of_nat (S b)));
+ rewrite > eq_eqex_S_x0_false;
+ [ alias id "andb_sym" = "cic:/matita/nat/propr_div_mod_lt_le_totient1_aux/andb_sym.con".
+ rewrite > andb_sym;
+ reflexivity
+ | assumption
+ ]
+ | unfold eqbyte;
+ change in ⊢ (? ? (? % ?) ?) with (eqex x0 (exadecimal_of_nat (S b/16)));
+ letin K ≝ (leq_m_n_to_eq_div_n_m_S (S b) 16 ? ?);
+ [ autobatch
+ | unfold in H1;
+ apply le_S_S;
+ assumption
+ | clearbody K;
+ elim K; clear K;
+ rewrite > H2;
+ rewrite > eq_eqex_S_x0_false;
+ [ reflexivity
+ | unfold lt;
+ unfold lt in H;
+ rewrite < H2;
+ clear H2; clear a; clear H1; clear Hcut;
+ elim daemon (* trivial arithmetic property over <= and div *)
+ ]
+ ]
+ ]
+ | elim daemon
+ ].
+qed.
+
+lemma eq_bpred_S_a_a:
+ ∀a. a < 255 → bpred (byte_of_nat (S a)) = byte_of_nat a.
+elim daemon. (*
+ intros;
+ unfold byte_of_nat;
+ cut (a \mod 16 = 15 ∨ a \mod 16 < 15);
+ [ elim Hcut;
+ [
+ |
+ ]
+ | autobatch
+ ].*)
+qed.
- letin s8 ≝ (execute s7 (cycles_of_opcode i7));
- letin pc8 ≝ (pc s8);
- reduce in pc8;
- letin i8 ≝ (opcode_of_byte (mem s8 pc8));
- reduce in i8;
-
- letin s9 ≝ (execute s8 (cycles_of_opcode i8));
- letin pc9 ≝ (pc s9);
- reduce in pc9;
- letin i9 ≝ (opcode_of_byte (mem s9 pc9));
- reduce in i9;
+lemma plusbyteenc_S:
+ ∀x:byte.∀n.plusbytenc (byte_of_nat (x*n)) x = byte_of_nat (x * S n).
+ intros;
+ rewrite < byte_of_nat_nat_of_byte;
+ rewrite > (plusbytenc_ok (byte_of_nat (x*n)) x);
+ rewrite > na
+
+(*CSC*)
+ intros;
+ unfold byte_of_nat;
+ unfold plusbytenc;
+ unfold plusbyte;
- exact I.
+ elim daemon.
+qed.
+
+lemma eq_plusbytec_x0_x0_x_false:
+ ∀x.plusbytec (mk_byte x0 x0) x = false.
+ intro;
+ elim x;
+ elim e;
+ elim e1;
+ reflexivity.
+qed.
+
+lemma loop_invariant':
+ ∀x,y:byte.∀j:nat. j ≤ y →
+ execute (mult_status x y) (5 + 23*j)
+ =
+ mk_status (byte_of_nat (x * j)) 4 0 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*j)))
+ (plusbytec (byte_of_nat (x*pred j)) x)
+ (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32
+ (byte_of_nat (x * j)))
+ 0.
+ intros 3;
+ elim j;
+ [ do 2 (rewrite < times_n_O);
+ apply status_eq;
+ [1,2,3,4,7: normalize; reflexivity
+ | rewrite > eq_plusbytec_x0_x0_x_false;
+ normalize;
+ reflexivity
+ | intro;
+ elim daemon
+ ]
+ | cut (5 + 23 * S n = 5 + 23 * n + 23);
+ [ letin K ≝ (breakpoint (mult_status x y) (5 + 23 * n) 23); clearbody K;
+ letin H' ≝ (H ?); clearbody H'; clear H;
+ [ autobatch
+ | letin xxx ≝ (eq_f ? ? (λz. execute (mult_status x y) z) ? ? Hcut); clearbody xxx;
+ clear Hcut;
+ rewrite > xxx;
+ clear xxx;
+ apply (transitive_eq ? ? ? ? K);
+ clear K;
+ rewrite > H';
+ clear H';
+ cut (∃z.y-n=S z ∧ z < 255);
+ [ elim Hcut; clear Hcut;
+ elim H; clear H;
+ rewrite > H2;
+ (* instruction LDAd *)
+ letin K ≝
+ (breakpoint
+ (mk_status (byte_of_nat (x*n)) 4 O
+ (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
+ (plusbytec (byte_of_nat (x*pred n)) x)
+ (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
+ (byte_of_nat (x*n))) O)
+ 3 20); clearbody K;
+ normalize in K:(? ? (? ? %) ?);
+ apply transitive_eq; [2: apply K | skip | ]; clear K;
+ whd in ⊢ (? ? (? % ?) ?);
+ normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
+ change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?)
+ with (byte_of_nat (S a));
+ change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
+ (byte_of_nat (S a));
+ (* instruction BEQ *)
+ letin K ≝
+ (breakpoint
+ (mk_status (byte_of_nat (S a)) 6 O
+ (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
+ (plusbytec (byte_of_nat (x*pred n)) x)
+ (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
+ (byte_of_nat (x*n))) O)
+ 3 17); clearbody K;
+ normalize in K:(? ? (? ? %) ?);
+ apply transitive_eq; [2: apply K | skip | ]; clear K;
+ whd in ⊢ (? ? (? % ?) ?);
+ letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
+ rewrite > K; clear K;
+ simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
+ (* instruction LDAd *)
+ letin K ≝
+ (breakpoint
+ (mk_status (byte_of_nat (S a)) 8 O
+ (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
+ (plusbytec (byte_of_nat (x*pred n)) x)
+ (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
+ (byte_of_nat (x*n))) O)
+ 3 14); clearbody K;
+ normalize in K:(? ? (? ? %) ?);
+ apply transitive_eq; [2: apply K | skip | ]; clear K;
+ whd in ⊢ (? ? (? % ?) ?);
+ change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
+ normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
+ change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)));
+ (* instruction DECd *)
+ letin K ≝
+ (breakpoint
+ (mk_status (byte_of_nat (x*n)) 10 O
+ (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
+ (plusbytec (byte_of_nat (x*pred n)) x)
+ (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
+ (byte_of_nat (x*n))) O)
+ 5 9); clearbody K;
+ normalize in K:(? ? (? ? %) ?);
+ apply transitive_eq; [2: apply K | skip | ]; clear K;
+ whd in ⊢ (? ? (? % ?) ?);
+ change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a)));
+ rewrite > (eq_bpred_S_a_a ? H3);
+ normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
+ normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
+ cut (y - S n = a);
+ [2: elim daemon | ];
+ rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;
+ (* instruction ADDd *)
+ letin K ≝
+ (breakpoint
+ (mk_status (byte_of_nat (x*n)) 12
+ O (eqbyte (mk_byte x0 x0) (byte_of_nat (y-S n)))
+ (plusbytec (byte_of_nat (x*pred n)) x)
+ (update
+ (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
+ 32 (byte_of_nat (x*n))) 31
+ (byte_of_nat (y-S n))) O)
+ 3 6); clearbody K;
+ normalize in K:(? ? (? ? %) ?);
+ apply transitive_eq; [2: apply K | skip | ]; clear K;
+ whd in ⊢ (? ? (? % ?) ?);
+ change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
+ (plusbytenc (byte_of_nat (x*n)) x);
+ change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
+ (plusbytenc (byte_of_nat (x*n)) x);
+ normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
+ change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?)
+ with (plusbytec (byte_of_nat (x*n)) x);
+ rewrite > plusbyteenc_S;
+ (* instruction STAd *)
+ letin K ≝
+ (breakpoint
+ (mk_status (byte_of_nat (x*S n)) 14 O
+ (eqbyte (mk_byte x0 x0) (byte_of_nat (x*S n)))
+ (plusbytec (byte_of_nat (x*n)) x)
+ (update
+ (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
+ 32 (byte_of_nat (x*n))) 31
+ (byte_of_nat (y-S n))) O)
+ 3 3); clearbody K;
+ normalize in K:(? ? (? ? %) ?);
+ apply transitive_eq; [2: apply K | skip | ]; clear K;
+ whd in ⊢ (? ? (? % ?) ?);
+ normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
+ (* instruction BRA *)
+ whd in ⊢ (? ? % ?);
+ normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
+ rewrite < pred_Sn;
+ apply status_eq;
+ [1,2,3,4,7: normalize; reflexivity
+ | change with (plusbytec (byte_of_nat (x*n)) x =
+ plusbytec (byte_of_nat (x*n)) x);
+ reflexivity
+ |6: intro;
+ elim daemon
+ ]
+ | exists;
+ [ apply (y - S n)
+ | split;
+ [ rewrite < (minus_S_S y n);
+ autobatch
+ | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
+ letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
+ autobatch
+ ]
+ ]
+ ]
+ ]
+ | rewrite > associative_plus;
+ autobatch paramodulation
+ ]
+ ]
+qed.
+
+theorem test_x_y:
+ ∀x,y:byte.
+ let i ≝ 14 + 23 * y in
+ execute (mult_status x y) i =
+ mk_status (byte_of_nat (x*y)) 20 0
+ (eqbyte (mk_byte x0 x0) (byte_of_nat (x*y)))
+ (plusbytec (byte_of_nat (x*pred y)) x)
+ (update
+ (update (mult_memory x y) 31 (mk_byte x0 x0))
+ 32 (byte_of_nat (x*y)))
+ 0.
+ intros;
+ cut (14 + 23 * y = 5 + 23*y + 9);
+ [2: autobatch paramodulation;
+ | rewrite > Hcut; (* clear Hcut; *)
+ rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
+ rewrite > loop_invariant';
+ [2: apply le_n
+ | rewrite < minus_n_n;
+ apply status_eq;
+ [1,2,3,4,5,7: normalize; reflexivity
+ | elim daemon
+ ]
+ ]
+ ].
qed.
projects / helm.git / blobdiff