import Cryptol to include access to private methods

[weaversa]

When importing a Cryptol spec with a private block, the definitions in the private block are not accessible in the saw repl. This runs counter to how the Cryptol repl - namely, the definitions are accessible in the Cryptol repl. I often put properties under a private block to stop them from muddying the namespace of parent modules. However, since saw doesn't give access to these definitions, I can't use saw to prove the properties.

Consider allowing saw to access first-class private definitions when importing a Cryptol spec (same as how Cryptol works currently).

$ cat test.cry
module test where

a = 1

private

  b = 2
$ cryptol-nightly test.cry
nightly: Pulling from galoisinc/cryptol
Digest: sha256:92ba978baca6d8ff523ffa5a6fb9ef3bfcfaad9deb804ef1de271e837814ccc8
Status: Image is up to date for galoisinc/cryptol:nightly
docker.io/galoisinc/cryptol:nightly
                        _        _
   ___ _ __ _   _ _ __ | |_ ___ | |
  / __| '__| | | | '_ \| __/ _ \| |
 | (__| |  | |_| | |_) | || (_) | |
  \___|_|   \__, | .__/ \__\___/|_|
            |___/|_| version 2.10.0.99
https://cryptol.net  :? for help

Loading module Cryptol
Loading module test
test> :b test
Symbols
=======

  Public
  ------

    a : {a} (Literal 1 a) => a

  Private
  -------

    b : {a} (Literal 2 a) => a

test> b
Showing a specific instance of polymorphic result:
  * Using 'Integer' for the type of 'test::b'
2
test> :q
$ saw-nightly
nightly: Pulling from galoisinc/saw
Digest: sha256:f76b61db106652434192d909552a308e20d92ee56c81b4aa37887c76e657d218
Status: Image is up to date for galoisinc/saw:nightly
docker.io/galoisinc/saw:nightly
 ┏━━━┓━━━┓━┓━┓━┓
 ┃ ━━┓ ╻ ┃ ┃ ┃ ┃
 ┣━━ ┃ ╻ ┃┓ ╻ ┏┛
 ┗━━━┛━┛━┛┗━┛━┛ version 0.6.0.99 (<non-dev-build>)



sawscript> import "test.cry"
sawscript> print {{ a }}
[21:43:53.505] Assuming a = Integer
[21:43:53.506] 1
sawscript> print {{ b }}

Cryptol error:
[error] at <stdin>:1:10--1:11 Value not in scope: b
sawscript> 

[weaversa]

It's possible this is related to #798.

[atomb]

After inspecting this a little more, it seems as though the key issue here is the context used to type check Cryptol expressions in curly braces. The current Cryptol to SAWCore translator already includes both public and private definitions already, but expressions referencing private definitions don't type check in the Cryptol context we're using.

[brianhuffman]

Fixed in #1020.