Skip to content

Commit

Permalink
Add lt field to Cmp dictionary.
Browse files Browse the repository at this point in the history
Also add similar `slt` field to `SignedCmp` dictionary.

These fields are used to simplify the formulas generated by the
cryptol-saw-core translator for Cryptol operators like `<` and
`<$`, avoiding redundant logical connectives.

Fixes #1565.
  • Loading branch information
Brian Huffman committed Feb 14, 2022
1 parent 81287fb commit 2eb734f
Showing 1 changed file with 41 additions and 10 deletions.
51 changes: 41 additions & 10 deletions cryptol-saw-core/saw/Cryptol.sawcore
Original file line number Diff line number Diff line change
Expand Up @@ -455,6 +455,9 @@ errorBinary s a _ _ = error a s;
boolCmp : Bool -> Bool -> Bool -> Bool;
boolCmp x y k = ite Bool x (and y k) (or y k);

boolLt : Bool -> Bool -> Bool;
boolLt x y = and (not x) y;

integerCmp : Integer -> Integer -> Bool -> Bool;
integerCmp x y k = or (intLt x y) (and (intEq x y) k);

Expand All @@ -473,14 +476,32 @@ vecCmp n a f xs ys k =
foldr (Bool -> Bool) Bool n (\ (f : Bool -> Bool) -> f) k
(zipWith a a (Bool -> Bool) f n xs ys);

vecLt :
(n : Nat) -> (a : isort 0) ->
(a -> a -> Bool -> Bool) ->
(a -> a -> Bool) ->
(Vec n a -> Vec n a -> Bool);
vecLt n a f g xs ys =
foldr (Bool -> Bool) Bool n (\ (f : Bool -> Bool) -> f) False
(zipWith a a (Bool -> Bool) f n xs ys);

unitCmp : #() -> #() -> Bool -> Bool;
unitCmp _ _ _ = False;

unitLt : #() -> #() -> Bool;
unitLt _ _ = False;

pairCmp : (a b : sort 0) -> (a -> a -> Bool -> Bool) -> (b -> b -> Bool -> Bool)
-> a * b -> a * b -> Bool -> Bool;
pairCmp a b f g x12 y12 k =
f (fst a b x12) (fst a b y12) (g (snd a b x12) (snd a b y12) k);

pairLt :
(a b : sort 0) -> (a -> a -> Bool -> Bool) -> (b -> b -> Bool) ->
a * b -> a * b -> Bool;
pairLt a b f g x y =
f (fst a b x) (fst a b y) (g (snd a b x) (snd a b y));

--------------------------------------------------------------------------------
-- Dictionaries and overloading

Expand Down Expand Up @@ -538,19 +559,24 @@ PCmp : sort 0 -> sort 1;
PCmp a =
#{ cmpEq : PEq a
, cmp : a -> a -> Bool -> Bool
, lt : a -> a -> Bool
};

PCmpBit : PCmp Bool;
PCmpBit = { cmpEq = PEqBit, cmp = boolCmp };
PCmpBit = { cmpEq = PEqBit, cmp = boolCmp, lt = boolLt };

PCmpInteger : PCmp Integer;
PCmpInteger = { cmpEq = PEqInteger, cmp = integerCmp };
PCmpInteger = { cmpEq = PEqInteger, cmp = integerCmp, lt = intLt };

PCmpRational : PCmp Rational;
PCmpRational = { cmpEq = PEqRational, cmp = rationalCmp };
PCmpRational = { cmpEq = PEqRational, cmp = rationalCmp, lt = ltRational };

PCmpVec : (n : Nat) -> (a : isort 0) -> PCmp a -> PCmp (Vec n a);
PCmpVec n a pa = { cmpEq = PEqVec n a pa.cmpEq, cmp = vecCmp n a pa.cmp };
PCmpVec n a pa =
{ cmpEq = PEqVec n a pa.cmpEq
, cmp = vecCmp n a pa.cmp
, lt = \ (x : Vec n a) -> \ (y : Vec n a) -> vecCmp n a pa.cmp x y False
};

PCmpSeq : (n : Num) -> (a : isort 0) -> PCmp a -> PCmp (seq n a);
PCmpSeq n =
Expand All @@ -560,7 +586,7 @@ PCmpSeq n =
n;

PCmpWord : (n : Nat) -> PCmp (Vec n Bool);
PCmpWord n = { cmpEq = PEqWord n, cmp = bvCmp n };
PCmpWord n = { cmpEq = PEqWord n, cmp = bvCmp n, lt = bvult n };

