Skip to content

Commit e305a0e

Browse files
robdockinsrobdockins
authored
Merge pull request #1391 from GaloisInc/explicit-stride
Explicit stride
2 parents da7d859 + 45fa137 commit e305a0e

File tree

4 files changed

+160
-60
lines changed

4 files changed

+160
-60
lines changed

‎cryptol-saw-core/saw/Cryptol.sawcore

+129-45
Original file line numberDiff line numberDiff line change
@@ -128,7 +128,6 @@ tcDiv =
128128
(\ (y:Nat) -> TCInf)
129129
-- infinity / infinity = 1
130130
(TCNum 1);
131-
132131
tcMod : Num -> Num -> Num;
133132
tcMod =
134133
binaryNumFun (\ (x:Nat) -> \ (y:Nat) -> modNat x y)
@@ -170,7 +169,7 @@ tcCeilDiv =
170169

171170
tcCeilMod : Num -> Num -> Num;
172171
tcCeilMod =
173-
binaryNumFun ceilModNat (\ (x:Nat) -> TCNum 0) (\ (y:Nat) -> TCInf) TCInf;
172+
binaryNumFun ceilModNat (\ (x:Nat) -> TCNum 0) (\ (y:Nat) -> TCNum 0) TCInf;
174173

175174
tcLenFromThenTo_Nat : Nat -> Nat -> Nat -> Nat;
176175
tcLenFromThenTo_Nat x y z =
@@ -848,9 +847,9 @@ PIntegral a =
848847
, toInt : a -> Integer
849848
, posNegCases :
850849
(r : sort 0) ->
851-
(Nat -> r) ->
852-
(Nat -> r) ->
853-
a -> r
850+
(Nat -> r) ->
851+
(Nat -> r) ->
852+
a -> r
854853
};
855854

856855
PIntegralInteger : PIntegral Integer;
@@ -879,7 +878,7 @@ PIntegralSeqBool n =
879878
Num#rec (\ (n:Num) -> PIntegral (seq n Bool))
880879
(\ (n:Nat) -> PIntegralWord n)
881880
(error (PIntegral (Stream Bool)) "PIntegralSeqBool: no instance for streams")
882-
n;
881+
n;
883882

884883

885884
-- Field class
@@ -928,12 +927,12 @@ PRound a =
928927

929928
PRoundRational : PRound Rational;
930929
PRoundRational =
931-
{ roundField = PFieldRational
932-
, roundCmp = PCmpRational
933-
, floor = \(x : Rational) -> error Integer "Unimplemented: floor Rational"
934-
, ceiling = \(x : Rational) -> error Integer "Unimplemented: ceiling Rational"
935-
, trunc = \(x : Rational) -> error Integer "Unimplemented: trunc Rational"
936-
, roundAway = \(x : Rational) -> error Integer "Unimplemented: roundAway Rational"
930+
{ roundField = PFieldRational
931+
, roundCmp = PCmpRational
932+
, floor = \(x : Rational) -> error Integer "Unimplemented: floor Rational"
933+
, ceiling = \(x : Rational) -> error Integer "Unimplemented: ceiling Rational"
934+
, trunc = \(x : Rational) -> error Integer "Unimplemented: trunc Rational"
935+
, roundAway = \(x : Rational) -> error Integer "Unimplemented: roundAway Rational"
937936
, roundToEven = \(x : Rational) -> error Integer "Unimplemented: roundToEven Rational"
938937
};
939938

@@ -986,8 +985,8 @@ ecFromZ : (n : Num) -> IntModNum n -> Integer;
986985
ecFromZ n =
987986
Num#rec (\ (n : Num) -> IntModNum n -> Integer)
988987
fromIntMod
989-
(\ (x : Integer) -> x)
990-
n;
988+
(\ (x : Integer) -> x)
989+
n;
991990

992991
-- Ring
993992
ecFromInteger : (a : sort 0) -> PRing a -> Integer -> a;
@@ -1131,15 +1130,15 @@ ecShiftL m =
11311130
-- Case for (TCNum m)
11321131
(\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix : PIntegral ix) -> \ (pz:PZero a) -> \ (xs:Vec m a) ->
11331132
pix.posNegCases (Vec m a)
1134-
(shiftL m a (ecZero a pz) xs)
1135-
(shiftR m a (ecZero a pz) xs))
1133+
(shiftL m a (ecZero a pz) xs)
1134+
(shiftR m a (ecZero a pz) xs))
11361135

