From af8dc7748ba064d1fd8f1e3abd432f15a4a620bc Mon Sep 17 00:00:00 2001 From: Brett Boston Date: Fri, 1 Sep 2023 14:13:43 -0700 Subject: [PATCH] Bump Cryptol submodule for constraint guard fix Closes #1923 This change updates the cryptol submodule to pull in the fix for constraint guards with types dependent on module parameters. See https://github.com/GaloisInc/cryptol/issues/1569 for the relevant cryptol issue and https://github.com/GaloisInc/cryptol/pull/1570 for the fix. --- deps/cryptol | 2 +- intTests/test_constraint_guards/Instantiated.cry | 3 +++ intTests/test_constraint_guards/Parameterized.cry | 9 +++++++++ intTests/test_constraint_guards/test.saw | 4 ++++ 4 files changed, 17 insertions(+), 1 deletion(-) create mode 100644 intTests/test_constraint_guards/Instantiated.cry create mode 100644 intTests/test_constraint_guards/Parameterized.cry diff --git a/deps/cryptol b/deps/cryptol index 63f0ac6968..3973b15236 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit 63f0ac6968967fb7898333778b5206083fdcb375 +Subproject commit 3973b15236ace5c11fdfabbf811d97daee7885ed diff --git a/intTests/test_constraint_guards/Instantiated.cry b/intTests/test_constraint_guards/Instantiated.cry new file mode 100644 index 0000000000..490cdb4ec2 --- /dev/null +++ b/intTests/test_constraint_guards/Instantiated.cry @@ -0,0 +1,3 @@ +module Instantiated = Parameterized where + +type gamma = 3 \ No newline at end of file diff --git a/intTests/test_constraint_guards/Parameterized.cry b/intTests/test_constraint_guards/Parameterized.cry new file mode 100644 index 0000000000..0cb7b8b00a --- /dev/null +++ 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 index e2b443bb91..d1364bda50 100644 --- 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 }}; \ No newline at end of file