SAW panic when using constraint guards with types dependent on module parameters

[bboston7]

Given the parameterized module:

module Parameterized where

parameter
    type gamma1 : #
    type constraint (fin gamma1, gamma1 >= 2, 32 >= width gamma1)

x : [gamma1]
x | () => 0

and instantiation:

module Instantiated = Parameterized where

type gamma1 =  3

and SAW file importing the instantiated module:

import "Instantiated.cry";

SAW panics with the error:

[20:44:58.951] You have encountered a bug in cryptol-saw-core's implementation.
*** Please create an issue at https://github.com/GaloisInc/saw-script/issues

%< --------------------------------------------------- 
  Revision:  0aa2492e78f09b16e8d40e0ac3f71c5b40978731
  Branch:    master (uncommited files present)
  Location:  importType TVBound
  Message:   
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Cryptol/Panic.hs:13:9 in cryptol-saw-core-0.1-inplace:Verifier.SAW.Cryptol.Panic
  panic, called at src/Verifier/SAW/Cryptol.hs:264:37 in cryptol-saw-core-0.1-inplace:Verifier.SAW.Cryptol
%< --------------------------------------------------- 

I'm still debugging exactly what's going on, but here are some things I learned in minimizing the example:

• When built with profiling to get a stack trace, the relevant stack trace for the error appears to be:

*** Exception (reporting due to +RTS -xc): (THUNK), stack trace:                                                                                                                    [112/15100]
  Panic.panic,                                                                                 
  called from Verifier.SAW.Cryptol.Panic.panic,                                                
  called from Verifier.SAW.Cryptol.importType,                                                 
  called from Verifier.SAW.Cryptol.CAF                                                         
  --> evaluated by: Verifier.SAW.Cryptol.importType,                                           
  called from Verifier.SAW.Cryptol.importExpr,                                                 
  called from Verifier.SAW.Cryptol.importTopLevelDeclGroups,                                   
  called from Verifier.SAW.CryptolEnv.importModule,                                                                                                                                            
  called from SAWScript.Value.getSharedContext,                                                                                                                                                
  called from Lang.Crucible.Utils.StateContT.get,                                              
  called from SAWScript.Value.getTopLevelRW,                                                   
  called from SAWScript.Interpreter.interpretStmt,                                             
  called from Lang.Crucible.Utils.StateContT.<$,                                               
  called from Lang.Crucible.Utils.StateContT.*>,                                               
  called from SAWScript.Value.getOptions,                                                      
  called from Lang.Crucible.Utils.StateContT.lift,                                             
  called from Lang.Crucible.Utils.StateContT.liftIO,                                           
  called from Lang.Crucible.Utils.StateContT.catch,                                            
  called from SAWScript.Value.io,                                                              
  called from SAWScript.Value.bracketTopLevel,                                                 
  called from SAWScript.Interpreter.interpretFile,                                                                                                                                             
  called from SAWScript.Value.runTopLevel,                                                                                                                                                     
  called from SAWScript.Interpreter.processFile,                                                                                                                                               
  called from Main.main 

• The panic itself occurs because looking up gamma1 in the environment fails (see this line of the translator), so I imagine some other part of the translator isn't adding gamma1 to the environment like it should.
• I'm not sure whether the constraint guard itself is relevant. The stack trace doesn't include the constraint guard handling part of the cryptol translator, and adding debug tracing shows that this panic occurs before any constraint guard translation. However, I couldn't reproduce this bug without using a constraint guard. Maybe constraint guards change something else earlier in the translation that I didn't properly handle in Add support for translating Cryptol constraint guards #1911.

@qsctr I know you've been looking at the Cryptol translator lately and you have experience with the Cryptol AST. Do you have any ideas about what might be going wrong here?

I'm going to keep digging and I'll add comments for anything else I learn.

[qsctr]

In my testing it does seem to be happening in the constraint guard handling -- specifically in this call to importType.

