cleanup for #1437

* add entry to CHANGES.md * drop `deriving Generic` from `FinSeq` newtype
GaloisInc · Feb 20, 2025 · 3829b63 · 3829b63
1 parent a0ecfa8
commit 3829b63
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 3 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -1,9 +1,15 @@
 # next -- TBA
 
+
 ## Language changes
 
 ## Bug fixes
 
+* Fix #1437, enforce the VSeq invariant that it is not a sequence of bits.
+  Replaces the VSeq constructor with a view-only pattern, and smart constructors
+  `mkSeq` and `finSeq`.
+  ([#1437](https://github.com/GaloisInc/cryptol/issues/1437))
+
 * Fix #1740, removes duplicated width from word values.
   Note that since this changes the types, it may require changes to libraries
   depending on Cryptol.

diff --git a/src/Cryptol/Eval/Value.hs b/src/Cryptol/Eval/Value.hs
@@ -399,8 +399,7 @@ ilam sym f =
 
 -- | A finite sequence of non-VBit values. Used in 'finSeq' to
 --   safely construct a 'VSeq'.
-newtype FinSeq sym = FinSeq { fromFinSeq :: [GenValue sym] }
-  deriving Generic
+newtype FinSeq sym = FinSeq [GenValue sym]
 
 -- | Safely wrap a 'GenValue' list as a 'FinSeq'. Returns 'Nothing'
 --   if any values are a 'VBit'.
@@ -412,7 +411,7 @@ toFinSeq xs = FinSeq <$> mapM go xs
       _ -> Just x
 
 -- | Wrap a 'GenValue' list as a 'FinSeq'. Raises a runtime
---   error if any values are a 'VBit'
+--   error if any values are a 'VBit'.
 unsafeToFinSeq :: [GenValue sym] -> FinSeq sym
 unsafeToFinSeq xs = FinSeq (map go xs)
   where