Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for arrayCopy, arraySet, and arrayRangeEqual primitives #1428

Merged
merged 5 commits into from
Aug 27, 2021
Merged

Add support for arrayCopy, arraySet, and arrayRangeEqual primitives #1428

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
858afd6
Add support for arrayCopy, arraySet, and arrayRangeEqual primitives.
andreistefanescu Jul 7, 2021
ecebbe2
Merge branch 'master' of github.com:GaloisInc/saw-script into array-c…
andreistefanescu Aug 25, 2021
0daf9c7
Merge branch 'master' of github.com:GaloisInc/saw-script into array-c…
andreistefanescu Aug 26, 2021
484e439
Add comments.
andreistefanescu Aug 26, 2021
ac5c38e
Bump submodules.
andreistefanescu Aug 26, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions cryptol-saw-core/saw/Cryptol.sawcore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1741,6 +1741,15 @@ ecArrayLookup = arrayLookup;
ecArrayUpdate : (a b : sort 0) -> (Array a b) -> a -> b -> (Array a b);
ecArrayUpdate = arrayUpdate;

ecArrayCopy : (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Array (seq n Bool) a;
ecArrayCopy = finNumRec (\(n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Array (seq n Bool) a) arrayCopy;

ecArraySet : (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> a -> seq n Bool -> Array (seq n Bool) a;
ecArraySet = finNumRec (\(n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> a -> seq n Bool -> Array (seq n Bool) a) arraySet;

ecArrayRangeEq : (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Bool;
ecArrayRangeEq = finNumRec (\(n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Bool) arrayRangeEq;

--------------------------------------------------------------------------------
-- Suite-B Primitives

Expand Down
3 changes: 3 additions & 0 deletions cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -809,6 +809,9 @@ arrayPrims =
[ ("arrayConstant", flip scGlobalDef "Cryptol.ecArrayConstant") -- {a,b} b -> Array a b
, ("arrayLookup", flip scGlobalDef "Cryptol.ecArrayLookup") -- {a,b} Array a b -> a -> b
, ("arrayUpdate", flip scGlobalDef "Cryptol.ecArrayUpdate") -- {a,b} Array a b -> a -> b -> Array a b
, ("arrayCopy", flip scGlobalDef "Cryptol.ecArrayCopy") -- {n,a} Array [n] a -> [n] -> Array [n] a -> [n] -> [n] -> Array [n] a
, ("arraySet", flip scGlobalDef "Cryptol.ecArraySet") -- {n,a} Array [n] a -> [n] -> a -> [n] -> Array [n] a
, ("arrayRangeEqual", flip scGlobalDef "Cryptol.ecArrayRangeEq") -- {n,a} Array [n] a -> [n] -> Array [n] a -> [n] -> [n] -> Bit
]

floatPrims :: Map C.PrimIdent (SharedContext -> IO Term)
Expand Down
4 changes: 4 additions & 0 deletions saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -184,6 +184,7 @@ prims be =
, Prims.bpMuxBool = \b x y -> AIG.lazyMux be b (pure x) (pure y)
, Prims.bpMuxWord = \b x y -> AIG.iteM be b (pure x) (pure y)
, Prims.bpMuxInt = muxInt
, Prims.bpMuxArray = unsupportedAIGPrimitive "bpMuxArray"
, Prims.bpMuxExtra = muxBExtra be
-- Booleans
, Prims.bpTrue = AIG.trueLit be
Expand Down Expand Up @@ -252,6 +253,9 @@ prims be =
, Prims.bpArrayLookup = unsupportedAIGPrimitive "bpArrayLookup"
, Prims.bpArrayUpdate = unsupportedAIGPrimitive "bpArrayUpdate"
, Prims.bpArrayEq = unsupportedAIGPrimitive "bpArrayEq"
, Prims.bpArrayCopy = unsupportedAIGPrimitive "bpArrayCopy"
, Prims.bpArraySet = unsupportedAIGPrimitive "bpArraySet"
, Prims.bpArrayRangeEq = unsupportedAIGPrimitive "bpArrayRangeEq"
}

unsupportedAIGPrimitive :: String -> a
Expand Down
4 changes: 4 additions & 0 deletions saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -118,6 +118,7 @@ prims =
, Prims.bpMuxBool = pure3 svIte
, Prims.bpMuxWord = pure3 svIte
, Prims.bpMuxInt = pure3 svIte
, Prims.bpMuxArray = unsupportedSBVPrimitive "bpMuxArray"
, Prims.bpMuxExtra = muxSbvExtra
-- Booleans
, Prims.bpTrue = svTrue
Expand Down Expand Up @@ -184,6 +185,9 @@ prims =
, Prims.bpArrayLookup = unsupportedSBVPrimitive "bpArrayLookup"
, Prims.bpArrayUpdate = unsupportedSBVPrimitive "bpArrayUpdate"
, Prims.bpArrayEq = unsupportedSBVPrimitive "bpArrayEq"
, Prims.bpArrayCopy = unsupportedSBVPrimitive "bpArrayCopy"
, Prims.bpArraySet = unsupportedSBVPrimitive "bpArraySet"
, Prims.bpArrayRangeEq = unsupportedSBVPrimitive "bpArrayRangeEq"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This PR wouldn't be the place to implement it, probably, but doesn't the SBV library have support for SMT arrays? Is there anything stopping us from supporting them?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As I recall, the "dynamic" SBV interface we use doesn't expose that functionality. I should double check to be sure, but I think that's why we don't support arrays or uninterpreted functions via Cryptol or SAW. It's one of the reasons I want to find a way to use the standard interface instead.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't remember exactly why I didn't implement array support in the SBV backend in the first place. I am not that familiar with SBV, if it's not that complicated we could add support in the future

}

unsupportedSBVPrimitive :: String -> a
Expand Down
92 changes: 92 additions & 0 deletions saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -175,6 +175,7 @@ prims sym =
, Prims.bpMuxBool = W.itePred sym
, Prims.bpMuxWord = SW.bvIte sym
, Prims.bpMuxInt = W.intIte sym
, Prims.bpMuxArray = arrayIte sym
, Prims.bpMuxExtra = muxWhat4Extra sym
-- Booleans
, Prims.bpTrue = W.truePred sym
Expand Down Expand Up @@ -241,6 +242,9 @@ prims sym =
, Prims.bpArrayLookup = arrayLookup sym
, Prims.bpArrayUpdate = arrayUpdate sym
, Prims.bpArrayEq = arrayEq sym
, Prims.bpArrayCopy = arrayCopy sym
, Prims.bpArraySet = arraySet sym
, Prims.bpArrayRangeEq = arrayRangeEq sym
}


Expand Down Expand Up @@ -647,6 +651,75 @@ arrayUpdate sym arr idx elm
| otherwise =
panic "Verifier.SAW.Simulator.What4.Panic.arrayUpdate" ["argument type mismatch"]

arrayCopy ::
W.IsSymExprBuilder sym =>
sym ->
SArray sym ->
SWord sym ->
SArray sym ->
SWord sym ->
SWord sym ->
IO (SArray sym)
arrayCopy sym dest_arr dest_idx src_arr src_idx len
| SArray dest_arr_expr <- dest_arr
, DBV dest_idx_expr <- dest_idx
, SArray src_arr_expr <- src_arr
, DBV src_idx_expr <- src_idx
, DBV len_expr <- len
, W.BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) _ <- W.exprType dest_arr_expr
, Just Refl <- testEquality (W.exprType dest_arr_expr) (W.exprType src_arr_expr)
, Just Refl <- testEquality idx_repr (W.exprType dest_idx_expr)
, Just Refl <- testEquality idx_repr (W.exprType src_idx_expr)
, Just Refl <- testEquality idx_repr (W.exprType len_expr) =
SArray <$> W.arrayCopy sym dest_arr_expr dest_idx_expr src_arr_expr src_idx_expr len_expr
| otherwise =
panic "Verifier.SAW.Simulator.What4.Panic.arrayCopy" ["argument type mismatch"]

arraySet ::
W.IsSymExprBuilder sym =>
sym ->
SArray sym ->
SWord sym ->
SValue sym ->
SWord sym ->
IO (SArray sym)
arraySet sym arr idx elm len
| SArray arr_expr <- arr
, DBV idx_expr <- idx
, Just (Some elm_expr) <- valueToSymExpr elm
, DBV len_expr <- len
, W.BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr <- W.exprType arr_expr
, Just Refl <- testEquality idx_repr (W.exprType idx_expr)
, Just Refl <- testEquality idx_repr (W.exprType len_expr)
, Just Refl <- testEquality elm_repr (W.exprType elm_expr) =
SArray <$> W.arraySet sym arr_expr idx_expr elm_expr len_expr
| otherwise =
panic "Verifier.SAW.Simulator.What4.Panic.arraySet" ["argument type mismatch"]

arrayRangeEq ::
W.IsSymExprBuilder sym =>
sym ->
SArray sym ->
SWord sym ->
SArray sym ->
SWord sym ->
SWord sym ->
IO (SBool sym)
arrayRangeEq sym x_arr x_idx y_arr y_idx len
| SArray x_arr_expr <- x_arr
, DBV x_idx_expr <- x_idx
, SArray y_arr_expr <- y_arr
, DBV y_idx_expr <- y_idx
, DBV len_expr <- len
, W.BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) _ <- W.exprType x_arr_expr
, Just Refl <- testEquality (W.exprType x_arr_expr) (W.exprType y_arr_expr)
, Just Refl <- testEquality idx_repr (W.exprType x_idx_expr)
, Just Refl <- testEquality idx_repr (W.exprType y_idx_expr)
, Just Refl <- testEquality idx_repr (W.exprType len_expr) =
W.arrayRangeEq sym x_arr_expr x_idx_expr y_arr_expr y_idx_expr len_expr
| otherwise =
panic "Verifier.SAW.Simulator.What4.Panic.arrayRangeEq" ["argument type mismatch"]

arrayEq ::
W.IsSymExprBuilder sym =>
sym ->
Expand All @@ -664,6 +737,24 @@ arrayEq sym lhs_arr rhs_arr
| otherwise =
panic "Verifier.SAW.Simulator.What4.Panic.arrayEq" ["argument type mismatch"]

arrayIte ::
W.IsSymExprBuilder sym =>
sym ->
W.Pred sym ->
SArray sym ->
SArray sym ->
IO (SArray sym)
arrayIte sym cond lhs_arr rhs_arr
| SArray lhs_arr_expr <- lhs_arr
, SArray rhs_arr_expr <- rhs_arr
, W.BaseArrayRepr (Ctx.Empty Ctx.:> lhs_idx_repr) lhs_elm_repr <- W.exprType lhs_arr_expr
, W.BaseArrayRepr (Ctx.Empty Ctx.:> rhs_idx_repr) rhs_elm_repr <- W.exprType rhs_arr_expr
, Just Refl <- testEquality lhs_idx_repr rhs_idx_repr
, Just Refl <- testEquality lhs_elm_repr rhs_elm_repr =
SArray <$> W.arrayIte sym cond lhs_arr_expr rhs_arr_expr
| otherwise =
panic "Verifier.SAW.Simulator.What4.Panic.arrayIte" ["argument type mismatch"]

----------------------------------------------------------------------
-- | A basic symbolic simulator/evaluator: interprets a saw-core Term as
-- a symbolic value
Expand Down Expand Up @@ -1391,6 +1482,7 @@ mkArgTerm sc ty val =
(VIntType, VInt _) -> return ArgTermVar
(_, VWord ZBV) -> return ArgTermBVZero -- 0-width bitvector is a constant
(_, VWord (DBV _)) -> return ArgTermVar
(_, VArray{}) -> return ArgTermVar
(VUnitType, VUnit) -> return ArgTermUnit
(VIntModType n, VIntMod _ _) -> pure (ArgTermToIntMod n ArgTermVar)

Expand Down
38 changes: 38 additions & 0 deletions saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -367,6 +367,15 @@ scEq sym sc tp x y =
BaseBoolRepr -> scBoolEq sc x y
BaseRealRepr -> scRealEq sym sc x y
BaseIntegerRepr -> scIntEq sc x y
BaseArrayRepr idxTypes range
| Ctx.Empty Ctx.:> idx_type <- idxTypes ->
do let SAWExpr x' = x
let SAWExpr y' = y
sc_idx_type <- baseSCType sym sc idx_type
sc_elm_type <- baseSCType sym sc range
SAWExpr <$> SC.scArrayEq sc sc_idx_type sc_elm_type x' y'
| otherwise ->
unsupported sym ("SAW backend: equality comparison on unsupported multidimensional array type:" ++ show tp)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is the reason not to support multi-dimensional arrays here that it would be extra work, in this function, that we don't need right now? Or are there limitations elsewhere in the codebase that would make it hard to support them?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

we don't support multi-dimensional arrays in cryptol or saw-core, and we don't need them at the moment. Adding representation for multi-dimensional arrays in cryptol and saw-core, and translations for all the round-tripping would add a lot of complexity, and I wanted to keep things simple

BaseBVRepr w ->
do let SAWExpr x' = x
let SAWExpr y' = y
Expand Down Expand Up @@ -797,6 +806,35 @@ evaluateExpr sym st sc cache = f []
SAWExpr <$> SC.scArrayUpdate sc sc_idx_type sc_elm_type sc_arr sc_idx sc_elm
| otherwise -> unimplemented "multidimensional UpdateArray"

B.CopyArray w a_repr dest_arr dest_idx src_arr src_idx len _dest_end_idx _src_end_idx ->
do sc_w <- SC.scNat sc (natValue w)
sc_a <- baseSCType sym sc a_repr
sc_dest_arr <- f env dest_arr
sc_dest_idx <- f env dest_idx
sc_src_arr <- f env src_arr
sc_src_idx <- f env src_idx
sc_len <- f env len
SAWExpr <$> SC.scArrayCopy sc sc_w sc_a sc_dest_arr sc_dest_idx sc_src_arr sc_src_idx sc_len

B.SetArray w a_repr arr idx val len _end_idx ->
do sc_w <- SC.scNat sc (natValue w)
sc_a <- baseSCType sym sc a_repr
sc_arr <- f env arr
sc_idx <- f env idx
sc_val <- f env val
sc_len <- f env len
SAWExpr <$> SC.scArraySet sc sc_w sc_a sc_arr sc_idx sc_val sc_len

B.EqualArrayRange w a_repr x_arr x_idx y_arr y_idx len _x_end_idx _y_end_idx ->
do sc_w <- SC.scNat sc (natValue w)
sc_a <- baseSCType sym sc a_repr
sc_x_arr <- f env x_arr
sc_x_idx <- f env x_idx
sc_y_arr <- f env y_arr
sc_y_idx <- f env y_idx
sc_len <- f env len
SAWExpr <$> SC.scArrayRangeEq sc sc_w sc_a sc_x_arr sc_x_idx sc_y_arr sc_y_idx sc_len

B.IntDiv x y ->
do x' <- f env x
y' <- f env y
Expand Down
3 changes: 3 additions & 0 deletions saw-core/prelude/Prelude.sawcore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2241,6 +2241,9 @@ primitive Array : sort 0 -> sort 0 -> sort 0;
primitive arrayConstant : (a b : sort 0) -> b -> (Array a b);
primitive arrayLookup : (a b : sort 0) -> (Array a b) -> a -> b;
primitive arrayUpdate : (a b : sort 0) -> (Array a b) -> a -> b -> (Array a b);
primitive arrayCopy : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> Array (Vec n Bool) a -> Vec n Bool -> Vec n Bool -> Array (Vec n Bool) a;
primitive arraySet : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> a -> Vec n Bool -> Array (Vec n Bool) a;
primitive arrayRangeEq : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> Array (Vec n Bool) a -> Vec n Bool -> Vec n Bool -> Bool;
primitive arrayEq : (a b : sort 0) -> (Array a b) -> (Array a b) -> Bool;

--------------------------------------------------------------------------------
Expand Down
5 changes: 5 additions & 0 deletions saw-core/src/Verifier/SAW/Rewriter.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -290,6 +290,9 @@ boolEqIdent = mkIdent (mkModuleName ["Prelude"]) "boolEq"
vecEqIdent :: Ident
vecEqIdent = mkIdent (mkModuleName ["Prelude"]) "vecEq"

arrayEqIdent :: Ident
arrayEqIdent = mkIdent (mkModuleName ["Prelude"]) "arrayEq"

equalNatIdent :: Ident
equalNatIdent = mkIdent (mkModuleName ["Prelude"]) "equalNat"

Expand Down Expand Up @@ -345,6 +348,8 @@ ruleOfProp (R.asApplyAll -> (R.isGlobalDef boolEqIdent -> Just (), [x, y])) ann
Just $ mkRewriteRule [] x y ann
ruleOfProp (R.asApplyAll -> (R.isGlobalDef vecEqIdent -> Just (), [_, _, _, x, y])) ann =
Just $ mkRewriteRule [] x y ann
ruleOfProp (R.asApplyAll -> (R.isGlobalDef arrayEqIdent -> Just (), [_, _, x, y])) ann =
Just $ mkRewriteRule [] x y ann
ruleOfProp (unwrapTermF -> Constant _ body) ann = ruleOfProp body ann
ruleOfProp (R.asEq -> Just (_, x, y)) ann =
Just $ mkRewriteRule [] x y ann
Expand Down
17 changes: 16 additions & 1 deletion saw-core/src/Verifier/SAW/SharedTerm.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -231,6 +231,9 @@ module Verifier.SAW.SharedTerm
, scArrayLookup
, scArrayUpdate
, scArrayEq
, scArrayCopy
, scArraySet
, scArrayRangeEq
-- ** Utilities
-- , scTrue
-- , scFalse
Expand Down Expand Up @@ -2230,7 +2233,7 @@ scArrayConstant sc a b e = scGlobalApply sc "Prelude.arrayConstant" [a, b, e]
scArrayLookup :: SharedContext -> Term -> Term -> Term -> Term -> IO Term
scArrayLookup sc a b f i = scGlobalApply sc "Prelude.arrayLookup" [a, b, f, i]

-- Create a term computing an array updated at a particular index.
-- | Create a term computing an array updated at a particular index.
--
-- > arrayUpdate : (a b : sort 0) -> (Array a b) -> a -> b -> (Array a b);
scArrayUpdate :: SharedContext -> Term -> Term -> Term -> Term -> Term -> IO Term
Expand All @@ -2242,6 +2245,18 @@ scArrayUpdate sc a b f i e = scGlobalApply sc "Prelude.arrayUpdate" [a, b, f, i,
scArrayEq :: SharedContext -> Term -> Term -> Term -> Term -> IO Term
scArrayEq sc a b x y = scGlobalApply sc "Prelude.arrayEq" [a, b, x, y]

-- > arrayCopy : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> Array (Vec n Bool) a -> Vec n Bool -> Vec n Bool -> Array (Vec n Bool) a;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's list the names of the arguments for these. There are a lot of them, and it's easy to swap around src/dest, etc.

scArrayCopy :: SharedContext -> Term -> Term -> Term -> Term -> Term -> Term -> Term -> IO Term
scArrayCopy sc n a f i g j l = scGlobalApply sc "Prelude.arrayCopy" [n, a, f, i, g, j, l]

-- > arraySet : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> a -> Vec n Bool -> Array (Vec n Bool) a;
scArraySet :: SharedContext -> Term -> Term -> Term -> Term -> Term -> Term -> IO Term
scArraySet sc n a f i e l = scGlobalApply sc "Prelude.arraySet" [n, a, f, i, e, l]

-- > arrayRangeEq : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> Array (Vec n Bool) a -> Vec n Bool -> Vec n Bool -> Bool;
scArrayRangeEq :: SharedContext -> Term -> Term -> Term -> Term -> Term -> Term -> Term -> IO Term
scArrayRangeEq sc n a f i g j l = scGlobalApply sc "Prelude.arrayRangeEq" [n, a, f, i, g, j, l]

------------------------------------------------------------
-- | The default instance of the SharedContext operations.
mkSharedContext :: IO SharedContext
Expand Down
4 changes: 4 additions & 0 deletions saw-core/src/Verifier/SAW/Simulator/Concrete.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -145,6 +145,7 @@ prims =
, Prims.bpMuxBool = pure3 ite
, Prims.bpMuxWord = pure3 ite
, Prims.bpMuxInt = pure3 ite
, Prims.bpMuxArray = unsupportedConcretePrimitive "bpMuxArray"
, Prims.bpMuxExtra = \_tp -> pure3 ite
-- Booleans
, Prims.bpTrue = True
Expand Down Expand Up @@ -213,6 +214,9 @@ prims =
, Prims.bpArrayLookup = unsupportedConcretePrimitive "bpArrayLookup"
, Prims.bpArrayUpdate = unsupportedConcretePrimitive "bpArrayUpdate"
, Prims.bpArrayEq = unsupportedConcretePrimitive "bpArrayEq"
, Prims.bpArrayCopy = unsupportedConcretePrimitive "bpArrayCopy"
, Prims.bpArraySet = unsupportedConcretePrimitive "bpArraySet"
, Prims.bpArrayRangeEq = unsupportedConcretePrimitive "bpArrayRangeEq"
}

unsupportedConcretePrimitive :: String -> a
Expand Down
Loading