1964 allow importing cryptol submodules into saw

[mtullsen]

• see title and Allow importing Cryptol submodules into SAW #1964.

[RyanGlScott]

Note that you'll need to resolve the merge conflicts in order for the CI to run.

[sauclovian-g]

The large merge conflict in Value.hs arises from this change:

-    fromValue _ = error "fromValue ModuleEnv"
+    fromValue _ = error "fromValue CryptolModule"

which you can (please do) instead apply in the current FromValue definitions, which got moved to Interpreter.hs.

[mtullsen]

• This PR now supports (see tests) submodules in cryptol modules loaded using SAWScript's import command.
• Note the new tests
• Supporting cryptol_load is not in scope for this PR.

[sauclovian-g]

Are there changes needed to build/run with the Cryptol submodule bump? If so, do you want to apply them separately (so they can go on the release branch) or do we want to commit to merging this PR and backporting it onto the release branch?

I would not be averse to including these changes in the release :-) but it means we probably need to merge them in the next couple days.

[mtullsen]

Are there changes needed to build/run with the Cryptol submodule bump?

• the "Cryptol submodel bump" can be applied separately (no API is changed, just a fix).

If so, do you want to apply them separately (so they can go on the release branch) or do we want to commit to merging this PR and backporting it onto the release branch?
I would not be averse to including these changes in the release :-) but it means we probably need to merge them in the next couple days.

... sorry, I'm not 100% sure I follow you: we talking about deps/cryptol/ and/or saw-script/ ... and how exactly do we like to manage submodules in releases...?. (I've setup a meeting, @sauclovian-g). Either way, both the PRs should be pretty robust with where they can be merged ...

I've addressed @RyanGlScott 's most recent comments and am comfortable with this being merged.

[mtullsen]

@RyanGlScott @sauclovian-g @brianhuffman
I had a FIXME in the code, but thanks to @RyanGlScott 's comments above, I've
removed it. I think I need to turn this into a discussion and/or Issue.
The issue is documenting the need and use and implementation of what's
going on with deps/cryptol/lib/Cryptol/Reference.cry:

• Questions
  • We have any documentation for users as to why this exists?
  • Regarding implementation:
    • In cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs
      • No haddock for the constructor field envRefPrims
    • In cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
      • why is "special processing needed?" and what exactly is going on here:

        -- Set up reference implementation redirections
        let refDecls = T.mDecls refMod
        let nms = Set.toList (MI.ifsPublic (TIface.genIfaceNames refMod))
        let refPrims = Map.fromList
                        [ (prelPrim (identText (MN.nameIdent nm)), T.EWhere (T.EVar nm) refDecls)
                        | nm <- nms ]
        let cryEnv0 = C.emptyEnv{ C.envRefPrims = refPrims }
      

Right now, this comment is the "meta-question": this important? should I make an Issue with the above in it?

[RyanGlScott]

We have any documentation for users as to why this exists?

Cryptol::Reference's purpose could stand to be documented better in Cryptol. The short version is: yes, the special handling is required.

Longer answer: Cryptol has several primitive functions, and nearly all of them have backend-specific implementations (i.e., SBV and What4 implementations) that translate each primitive to SMT-LIB. There are a small handful of primitive functions that lack backend-specific implementations, however. For these primitives, Cryptol::Reference provides reference implementations as Cryptol functions. There is special handling inside of Cryptol to ensure that these primitives look up their corresponding Cryptol::Reference implementations when called (see, for instance, this code), and SAW needs similar special handling as well.

No haddock for the constructor field envRefPrims

This is where the implementations of the functions in Cryptol::Reference are stored after loading them, as far as I can tell. Later, envRefPrims is used here to ensure to allow these Cryptol::Reference primitives to look up their implementations properly.

(The code with the "Set up reference implementation redirections" comment you highlight above exists to populate the envRefPrims with the loaded implementations.)

this important? should I make an Issue with the above in it?

If you'd like, please feel free to open a Cryptol issue to document Cryptol::Reference better. It's a question that's come up before, so it would be worthwhile to write all this down in an easier-to-discover location.

[mtullsen]

@sauclovian-g did you want to review before I merge this?

[sauclovian-g]

Probably I should but go ahead, anything I find will be minor and can be taken up later