Improve support for ByteArrays (#21)

* Improve support for ByteArrays

Adds:

ByteArray
* Ord instance
* Eq instance
* concatenate
* empty
* singleton
* toListByte

* Add quickcheck tests for bytearray

.github/workflows/test.yaml

@@ -21,4 +21,4 @@ jobs:
           cache: enable
 
       - name: Run tests
-        run: juvix eval test/Main.juvix
+        run: make -C test

Anoma/Data/ByteArray.juvix

@@ -1,20 +1,52 @@
 module Anoma.Data.ByteArray;
 
 import Stdlib.Prelude open;
+import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+import Anoma.Data.Byte;
+import Anoma.Data.ByteArray.Base as ByteArray open using {ByteArray};
 
-builtin bytearray
-axiom ByteArray : Type;
+module Internal;
 
-builtin bytearray-from-list-byte
-axiom mk : List Byte -> ByteArray;
+  --- For input n, returns 2^n
+  pow2 : Nat -> Nat
+    | zero := 1
+    | (suc n) := foldl {_} {Nat} {{_}} \ {acc _ := 2 * acc} 1 (0 to n);
 
-builtin bytearray-length
-axiom length : ByteArray -> Nat;
+  --- The size of a byte in bits
+  byteSize : Nat := 8;
 
-syntax alias AnomaContents := Nat;
+end;
 
-builtin anoma-bytearray-to-anoma-contents
-axiom toAnomaContents : ByteArray -> AnomaContents;
+syntax operator <> cons;
 
-builtin anoma-bytearray-from-anoma-contents
-axiom fromAnomaContents : Nat -> AnomaContents -> ByteArray;
+--- Concatenate two ;ByteArray;s.
+<> (ba1 ba2 : ByteArray) : ByteArray :=
+  let
+    ba1Size := ByteArray.length ba1;
+    ba2Size := ByteArray.length ba2;
+    ba1Content := ByteArray.toAnomaContents ba1;
+    ba2Content := ByteArray.toAnomaContents ba2;
+  in ByteArray.fromAnomaContents
+    (ba1Size + ba2Size)
+    (ba2Content * Internal.pow2 (Internal.byteSize * ba1Size) + ba1Content);
+
+--- Unpack a ;ByteArray; to a list of ;Byte;s.
+toListByte (ba : ByteArray) : List Byte :=
+  let
+    byteMax := Internal.pow2 Internal.byteSize;
+    go (contents : Nat) : Nat -> List Byte
+      | zero := []
+      | (suc n) := Byte.fromNat (mod contents byteMax) :: go (div contents byteMax) n;
+  in go (ByteArray.toAnomaContents ba) (ByteArray.length ba);
+
+empty : ByteArray := ByteArray.mk [];
+
+singleton (b : Byte) : ByteArray := ByteArray.mk [b];
+
+instance
+ByteArrayOrdI : Ord ByteArray := mkOrd (Ord.cmp on toListByte);
+
+instance
+ByteArrayEqI : Eq ByteArray := fromOrdToEq;
+
+open ByteArray public;

Anoma/Data/ByteArray/Base.juvix

@@ -0,0 +1,20 @@
+module Anoma.Data.ByteArray.Base;
+
+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;
+
+syntax alias AnomaContents := Nat;
+
+builtin anoma-bytearray-to-anoma-contents
+axiom toAnomaContents : ByteArray -> AnomaContents;
+
+builtin anoma-bytearray-from-anoma-contents
+axiom fromAnomaContents : Nat -> AnomaContents -> ByteArray;

test/ByteArrayTests.juvix

@@ -0,0 +1,27 @@
+module ByteArrayTests;
+
+import Stdlib.Prelude open;
+import Anoma.Data.ByteArray as ByteArray open using {ByteArray; <>};
+
+import Test.QuickCheck.Arbitrary as Arbitrary open using {Arbitrary; mkArbitrary; runArb};
+import Test.QuickCheck.Gen open using {mkGen};
+import Test.QuickCheckTest as QC;
+
+instance
+ByteArbitraryI : Arbitrary Byte := runArb >> Byte.fromNat |> mkGen |> mkArbitrary;
+
+mkToListByteId : QC.Test :=
+  QC.mkTest
+    "mk composed with toListByte is identity"
+    \ {bs := (ByteArray.mk bs |> ByteArray.toListByte) == bs};
+
+concatToListByte : QC.Test :=
+  QC.mkTest
+    "concat of two ByteArrays is concat of bytes"
+    \ {bs1 bs2 :=
+      let
+        ba1 := ByteArray.mk bs1;
+        ba2 := ByteArray.mk bs2;
+      in ByteArray.toListByte (ba1 <> ba2) == (bs1 ++ bs2)};
+
+allTests : List QC.Test := [mkToListByteId; concatToListByte];

test/Main.juvix

@@ -3,7 +3,10 @@ module Main;
 import Stdlib.Prelude open;
 import Test.JuvixUnit open;
 import AlwaysValid.Tests as AlwaysValid;
+import ByteArrayTests as BT;
 import Resource.Tests as Resource;
+import Test.QuickCheckTest as QC;
 
 main : IO :=
-  runTestSuite (testSuite "Juvix Anoma Stdlib tests" (AlwaysValid.tests ++ Resource.tests));
+  runTestSuite (testSuite "Juvix Anoma Stdlib tests" (AlwaysValid.tests ++ Resource.tests))
+    >>> readLn \ {seed := QC.runTestsIO 100 (stringToNat seed) BT.allTests};

test/Makefile

@@ -0,0 +1,5 @@
+all: test
+
+.PHONY: test
+test:
+	od -An -N2 -t u2 /dev/urandom | xargs | juvix eval Main.juvix

test/Package.juvix

@@ -6,5 +6,9 @@ package : Package :=
   defaultPackage@?{
     name := "juvix-anoma-stdlib-test";
     dependencies :=
-      [github "anoma" "juvix-stdlib" "v0.6.0"; path "../"; github "anoma" "juvix-test" "v0.13.0"]
+      [ github "anoma" "juvix-stdlib" "v0.6.0"
+      ; path "../"
+      ; github "anoma" "juvix-test" "v0.13.0"
+      ; github "anoma" "juvix-quickcheck" "v0.14.0"
+      ]
   };

test/juvix.lock.yaml

@@ -2,7 +2,7 @@
 # Do not edit this file manually.
 
 version: 2
-checksum: 2bd62b79f2d679d8a211b1e1687bf7c6bb68ef74a675cc59a8a7b57683c9e9e4
+checksum: f63de778142e7d4ae40060e30ce7e133abe661053c5674851c4be08576e000fc
 dependencies:
 - git:
     name: anoma_juvix-stdlib
@@ -26,3 +26,13 @@ dependencies:
       ref: 17a82dd466010b51924677b16a3f09a6c4c86a80
       url: https://github.com/anoma/juvix-stdlib
     dependencies: []
+- git:
+    name: anoma_juvix-quickcheck
+    ref: 72a517d5da0e9b8f0775fe5639094983916b8bd7
+    url: https://github.com/anoma/juvix-quickcheck
+  dependencies:
+  - git:
+      name: anoma_juvix-stdlib
+      ref: 17a82dd466010b51924677b16a3f09a6c4c86a80
+      url: https://github.com/anoma/juvix-stdlib
+    dependencies: []