11371136
-- Case for (infinity)
11381137
(\ (ix:sort 0) -> \ (a:sort 0) -> \ (pix : PIntegral ix) -> \ (pz:PZero a) ->
11391138
\ (xs:Stream a) ->
11401139
pix.posNegCases (Stream a)
1141-
(streamShiftL a xs)
1142-
(streamShiftR a pz xs))
1140+
(streamShiftL a xs)
1141+
(streamShiftR a pz xs))
11431142
m;
11441143

11451144
ecShiftR : (m : Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a ->
@@ -1151,14 +1150,14 @@ ecShiftR m =
11511150
-- Case for (TCNum m)
11521151
(\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix : PIntegral ix) -> \ (pz:PZero a) -> \ (xs:Vec m a) ->
11531152
pix.posNegCases (Vec m a)
1154-
(shiftR m a (ecZero a pz) xs)
1155-
(shiftL m a (ecZero a pz) xs))
1153+
(shiftR m a (ecZero a pz) xs)
1154+
(shiftL m a (ecZero a pz) xs))
11561155

11571156
-- Case for (infinity)
11581157
(\ (ix:sort 0) -> \ (a:sort 0) -> \ (pix : PIntegral ix) -> \ (pz:PZero a) -> \ (xs:Stream a) ->
11591158
pix.posNegCases (Stream a)
1160-
(streamShiftR a pz xs)
1161-
(streamShiftL a xs))
1159+
(streamShiftR a pz xs)
1160+
(streamShiftL a xs))
11621161
m;
11631162

11641163
ecSShiftR : (n : Num) -> (ix : sort 0) -> PIntegral ix -> seq n Bool -> ix -> seq n Bool;
@@ -1172,8 +1171,8 @@ ecSShiftR =
11721171
(\ (xs : Vec 0 Bool) -> \ (_ : ix) -> xs)
11731172
(\ (w : Nat) -> \ (xs : Vec (Succ w) Bool) ->
11741173
pix.posNegCases (Vec (Succ w) Bool)
1175-
(bvSShr w xs)
1176-
(bvShl (Succ w) xs))
1174+
(bvSShr w xs)
1175+
(bvShl (Succ w) xs))
11771176
n));
11781177

11791178
ecRotL : (m : Num) -> (ix a : sort 0) -> PIntegral ix -> seq m a -> ix -> seq m a;
@@ -1183,7 +1182,7 @@ ecRotL =
11831182
(\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec m a) ->
11841183
pix.posNegCases (Vec m a)
11851184
(rotateL m a xs)
1186-
(rotateR m a xs));
1185+
(rotateR m a xs));
11871186

11881187
ecRotR : (m : Num) -> (ix a : sort 0) -> PIntegral ix -> seq m a -> ix -> seq m a;
11891188
ecRotR =
@@ -1192,7 +1191,7 @@ ecRotR =
11921191
(\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec m a) ->
11931192
pix.posNegCases (Vec m a)
11941193
(rotateR m a xs)
1195-
(rotateL m a xs));
1194+
(rotateL m a xs));
11961195

11971196
ecCat : (m n : Num) -> (a : sort 0) -> seq m a -> seq n a -> seq (tcAdd m n) a;
11981197
ecCat =
@@ -1224,9 +1223,9 @@ ecTake =
12241223
(Num_rec
12251224
(\ (n:Num) -> (a:sort 0) -> seq (tcAdd TCInf n) a -> Stream a)
12261225
-- The case (TCInf, TCNum n)
1227-
(\ (n:Nat) -> \ (a:sort 0) -> \ (xs:Stream a) -> xs)
1228-
-- The case (TCInf, TCInf)
1229-
(\ (a:sort 0) -> \ (xs:Stream a) -> xs));
1226+
(\ (n:Nat) -> \ (a:sort 0) -> \ (xs:Stream a) -> xs)
1227+
-- The case (TCInf, TCInf)
1228+
(\ (a:sort 0) -> \ (xs:Stream a) -> xs));
12301229

12311230
ecDrop : (m n : Num) -> (a : sort 0) -> seq (tcAdd m n) a -> seq n a;
12321231
ecDrop =
@@ -1336,30 +1335,30 @@ ecAt n =
13361335
(\ (n:Num) -> (a ix: sort 0) -> PIntegral ix -> seq n a -> ix -> a)
13371336
(\ (n:Nat) -> \ (a:sort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec n a) ->
13381337
pix.posNegCases a
1339-
(at n a xs)
1340-
(\ (_:Nat) -> at n a xs 0))
1341-
-- (error (Nat -> a) "ecAt : negative index"))
1338+
(at n a xs)
1339+
(\ (_:Nat) -> at n a xs 0))
1340+
-- (error (Nat -> a) "ecAt : negative index"))
13421341
(\ (a:sort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Stream a) ->
13431342
pix.posNegCases a
1344-
(streamGet a xs)
1345-
(\ (_:Nat) -> streamGet a xs 0))
1346-
-- (error (Nat -> a) "ecAt : negative index"))
1343+
(streamGet a xs)
1344+
(\ (_:Nat) -> streamGet a xs 0))
1345+
-- (error (Nat -> a) "ecAt : negative index"))
13471346
n;
13481347

