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

SAW can't access module parameters #798

Open
weaversa opened this issue Jul 26, 2020 · 0 comments
Open

SAW can't access module parameters #798

weaversa opened this issue Jul 26, 2020 · 0 comments
Labels
missing cryptol features Issues about features in Cryptol that don't work in SAW subsystem: cryptol-saw-core Issues related to Cryptol -> saw-core translation with cryptol-saw-core type: bug Issues reporting bugs or unexpected/unwanted behavior usability An issue that impedes efficient understanding and use
Milestone

Comments

@weaversa
Copy link
Contributor

module SHA::SHA384 = SHA::SHA where

type w = 64
...

SAW can't access w.

sawscript> import "SHA/SHA384.cry" 
sawscript> print {{ `w }}

user error (Cryptol error:
[error] at <stdin>:1:11--1:12 Type not in scope: w)
sawscript> 

Cryptol can:

$ cryptol SHA/SHA384.cry 
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.8.1 (e914cef)
https://cryptol.net  :? for help

Loading module Cryptol
Loading module SHA::SHA
Loading module SHA::SHA384
SHA::SHA384> `w
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type argument 'rep' of 'Cryptol::number'
64
SHA::SHA384>

I was trying to use SAW to verify some code and wanted it to just work with whatever parameterized module I passed in. To do that, SAW needs to be able to access parameters.

@weaversa weaversa changed the title SAW Can't access module parameters SAW can't access module parameters Jul 26, 2020
@robdockins robdockins added the usability An issue that impedes efficient understanding and use label Jun 25, 2021
@sauclovian-g sauclovian-g added type: bug Issues reporting bugs or unexpected/unwanted behavior subsystem: cryptol-saw-core Issues related to Cryptol -> saw-core translation with cryptol-saw-core missing cryptol features Issues about features in Cryptol that don't work in SAW labels Oct 29, 2024
@sauclovian-g sauclovian-g added this to the 2025T1 milestone Oct 29, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
missing cryptol features Issues about features in Cryptol that don't work in SAW subsystem: cryptol-saw-core Issues related to Cryptol -> saw-core translation with cryptol-saw-core type: bug Issues reporting bugs or unexpected/unwanted behavior usability An issue that impedes efficient understanding and use
Projects
None yet
Development

No branches or pull requests

3 participants