PCmpSeqBool : (n : Num) -> PCmp (seq n Bool);
PCmpSeqBool n =
Expand All @@ -570,12 +596,13 @@ PCmpSeqBool n =
n;

PCmpUnit : PCmp #();
PCmpUnit = { cmpEq = PEqUnit, cmp = unitCmp };
PCmpUnit = { cmpEq = PEqUnit, cmp = unitCmp, lt = unitLt };

PCmpPair : (a b : sort 0) -> PCmp a -> PCmp b -> PCmp (a * b);
PCmpPair a b pa pb =
{ cmpEq = PEqPair a b pa.cmpEq pb.cmpEq
, cmp = pairCmp a b pa.cmp pb.cmp
, lt = pairLt a b pa.cmp pb.lt
};

-- SignedCmp class
Expand All @@ -584,12 +611,14 @@ PSignedCmp : sort 0 -> sort 1;
PSignedCmp a =
#{ signedCmpEq : PEq a
, scmp : a -> a -> Bool -> Bool
, slt : a -> a -> Bool
};

PSignedCmpVec : (n : Nat) -> (a : isort 0) -> PSignedCmp a -> PSignedCmp (Vec n a);
PSignedCmpVec n a pa =
{ signedCmpEq = PEqVec n a pa.signedCmpEq
, scmp = vecCmp n a pa.scmp
, slt = \ (x : Vec n a) -> \ (y : Vec n a) -> vecCmp n a pa.scmp x y False
};

PSignedCmpSeq : (n : Num) -> (a : isort 0) -> PSignedCmp a -> PSignedCmp (seq n a);
Expand All @@ -600,7 +629,7 @@ PSignedCmpSeq n =
n;

PSignedCmpWord : (n : Nat) -> PSignedCmp (Vec n Bool);
PSignedCmpWord n = { signedCmpEq = PEqWord n, scmp = bvSCmp n };
PSignedCmpWord n = { signedCmpEq = PEqWord n, scmp = bvSCmp n, slt = bvslt n };

PSignedCmpSeqBool : (n : Num) -> PSignedCmp (seq n Bool);
PSignedCmpSeqBool n =
Expand All @@ -610,12 +639,13 @@ PSignedCmpSeqBool n =
n;

PSignedCmpUnit : PSignedCmp #();
PSignedCmpUnit = { signedCmpEq = PEqUnit, scmp = unitCmp };
PSignedCmpUnit = { signedCmpEq = PEqUnit, scmp = unitCmp, slt = unitLt };

PSignedCmpPair : (a b : sort 0) -> PSignedCmp a -> PSignedCmp b -> PSignedCmp (a * b);
PSignedCmpPair a b pa pb =
{ signedCmpEq = PEqPair a b pa.signedCmpEq pb.signedCmpEq
, scmp = pairCmp a b pa.scmp pb.scmp
, slt = pairLt a b pa.scmp pb.slt
};


Expand Down Expand Up @@ -1110,7 +1140,7 @@ ecNotEq a pa x y = not (ecEq a pa x y);

-- Cmp
ecLt : (a : sort 0) -> PCmp a -> a -> a -> Bool;
ecLt a pa x y = pa.cmp x y False;
ecLt a pa x y = pa.lt x y;

ecGt : (a : sort 0) -> PCmp a -> a -> a -> Bool;
ecGt a pa x y = ecLt a pa y x;
Expand All @@ -1123,7 +1153,7 @@ ecGtEq a pa x y = not (ecLt a pa x y);

-- SignedCmp
ecSLt : (a : sort 0) -> PSignedCmp a -> a -> a -> Bool;
ecSLt a pa x y = pa.scmp x y False;
ecSLt a pa x y = pa.slt x y;

-- Logic
ecAnd : (a : sort 0) -> PLogic a -> a -> a -> a;
Expand Down Expand Up @@ -1592,6 +1622,7 @@ PCmpFloat : (e p : Num) -> PCmp (TCFloat e p);
PCmpFloat e p =
{ cmpEq = PEqFloat e p
, cmp = \(x y : TCFloat e p) (k : Bool) -> error Bool "Unimplemented: Cmp Float"
, lt = \(x y : TCFloat e p) -> error Bool "Unimplemented: Cmp Float"
};

PZeroFloat : (e p : Num) -> PZero (TCFloat e p);
Expand Down

0 comments on commit 2eb734f

Please sign in to comment.