13491348
ecAtBack : (n : Num) -> (a ix : sort 0) -> PIntegral ix -> seq n a -> ix -> a;
13501349
ecAtBack n a ix pix xs = ecAt n a ix pix (ecReverse n a xs);
13511350

1352-
ecFromTo : (first last : Num) -> (a : sort 0) -> PLiteral a -> PLiteral a ->
1351+
ecFromTo : (first last : Num) -> (a : sort 0) -> PLiteral a ->
13531352
seq (tcAdd (TCNum 1) (tcSub last first)) a;
13541353
ecFromTo =
13551354
finNumRec
1356-
(\ (first:Num) -> (last:Num) -> (a : sort 0) -> PLiteral a -> PLiteral a ->
1355+
(\ (first:Num) -> (last:Num) -> (a : sort 0) -> PLiteral a ->
13571356
seq (tcAdd (TCNum 1) (tcSub last first)) a)
13581357
(\ (first:Nat) ->
13591358
finNumRec
1360-
(\ (last:Num) -> (a : sort 0) -> PLiteral a -> PLiteral a ->
1359+
(\ (last:Num) -> (a : sort 0) -> PLiteral a ->
13611360
seq (tcAdd (TCNum 1) (tcSub last (TCNum first))) a)
1362-
(\ (last:Nat) -> \ (a : sort 0) -> \ (pa : PLiteral a) -> \ (_ : PLiteral a) ->
1361+
(\ (last:Nat) -> \ (a : sort 0) -> \ (pa : PLiteral a) ->
13631362
gen (addNat 1 (subNat last first)) a
13641363
(\ (i : Nat) -> pa (addNat i first))));
13651364

@@ -1394,6 +1393,91 @@ ecFromThenTo first next _ a =
13941393
(mulNat i (getFinNat next)))
13951394
(mulNat i (getFinNat first)))));
13961395

