Merge pull request #90 from GaloisInc/remove-bitvector

Remove saw-core `bitvector` type synonym; use `Vec n Bool` instead.

cryptol-saw-core/saw/Cryptol.sawcore

@@ -14,10 +14,10 @@ const a b x y = x;
 compose : (a b c : sort 0) -> (b -> c) -> (a -> b) -> (a -> c);
 compose _ _ _ f g x = f (g x);
 
-bvExp : (n : Nat) -> bitvector n -> bitvector n -> bitvector n;
-bvExp n x y = foldr Bool (bitvector n) n
-  (\ (b : Bool) -> \ (a : bitvector n) ->
-    ite (bitvector n) b (bvMul n x (bvMul n a a)) (bvMul n a a))
+bvExp : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
+bvExp n x y = foldr Bool (Vec n Bool) n
+  (\ (b : Bool) -> \ (a : Vec n Bool) ->
+    ite (Vec n Bool) b (bvMul n x (bvMul n a a)) (bvMul n a a))
   (bvNat n 1)
   (reverse n Bool y);
 
@@ -438,10 +438,10 @@ integerCmp x y k = or (intLt x y) (and (intEq x y) k);
 rationalCmp : Rational -> Rational -> Bool -> Bool;
 rationalCmp x y k = or (ltRational x y) (and (eqRational x y) k);
 
-bvCmp : (n : Nat) -> bitvector n -> bitvector n -> Bool -> Bool;
+bvCmp : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool -> Bool;
 bvCmp n x y k = or (bvult n x y) (and (bvEq n x y) k);
 
-bvSCmp : (n : Nat) -> bitvector n -> bitvector n -> Bool -> Bool;
+bvSCmp : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool -> Bool;
 bvSCmp n x y k = or (bvslt n x y) (and (bvEq n x y) k);
 
 vecCmp : (n : Nat) -> (a : sort 0) -> (a -> a -> Bool -> Bool)
