Skip to content

Commit

Permalink
Bump Cryptol submodule for constraint guard fix
Browse files Browse the repository at this point in the history
Closes #1923

This change updates the cryptol submodule to pull in the fix for
constraint guards with types dependent on module parameters.

See GaloisInc/cryptol#1569 for the relevant
cryptol issue and GaloisInc/cryptol#1570 for the
fix.
  • Loading branch information
Brett Boston committed Sep 1, 2023
1 parent aa550a8 commit af8dc77
Show file tree
Hide file tree
Showing 4 changed files with 17 additions and 1 deletion.
2 changes: 1 addition & 1 deletion deps/cryptol
3 changes: 3 additions & 0 deletions intTests/test_constraint_guards/Instantiated.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
module Instantiated = Parameterized where

type gamma = 3
9 changes: 9 additions & 0 deletions intTests/test_constraint_guards/Parameterized.cry
Original file line number Diff line number Diff line change
@@ -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
4 changes: 4 additions & 0 deletions intTests/test_constraint_guards/test.saw
Original file line number Diff line number Diff line change
Expand Up @@ -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 }};

0 comments on commit af8dc77

Please sign in to comment.