(* Formalisation of 32 bit words *)

Module word Import byte ;

Inductive [word : Prop]
Constructors [Word : byte->byte->byte->byte->word];

(* Some words *)
[ wZero     = Word bZero bZero bZero bZero ];
[ w00011111 = Word bZero bZero bZero b00011111 ];
[ w11100000 = Word bZero bZero bZero b11100000 ];
[ w11111111 = Word bZero bZero bZero b11111111 ];

[ wExp8 = Word bZero bZero bOne bZero ];
[ wExp21 = Word bZero bExp5 bZero bZero ];

(* Left shift by bit *)
Goal word -> word ;
intros W ;
Induction W ;
intros BA BB BC BD ;
Refine Word ;
Refine SHL BA (LeftBit BB);
Refine SHL BB (LeftBit BC);
Refine SHL BC (LeftBit BD);
Refine SHL BD FF;
Save wSHL ;

(* Right shift by bit *)
Goal word -> word ;
intros W ;
Induction W ;
intros BA BB BC BD ;
Refine Word ;
Refine SHR FF BA ;
Refine SHR (RightBit BA) BB ;
Refine SHR (RightBit BB) BC ;
Refine SHR (RightBit BC) BD ;
Save wSHR ;

(* Left shift by byte *)
Goal word -> word ;
intros W ;
Induction W ;
intros BA BB BC BD ;
Refine Word BB BC BD bZero;
Save wSHL8 ;

(* Right shift by byte *)
Goal word -> word ;
intros W ;
Induction W ;
intros BA BB BC BD ;
Refine Word bZero BA BB BC;
Save wSHR8 ;

(* Shifts by other numbers of bits *)
[ wSHL3 = [w:word] wSHL (wSHL (wSHL w)) ];
[ wSHL9 = [w:word] wSHL (wSHL8 w) ];
[ wSHL12 = [w:word] wSHL3 (wSHL9 w) ];
[ wSHL15 = [w:word] wSHL3 (wSHL12 w) ];
[ wSHL16 = [w:word] wSHL8 (wSHL8 w) ];
[ wSHL17 = [w:word] wSHL (wSHL16 w) ];

[ wSHR3 = [w:word] wSHR (wSHR (wSHR w)) ];
[ wSHR4 = [w:word] wSHR (wSHR3 w) ];
[ wSHR9 = [w:word] wSHR (wSHR8 w) ];
[ wSHR12 = [w:word] wSHR4 (wSHR8 w) ];
[ wSHR14 = [w:word] wSHR (wSHR (wSHR12 w)) ];
[ wSHR17 = [w:word] wSHR8 (wSHR9 w) ];

(* Left most byte *)
Goal word -> byte ;
intros W ;
Induction W ;
intros BA BB BC BD ;
Refine BA ;
Save wLeftByte ;

(* Right most byte *)
Goal word -> byte ;
intros W ;
Induction W ;
intros BA BB BC BD ;
Refine BD ;
Save wRightByte ;

[ wLeftBit = [W : word] LeftBit (wLeftByte W) ];
[ wRightBit = [W : word] RightBit (wRightByte W) ];

(* Byte wise ops *)
Goal (byte -> byte) -> word -> word ;
intros P W ;
Induction W ;
intros A B C D ;
Refine Word (P A) (P B) (P C) (P D);

Save wByteWise1 ;

Goal (byte -> byte -> byte) -> word -> word -> word ;
intros P w W ;
Induction w ;
intros a b c d ;
Induction W ;
intros A B C D ;
Refine Word (P a A) (P b B) (P c C) (P d D);
Save wByteWise2 ;

[ wBitWise1 = [f : bit->bit] wByteWise1 (BitWise1 f) ];
[ wBitWise2 = [f : bit->bit->bit] wByteWise2 (BitWise2 f) ];

[ wAnd = wBitWise2 And ];
[ wOr = wBitWise2 Or ];
[ wNot = wBitWise1 Not];
[ wXor = wBitWise2 Xor ];

(* The low byte of a word *)
Goal word->byte;
intros w;
Induction w;
intros a b c d;
Refine d;
Save wLowByte;

(* Zero extend byte to word *)
[ byteToWord = Word bZero bZero bZero ];

(* The PAL for words. *)
[ wPAL = [w:word] byteToWord (PAL (wLowByte w)) ];