The declaration that is causing the panic is this one, which has a TVBound referencing gamma1 inside it.

        , NonRecursive
            ( Decl
                { dName = Name
                    { nUnique = 4780
                    , nInfo = GlobalName UserName
                        ( OrigName
                            { ogNamespace = NSValue
                            , ogModule = TopModule
                                ( ModName "Instantiated" NormalName )
                            , ogSource = FromFunctorInst
                            , ogName = Ident False NormalName "x"
                            , ogFromParam = Nothing
                            }
                        )
                    , nFixity = Nothing
                    , nLoc = Range
                        { from = Position
                            { line = 8
                            , col = 1
                            }
                        , to = Position
                            { line = 8
                            , col = 2
                            }
                        , source = "./Parameterized.cry"
                        }
                    }
                , dSignature = Forall
                    { sVars = []
                    , sProps = []
                    , sType = TCon ( TC TCSeq )
                        [ TCon
                            ( TC
                                ( TCNum 3 )
                            ) []
                        , TCon ( TC TCBit ) []
                        ]
                    }
                , dDefinition = DExpr
                    ( EPropGuards
                        [
                            ( []
                            , EVar
                                ( Name
                                    { nUnique = 4781
                                    , nInfo = GlobalName UserName
                                        ( OrigName
                                            { ogNamespace = NSValue
                                            , ogModule = TopModule
                                                ( ModName "Instantiated" NormalName )
                                            , ogSource = FromFunctorInst
                                            , ogName = Ident False NormalName "x()"
                                            , ogFromParam = Nothing
                                            }
                                        )
                                    , nFixity = Nothing
                                    , nLoc = Range
                                        { from = Position
                                            { line = 8
                                            , col = 1
                                            }
                                        , to = Position
                                            { line = 8
                                            , col = 2
                                            }
                                        , source = "./Parameterized.cry"
                                        }
                                    }
                                )
                            )
                        ]
                        ( TCon ( TC TCSeq )
                            [ TVar
                                ( TVBound
                                    ( TParam
                                        { tpUnique = 4782
                                        , tpKind = KNum
                                        , tpFlav = TPModParam
                                            ( Name
                                                { nUnique = 4782
                                                , nInfo = GlobalName UserName
                                                    ( OrigName
                                                        { ogNamespace = NSType
                                                        , ogModule = TopModule
                                                            ( ModName "Instantiated" NormalName )
                                                        , ogSource = FromFunctorInst
                                                        , ogName = Ident False NormalName "gamma1"
                                                        , ogFromParam = Just
                                                            ( Ident False AnonIfaceModName "Parameterized" )
                                                        }
                                                    )
                                                , nFixity = Nothing
                                                , nLoc = Range
                                                    { from = Position
                                                        { line = 1
                                                        , col = 8
                                                        }
                                                    , to = Position
                                                        { line = 1
                                                        , col = 21
                                                        }
                                                    , source = "./Parameterized.cry"
                                                    }
                                                }
                                            )
                                        , tpInfo = TVarInfo
                                            { tvarSource = Range
                                                { from = Position
                                                    { line = 1
                                                    , col = 8
                                                    }
                                                , to = Position
                                                    { line = 1
                                                    , col = 21
                                                    }
                                                , source = "./Parameterized.cry"
                                                }
                                            , tvarDesc = TVFromModParam
                                                ( Name
                                                    { nUnique = 4782
                                                    , nInfo = GlobalName UserName
                                                        ( OrigName
                                                            { ogNamespace = NSType
                                                            , ogModule = TopModule
                                                                ( ModName "Instantiated" NormalName )
                                                            , ogSource = FromFunctorInst
                                                            , ogName = Ident False NormalName "gamma1"
                                                            , ogFromParam = Just
                                                                ( Ident False AnonIfaceModName "Parameterized" )
                                                            }
                                                        )
                                                    , nFixity = Nothing
                                                    , nLoc = Range
                                                        { from = Position
                                                            { line = 1
                                                            , col = 8
                                                            }
                                                        , to = Position
                                                            { line = 1
                                                            , col = 21
                                                            }
                                                        , source = "./Parameterized.cry"
                                                        }
                                                    }
                                                )
                                            }
                                        }
                                    )
                                )
                            , TCon ( TC TCBit ) []
                            ]
                        )
                    )
                , dPragmas = []
                , dInfix = False
                , dFixity = Nothing
                , dDoc = Nothing
                }
            )

[bboston7]

Thanks, I was looking for importNumericConstraintAsBool calls and completely missed that importType call. Now to figure out why gamma1 isn't in the environment.

[qsctr]

Actually, I think this might be a Cryptol bug, because the gamma1 is supposed to be substituted with 3 everywhere in the module after instantiation.

[qsctr]

I created GaloisInc/cryptol#1569 to track the Cryptol bug. The SAW import seems to work with the Cryptol fix applied.

[bboston7]

Great debugging! Thank you for looking into this!

[qsctr]

The Cryptol fix is merged now

[bboston7]

Thank you! I'll update the Cryptol submodule in SAW