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

Make things build with new module system #1751

Closed
wants to merge 6 commits into from
Closed

Conversation

yav
Copy link
Member

@yav yav commented Oct 11, 2022

No testing yet

@chameco
Copy link
Contributor

chameco commented Nov 20, 2022

I've tested the Cryptol module system a bit (with some small changes so SAW will compile given recent changes to the Cryptol branch, see here), and found a minor discrepancy that causes the AWSLC test to fail. Consider the following Cryptol modules:

// test1.cry
module test1 where
parameter
  type foo : #
  bar : [foo]
// test0.cry
module test0 = test1 where
  type foo = 32
  bar = 0xdeadbeef

And the following SAWScript source:

// test.saw
import "test0.cry";
print (eval_int {{ bar }});
print (eval_int {{ `foo : [64] }});

On master, test.saw runs to completion. With the updated Cryptol module system, it prints the value of bar and then produces the following error:

[03:28:55.469] Stack trace:
Cryptol error:
[error] at /tmp/test.saw:4:21--4:24
    Type not in scope: foo

I looked into this a bit, and it looks like foo is no longer present in the Cryptol NamingEnv for the imported module (vs. not being added to some environment on the SAW side).

RyanGlScott added a commit that referenced this pull request Jan 30, 2023
This brings in changes from Cryptol's constraint guards and FFI patches, which
require some light code changes on SAW's end. These changes are mostly taken
from #1751.

Co-authored-by: Iavor Diatchki <iavor.diatchki@gmail.com>
@RyanGlScott
Copy link
Contributor

Superseded by #1850.

@RyanGlScott RyanGlScott deleted the isd/cry-functors branch March 22, 2024 14:57
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants