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
Last Edited by: Louis Monier September 15, 1986 3:43:07 pm PDT
DIRECTORY BitOps, Rope;
EUProofs:
CEDAR
PROGRAM
IMPORTS BitOps =
BEGIN
Mask: TYPE = ARRAY [0..32) OF BOOL;
Trits: TYPE = {P, S, F, X};
Pat: TYPE = ARRAY [0..6) OF Trits;
XthBitOfN:
PUBLIC
PROC [x, n:
INT]
RETURNS [
BOOL] =
Warning: bit 0 is the LOW order bit (lsb)
{RETURN [IF x<0 THEN FALSE ELSE (n/BitOps.TwoToThe[x]) MOD 2 =1]};
-- 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.