diff --git a/src/Juvix/Compiler/Builtins/Anoma.hs b/src/Juvix/Compiler/Builtins/Anoma.hs index bde6c1666e..2805b8a9be 100644 --- a/src/Juvix/Compiler/Builtins/Anoma.hs +++ b/src/Juvix/Compiler/Builtins/Anoma.hs @@ -71,18 +71,19 @@ registerAnomaSign f = do (error "anomaSign must be of type {A : Type} -> A -> Nat -> Nat") registerBuiltin BuiltinAnomaSign (f ^. axiomName) -registerAnomaVerify :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r () -registerAnomaVerify f = do +registerAnomaVerifyWithMessage :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r () +registerAnomaVerifyWithMessage f = do let ftype = f ^. axiomType u = ExpressionUniverse smallUniverseNoLoc l = getLoc f dataT <- freshVar l "dataT" nat <- getBuiltinName (getLoc f) BuiltinNat + maybe_ <- getBuiltinName (getLoc f) BuiltinMaybe let freeVars = HashSet.fromList [dataT] unless - ((ftype ==% (u <>--> nat --> nat --> dataT)) freeVars) - (error "anomaVerify must be of type {A : Type} -> Nat -> Nat -> A") - registerBuiltin BuiltinAnomaVerify (f ^. axiomName) + ((ftype ==% (u <>--> nat --> nat --> maybe_ @@ dataT)) freeVars) + (error "anomaVerify must be of type {A : Type} -> Nat -> Nat -> Maybe A") + registerBuiltin BuiltinAnomaVerifyWithMessage (f ^. axiomName) registerAnomaSignDetached :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r () registerAnomaSignDetached f = do diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs index 1cc1f24ab6..0d06877769 100644 --- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs +++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs @@ -209,7 +209,7 @@ data BuiltinAxiom | BuiltinAnomaVerifyDetached | BuiltinAnomaSign | BuiltinAnomaSignDetached - | BuiltinAnomaVerify + | BuiltinAnomaVerifyWithMessage | BuiltinPoseidon | BuiltinEcOp | BuiltinRandomEcPoint @@ -246,7 +246,7 @@ instance HasNameKind BuiltinAxiom where BuiltinAnomaVerifyDetached -> KNameFunction BuiltinAnomaSign -> KNameFunction BuiltinAnomaSignDetached -> KNameFunction - BuiltinAnomaVerify -> KNameFunction + BuiltinAnomaVerifyWithMessage -> KNameFunction BuiltinPoseidon -> KNameFunction BuiltinEcOp -> KNameFunction BuiltinRandomEcPoint -> KNameFunction @@ -291,7 +291,7 @@ instance Pretty BuiltinAxiom where BuiltinAnomaVerifyDetached -> Str.anomaVerifyDetached BuiltinAnomaSignDetached -> Str.anomaSignDetached BuiltinAnomaSign -> Str.anomaSign - BuiltinAnomaVerify -> Str.anomaVerify + BuiltinAnomaVerifyWithMessage -> Str.anomaVerifyWithMessage BuiltinPoseidon -> Str.cairoPoseidon BuiltinEcOp -> Str.cairoEcOp BuiltinRandomEcPoint -> Str.cairoRandomEcPoint diff --git a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs index d0c0ceb5b3..26f84b00bf 100644 --- a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs +++ b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs @@ -277,6 +277,17 @@ declareNatBuiltins = do (tagSuc, "suc", \x -> mkPi' x x, Just BuiltinNatSuc) ] +declareMaybeBuiltins :: (Member InfoTableBuilder r) => Sem r () +declareMaybeBuiltins = do + tagNothing <- freshTag + tagJust <- freshTag + declareInductiveBuiltins + "Maybe" + (Just (BuiltinTypeInductive BuiltinMaybe)) + [ (tagNothing, "nothing", id, Just BuiltinMaybeNothing), + (tagJust, "just", mkPi' mkDynamic', Just BuiltinMaybeJust) + ] + reserveLiteralIntToNatSymbol :: (Member InfoTableBuilder r) => Sem r () reserveLiteralIntToNatSymbol = do sym <- freshSymbol diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs index 9aae4d69eb..957860479c 100644 --- a/src/Juvix/Compiler/Core/Evaluator.hs +++ b/src/Juvix/Compiler/Core/Evaluator.hs @@ -64,23 +64,31 @@ instance Show EvalError where instance Exception.Exception EvalError evalInfoTable :: Handle -> InfoTable -> Node -evalInfoTable herr info = eval herr idenCtxt [] mainNode +evalInfoTable herr tab = eval herr tab [] mainNode where - idenCtxt = info ^. identContext - mainSym = fromJust (info ^. infoMain) - mainNode = fromJust (HashMap.lookup mainSym idenCtxt) + mainSym = fromJust (tab ^. infoMain) + mainNode = fromJust (HashMap.lookup mainSym (tab ^. identContext)) -- | `eval ctx env n` evaluates a node `n` whose all free variables point into -- `env`. All nodes in `ctx` must be closed. All nodes in `env` must be values. -- Invariant for values v: eval ctx env v = v -eval :: Handle -> IdentContext -> Env -> Node -> Node +eval :: Handle -> InfoTable -> Env -> Node -> Node eval herr ctx env = geval defaultEvalOptions herr ctx env -geval :: EvalOptions -> Handle -> IdentContext -> Env -> Node -> Node -geval opts herr ctx env0 = eval' env0 +geval :: EvalOptions -> Handle -> InfoTable -> Env -> Node -> Node +geval opts herr tab env0 = eval' env0 where + ctx :: IdentContext + ctx = tab ^. identContext + + evalError' :: Text -> Maybe Node -> a + evalError' msg = Exception.throw . EvalError msg + evalError :: Text -> Node -> a - evalError msg node = Exception.throw (EvalError msg (Just node)) + evalError msg node = evalError' msg (Just node) + + evalErrorMsg' :: Text -> a + evalErrorMsg' msg = evalError' msg Nothing eval' :: Env -> Node -> Node eval' !env !n = case n of @@ -201,7 +209,7 @@ geval opts herr ctx env0 = eval' env0 OpAnomaVerifyDetached -> anomaVerifyDetachedOp OpAnomaSign -> anomaSignOp OpAnomaSignDetached -> anomaSignDetachedOp - OpAnomaVerify -> anomaVerifyOp + OpAnomaVerifyWithMessage -> anomaVerifyWithMessageOp OpPoseidonHash -> poseidonHashOp OpEc -> ecOp OpRandomEcPoint -> randomEcPointOp @@ -406,18 +414,18 @@ geval opts herr ctx env0 = eval' env0 Nothing -> err "anomaSignDetachedOp: second argument not an integer" {-# INLINE anomaSignDetachedOp #-} - anomaVerifyOp :: [Node] -> Node - anomaVerifyOp = checkApply $ \arg1 arg2 -> + anomaVerifyWithMessageOp :: [Node] -> Node + anomaVerifyWithMessageOp = checkApply $ \arg1 arg2 -> let !v1 = eval' env arg1 !v2 = eval' env arg2 in if | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure -> - mkBuiltinApp' OpAnomaVerify [v1, v2] + mkBuiltinApp' OpAnomaVerifyWithMessage [v1, v2] | otherwise -> case (integerFromNode v1, integerFromNode v2) of (Just i1, Just i2) -> verify i1 i2 - _ -> err "anomaVerifyOp: both arguments are not integers" - {-# INLINE anomaVerifyOp #-} + _ -> err "anomaVerifyWithMessageOp: both arguments are not integers" + {-# INLINE anomaVerifyWithMessageOp #-} poseidonHashOp :: [Node] -> Node poseidonHashOp = unary $ \arg -> @@ -482,8 +490,8 @@ geval opts herr ctx env0 = eval' env0 let !signedMessage = decodeByteString signedMessageInt !publicKey = publicKeyFromInteger publicKeyInt in if - | E.verify publicKey signedMessage -> deserializeNode (E.removeSignature signedMessage) - | otherwise -> err "signature verification failed" + | E.verify publicKey signedMessage -> nodeMaybeJust (deserializeNode (E.removeSignature signedMessage)) + | otherwise -> nodeMaybeNothing {-# INLINE verify #-} signDetached :: Node -> Integer -> Node @@ -530,6 +538,26 @@ geval opts herr ctx env0 = eval' env0 | otherwise = TagFalse {-# INLINE nodeFromBool #-} + mkBuiltinConstructor :: BuiltinConstructor -> [Node] -> Maybe Node + mkBuiltinConstructor ctor args = + (\tag -> mkConstr' tag args) + . (^. constructorTag) + <$> lookupTabBuiltinConstructor tab ctor + + nodeMaybeNothing :: Node + nodeMaybeNothing = + fromMaybe + (evalErrorMsg' "builtin Maybe is not available") + (mkBuiltinConstructor BuiltinMaybeNothing []) + {-# INLINE nodeMaybeNothing #-} + + nodeMaybeJust :: Node -> Node + nodeMaybeJust n = + fromMaybe + (evalErrorMsg' "builtin Maybe is not available") + (mkBuiltinConstructor BuiltinMaybeJust [n]) + {-# INLINE nodeMaybeJust #-} + integerFromNode :: Node -> Maybe Integer integerFromNode = \case NCst (Constant _ (ConstInteger int)) -> Just int @@ -613,15 +641,15 @@ geval opts herr ctx env0 = eval' env0 mkCase i sym b (map (substEnvInBranch env) bs) (fmap (substEnv env) def) -- Evaluate `node` and interpret the builtin IO actions. -hEvalIO' :: EvalOptions -> Handle -> Handle -> Handle -> IdentContext -> Env -> Node -> IO Node -hEvalIO' opts herr hin hout ctx env node = - let node' = geval opts herr ctx env node +hEvalIO' :: EvalOptions -> Handle -> Handle -> Handle -> InfoTable -> Env -> Node -> IO Node +hEvalIO' opts herr hin hout tab env node = + let node' = geval opts herr tab env node in case node' of NCtr (Constr _ (BuiltinTag TagReturn) [x]) -> return x NCtr (Constr _ (BuiltinTag TagBind) [x, f]) -> do - x' <- hEvalIO' opts herr hin hout ctx env x - hEvalIO' opts herr hin hout ctx env (mkApp Info.empty f x') + x' <- hEvalIO' opts herr hin hout tab env x + hEvalIO' opts herr hin hout tab env (mkApp Info.empty f x') NCtr (Constr _ (BuiltinTag TagWrite) [NCst (Constant _ (ConstString s))]) -> do hPutStr hout s return unitNode @@ -636,12 +664,6 @@ hEvalIO' opts herr hin hout ctx env node = where unitNode = mkConstr (Info.singleton (NoDisplayInfo ())) (BuiltinTag TagTrue) [] -hEvalIO :: Handle -> Handle -> Handle -> IdentContext -> Env -> Node -> IO Node -hEvalIO = hEvalIO' defaultEvalOptions - -evalIO :: IdentContext -> Env -> Node -> IO Node -evalIO = hEvalIO stderr stdin stdout - doEval :: forall r. (MonadIO (Sem r)) => @@ -652,8 +674,8 @@ doEval :: Node -> Sem r (Either CoreError Node) doEval mfsize noIO loc tab node - | noIO = catchEvalError loc (eval stderr (tab ^. identContext) [] node) - | otherwise = liftIO (catchEvalErrorIO loc (hEvalIO' opts stderr stdin stdout (tab ^. identContext) [] node)) + | noIO = catchEvalError loc (eval stderr tab [] node) + | otherwise = liftIO (catchEvalErrorIO loc (hEvalIO' opts stderr stdin stdout tab [] node)) where opts = maybe diff --git a/src/Juvix/Compiler/Core/Extra/Utils.hs b/src/Juvix/Compiler/Core/Extra/Utils.hs index e45843f2f4..042c354c2a 100644 --- a/src/Juvix/Compiler/Core/Extra/Utils.hs +++ b/src/Juvix/Compiler/Core/Extra/Utils.hs @@ -429,7 +429,7 @@ builtinOpArgTypes = \case OpAnomaVerifyDetached -> [mkDynamic', mkDynamic', mkDynamic'] OpAnomaSign -> [mkDynamic', mkDynamic'] OpAnomaSignDetached -> [mkDynamic', mkDynamic'] - OpAnomaVerify -> [mkDynamic', mkDynamic'] + OpAnomaVerifyWithMessage -> [mkDynamic', mkDynamic'] OpPoseidonHash -> [mkDynamic'] OpEc -> [mkDynamic', mkTypeField', mkDynamic'] OpRandomEcPoint -> [] diff --git a/src/Juvix/Compiler/Core/Keywords.hs b/src/Juvix/Compiler/Core/Keywords.hs index a00bf49a98..a2fb2b5e18 100644 --- a/src/Juvix/Compiler/Core/Keywords.hs +++ b/src/Juvix/Compiler/Core/Keywords.hs @@ -12,8 +12,8 @@ import Juvix.Data.Keyword.All kwAnomaEncode, kwAnomaSign, kwAnomaSignDetached, - kwAnomaVerify, kwAnomaVerifyDetached, + kwAnomaVerifyWithMessage, kwAny, kwAssign, kwBind, diff --git a/src/Juvix/Compiler/Core/Language/Builtins.hs b/src/Juvix/Compiler/Core/Language/Builtins.hs index ba45f8c122..3fd914cb32 100644 --- a/src/Juvix/Compiler/Core/Language/Builtins.hs +++ b/src/Juvix/Compiler/Core/Language/Builtins.hs @@ -32,7 +32,7 @@ data BuiltinOp | OpAnomaVerifyDetached | OpAnomaSign | OpAnomaSignDetached - | OpAnomaVerify + | OpAnomaVerifyWithMessage | OpPoseidonHash | OpEc | OpRandomEcPoint @@ -86,7 +86,7 @@ builtinOpArgsNum = \case OpAnomaVerifyDetached -> 3 OpAnomaSign -> 2 OpAnomaSignDetached -> 2 - OpAnomaVerify -> 2 + OpAnomaVerifyWithMessage -> 2 OpPoseidonHash -> 1 OpEc -> 3 OpRandomEcPoint -> 0 @@ -129,7 +129,7 @@ builtinIsFoldable = \case OpAnomaVerifyDetached -> False OpAnomaSign -> False OpAnomaSignDetached -> False - OpAnomaVerify -> False + OpAnomaVerifyWithMessage -> False OpPoseidonHash -> False OpEc -> False OpRandomEcPoint -> False @@ -153,6 +153,6 @@ builtinsAnoma = OpAnomaDecode, OpAnomaVerifyDetached, OpAnomaSign, - OpAnomaVerify, + OpAnomaVerifyWithMessage, OpAnomaSignDetached ] diff --git a/src/Juvix/Compiler/Core/Normalizer.hs b/src/Juvix/Compiler/Core/Normalizer.hs index d447e6e47c..fde36a3f13 100644 --- a/src/Juvix/Compiler/Core/Normalizer.hs +++ b/src/Juvix/Compiler/Core/Normalizer.hs @@ -29,7 +29,7 @@ normalize fsize md = run . evalInfoTableBuilder md . runReader normEnv . normali _normEnvLevel = 0, _normEnvEvalEnv = [] } - identCtx = computeCombinedIdentContext md + tab = computeCombinedInfoTable md normalize' :: Node -> Norm Node normalize' node0 = do @@ -39,7 +39,7 @@ normalize fsize md = run . evalInfoTableBuilder md . runReader normEnv . normali neval :: Node -> Norm Node neval node = do env <- asks (^. normEnvEvalEnv) - return $ geval opts stdout identCtx env node + return $ geval opts stdout tab env node where opts = defaultEvalOptions diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs index e9ac9824a1..4462952137 100644 --- a/src/Juvix/Compiler/Core/Pretty/Base.hs +++ b/src/Juvix/Compiler/Core/Pretty/Base.hs @@ -58,7 +58,7 @@ instance PrettyCode BuiltinOp where OpAnomaVerifyDetached -> return primAnomaVerifyDetached OpAnomaSign -> return primAnomaSign OpAnomaSignDetached -> return primAnomaSignDetached - OpAnomaVerify -> return primAnomaVerify + OpAnomaVerifyWithMessage -> return primAnomaVerifyWithMessage OpPoseidonHash -> return primPoseidonHash OpEc -> return primEc OpRandomEcPoint -> return primRandomEcPoint @@ -819,8 +819,8 @@ primAnomaSign = primitive Str.anomaSign primAnomaSignDetached :: Doc Ann primAnomaSignDetached = primitive Str.anomaSignDetached -primAnomaVerify :: Doc Ann -primAnomaVerify = primitive Str.anomaVerify +primAnomaVerifyWithMessage :: Doc Ann +primAnomaVerifyWithMessage = primitive Str.anomaVerifyWithMessage primPoseidonHash :: Doc Ann primPoseidonHash = primitive Str.cairoPoseidon diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs index 96f5825608..272dc8e8a2 100644 --- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs +++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs @@ -72,7 +72,7 @@ computeNodeTypeInfo md = umapL go OpAnomaVerifyDetached -> Info.getNodeType node OpAnomaSign -> Info.getNodeType node OpAnomaSignDetached -> Info.getNodeType node - OpAnomaVerify -> Info.getNodeType node + OpAnomaVerifyWithMessage -> Info.getNodeType node OpPoseidonHash -> case _builtinAppArgs of [arg] -> Info.getNodeType arg _ -> error "incorrect poseidon builtin application" diff --git a/src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs b/src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs index 41896cd505..75c9d7d26e 100644 --- a/src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs +++ b/src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs @@ -53,7 +53,7 @@ convertNode opts nonRecSyms tab md = umap go _ -> isType' node doEval' :: Node -> Node - doEval' = removeClosures . geval eopts stderr (tab ^. identContext) [] + doEval' = removeClosures . geval eopts stderr tab [] where eopts = defaultEvalOptions diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index 35a6b8ab40..f900b78c6e 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -591,7 +591,7 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive Internal.BuiltinAnomaVerifyDetached -> return () Internal.BuiltinAnomaSign -> return () Internal.BuiltinAnomaSignDetached -> return () - Internal.BuiltinAnomaVerify -> return () + Internal.BuiltinAnomaVerifyWithMessage -> return () Internal.BuiltinPoseidon -> return () Internal.BuiltinEcOp -> return () Internal.BuiltinRandomEcPoint -> return () @@ -767,7 +767,7 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin) ) ) ) - Internal.BuiltinAnomaVerify -> do + Internal.BuiltinAnomaVerifyWithMessage -> do natType <- getNatType registerAxiomDef ( mkLambda' @@ -776,7 +776,7 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin) natType ( mkLambda' natType - (mkBuiltinApp' OpAnomaVerify [mkVar' 1, mkVar' 0]) + (mkBuiltinApp' OpAnomaVerifyWithMessage [mkVar' 1, mkVar' 0]) ) ) ) @@ -1189,7 +1189,7 @@ goApplication a = do Just Internal.BuiltinAnomaVerifyDetached -> app Just Internal.BuiltinAnomaSign -> app Just Internal.BuiltinAnomaSignDetached -> app - Just Internal.BuiltinAnomaVerify -> app + Just Internal.BuiltinAnomaVerifyWithMessage -> app Just Internal.BuiltinPoseidon -> app Just Internal.BuiltinEcOp -> app Just Internal.BuiltinRandomEcPoint -> app diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs index e8dbdb6cde..1bb09ffd4e 100644 --- a/src/Juvix/Compiler/Core/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs @@ -78,6 +78,7 @@ parseToplevel = do lift declareIOBuiltins lift declareBoolBuiltins lift declareNatBuiltins + lift declareMaybeBuiltins space P.endBy statement (kw delimSemicolon) r <- optional expression @@ -576,7 +577,7 @@ builtinAppExpr varsNum vars = do <|> (kw kwAnomaEncode $> OpAnomaEncode) <|> (kw kwAnomaDecode $> OpAnomaDecode) <|> (kw kwAnomaSign $> OpAnomaSign) - <|> (kw kwAnomaVerify $> OpAnomaVerify) + <|> (kw kwAnomaVerifyWithMessage $> OpAnomaVerifyWithMessage) <|> (kw kwAnomaSignDetached $> OpAnomaSignDetached) <|> (kw kwAnomaVerifyDetached $> OpAnomaVerifyDetached) args <- P.many (atom varsNum vars) diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs index 6fc1dfe593..702edc449b 100644 --- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs +++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs @@ -103,7 +103,7 @@ fromCore fsize tab = BuiltinAnomaVerifyDetached -> False BuiltinAnomaSign -> False BuiltinAnomaSignDetached -> False - BuiltinAnomaVerify -> False + BuiltinAnomaVerifyWithMessage -> False BuiltinPoseidon -> False BuiltinEcOp -> False BuiltinRandomEcPoint -> False diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 62bb69a6e8..685d3bb45f 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -572,7 +572,7 @@ registerBuiltinAxiom d = \case BuiltinAnomaVerifyDetached -> registerAnomaVerifyDetached d BuiltinAnomaSign -> registerAnomaSign d BuiltinAnomaSignDetached -> registerAnomaSignDetached d - BuiltinAnomaVerify -> registerAnomaVerify d + BuiltinAnomaVerifyWithMessage -> registerAnomaVerifyWithMessage d BuiltinPoseidon -> registerPoseidon d BuiltinEcOp -> registerEcOp d BuiltinRandomEcPoint -> registerRandomEcPoint d diff --git a/src/Juvix/Compiler/Nockma/Evaluator.hs b/src/Juvix/Compiler/Nockma/Evaluator.hs index d7efc19727..8ee092432e 100644 --- a/src/Juvix/Compiler/Nockma/Evaluator.hs +++ b/src/Juvix/Compiler/Nockma/Evaluator.hs @@ -294,8 +294,14 @@ evalProfile inistack initerm = pubKey <- PublicKey <$> atomToByteStringLen publicKeyLength pubKeyT signedMessage <- atomToByteString signedMessageT if - | verify pubKey signedMessage -> TermAtom <$> byteStringToAtom (removeSignature signedMessage) - | otherwise -> throwVerificationFailed signedMessageT pubKeyT + | verify pubKey signedMessage -> mkMaybeJust . TermAtom <$> byteStringToAtom (removeSignature signedMessage) + | otherwise -> return mkMaybeNothing + + mkMaybeNothing :: Term a + mkMaybeNothing = TermAtom nockNil + + mkMaybeJust :: Term a -> Term a + mkMaybeJust t = TermCell (Cell (TermAtom nockNil) t) goAutoConsCell :: AutoConsCell a -> Sem r (Term a) goAutoConsCell c = do diff --git a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs index f4a105cfc6..d8431233b3 100644 --- a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs +++ b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs @@ -169,14 +169,19 @@ constructorPath = pathFromEnum stackPath :: AnomaCallablePathId -> Path stackPath s = indexStack (fromIntegral (fromEnum s)) -indexTuple :: Natural -> Natural -> Path -indexTuple len idx - | idx >= len = impossible +data IndexTupleArgs = IndexTupleArgs + { _indexTupleArgsLength :: Natural, + _indexTupleArgsIndex :: Natural + } + +indexTuple :: IndexTupleArgs -> Path +indexTuple IndexTupleArgs {..} + | _indexTupleArgsIndex >= _indexTupleArgsLength = impossible | otherwise = let lastL - | idx == len - 1 = [] + | _indexTupleArgsIndex == _indexTupleArgsLength - 1 = [] | otherwise = [L] - in replicate idx R ++ lastL + in replicate _indexTupleArgsIndex R ++ lastL indexStack :: Natural -> Path indexStack idx = replicate idx R ++ [L] @@ -202,7 +207,14 @@ runCompilerFunction ctx fun = pathToArg :: (Members '[Reader FunctionCtx] r) => Natural -> Sem r Path pathToArg n = do ari <- asks (^. functionCtxArity) - return (stackPath ArgsTuple <> indexTuple ari n) + return + ( stackPath ArgsTuple + <> indexTuple + IndexTupleArgs + { _indexTupleArgsLength = ari, + _indexTupleArgsIndex = n + } + ) termFromParts :: (Bounded p, Enum p) => (p -> Term Natural) -> Term Natural termFromParts f = remakeList [f pi | pi <- allElements] @@ -386,14 +398,31 @@ compile = \case ++ indexStack argIx NockmaMemRepTuple -> fr - ++ indexTuple arity argIx + ++ indexTuple + IndexTupleArgs + { _indexTupleArgsLength = arity, + _indexTupleArgsIndex = argIx + } NockmaMemRepList constr -> case constr of NockmaMemRepListConstrNil -> impossible - NockmaMemRepListConstrCons -> fr ++ indexTuple 2 argIx + NockmaMemRepListConstrCons -> + fr + ++ indexTuple + IndexTupleArgs + { _indexTupleArgsLength = 2, + _indexTupleArgsIndex = argIx + } NockmaMemRepMaybe constr -> case constr of NockmaMemRepMaybeConstrNothing -> impossible - -- just x is represented as [0 x] so argument index is offset by 1. - NockmaMemRepMaybeConstrJust -> fr ++ indexTuple 2 (argIx + 1) + -- just x is represented as [nil x] so argument index is offset by 1. + -- argIx will always be 0 because just has one argument + NockmaMemRepMaybeConstrJust -> + fr + ++ indexTuple + IndexTupleArgs + { _indexTupleArgsLength = 2, + _indexTupleArgsIndex = argIx + 1 + } (opAddress "constrRef") <$> path where goDirectRef :: Tree.DirectRef -> Sem r (Term Natural) @@ -459,7 +488,7 @@ compile = \case Tree.OpAnomaDecode -> return (goAnomaDecode args) Tree.OpAnomaVerifyDetached -> return (goAnomaVerifyDetached args) Tree.OpAnomaSign -> return (goAnomaSign args) - Tree.OpAnomaVerify -> return (goAnomaVerify args) + Tree.OpAnomaVerifyWithMessage -> return (goAnomaVerifyWithMessage args) Tree.OpAnomaSignDetached -> return (goAnomaSignDetached args) goUnop :: Tree.NodeUnop -> Sem r (Term Natural) @@ -506,10 +535,46 @@ compile = \case [message, privKey] -> callStdlib StdlibSignDetached [goAnomaEncode [message], privKey] _ -> impossible - goAnomaVerify :: [Term Natural] -> Term Natural - goAnomaVerify = \case - [signedMessage, pubKey] -> callStdlib StdlibDecode [callStdlib StdlibVerify [signedMessage, pubKey]] + -- Conceptually this function is: + -- anomaDecode <$> verify signedMessage pubKey + -- + -- verify returns a `Maybe Nat` that is `Just msg` if the signedMessage is verified. + goAnomaVerifyWithMessage :: [Term Natural] -> Term Natural + goAnomaVerifyWithMessage = \case + [signedMessage, pubKey] -> + opReplace + "callDecodeFromVerify-args" + (closurePath ArgsTuple) + (callStdlib StdlibVerify [signedMessage, pubKey]) + (opAddress "stack" emptyPath) + >># goDecodeResult _ -> impossible + where + goDecodeResult :: Term Natural + goDecodeResult = branch (OpIsCell # verifyResult) goDecodeResultJust goDecodeResultNothing + + -- just x is represented as [nil x] so the payload of just is always at index 1. + justPayloadPath :: Path + justPayloadPath = + indexTuple + IndexTupleArgs + { _indexTupleArgsLength = 2, + _indexTupleArgsIndex = 1 + } + + goDecodeResultJust :: Term Natural + goDecodeResultJust = + opReplace + "putDecodeResultInJust" + justPayloadPath + (callStdlib StdlibDecode [opAddress "verify-result-just" (closurePath ArgsTuple ++ justPayloadPath)]) + verifyResult + + goDecodeResultNothing :: Term Natural + goDecodeResultNothing = verifyResult + + verifyResult :: Term Natural + verifyResult = opAddress "verify-result" (closurePath ArgsTuple) goTrace :: Term Natural -> Sem r (Term Natural) goTrace arg = do diff --git a/src/Juvix/Compiler/Tree/Keywords.hs b/src/Juvix/Compiler/Tree/Keywords.hs index e0b958c70d..b878fb50c1 100644 --- a/src/Juvix/Compiler/Tree/Keywords.hs +++ b/src/Juvix/Compiler/Tree/Keywords.hs @@ -14,8 +14,8 @@ import Juvix.Data.Keyword.All kwAnomaGet, kwAnomaSign, kwAnomaSignDetached, - kwAnomaVerify, kwAnomaVerifyDetached, + kwAnomaVerifyWithMessage, kwArgsNum, kwAtoi, kwBr, @@ -85,7 +85,7 @@ allKeywords = kwAnomaVerifyDetached, kwAnomaSign, kwAnomaSignDetached, - kwAnomaVerify, + kwAnomaVerifyWithMessage, kwPoseidon, kwEcOp, kwRandomEcPoint diff --git a/src/Juvix/Compiler/Tree/Language/Builtins.hs b/src/Juvix/Compiler/Tree/Language/Builtins.hs index c776ff6f1a..7d99a39839 100644 --- a/src/Juvix/Compiler/Tree/Language/Builtins.hs +++ b/src/Juvix/Compiler/Tree/Language/Builtins.hs @@ -81,7 +81,7 @@ data AnomaOp | -- | Cryptographically sign an Anoma value using a secret key OpAnomaSign | -- | Verify a signature obtained from OpAnomaSign using a public key - OpAnomaVerify + OpAnomaVerifyWithMessage | -- | Produce a cryptographic signature of an Anoma value OpAnomaSignDetached deriving stock (Eq) diff --git a/src/Juvix/Compiler/Tree/Pretty/Base.hs b/src/Juvix/Compiler/Tree/Pretty/Base.hs index 1d18d035d9..aeae737a27 100644 --- a/src/Juvix/Compiler/Tree/Pretty/Base.hs +++ b/src/Juvix/Compiler/Tree/Pretty/Base.hs @@ -253,7 +253,7 @@ instance PrettyCode AnomaOp where OpAnomaDecode -> Str.anomaDecode OpAnomaVerifyDetached -> Str.anomaVerifyDetached OpAnomaSign -> Str.anomaSign - OpAnomaVerify -> Str.anomaVerify + OpAnomaVerifyWithMessage -> Str.anomaVerifyWithMessage OpAnomaSignDetached -> Str.anomaSignDetached instance PrettyCode UnaryOpcode where diff --git a/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs b/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs index 44561e0977..5ddfb1ae13 100644 --- a/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs +++ b/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs @@ -17,7 +17,7 @@ checkNoAnoma = walkT checkNode OpAnomaVerifyDetached -> unsupportedErr "OpAnomaVerifyDetached" OpAnomaSign -> unsupportedErr "OpAnomaSign" OpAnomaSignDetached -> unsupportedErr "OpAnomaSignDetached" - OpAnomaVerify -> unsupportedErr "OpAnomaVerify" + OpAnomaVerifyWithMessage -> unsupportedErr "OpAnomaVerifyWithMessage" where unsupportedErr :: Text -> Sem r () unsupportedErr opName = diff --git a/src/Juvix/Compiler/Tree/Translation/FromCore.hs b/src/Juvix/Compiler/Tree/Translation/FromCore.hs index 894fcc1a56..422ce1ecc7 100644 --- a/src/Juvix/Compiler/Tree/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Tree/Translation/FromCore.hs @@ -319,7 +319,7 @@ genCode infoTable fi = Core.OpAnomaVerifyDetached -> OpAnomaVerifyDetached Core.OpAnomaSign -> OpAnomaSign Core.OpAnomaSignDetached -> OpAnomaSignDetached - Core.OpAnomaVerify -> OpAnomaVerify + Core.OpAnomaVerifyWithMessage -> OpAnomaVerifyWithMessage _ -> impossible getArgsNum :: Symbol -> Int diff --git a/src/Juvix/Compiler/Tree/Translation/FromSource.hs b/src/Juvix/Compiler/Tree/Translation/FromSource.hs index 95b0792c01..77f1d99c15 100644 --- a/src/Juvix/Compiler/Tree/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Tree/Translation/FromSource.hs @@ -129,7 +129,7 @@ parseAnoma = <|> parseAnoma' kwAnomaVerifyDetached OpAnomaVerifyDetached <|> parseAnoma' kwAnomaSign OpAnomaSign <|> parseAnoma' kwAnomaSignDetached OpAnomaSignDetached - <|> parseAnoma' kwAnomaVerify OpAnomaVerify + <|> parseAnoma' kwAnomaVerifyWithMessage OpAnomaVerifyWithMessage parseAnoma' :: (Members '[Reader ParserSig, InfoTableBuilder, State LocalParams] r) => diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs index 0c118377c1..a48048b923 100644 --- a/src/Juvix/Data/Keyword/All.hs +++ b/src/Juvix/Data/Keyword/All.hs @@ -460,8 +460,8 @@ kwAnomaSign = asciiKw Str.anomaSign kwAnomaSignDetached :: Keyword kwAnomaSignDetached = asciiKw Str.anomaSignDetached -kwAnomaVerify :: Keyword -kwAnomaVerify = asciiKw Str.anomaVerify +kwAnomaVerifyWithMessage :: Keyword +kwAnomaVerifyWithMessage = asciiKw Str.anomaVerifyWithMessage delimBraceL :: Keyword delimBraceL = mkDelim Str.braceL diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index aa75d93f11..b401fa80dd 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -350,8 +350,8 @@ anomaSign = "anoma-sign" anomaSignDetached :: (IsString s) => s anomaSignDetached = "anoma-sign-detached" -anomaVerify :: (IsString s) => s -anomaVerify = "anoma-verify" +anomaVerifyWithMessage :: (IsString s) => s +anomaVerifyWithMessage = "anoma-verify-with-message" builtinSeq :: (IsString s) => s builtinSeq = "seq" diff --git a/test/Core/Eval/Base.hs b/test/Core/Eval/Base.hs index e44fe41a48..406665573a 100644 --- a/test/Core/Eval/Base.hs +++ b/test/Core/Eval/Base.hs @@ -190,7 +190,7 @@ doEval' :: Node -> IO (Either CoreError Node) doEval' opts f hout tab node = - catchEvalErrorIO defaultLoc (hEvalIO' opts hout stdin hout (tab ^. identContext) [] node) + catchEvalErrorIO defaultLoc (hEvalIO' opts hout stdin hout tab [] node) where defaultLoc = singletonInterval (mkInitialLoc f) diff --git a/test/Tree/Transformation/CheckNoAnoma.hs b/test/Tree/Transformation/CheckNoAnoma.hs index e36186bb4e..2ba71e259e 100644 --- a/test/Tree/Transformation/CheckNoAnoma.hs +++ b/test/Tree/Transformation/CheckNoAnoma.hs @@ -81,7 +81,7 @@ tests = $(mkRelDir ".") $(mkRelFile "test013.jvt"), Eval.NegTest - "anomaVerify" + "anomaVerifyWithMessage" $(mkRelDir ".") $(mkRelFile "test014.jvt"), Eval.NegTest diff --git a/tests/Anoma/Compilation/positive/test078.juvix b/tests/Anoma/Compilation/positive/test078.juvix index c6ecde6dbb..69f75d56d0 100644 --- a/tests/Anoma/Compilation/positive/test078.juvix +++ b/tests/Anoma/Compilation/positive/test078.juvix @@ -5,8 +5,11 @@ import Stdlib.Prelude open; builtin anoma-sign axiom anomaSign : {A : Type} -> A -> Nat -> Nat; -builtin anoma-verify -axiom anomaVerify : {A : Type} -> Nat -> Nat -> A; +builtin anoma-verify-with-message +axiom anomaVerifyWithMessage : {A : Type} + -> Nat + -> Nat + -> Maybe A; privKey : Nat := 0x3181f891cd2323ffe802dd8f36f7e77cd072e3bd8f49884e8b38a297646351e9015535fa1125ec092c85758756d51bf29eed86a118942135c1657bf4cb5c6fc9; @@ -14,4 +17,6 @@ privKey : Nat := pubKey : Nat := 0x3181f891cd2323ffe802dd8f36f7e77cd072e3bd8f49884e8b38a297646351e9; -main (input : List Nat) : List Nat := anomaVerify (anomaSign input privKey) pubKey; +main (input : List Nat) : List Nat := + fromMaybe [] + <| anomaVerifyWithMessage (anomaSign input privKey) pubKey; diff --git a/tests/Core/positive/out/test062.out b/tests/Core/positive/out/test062.out index e538220165..6f33fe1802 100644 --- a/tests/Core/positive/out/test062.out +++ b/tests/Core/positive/out/test062.out @@ -2,4 +2,5 @@ true true true true +true false diff --git a/tests/Core/positive/test062.jvc b/tests/Core/positive/test062.jvc index e474c4b555..1e1a9175e2 100644 --- a/tests/Core/positive/test062.jvc +++ b/tests/Core/positive/test062.jvc @@ -25,6 +25,7 @@ def projectClosure := \t match t with { writeLn (anoma-decode (anoma-encode v1) = v1) >> writeLn (projectClosure (anoma-decode (anoma-encode v3)) 10 = 20) ->> writeLn (anoma-verify (anoma-sign v1 privKey) pubKey = v1) +>> writeLn (anoma-verify-with-message (anoma-sign v1 privKey) pubKey = just v1) +>> writeLn (anoma-verify-with-message (anoma-sign v1 privKey) privKey = nothing) >> writeLn (anoma-verify-detached (anoma-sign-detached v1 privKey) v1 pubKey) >> writeLn (anoma-verify-detached (anoma-sign-detached v1 privKey) v2 pubKey) diff --git a/tests/Tree/negative/test014.jvt b/tests/Tree/negative/test014.jvt index b11fffaba1..a896bb6e8e 100644 --- a/tests/Tree/negative/test014.jvt +++ b/tests/Tree/negative/test014.jvt @@ -1,5 +1,5 @@ -- calling unsupported anoma-verify function main() : * { - anoma-verify(1,2) + anoma-verify-with-message(1,2) }