Adapt builtins to have a clearer juvix-anoma-stdlib API

[heueristik]

Problem

Libsodium / enacl creates some confusion with its sign_open/2 function verifying a SignedMessage and returning the original Message on successful verification instead of a bool. This is a bit odd, and we would like to not return the message to have a clearer API in the juvix-anoma-stdlib.

This is the current API

axiom anomaSignDetached : {Message : Type} -> Message -> PrivateKey -> Signature;
axiom anomaSign : {Message : Type} -> Message -> PrivateKey -> SignedMessage;

axiom anomaVerifyDetached : {Message : Type} -> Signature -> Message -> PublicKey -> Bool;
axiom anomaVerify : {Message : Type} -> SignedMessage -> PublicKey -> Message; -- 👈 NOTE: This is confusing.

Solution

Instead, we would like to have:

axiom anomaSignDetached : {Message : Type} -> Message -> PrivateKey -> Signature;
axiom anomaSign : {Message : Type} -> Message -> PrivateKey -> SignedMessage;

axiom anomaVerifyDetached : {Message : Type} -> Signature -> Message -> PublicKey -> Bool;
axiom anomaVerify : SignedMessage -> PublicKey -> Bool; -- 👈 NOTE: This has changed and is clearer now.

axiom anomaVerifyWithMessage {Message : Type} : -> SignedMessage -> PublicKey -> Maybe Message; -- 👈 NOTE: This is new.

Accordingly, the definitions of the compiler Builtins.hs have to be changed.

Note

This depends also on issue https://github.com/anoma/anoma/issues/569 to change the verify implementation to return a Maybe instead of crashing on failure.