Merge pull request #1930 from GaloisInc/bb/bump-cryptol

Bump Cryptol submodule for constraint guard fix
GaloisInc · Sep 2, 2023 · aecabca · aecabca
2 parents 18ca05a + acfadc5
commit aecabca
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 1 deletion.
diff --git a/deps/cryptol b/deps/cryptol
diff --git a/intTests/test_constraint_guards/Instantiated.cry b/intTests/test_constraint_guards/Instantiated.cry
@@ -0,0 +1,3 @@
+module Instantiated = Parameterized where
+
+type gamma =  3
diff --git a/intTests/test_constraint_guards/Parameterized.cry b/intTests/test_constraint_guards/Parameterized.cry
@@ -0,0 +1,9 @@
+module Parameterized where
+
+parameter
+    type gamma : #
+    type constraint (fin gamma, gamma >= 2, 32 >= width gamma)
+
+// Constraint guard with type dependent on module parameter value
+v : [gamma]
+v | () => 0
diff --git a/intTests/test_constraint_guards/test.saw b/intTests/test_constraint_guards/test.saw
@@ -16,3 +16,7 @@ fails (prove_print z3 {{ \(x : [64]) -> incomplete x }});
 prove_print z3 {{ dependent`{1} == [True] }};
 prove_print z3 {{ dependent`{3} == [False, False, False] }};
 prove_print z3 {{ dependent`{0} == [] }};
+
+// Test constraint guards dependently typed on module parameters
+import "Instantiated.cry";
+prove_print z3 {{ v == 0 }};
+2 −1		src/Cryptol/IR/FreeVars.hs
+3 −1		src/Cryptol/TypeCheck/Subst.hs
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		module Instantiated = Parameterized where

		type gamma = 3