EUProofs.mesa
Copyright © 1985 by Xerox Corporation. All rights reserved.
Louis Monier June 9, 1986 4:15:41 pm PDT
Bertrand Serlet June 9, 1986 0:25:43 am PDT
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: BOOLFALSE] ~ {
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: BOOLTRUE, bug: INT ← -1] ~ {
Diff: PROC [m1, m2: Mask] RETURNS [BOOLFALSE] ~ {
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.