1396+
ecFromToBy :
1397+
(first last stride : Num) -> (a : sort 0) -> PLiteral a ->
1398+
seq (tcAdd (TCNum 1) (tcDiv (tcSub last first) stride)) a;
1399+
ecFromToBy =
1400+
finNumRec
1401+
(\ (first:Num) -> (last:Num) -> (stride : Num) -> (a : sort 0) -> PLiteral a ->
1402+
seq (tcAdd (TCNum 1) (tcDiv (tcSub last first) stride)) a)
1403+
(\ (first:Nat) ->
1404+
finNumRec
1405+
(\ (last:Num) -> (stride : Num) -> (a : sort 0) -> PLiteral a ->
1406+
seq (tcAdd (TCNum 1) (tcDiv (tcSub last (TCNum first)) stride)) a)
1407+
(\ (last:Nat) ->
1408+
finNumRec
1409+
(\ (stride:Num) -> (a : sort 0) -> PLiteral a ->
1410+
seq (tcAdd (TCNum 1) (tcDiv (TCNum (subNat last first)) stride)) a)
1411+
(\ (stride:Nat) -> \ (a : sort 0) -> \ (pa : PLiteral a) ->
1412+
gen (addNat 1 (divNat (subNat last first) stride)) a
1413+
(\ (i : Nat) -> pa (addNat first (mulNat i stride))))));
1414+
1415+
ecFromToByLessThan :
1416+
(first bound stride : Num) -> (a : sort 0) -> PLiteralLessThan a ->
1417+
seq (tcCeilDiv (tcSub bound first) stride) a;
1418+
ecFromToByLessThan =
1419+
finNumRec
1420+
(\ (first:Num) -> (bound:Num) -> (stride:Num) -> (a : sort 0) -> PLiteralLessThan a ->
1421+
seq (tcCeilDiv (tcSub bound first) stride) a)
1422+
(\ (first:Nat) ->
1423+
Num_rec
1424+
(\ (bound:Num) -> (stride:Num) -> (a : sort 0) -> PLiteralLessThan a ->
1425+
seq (tcCeilDiv (tcSub bound (TCNum first)) stride) a)
1426+
1427+
-- bound is finite case
1428+
(\ (bound:Nat) ->
1429+
finNumRec
1430+
(\ (stride:Num) -> (a : sort 0) -> PLiteralLessThan a ->
1431+
seq (tcCeilDiv (TCNum (subNat bound first)) stride) a)
1432+
(\ (stride:Nat) -> \ (a:sort 0) -> \ (pa:PLiteralLessThan a) ->
1433+
gen (ceilDivNat (subNat bound first) stride) a
1434+
(\ (i:Nat) -> pa (addNat first (mulNat i stride)))))
1435+
1436+
-- bound is infinite case
1437+
(finNumRec
1438+
(\ (stride:Num) -> (a : sort 0) -> PLiteralLessThan a ->
1439+
seq (tcCeilDiv TCInf stride) a)
1440+
(\ (stride:Nat) -> \ (a : sort 0) -> \ (pa:PLiteralLessThan a) ->
1441+
MkStream a (\ (i:Nat) -> pa (addNat first (mulNat i stride))))));
1442+
1443+
ecFromToDownBy :
1444+
(first last stride : Num) -> (a : sort 0) -> PLiteral a ->
1445+
seq (tcAdd (TCNum 1) (tcDiv (tcSub first last) stride)) a;
1446+
ecFromToDownBy =
1447+
finNumRec
1448+
(\ (first:Num) -> (last:Num) -> (stride:Num) -> (a : sort 0) -> PLiteral a ->
1449+
seq (tcAdd (TCNum 1) (tcDiv (tcSub first last) stride)) a)
1450+
(\ (first:Nat) ->
1451+
finNumRec
1452+
(\ (last:Num) -> (stride:Num) -> (a : sort 0) -> PLiteral a ->
1453+
seq (tcAdd (TCNum 1) (tcDiv (tcSub (TCNum first) last) stride)) a)
1454+
(\ (last:Nat) ->
1455+
finNumRec
1456+
(\ (stride:Num) -> (a : sort 0) -> PLiteral a ->
1457+
seq (tcAdd (TCNum 1) (tcDiv (TCNum (subNat first last)) stride)) a)
1458+
(\ (stride:Nat) -> \ (a : sort 0) -> \ (pa : PLiteral a) ->
1459+
gen (addNat 1 (divNat (subNat first last) stride)) a
1460+
(\ (i:Nat) -> pa (subNat first (mulNat i stride))))));
1461+
1462+
ecFromToDownByGreaterThan :
1463+
(first bound stride : Num) -> (a : sort 0) -> PLiteral a ->
1464+
seq (tcCeilDiv (tcSub first bound) stride) a;
1465+
ecFromToDownByGreaterThan =
1466+
finNumRec
1467+
(\ (first:Num) -> (bound:Num) -> (stride:Num) -> (a : sort 0) -> PLiteral a ->
1468+
seq (tcCeilDiv (tcSub first bound) stride) a)
1469+
(\ (first:Nat) ->
1470+
finNumRec
1471+
(\ (bound:Num) -> (stride:Num) -> (a : sort 0) -> PLiteral a ->
1472+
seq (tcCeilDiv (tcSub (TCNum first) bound) stride) a)
1473+
(\ (bound:Nat) ->
1474+
finNumRec
1475+
(\ (stride:Num) -> (a : sort 0) -> PLiteral a ->
1476+
seq (tcCeilDiv (TCNum (subNat first bound)) stride) a)
1477+
(\ (stride:Nat) -> \ (a : sort 0) -> \ (pa:PLiteral a) ->
1478+
gen (ceilDivNat (subNat first bound) stride) a
1479+
(\ (i:Nat) -> pa (subNat first (mulNat i stride))))));
1480+
13971481
-- Infinite word sequences
13981482
ecInfFrom : (a : sort 0) -> PIntegral a -> a -> seq TCInf a;
13991483
ecInfFrom a pa x =
@@ -1582,13 +1666,13 @@ ecUpdate n =
15821666
-- Case for (TCNum n, TCNum w)
15831667
pix.posNegCases (a -> Vec n a)
15841668
(upd n a xs)
1585-
(\ (_:Nat) -> \ (_:a) -> xs))
1586-
-- (error (Nat -> a -> Vec n a) "ecUpdate: negative index"))
1669+
(\ (_:Nat) -> \ (_:a) -> xs))
1670+
-- (error (Nat -> a -> Vec n a) "ecUpdate: negative index"))
15871671
(\ (a:sort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs : Stream a) ->
15881672
pix.posNegCases (a -> Stream a)
15891673
(streamUpd a xs)
1590-
(\ (_:Nat) -> \ (_:a) -> xs))
1591-
--(error (Nat -> a -> Stream a) "ecUpdate: negative index"))
1674+
(\ (_:Nat) -> \ (_:a) -> xs))
1675+
--(error (Nat -> a -> Stream a) "ecUpdate: negative index"))
15921676
n;
15931677

