Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Parameterized modules don't consider their own type contraints #1240

Closed
weaversa opened this issue Jul 20, 2021 · 1 comment · Fixed by #1245
Closed

Parameterized modules don't consider their own type contraints #1240

weaversa opened this issue Jul 20, 2021 · 1 comment · Fixed by #1245
Assignees
Labels
parameterized modules Related to Cryptol's parameterized modules

Comments

@weaversa
Copy link
Collaborator

This was happily accepted via version 2.10 but not with the current 2.11 nightly. @yav ?

$  more test.cry
module test where

parameter

  type a : #
  type constraint (fin a, a >= 1)

  b : Z a
$ cryptol test.cry 
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.11.0.99
https://cryptol.net  :? for help

Loading module Cryptol
Loading module test
[error] at test.cry:1:1--8:4:
  Failed to validate user-specified signature.
    in the definition of 'test::b', at test.cry:8:3--8:4,
    we need to show that
      for any type test::a
      the following constraints hold:
        • fin test::a
            arising from
            use of partial type function Cryptol::Z
            at test.cry:8:7--8:10
        • test::a >= 1
            arising from
            use of partial type function Cryptol::Z
            at test.cry:8:7--8:10
Loading module Cryptol
Cryptol> 
@robdockins robdockins added the parameterized modules Related to Cryptol's parameterized modules label Jul 20, 2021
@yav yav self-assigned this Jul 22, 2021
yav added a commit that referenced this issue Jul 22, 2021
@yav yav closed this as completed in #1245 Jul 22, 2021
@weaversa
Copy link
Collaborator Author

@yav thank you!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
parameterized modules Related to Cryptol's parameterized modules
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants