(* Formalisation of bits and bytes *) Module byte Import lib_bool ; Inductive [bit : Prop] Constructors [TT : bit][FF : bit]; Inductive [byte : Prop] Constructors [Byte : bit->bit->bit->bit->bit->bit->bit->bit->byte]; (* A useful byte *) [ bZero = Byte FF FF FF FF FF FF FF FF ]; (* Some other bytes *) [ bOne = Byte FF FF FF FF FF FF FF TT ]; [ b00011111 = Byte FF FF FF TT TT TT TT TT ]; [ b11100000 = Byte TT TT TT FF FF FF FF FF ]; [ b11111111 = Byte TT TT TT TT TT TT TT TT ]; [ bExp5 = Byte FF FF TT FF FF FF FF FF ]; (* Definition of left shift. *) Goal byte -> bit -> byte ; intros B8 B ; Induction B8 ; intros a b c d e f g h ; Refine Byte ; Refine b ; Refine c ; Refine d ; Refine e ; Refine f ; Refine g ; Refine h ; Refine B ; Save SHL ; (* Definition of right shift *) Goal bit -> byte -> byte; intros B B8 ; Induction B8 ; intros a b c d e f g h ; Refine Byte ; Refine B; Refine a ; Refine b ; Refine c ; Refine d ; Refine e ; Refine f ; Refine g ; Save SHR ; (* Left most bit *) Goal byte -> bit ; intros B8 ; Induction B8 ; intros a b c d e f g h ; Refine a ; Save LeftBit ; (* Right most bit *) Goal byte -> bit ; intros B8 ; Induction B8; intros a b c d e f g h ; Refine h ; Save RightBit ; (* Bitwise unary ops *) Goal (bit -> bit) -> byte -> byte ; intros F B ; Induction B ; intros a b c d e f g h ; Refine Byte (F a) (F b) (F c) (F d) (F e) (F f) (F g) (F h) ; Save BitWise1 ; (* Bitwise binary ops *) Goal (bit -> bit -> bit) -> byte -> byte -> byte; intros P x X ; Induction x ; intros a b c d e f g h ; Induction X ; intros A B C D E F G H ; Refine Byte (P a A) (P b B) (P c C) (P d D) (P e E) (P f F) (P g G) (P h H); Save BitWise2 ; [ And = [x,y:bit] bit_elim ([_:bit]bit) y FF x ]; [ Or = [x,y:bit] bit_elim ([_:bit]bit) TT y x ]; [ Not = [x:bit] bit_elim ([_:bit]bit) FF TT x ]; [ Xor = [x,y:bit] bit_elim ([_:bit]bit) (Not y) y x]; [ Nand = [x,y:bit] Not (And x y)]; [ Nor = [x,y:bit] Not (Or x y)]; [ bAnd = BitWise2 And ]; [ bOr = BitWise2 Or ]; [ bXor = BitWise2 Xor ]; [ bNot = BitWise1 Not ]; (* This is the PAL of DeCSS, PALfunc maps 8 bits to a byte, PAL maps bytes to bytes *) [a,b,c,d,e,f,g,h:bit]; $[ A = Xor (Nand a b) d ]; $[ B = Xor (Nand e f) g ]; $[ C = Xor (Nand A B) f ]; $[ D = Xor (Nand A B) b ]; $[ E = Xor (Nand a b) c ]; $[ F = Xor (Nor e f) h ]; $[ G = Xor (Nand E F) a ]; $[ H = Xor (Nor E F) e ]; [ PALfunc = Byte A B C D E F G H]; Discharge a; Goal byte -> byte ; intros B; Induction B; Refine PALfunc; Save PAL; (* Reverse the bits *) Goal byte->byte; intros B; Induction B; intros a b c d e f g h ; Refine Byte h g f e d c b a ; Save reverse ;