15941678

@@ -1599,8 +1683,8 @@ ecUpdateEnd =
15991683
(\ (n:Nat) -> \ (a:sort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec n a) ->
16001684
pix.posNegCases (a -> Vec n a)
16011685
(\ (i:Nat) -> upd n a xs (subNat (subNat n 1) i))
1602-
(\ (_:Nat) -> \ (_:a) -> xs));
1603-
-- (error (Nat -> a -> Vec n a) "ecUpdateEnd: negative index"));
1686+
(\ (_:Nat) -> \ (_:a) -> xs));
1687+
-- (error (Nat -> a -> Vec n a) "ecUpdateEnd: negative index"));
16041688

16051689

16061690
-- Bitvector truncation

‎cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

+29-13
Original file line numberDiff line numberDiff line change
@@ -759,21 +759,37 @@ prelPrims =
759759

760760
-- -- Enumerations
761761
, ("fromTo", flip scGlobalDef "Cryptol.ecFromTo")
762-
-- -- fromTo : {first, last, bits, a}
763-
-- -- ( fin last, fin bits, last >== first,
764-
-- -- Literal first a, Literal last a)
765-
-- -- => [1 + (last - first)]a
762+
-- fromTo : {first, last, bits, a}
763+
-- ( fin last, fin bits, last >== first,
764+
-- Literal first a, Literal last a)
765+
-- => [1 + (last - first)]a
766766
, ("fromToLessThan", flip scGlobalDef "Cryptol.ecFromToLessThan")
767-
-- -- fromToLessThan : {first, bound, a}
768-
-- -- ( fin first, bound >= first,
769-
-- -- LiteralLessThan bound a)
770-
-- -- => [bound - first]a
767+
-- fromToLessThan : {first, bound, a}
768+
-- ( fin first, bound >= first,
769+
-- LiteralLessThan bound a)
770+
-- => [bound - first]a
771771
, ("fromThenTo", flip scGlobalDef "Cryptol.ecFromThenTo")
772-
-- -- fromThenTo : {first, next, last, a, len}
773-
-- -- ( fin first, fin next, fin last
774-
-- -- , Literal first a, Literal next a, Literal last a
775-
-- -- , first != next
776-
-- -- , lengthFromThenTo first next last == len) => [len]a
772+
-- fromThenTo : {first, next, last, a, len}
773+
-- ( fin first, fin next, fin last
774+
-- , Literal first a, Literal next a, Literal last a
775+
-- , first != next
776+
-- , lengthFromThenTo first next last == len) => [len]a
777+
, ("fromToBy", flip scGlobalDef "Cryptol.ecFromToBy")
778+
-- fromToBy : {first, last, stride, a}
779+
-- (fin last, fin stride, stride >= 1, last >= first, Literal last a) =>
780+
-- [1 + (last - first)/stride]a
781+
, ("fromToByLessThan", flip scGlobalDef "Cryptol.ecFromToByLessThan")
782+
-- fromToByLessThan : {first, bound, stride, a}
783+
-- (fin first, fin stride, stride >= 1, bound >= first, LiteralLessThan bound a) =>
784+
-- [(bound - first)/^stride]a
785+
, ("fromToDownBy", flip scGlobalDef "Cryptol.ecFromToDownBy")
786+
-- fromToDownBy : {first, last, stride, a}
787+
-- (fin first, fin stride, stride >= 1, first >= last, Literal first a) =>
788+
-- [1 + (first - last)/stride]a
789+
, ("fromToDownByGreaterThan", flip scGlobalDef "Cryptol.ecFromToDownByGreaterThan")
790+
-- fromToDownByGreaterThan : {first, bound, stride, a}
791+
-- (fin first, fin stride, stride >= 1, first >= bound, Literal first a) =>
792+
-- [(first - bound)/^stride]a
777793

778794
-- Evaluation primitives: deepseq, parmap
779795
, ("deepseq", flip scGlobalDef "Cryptol.ecDeepseq") -- {a, b} (Eq b) => a -> b -> b

‎deps/cryptol

Submodule cryptol updated 79 files

‎deps/what4

Submodule what4 updated 34 files

0 commit comments

Comments
 (0)