anoma / juvix

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

Support Anoma stdlib sign-detached API #2798

Closed paulcadman closed 4 weeks ago

paulcadman commented 4 weeks ago

This PR adds support for the Anoma stdlib sign-detached API.

builtin anoma-sign-detached
axiom anomaSignDetached : {A : Type}
  -- message to sign
  -> A
  -- private key
  -> Nat
 -- signature
  -> Nat;

This corresponds to the sign_detached libsodium API.

This is requried to support to new Anoma nullifier format:

https://github.com/anoma/anoma/commit/d6a61451ae8fd0f046c083f5ca4a4f38e7ecffb1

Previously resource nullifiers were defined using anomaSign:

nullifier (r : Resource) (secretKey : Nat) : Nat :=
  anomaSign (anomaEncode (nullifierHeader, r)) secretKey;

They are now defined using anomaSignDetached:

nullifier (r : Resource) (secretKey : Nat) : Nat :=
  let encodedResource : Nat := anomaEncode (nullifierHeader, r) in
  anomaEncode (encodedResource , anomaSignDetached encodedResource secretKey);

This is so that a logic function can access the nullified resources directly from the nullifier field.

Evaluator Note

When decoding a public key, private key or signature from an integer atom to a bytestring it's important to pad the bytestring to the appropriate number of bytes. For example a private key must be 64 bytes but the corresponding encoded integer may fit into 63 bytes or fewer bytes (depending on leading zeros). This PR also fixes this issue by adding a atomToByteStringLen function with also accepts the expected size of the resulting bytestring.