(* Arithmetic for bytes and words *) Module arith Import byte word ; [ Sum = [x,y,z:bit] Xor (Xor x y) z ] ; [ Car = [x,y,z:bit] Or (And x y) (Or (And y z) (And x z)) ]; [ a, b, c, d, e, f, g, h, A, B, C, D, E, F, G, H, cin : bit]; (* We are big endian, so h is least significant *) \$[ Sh = Sum h H cin ]; \$[ Ch = Car h H cin ]; \$[ Sg = Sum g G Ch ]; \$[ Cg = Car g G Ch ]; \$[ Sf = Sum f F Cg ]; \$[ Cf = Car f F Cg ]; \$[ Se = Sum e E Cf ]; \$[ Ce = Car e E Cf ]; \$[ Sd = Sum d D Ce ]; \$[ CD = Car d D Ce ]; \$[ Sc = Sum c C CD ]; \$[ Cc = Car c C CD ]; \$[ Sb = Sum b B Cc ]; \$[ Cb = Car b B Cc ]; \$[ Sa = Sum a A Cb ]; [ bRawCar = Car a A Cb ]; [ bRawSum = Byte Sa Sb Sc Sd Se Sf Sg Sh ]; Discharge a; (* Full byte sum *) Goal byte->byte->bit->byte; intros bb BB ; Induction bb; intros a b c d e f g h ; Induction BB; intros A B C D E F G H ; Refine bRawSum a b c d e f g h A B C D E F G H ; Save bFullSum ; (* Full byte carry *) Goal byte->byte->bit->bit; intros bb BB ; Induction bb; intros a b c d e f g h ; Induction BB; intros A B C D E F G H ; Refine bRawCar a b c d e f g h A B C D E F G H ; Save bFullCar ; (***** WORD SUMMING ****) [ a,b,c,d,A,B,C,D : byte ]; \$[ SD = bFullSum d D FF ]; \$[ CD = bFullCar d D FF ]; \$[ SC = bFullSum c C CD ]; \$[ CC = bFullCar c C CD ]; \$[ SB = bFullSum b B CC ]; \$[ CB = bFullCar b B CC ]; \$[ SA = bFullSum a A CB ]; [ wRawSum = Word SA SB SC SD ]; Discharge a ; Goal word->word->word ; intros x X; Induction x ; intros a b c d ; Induction X; intros A B C D ; Refine wRawSum a b c d A B C D ; Save wSum ;