anoma / juvix

A language for intent-centric and declarative decentralised applications
https://docs.juvix.org
GNU General Public License v3.0
449 stars 54 forks source link

Support Anoma stdlib APIs `sign` and `verify` #2788

Closed paulcadman closed 4 months ago

paulcadman commented 4 months ago

This PR adds support for the Anoma stdlib sign and verify APIs.

builtin anoma-sign
axiom anomaSign : {A : Type}
  -- message to sign
  -> A
  -- secret key
  -> Nat
  -- signed message
  -> Nat;

builtin anoma-verify
axiom anomaVerify : {A : Type}
  -- signed message to verify 
  -> Nat 
  -- public key
  -> Nat 
  -- message with signature removed
  -> A;

These correspond to the sign and sign_open APIs from libsodium respectively.

If signature verification fails in anomaVerify, the Anoma program exits. We copy this behaviour in the evaluator by throwing an error in this case.

Notes

The Haskell Ed25519 library does not support sign_open. Its verification function returns Bool, i.e it checks that the signature is valid. The signed message is simply the concatenation of the signature (64 bytes) and the original message so I added a function to remove the signature from a signed message.