Skip to content

Commit

Permalink
Update to support Juvix 0.6.5 and new Anoma builtins (#16)
Browse files Browse the repository at this point in the history
  • Loading branch information
paulcadman authored Aug 15, 2024
1 parent 897928f commit 80bc788
Show file tree
Hide file tree
Showing 12 changed files with 159 additions and 51 deletions.
8 changes: 8 additions & 0 deletions Anoma/Data/Byte.juvix
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
module Anoma.Data.Byte;

import Stdlib.Prelude open;
import Stdlib.Data.Byte open;

{-# specialize: true, inline: case #-}
instance
ordByteI : Ord Byte := mkOrd (Ord.cmp on Byte.toNat);
12 changes: 12 additions & 0 deletions Anoma/Data/ByteArray.juvix
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
module Anoma.Data.ByteArray;

import Stdlib.Prelude open;

builtin bytearray
axiom ByteArray : Type;

builtin bytearray-from-list-byte
axiom mk : List Byte -> ByteArray;

builtin bytearray-length
axiom length : ByteArray -> Nat;
10 changes: 6 additions & 4 deletions Anoma/System.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,8 @@ anomaSign
-> PrivateKey
-- | The resulting signed message.
-> SignedMessage
| message (PrivateKey.mk privKey) := Builtin.anomaSign message privKey |> SignedMessage.mk;
| message (PrivateKey.mk privKey) :=
Builtin.anomaSign message (ByteArray.mk privKey) |> SignedMessage.mk;

--- Signs a message with a private key and returns the signature.
{-# inline: true #-}
Expand All @@ -30,7 +31,8 @@ anomaSignDetached
-> PrivateKey
-- The resulting signature
-> Signature
| message (PrivateKey.mk privKey) := Builtin.anomaSignDetached message privKey |> Signature.mk;
| message (PrivateKey.mk privKey) :=
Builtin.anomaSignDetached message (ByteArray.mk privKey) |> Signature.mk;

--- Verifies a signed message against a public key.
---
Expand All @@ -57,7 +59,7 @@ anomaVerifyDetached
-- | The verification result.
-> Bool
| (Signature.mk signature) message (PublicKey.mk pubKey) :=
Builtin.anomaVerifyDetached signature message pubKey;
Builtin.anomaVerifyDetached signature message (ByteArray.mk pubKey);

--- Verifies a signature against a message and public key and return the message on success.
{-# inline: true #-}
Expand All @@ -70,4 +72,4 @@ anomaVerifyWithMessage
-- | The original message.
-> Maybe Message
| (SignedMessage.mk signedMessage) (PublicKey.mk pubKey) :=
Builtin.anomaVerifyWithMessage signedMessage pubKey;
Builtin.anomaVerifyWithMessage signedMessage (ByteArray.mk pubKey);
9 changes: 5 additions & 4 deletions Anoma/System/Builtin.juvix
Original file line number Diff line number Diff line change
@@ -1,13 +1,14 @@
module Anoma.System.Builtin;

import Anoma.Data.ByteArray open;
import Anoma.Data.Maybe open;
import Stdlib.Prelude open;

syntax alias PublicKey := Nat;
syntax alias PrivateKey := Nat;
syntax alias PublicKey := ByteArray;
syntax alias PrivateKey := ByteArray;

syntax alias Signature := Nat;
syntax alias SignedMessage := Nat;
syntax alias Signature := ByteArray;
syntax alias SignedMessage := ByteArray;

--- Retrieves a value by key from Anoma's key-value store.
builtin anoma-get
Expand Down
31 changes: 7 additions & 24 deletions Anoma/Types.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,9 @@
module Anoma.Types;

import Stdlib.Prelude open;
import Anoma.Data.ByteArray open using {ByteArray} public;
import Anoma.Data.ByteArray as ByteArray public;
import Anoma.Data.Byte;

import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};

Expand Down Expand Up @@ -34,7 +37,7 @@ open Kind using {Kind} public;

module PublicKey;

type PublicKey := mk {unPublicKey : Nat};
type PublicKey := mk {unPublicKey : List Byte};

open PublicKey public;
end;
Expand All @@ -43,7 +46,7 @@ open PublicKey using {PublicKey} public;

module PrivateKey;

type PrivateKey := mk {unPrivateKey : Nat};
type PrivateKey := mk {unPrivateKey : List Byte};

open PrivateKey public;
end;
Expand All @@ -52,7 +55,7 @@ open PrivateKey using {PrivateKey} public;

module Signature;

type Signature := mk {unSignature : Nat};
type Signature := mk {unSignature : ByteArray};

open Signature public;
end;
Expand All @@ -61,7 +64,7 @@ open Signature using {Signature} public;

module SignedMessage;

type SignedMessage := mk {unSignedMessage : Nat};
type SignedMessage := mk {unSignedMessage : ByteArray};

open SignedMessage public;
end;
Expand Down Expand Up @@ -133,26 +136,6 @@ PrivateKeyOrd : Ord PrivateKey :=
instance
PrivateKeyEq : Eq PrivateKey := fromOrdToEq;

instance
SignatureOrd : Ord Signature :=
mkOrd@{
cmp : Signature -> Signature -> Ordering
| (Signature.mk x1) (Signature.mk x2) := Ord.cmp x1 x2
};

instance
SignatureEq : Eq Signature := fromOrdToEq;

instance
SignedMessageOrd : Ord SignedMessage :=
mkOrd@{
cmp : SignedMessage -> SignedMessage -> Ordering
| (SignedMessage.mk x1) (SignedMessage.mk x2) := Ord.cmp x1 x2
};

instance
SignedMessageEq : Eq SignedMessage := fromOrdToEq;

instance
KeyPairOrd : Ord KeyPair :=
let
Expand Down
4 changes: 2 additions & 2 deletions Package.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,6 @@ import PackageDescription.V2 open;
package : Package :=
defaultPackage@?{
name := "anoma";
version := mkVersion 0 4 0;
dependencies := [github "anoma" "juvix-stdlib" "v0.5.0"]
version := mkVersion 0 5 0;
dependencies := [github "anoma" "juvix-stdlib" "v0.6.0"]
};
6 changes: 3 additions & 3 deletions juvix.lock.yaml
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@
# This file was autogenerated by Juvix version 0.6.4.
# This file was autogenerated by Juvix version 0.6.5.
# Do not edit this file manually.

version: 2
checksum: 991d05a3078cab0b630ff2de9b268a8fb2f164680d806dfb92454865e481b3c4
checksum: fbd6203d95670277a5355e725ae45b752f3a3e251dfa8cbff8b8b7d70b4bb6cf
dependencies:
- git:
name: anoma_juvix-stdlib
ref: 16211500dc59a944f851fbaeeef703fdd09163fa
ref: 17a82dd466010b51924677b16a3f09a6c4c86a80
url: https://github.com/anoma/juvix-stdlib
dependencies: []
107 changes: 107 additions & 0 deletions test/AlwaysValid/Keys.juvix
Original file line number Diff line number Diff line change
@@ -0,0 +1,107 @@
module AlwaysValid.Keys;

import Anoma open;

privKey : PrivateKey :=
PrivateKey.mk
[ 0x0
; 0x60
; 0xa3
; 0x6b
; 0xb1
; 0x3e
; 0x45
; 0x45
; 0xc6
; 0x41
; 0x8f
; 0x46
; 0xc9
; 0x72
; 0xa8
; 0x4e
; 0x24
; 0x29
; 0xcb
; 0x7b
; 0x1b
; 0x76
; 0xc3
; 0xa1
; 0xf6
; 0xf2
; 0x28
; 0xcc
; 0xc4
; 0x39
; 0x1d
; 0x1c
; 0x91
; 0x7
; 0xfd
; 0xe6
; 0xc6
; 0x54
; 0x6b
; 0x5f
; 0xc4
; 0x57
; 0xf6
; 0xc8
; 0xf8
; 0x80
; 0x94
; 0xe8
; 0x2f
; 0xa6
; 0x30
; 0x13
; 0xdc
; 0x7e
; 0x50
; 0x78
; 0x8f
; 0x2f
; 0xb2
; 0xaf
; 0xcb
; 0xd0
; 0xa
; 0x52
];

pubKey : PublicKey :=
PublicKey.mk
[ 0x91
; 0x7
; 0xfd
; 0xe6
; 0xc6
; 0x54
; 0x6b
; 0x5f
; 0xc4
; 0x57
; 0xf6
; 0xc8
; 0xf8
; 0x80
; 0x94
; 0xe8
; 0x2f
; 0xa6
; 0x30
; 0x13
; 0xdc
; 0x7e
; 0x50
; 0x78
; 0x8f
; 0x2f
; 0xb2
; 0xaf
; 0xcb
; 0xd0
; 0xa
; 0x52
];
7 changes: 1 addition & 6 deletions test/AlwaysValid/Transaction.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -7,12 +7,7 @@ import Anoma open;
open Transaction;
open DeltaComponent;

privKey : PrivateKey :=
PrivateKey.mk
0xddd315c76991f8e058760cacdd19c21bf6a12c72bc229a60ad6aaa314fa07ac11662fc6e7829efcb0f4500827d49bb699af7b5475cef5220fd600ebbf9709a58;

pubKey : PublicKey :=
PublicKey.mk 0xddd315c76991f8e058760cacdd19c21bf6a12c72bc229a60ad6aaa314fa07ac1;
import AlwaysValid.Keys open;

alwaysTrueLogic (r : Resource) (tx : Transaction) : Bool := true;

Expand Down
2 changes: 1 addition & 1 deletion test/Package.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -6,5 +6,5 @@ package : Package :=
defaultPackage@?{
name := "juvix-anoma-stdlib-test";
dependencies :=
[github "anoma" "juvix-stdlib" "v0.5.0"; path "../"; github "anoma" "juvix-test" "v0.12.0"]
[github "anoma" "juvix-stdlib" "v0.6.0"; path "../"; github "anoma" "juvix-test" "v0.13.0"]
};
2 changes: 1 addition & 1 deletion test/Resource/Tests.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ testResource : Resource :=
data := 0;
eph := true;
nonce := 0;
npk := PublicKey.mk 0;
npk := PublicKey.mk (replicate 32 0x0);
rseed := 0
};

Expand Down
12 changes: 6 additions & 6 deletions test/juvix.lock.yaml
Original file line number Diff line number Diff line change
@@ -1,28 +1,28 @@
# This file was autogenerated by Juvix version 0.6.4.
# This file was autogenerated by Juvix version 0.6.5.
# Do not edit this file manually.

version: 2
checksum: 5cddee95c6408d8f699c799178f5e3c7368e9c543c7734d3b1b69ac6285831a0
checksum: 2bd62b79f2d679d8a211b1e1687bf7c6bb68ef74a675cc59a8a7b57683c9e9e4
dependencies:
- git:
name: anoma_juvix-stdlib
ref: 16211500dc59a944f851fbaeeef703fdd09163fa
ref: 17a82dd466010b51924677b16a3f09a6c4c86a80
url: https://github.com/anoma/juvix-stdlib
dependencies: []
- path: ../
dependencies:
- git:
name: anoma_juvix-stdlib
ref: 16211500dc59a944f851fbaeeef703fdd09163fa
ref: 17a82dd466010b51924677b16a3f09a6c4c86a80
url: https://github.com/anoma/juvix-stdlib
dependencies: []
- git:
name: anoma_juvix-test
ref: f7e822969fa82c510f38d6569a9b5ac7f1180221
ref: 12b72c6f91126f08e19ef183cc377bb86e629de9
url: https://github.com/anoma/juvix-test
dependencies:
- git:
name: anoma_juvix-stdlib
ref: 16211500dc59a944f851fbaeeef703fdd09163fa
ref: 17a82dd466010b51924677b16a3f09a6c4c86a80
url: https://github.com/anoma/juvix-stdlib
dependencies: []

0 comments on commit 80bc788

Please sign in to comment.