Panic - `not a word value` `ccatV left` and `ccatV right`

[weaversa]

nightly: Pulling from galoisinc/cryptol
Digest: sha256:87b94650e66333dadcca914f77ebfdad158ec920b960cf19f714e4181b57eb10
Status: Image is up to date for ghcr.io/galoisinc/cryptol:nightly
ghcr.io/galoisinc/cryptol:nightly
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.13.0.99
https://cryptol.net  :? for help

Loading module Cryptol
Cryptol> 0
Showing a specific instance of polymorphic result:
  * Using 'Integer' for the type of '(expression)'
0
Cryptol> [0..0]
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type argument 'a' of 'Cryptol::fromTo'
[0]
Cryptol> 0 # [0..0]
Showing a specific instance of polymorphic result:
  * Using '0' for type argument 'front' of '(Cryptol::#)'
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  UNKNOWN
  Branch:    UNKNOWN
  Location:  [Eval] fromWordVal
  Message:   not a word value
             ccatV right
             seq:1
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.13.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Backend/Monad.hs:410:17 in cryptol-2.13.0.99-inplace:Cryptol.Backend.Monad
  evalPanic, called at src/Cryptol/Eval/Value.hs:377:23 in cryptol-2.13.0.99-inplace:Cryptol.Eval.Value
%< --------------------------------------------------- 
...restarting cryptol...
Cryptol> [0..0] # 0
Showing a specific instance of polymorphic result:
  * Using '0' for type argument 'back' of '(Cryptol::#)'
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  UNKNOWN
  Branch:    UNKNOWN
  Location:  [Eval] fromWordVal
  Message:   not a word value
             ccatV left
             seq:1
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.13.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Backend/Monad.hs:410:17 in cryptol-2.13.0.99-inplace:Cryptol.Backend.Monad
  evalPanic, called at src/Cryptol/Eval/Value.hs:377:23 in cryptol-2.13.0.99-inplace:Cryptol.Eval.Value
%< --------------------------------------------------- 

[weaversa]

Oddly enough [0..2] works but [0..1] doesn't. I wonder if the mistake is with the case where [0, 1] is a 2-bit bitvector (because 1 and 0 can also be True and False)

Cryptol> [0..2] # 0

[error] at <interactive>:2:1--2:11:
  • Unsolvable constraint:
      1 >= 2
        arising from
        use of finite enumeration
        at <interactive>:2:1--2:11
Cryptol> [0..1] # 0
Showing a specific instance of polymorphic result:
  * Using '0' for type argument 'back' of '(Cryptol::#)'
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  UNKNOWN
  Branch:    UNKNOWN
  Location:  [Eval] fromWordVal
  Message:   not a word value
             ccatV left
             seq:2
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.13.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Backend/Monad.hs:410:17 in cryptol-2.13.0.99-inplace:Cryptol.Backend.Monad
  evalPanic, called at src/Cryptol/Eval/Value.hs:377:23 in cryptol-2.13.0.99-inplace:Cryptol.Eval.Value
%< --------------------------------------------------- 

[RyanGlScott]

Focusing on the [0..0] # 0 example, we have:

• [0 .. 0] : {a} (Literal 0 a) => [1]a
• 0 : {a} (Literal 0 a) => a

The only way to make 0 have type [n]a is if a equals Bit, as you can have 0 : [1] but not, say, 0 : [1]Integer. This is why [0..0] and [0..1] typecheck in the examples above but [0..2] does not, since 0 and 1 have interpretations as Bits but 2 does not.

---

Anyways, why does [0 .. 0] # 0 panic? Looking at the site where the call to fromWordVal panics, we can see that it arises from the implementation of (#). Specifically, in the special case where both arguments are finite-length bitvectors:

cryptol/src/Cryptol/Eval/Generic.hs

Lines 1188 to 1200 in 8cca245

	-- Finite bitvectors
	ccatV sym front (Nat back) TVBit l r =
	do ml <- isReady sym l
	mr <- isReady sym r
	case (ml, mr) of
	(Just l', Just r') ->
	VWord (front+back) <$>
	joinWordVal sym (fromWordVal "ccatV left" l') (fromWordVal "ccatV right" r')
	_ ->
	VWord (front+back) <$> delayWordValue sym (front+back)
	(do l' <- fromWordVal "ccatV left" <$> l
	r' <- fromWordVal "ccatV right" <$> r
	joinWordVal sym l' r')

This code is correct if we uphold the invariant that both l and r are VWords. As a result, something must be violating that invariant. A clue is that [0..0] # 0 panics but [0] # 0 does not. Indeed, the implementation of fromTo (which powers the [x..y] notation) looks suspect:

cryptol/src/Cryptol/Eval/Generic.hs

Lines 1449 to 1461 in 8cca245

	-- @[ 0 .. 10 ]@
	fromToV :: Backend sym => sym -> Prim sym
	fromToV sym =
	PNumPoly \first ->
	PNumPoly \lst ->
	PTyPoly \ty ->
	PVal
	let !f = mkLit sym ty in
	case (first, lst) of
	(Nat first', Nat lst') ->
	let len = 1 + (lst' - first')
	in VSeq len $ indexSeqMap $ \i -> f (first' + i)
	_ -> evalPanic "fromToV" ["invalid arguments"]

This always returns a VSeq. But if ty is a TBit, then this will violate the invariant that bitvectors are represented with VWords, which causes havoc when the VSeq is passed to (#).

Instead of returning VSeq, I think it would suffice to use mkSeq, which returns a VWord or VSeq depending on what the type argument is:

diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs
index 204658b9..946f41ee 100644
--- a/src/Cryptol/Eval/Generic.hs
+++ b/src/Cryptol/Eval/Generic.hs
@@ -1452,12 +1452,12 @@ fromToV sym =
   PNumPoly \first ->
   PNumPoly \lst ->
   PTyPoly  \ty ->
-  PVal
+  PPrim
     let !f = mkLit sym ty in
     case (first, lst) of
       (Nat first', Nat lst') ->
         let len = 1 + (lst' - first')
-        in VSeq len $ indexSeqMap $ \i -> f (first' + i)
+        in mkSeq sym (Nat len) ty $ indexSeqMap $ \i -> f (first' + i)
       _ -> evalPanic "fromToV" ["invalid arguments"]
 
 {-# INLINE fromThenToV #-}

I think we'd need to do something similar for various other operations that always return VSeqs (e.g., [0, 0 .. 0]).