(* 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 ;