switched to using intToBv for writing bitvector literals instead of bvLit (as the two had the same definition anyway); also changed bitvector literals to use signed integers, and switched to using the bv-sized library to do this translation instead of rolling our own; all of this in support of #25

Author: Eddy Westbrook

coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v

@@ -194,14 +194,12 @@ Fixpoint bvNat (size : Nat) (number : Nat) : bitvector size :=
 
 (* Arguments bvNat : simpl never. *)
 
-(* Use this to write decimal number literals of bitvector type, e.g. bvLit 64 3 *)
-Definition bvLit (size : Nat) (lit : Z) : bitvector size := bitsToBv (fromZ lit).
-
 Definition bvToNatFolder (n : nat) (b : bool) := b + n.*2.
 
 Fixpoint bvToNat (size : Nat) (v : bitvector size) : Nat :=
   Vector.fold_left bvToNatFolder 0 v.
 
+(* This is used to write literals of bitvector type, e.g. intToBv 64 3 *)
 Definition intToBv (n : Nat) (z : Z) : bitvector n := bitsToBv (fromZ z).
 Opaque intToBv.
 

saw-core-coq.cabal

@@ -24,6 +24,8 @@ library
     lens,
     mtl,
     saw-core,
+    parameterized-utils,
+    bv-sized,
     vector
   hs-source-dirs: src
   exposed-modules:

src/Verifier/SAW/Translation/Coq/Term.hs

@@ -12,6 +12,9 @@
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PatternGuards #-}
 
 {- |
 Module      : Verifier.SAW.Translation.Coq
@@ -34,8 +37,10 @@ import           Data.Maybe                                    (fromMaybe)
 import           Prelude                                       hiding (fail)
 import           Text.PrettyPrint.ANSI.Leijen                  hiding ((<$>))
 
-import           Data.Bits                                     ((.|.), bit)
-import qualified Data.Vector                                   as Vector (reverse, imap)
+import           Data.Parameterized.Pair
+import           Data.Parameterized.NatRepr
+import qualified Data.BitVector.Sized                          as BV
+import qualified Data.Vector                                   as Vector (reverse, toList)
 import qualified Language.Coq.AST                              as Coq
 import qualified Language.Coq.Pretty                           as Coq
 import           Verifier.SAW.Recognizer
@@ -188,12 +193,11 @@ flatTermFToExpr tf = -- traceFTermF "flatTermFToExpr" tf $
          Coq.App rect_var <$> mapM translateTerm args
     Sort s -> pure (Coq.Sort (translateSort s))
     NatLit i -> pure (Coq.NatLit (toInteger i))
-    ArrayValue (asBoolType -> Just ()) (traverse asBool -> Just bits) -> do
-      return (Coq.App (Coq.Var "bvLit")
-              [Coq.NatLit (toInteger $ length bits),
-               Coq.ZLit (foldl (.|.) 0 $
-                         Vector.imap (\i b -> if b then bit i else 0) $
-                         Vector.reverse bits)])
+    ArrayValue (asBoolType -> Just ()) (traverse asBool -> Just bits)
+      | Pair w bv <- BV.bitsBE (Vector.toList bits)
+      , Left LeqProof <- decideLeq (knownNat @1) w -> do
+          return (Coq.App (Coq.Var "intToBv")
+                  [Coq.NatLit (intValue w), Coq.ZLit (BV.asSigned w bv)])
     ArrayValue _ vec -> do
       let addElement accum element = do
             elementTerm <- translateTerm element