<> <> <> <> DIRECTORY BitHacks, Rope; EUProofs: CEDAR PROGRAM IMPORTS BitHacks = BEGIN OPEN BitHacks; Mask: TYPE = ARRAY [0..32) OF BOOL; Trits: TYPE = {P, S, F, X}; Pat: TYPE = ARRAY [0..6) OF Trits; <<>> <<-- Proves the mask generator for the field unit; i is the slice number, k the input>> <<-- Recursive construction>> F: PROC [n, k, i: NAT] RETURNS [BOOL] ~ { in: BOOL = XthBitOfN[n, i]; kn: BOOL = XthBitOfN[n, k]; IF ~in THEN { IF n=0 THEN RETURN [kn] ELSE RETURN [kn OR F[n-1, k, i]]} ELSE { IF n=0 THEN RETURN [FALSE] ELSE RETURN [kn AND F[n-1, k, i]] }; }; RMask: PROC [k: NAT] RETURNS [t: Mask] ~ { FOR i: INT IN [0..32) DO t[i] _ F[5, k, 31-i]; ENDLOOP; }; <<-- Serial construction, used to make the layout>> Pattern: PROC [k: NAT] RETURNS [lowToHi: Pat] ~ { isOne: BOOL _ XthBitOfN[0, k]; lowToHi[0] _ IF isOne THEN X ELSE F; FOR bit: NAT IN [1..6) DO isOne _ XthBitOfN[bit, k]; lowToHi[bit] _ SELECT TRUE FROM isOne AND lowToHi[bit-1]=X => X, isOne => S, ~isOne AND lowToHi[bit-1]=X => F, ~isOne => P, ENDCASE => ERROR; ENDLOOP; }; ApplyPattern: PROC [k, i: NAT] RETURNS [b: BOOL _ FALSE] ~ { lowToHi: Pat _ Pattern[i]; IF lowToHi[0]=F THEN b _ XthBitOfN[0, k]; FOR bit: NAT IN [1..6) DO b _ SELECT lowToHi[bit] FROM X => b, S => b AND XthBitOfN[bit, k], F, P => b OR XthBitOfN[bit, k], ENDCASE => ERROR; ENDLOOP; }; SMask: PROC [k: NAT] RETURNS [t: Mask] ~ { lowToHi: Pat _ Pattern[k]; FOR i: INT IN [0..32) DO t[i] _ ApplyPattern[k, 31-i]; ENDLOOP; }; <<-- The ultimate check>> <<>> Check: PROC RETURNS [ok: BOOL _ TRUE, bug: INT _ -1] ~ { Diff: PROC [m1, m2: Mask] RETURNS [BOOL _ FALSE] ~ { FOR i: NAT IN [0..32) DO IF m1[i]#m2[i] THEN RETURN[TRUE]; ENDLOOP; }; FOR k: NAT IN [0..32) DO IF Diff[SMask[k], RMask[k]] THEN RETURN[FALSE, k]; ENDLOOP; }; <<>> END.