@@ -1163,10 +1163,10 @@ ecSShiftR =
     (\ (n:Nat) ->
          (\ (ix : sort 0) -> \ (pix : PIntegral ix) ->
             natCase
-              (\ (w : Nat) -> bitvector w -> ix -> bitvector w)
-              (\ (xs : bitvector 0) -> \ (_ : ix) -> xs)
-              (\ (w : Nat) -> \ (xs : bitvector (Succ w)) ->
-                   pix.posNegCases (bitvector (Succ w))
+              (\ (w : Nat) -> Vec w Bool -> ix -> Vec w Bool)
+              (\ (xs : Vec 0 Bool) -> \ (_ : ix) -> xs)
+              (\ (w : Nat) -> \ (xs : Vec (Succ w) Bool) ->
+                   pix.posNegCases (Vec (Succ w) Bool)
 		     (bvSShr w xs)
 		     (bvShl (Succ w) xs))
               n));
@@ -1368,24 +1368,24 @@ ecInfFromThen a pa x y =
 
 
 -- Run-time error
-ecError : (a : sort 0) -> (len : Num) -> seq len (bitvector 8) -> a;
+ecError : (a : sort 0) -> (len : Num) -> seq len (Vec 8 Bool) -> a;
 ecError a len msg = error a "encountered call to the Cryptol 'error' function"; -- FIXME: don't throw away message
 {-
-primitive cryError : (a : sort 0) -> (n : Nat) -> Vec n (bitvector 8) -> a;
+primitive cryError : (a : sort 0) -> (n : Nat) -> Vec n (Vec 8 Bool) -> a;
 
-ecError : (a : sort 0) -> (len : Num) -> seq len (bitvector 8) -> a;
+ecError : (a : sort 0) -> (len : Num) -> seq len (Vec 8 Bool) -> a;
 ecError a =
   finNumRec
-    (\ (len:Num) -> seq len (bitvector 8) -> a)
+    (\ (len:Num) -> seq len (Vec 8 Bool) -> a)
     (\ (len:Nat) -> cryError a len);
 -}
 
 -- Random values
-ecRandom : (a : sort 0) -> bitvector 32 -> a;
+ecRandom : (a : sort 0) -> Vec 32 Bool -> a;
 ecRandom a _ = error a "Cryptol.random";
 
 -- Trace function; simply return the final argument
-ecTrace : (n : Num) -> (a b : sort 0) -> seq n (bitvector 8) -> a -> b -> b;
+ecTrace : (n : Num) -> (a b : sort 0) -> seq n (Vec 8 Bool) -> a -> b -> b;
 ecTrace _ _ _ _ _ x = x;
 
 
@@ -1481,16 +1481,16 @@ ecFpToBits e p _ = error (seq (tcAdd e p) Bool) "Unimplemented: fpToBits";
 ecFpEq : (e : Num) -> (p : Num) -> TCFloat e p -> TCFloat e p -> Bool;
 ecFpEq e p _ _ = error Bool "Unimplemented: =.=";
 
-ecFpAdd : (e : Num) -> (p : Num) -> bitvector 3 -> TCFloat e p -> TCFloat e p -> TCFloat e p;
+ecFpAdd : (e : Num) -> (p : Num) -> Vec 3 Bool -> TCFloat e p -> TCFloat e p -> TCFloat e p;
 ecFpAdd e p _ _ _ = error (TCFloat e p) "Unimplemented: fpAdd";
 
-ecFpSub : (e : Num) -> (p : Num) -> bitvector 3 -> TCFloat e p -> TCFloat e p -> TCFloat e p;
+ecFpSub : (e : Num) -> (p : Num) -> Vec 3 Bool -> TCFloat e p -> TCFloat e p -> TCFloat e p;
 ecFpSub e p _ _ _ = error (TCFloat e p) "Unimplemented: fpSub";
 
-ecFpMul : (e : Num) -> (p : Num) -> bitvector 3 -> TCFloat e p -> TCFloat e p -> TCFloat e p;
+ecFpMul : (e : Num) -> (p : Num) -> Vec 3 Bool -> TCFloat e p -> TCFloat e p -> TCFloat e p;
 ecFpMul e p _ _ _ = error (TCFloat e p) "Unimplemented: fpMul";
 
-ecFpDiv : (e : Num) -> (p : Num) -> bitvector 3 -> TCFloat e p -> TCFloat e p -> TCFloat e p;
+ecFpDiv : (e : Num) -> (p : Num) -> Vec 3 Bool -> TCFloat e p -> TCFloat e p -> TCFloat e p;
 ecFpDiv e p _ _ _ = error (TCFloat e p) "Unimplemented: fpDiv";
 
 ecFpIsFinite : (e : Num) -> (p : Num) -> TCFloat e p -> Bool;
@@ -1499,7 +1499,7 @@ ecFpIsFinite e p _ = error Bool "Unimplemented: fpIsFinite";
 ecFpToRational : (e : Num) -> (p : Num) -> TCFloat e p -> Rational;
 ecFpToRational e p _ = error Rational "Unimplemented: fpToRational";
 
-ecFpFromRational : (e : Num) -> (p : Num) -> bitvector 3 -> Rational -> TCFloat e p;
+ecFpFromRational : (e : Num) -> (p : Num) -> Vec 3 Bool -> Rational -> TCFloat e p;
 ecFpFromRational e p _ _ = error (TCFloat e p) "Unimplemented: fpFromRational";
 
 
@@ -1555,8 +1555,8 @@ ecSExt =
     (\ (m n : Num) -> seq n Bool -> seq (tcAdd m n) Bool)
     (\ (m n : Nat) ->
        natCase
-         (\ (n' : Nat) -> bitvector n' -> bitvector (addNat m n'))
-         (\ (_ : bitvector 0) -> bvNat (addNat m 0) 0)
+         (\ (n' : Nat) -> Vec n' Bool -> Vec (addNat m n') Bool)
+         (\ (_ : Vec 0 Bool) -> bvNat (addNat m 0) 0)
          (bvSExt m)
          n);
 
@@ -1593,15 +1593,15 @@ ecArrayUpdate = arrayUpdate;
 --------------------------------------------------------------------------------
 -- Rewrite rules
 
-axiom replicate_False : (n : Nat) -> Eq (bitvector n) (replicate n Bool False) (bvNat n 0);
+axiom replicate_False : (n : Nat) -> Eq (Vec n Bool) (replicate n Bool False) (bvNat n 0);
 
 axiom subNat_0 : (n : Nat) -> Eq Nat (subNat n 0) n;
 
 {-
 axiom demote_add_distr
   : (w : Nat)
   -> (x y : Num)
-  -> Eq (bitvector w)
+  -> Eq (Vec w Bool)
         (ecNumber (tcAdd x y) (TCNum w))
         (bvAdd w (ecNumber x (TCNum w)) (ecNumber y (TCNum w)));
 -}

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

@@ -1412,7 +1412,7 @@ scCryptolType sc t =
 -- | Deprecated.
 scCryptolEq :: SharedContext -> Term -> Term -> IO Term
 scCryptolEq sc x y =
-  do rules <- concat <$> traverse defRewrites (defs1 ++ defs2)
+  do rules <- concat <$> traverse defRewrites defs
      let ss = addConvs natConversions (addRules rules emptySimpset)
      tx <- scTypeOf sc x >>= rewriteSharedTerm sc ss >>= scCryptolType sc
      ty <- scTypeOf sc y >>= rewriteSharedTerm sc ss >>= scCryptolType sc
@@ -1432,8 +1432,7 @@ scCryptolEq sc x y =
      scGlobalApply sc "Cryptol.ecEq" [k, eqPrf, x, y]
 
   where
-    defs1 = map (mkIdent (mkModuleName ["Prelude"])) ["bitvector"]
-    defs2 = map (mkIdent (mkModuleName ["Cryptol"])) ["seq", "ty"]
+    defs = map (mkIdent (mkModuleName ["Cryptol"])) ["seq", "ty"]
     defRewrites ident =
       do maybe_def <- scFindDef sc ident
          case maybe_def of

saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs

@@ -138,7 +138,7 @@ wordFun f = strictFun (\x -> toWord x >>= f)
 
 ------------------------------------------------------------
 
--- | op :: (n :: Nat) -> bitvector n -> Nat -> bitvector n
+-- | op : (n : Nat) -> Vec n Bool -> Nat -> Vec n Bool
 bvShiftOp :: (LitVector l -> LitVector l -> IO (LitVector l))
           -> (LitVector l -> Natural -> LitVector l)
           -> BValue l
@@ -324,21 +324,21 @@ bitblastLogBase2 g x = do
 -----------------------------------------
 -- Integer/bitvector conversions
 
--- primitive bvToInt :: (n::Nat) -> bitvector n -> Integer;
+-- primitive bvToInt : (n : Nat) -> Vec n Bool -> Integer;
 bvToIntOp :: AIG.IsAIG l g => g s -> BValue (l s)
 bvToIntOp g = constFun $ wordFun $ \v ->
    case AIG.asUnsigned g v of
       Just i -> return $ VInt i
       Nothing -> fail "Cannot convert symbolic bitvector to integer"
 
--- primitive sbvToInt :: (n::Nat) -> bitvector n -> Integer;
+-- primitive sbvToInt : (n : Nat) -> Vec n Bool -> Integer;
 sbvToIntOp :: AIG.IsAIG l g => g s -> BValue (l s)
 sbvToIntOp g = constFun $ wordFun $ \v ->
    case AIG.asSigned g v of
       Just i -> return $ VInt i
       Nothing -> fail "Cannot convert symbolic bitvector to integer"
 
--- primitive intToBv :: (n::Nat) -> Integer -> bitvector n;
+-- primitive intToBv : (n : Nat) -> Integer -> Vec n Bool;
 intToBvOp :: AIG.IsAIG l g => g s -> BValue (l s)
 intToBvOp g =
   Prims.natFun' "intToBv n" $ \n -> return $

saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs

@@ -332,7 +332,7 @@ svSlice i j x = svExtract (w - i - 1) (w - i - j) x
 ----------------------------------------
 -- Shift operations
 
--- | op :: (n :: Nat) -> bitvector n -> Nat -> bitvector n
+-- | op : (n : Nat) -> Vec n Bool -> Nat -> Vec n Bool
 bvShiftOp :: (SWord -> SWord -> SWord) -> (SWord -> Int -> SWord) -> SValue
 bvShiftOp bvOp natOp =
   constFun $
@@ -344,15 +344,15 @@ bvShiftOp bvOp natOp =
       VToNat v -> fmap (vWord . bvOp x) (toWord v)
       _        -> error $ unwords ["Verifier.SAW.Simulator.SBV.bvShiftOp", show y]
 
--- bvShl :: (w :: Nat) -> bitvector w -> Nat -> bitvector w;
+-- bvShl : (w : Nat) -> Vec w Bool -> Nat -> Vec w Bool;
 bvShLOp :: SValue
 bvShLOp = bvShiftOp svShiftLeft svShl
 
--- bvShR :: (w :: Nat) -> bitvector w -> Nat -> bitvector w;
+-- bvShR : (w : Nat) -> Vec w Bool -> Nat -> Vec w Bool;
 bvShROp :: SValue
 bvShROp = bvShiftOp svShiftRight svShr
 
--- bvSShR :: (w :: Nat) -> bitvector w -> Nat -> bitvector w;
+-- bvSShR : (w : Nat) -> Vec w Bool -> Nat -> Vec w Bool;
 bvSShROp :: SValue
 bvSShROp = bvShiftOp bvOp natOp
   where
@@ -382,21 +382,21 @@ natToIntOp =
   Prims.natFun' "natToInt" $ \n -> return $
     VInt (literalSInteger (toInteger n))
 
--- primitive bvToInt :: (n::Nat) -> bitvector n -> Integer;
+-- primitive bvToInt : (n : Nat) -> Vec n Bool -> Integer;
 bvToIntOp :: SValue
 bvToIntOp = constFun $ wordFun $ \v ->
    case svAsInteger v of
       Just i -> return $ VInt (literalSInteger i)
       Nothing -> return $ VInt (svFromIntegral KUnbounded v)
 
--- primitive sbvToInt :: (n::Nat) -> bitvector n -> Integer;
+-- primitive sbvToInt : (n : Nat) -> Vec n Bool -> Integer;
 sbvToIntOp :: SValue
 sbvToIntOp = constFun $ wordFun $ \v ->
    case svAsInteger (svSign v) of
       Just i -> return $ VInt (literalSInteger i)
       Nothing -> return $ VInt (svFromIntegral KUnbounded (svSign v))
 
--- primitive intToBv :: (n::Nat) -> Integer -> bitvector n;
+-- primitive intToBv : (n : Nat) -> Integer -> Vec n Bool;
 intToBvOp :: SValue
 intToBvOp =
   Prims.natFun' "intToBv n" $ \n -> return $

saw-core-what4/src/Verifier/SAW/Simulator/What4.hs

@@ -339,18 +339,18 @@ natToIntOp =
     VInt <$> W.intLit (given :: sym) (toInteger n)
 
 -- interpret bitvector as unsigned integer
--- primitive bvToInt :: (n::Nat) -> bitvector n -> Integer;
+-- primitive bvToInt : (n : Nat) -> Vec n Bool -> Integer;
 bvToIntOp :: forall sym. (Sym sym) => SValue sym
 bvToIntOp = constFun $ wordFun $ \(v :: SWord sym) -> do
   VInt <$> SW.bvToInteger (given :: sym) v
 
 -- interpret bitvector as signed integer
--- primitive sbvToInt :: (n::Nat) -> bitvector n -> Integer;
+-- primitive sbvToInt : (n : Nat) -> Vec n Bool -> Integer;
 sbvToIntOp :: forall sym. (Sym sym) => SValue sym
 sbvToIntOp = constFun $ wordFun $ \v -> do
    VInt <$> SW.sbvToInteger (given :: sym) v
 
--- primitive intToBv :: (n::Nat) -> Integer -> bitvector n;
+-- primitive intToBv : (n : Nat) -> Integer -> Vec n Bool;
 intToBvOp :: forall sym. (Sym sym) => SValue sym
 intToBvOp =
   Prims.natFun' "intToBv n" $ \n -> return $
@@ -393,7 +393,7 @@ liftRotate sym f w i =
   f w =<< SW.bvLit sym (SW.bvWidth w) (i `mod` SW.bvWidth w)
 
 
--- | op :: (n :: Nat) -> bitvector n -> Nat -> bitvector n
+-- | op : (n : Nat) -> Vec n Bool -> Nat -> Vec n Bool
 bvShiftOp :: (Sym sym) =>
              (SWord sym -> SWord sym -> IO (SWord sym)) ->
              (SWord sym -> Integer   -> IO (SWord sym)) -> SValue sym
@@ -408,17 +408,17 @@ bvShiftOp bvOp natOp =
       VToNat v -> VWord <$> (bvOp x =<< toWord v)
       _        -> error $ unwords ["Verifier.SAW.Simulator.What4.bvShiftOp", show y]
 
--- bvShl :: (w :: Nat) -> bitvector w -> Nat -> bitvector w;
+-- bvShl : (w : Nat) -> Vec w Bool -> Nat -> Vec w Bool;
 bvShLOp :: forall sym. (Sym sym) => SValue sym
 bvShLOp = bvShiftOp (SW.bvShl given)
                     (liftShift given (SW.bvShl given))
 
--- bvShR :: (w :: Nat) -> bitvector w -> Nat -> bitvector w;
+-- bvShR : (w : Nat) -> Vec w Bool -> Nat -> Vec w Bool;
 bvShROp :: forall sym. (Sym sym) => SValue sym
 bvShROp = bvShiftOp (SW.bvLshr given)
                     (liftShift given (SW.bvLshr given))
 
--- bvSShR :: (w :: Nat) -> bitvector w -> Nat -> bitvector w;
+-- bvSShR : (w : Nat) -> Vec w Bool -> Nat -> Vec w Bool;
 bvSShROp :: forall sym. (Sym sym) => SValue sym
 bvSShROp = bvShiftOp (SW.bvAshr given)
                      (liftShift given (SW.bvAshr given))