Merge branch 'master' of https://github.com/uwu-tech/Kind

base/Bits/to_nat.kind

@@ -1,6 +1,6 @@
 Bits.to_nat(b: Bits): Nat
   case b {
-    e: 0,
-    o: Nat.mul(2, Bits.to_nat(b.pred)),
-    i: Nat.succ(Nat.mul(2, Bits.to_nat(b.pred)))
-  }
+    e: Nat.zero
+    o: Nat.double(Bits.to_nat(b.pred))
+    i: Nat.succ(Nat.double(Bits.to_nat(b.pred)))
+  }

base/Bits/to_nat/identity.kind

@@ -0,0 +1,22 @@
+Bits.to_nat.identity.aux0(x: Bits): Bits.to_nat(Bits.inc(x)) == Nat.succ(Bits.to_nat(x))
+  case x {
+    e: refl
+    o: refl
+    i: apply(Nat.double, Bits.to_nat.identity.aux0(x.pred))
+  }!
+
+Bits.to_nat.identity.aux1(x: Nat): Nat.to_bits(Nat.succ(x)) == Bits.inc(Nat.to_bits(x))
+  case x {
+    zero: refl
+    succ: apply(Bits.inc, Bits.to_nat.identity.aux1(x.pred))
+  }!
+
+Bits.to_nat.identity(n: Nat): Equal<Nat, n, Bits.to_nat(Nat.to_bits(n))>
+  case n {
+    zero:
+      refl
+    succ: 
+      rewrite X in Nat.succ(n.pred) == Bits.to_nat(X) with Bits.to_nat.identity.aux1(n.pred)
+      rewrite X in Nat.succ(n.pred) == X with Bits.to_nat.identity.aux0(Nat.to_bits(n.pred))
+      apply(Nat.succ, Bits.to_nat.identity(n.pred))
+  }!

base/Bits/to_string.kind

@@ -0,0 +1,3 @@
+// TODO:
+Bits.to_string(bits: Bits): String
+  Bits.to_string(bits)

base/Ether/RLP/README.md

@@ -0,0 +1,20 @@
+# RLP
+
+The purpose of RLP (Recursive Length Prefix) is to encode arbitrarily nested arrays of binary data, and RLP is the main encoding method used to serialize objects in Ethereum. The only purpose of RLP is to encode structure; encoding specific data types (eg. strings, floats) is left up to higher-order protocols;
+
+### Example  
+The string “dog” = `[ 0x83, ‘d’, ‘o’, ‘g’ ]`   
+The list [ “cat”, “dog” ] = `[ 0xc8, 0x83, 'c', 'a', 't', 0x83, 'd', 'o', 'g' ]`  
+The empty string (‘null’) = `[ 0x80 ]`  
+The empty list = `[ 0xc0 ]`  
+The integer 0 = `[ 0x80 ]`  
+The encoded integer 0 (’\x00’) = `[ 0x00 ]`  
+The encoded integer 15 (’\x0f’) = `[ 0x0f ]`  
+The encoded integer 1024 (’\x04\x00’) = `[ 0x82, 0x04, 0x00 ]`  
+The set theoretical representation of three, [ [], [[]], [ [], [[]] ] ] = `[ 0xc7, 0xc0, 0xc1, 0xc0, 0xc3, 0xc0, 0xc1, 0xc0 ]`  
+The string “Lorem ipsum dolor sit amet, consectetur adipisicing elit” = `[ 0xb8, 0x38, 'L', 'o', 'r', 'e', 'm', ' ', ... , 'e', 'l', 'i', 't' ]`  
+
+
+### Reference
+- [Ethereum Wiki](https://eth.wiki/fundamentals/rlp)
+- [Ethers.js](https://github.com/ethers-io/ethers.js/tree/master/packages/rlp)

base/Ether/RLP/bitify/byte.kind

@@ -0,0 +1,3 @@
+// TODO:
+Ether.RLP.bitify.byte(b: Byte): Ether.RLP.Tree
+  Ether.RLP.Tree.tip(Bits.empty)

base/Ether/RLP/bitify/empty.kind

@@ -0,0 +1,2 @@
+Ether.RLP.bitify.empty: Ether.RLP.Tree
+  Ether.RLP.Tree.tip(Bits.e)

base/Ether/RLP/bitify/nat.kind

@@ -0,0 +1,2 @@
+Ether.RLP.bifity.nat(n: Nat): Ether.RLP.Tree
+  Ether.RLP.Tree.tip(Nat.to_bits(n))

base/Ether/RLP/bitify/string.kind

@@ -0,0 +1,2 @@
+Ether.RLP.bitify.string(s: String): Ether.RLP.Tree
+  Ether.RLP.Tree.tip(String.to_bits(s))

base/Ether/RLP/show.kind

@@ -0,0 +1,11 @@
+Ether.RLP.to_string(t: List(Ether.RLP.Tree) ): String
+  case t {
+    nil : ""
+    cons: 
+      "[ " |
+      case t.head as tree {
+        tip : Bits.show(tree.value) | ", "
+        list: Ether.RLP.to_string(t.tail)
+      }
+      | " ]"
+  }

base/Ether/RLP/show_list_tree.kind

@@ -0,0 +1,10 @@
+Ether.RLP.show_list_tree(l: List<Ether.RLP.Tree>): String
+  Ether.RLP.show_list_tree.aux(l, "")
+
+Ether.RLP.show_list_tree.aux(l: List<Ether.RLP.Tree>, aux: String): String
+  case l {
+    nil : aux
+    cons: 
+      let s = aux | Ether.RLP.show_tree(l.head)
+      Ether.RLP.show_list_tree.aux(l.tail, s)
+  }

base/Ether/RLP/show_tree.kind

@@ -0,0 +1,5 @@
+Ether.RLP.show_tree(t: Ether.RLP.Tree): String 
+  case t {
+    tip : "[" | Bits.show(t.value) | "]"
+    list: Ether.RLP.show_list_tree(t.value)
+  }

base/Ether/RLP/test/all.kind

@@ -0,0 +1,10 @@
+RLP.test.all: TestSuite
+  TestSuite.many("RLP", 
+    [ 
+     RLP.test.encode
+    ])
+
+// Show all tests for String
+RLP.test.show: _
+  log(TestSuite.show(RLP.test.all, 0))
+  0

base/Ether/RLP/test/encode.kind

@@ -0,0 +1,171 @@
+RLP.test.encode: TestSuite
+  TestSuite.many("RLP.encode", [
+    RLP.test.encode.0, RLP.test.encode.1, RLP.test.encode.2,
+    RLP.test.encode.3, RLP.test.encode.4, RLP.test.encode.5,
+    RLP.test.encode.6, RLP.test.encode.7, RLP.test.encode.8,
+    RLP.test.encode.9, RLP.test.encode.10, RLP.test.encode.11
+
+  ])
+
+// zero
+RLP.test.encode.0: TestSuite
+  let test = "0"
+  let bin = Ether.RPL.encode.binary(0)
+  let got = Ether.RLP.encode.read(bin)
+  let exp = "0x80"
+  let name = "0"
+  TestSuite.show.log_string(name, test, exp, got)
+
+// Small int
+RLP.test.encode.1: TestSuite
+  let test = "1"
+  let bin = Ether.RPL.encode.binary(1)
+  let got = Ether.RLP.encode.read(bin)
+  let exp = "0x01"
+  let name = "1"
+  TestSuite.show.log_string(name, test, exp, got)
+
+// Small int
+RLP.test.encode.2: TestSuite
+  let test = "16"
+  let bin = Ether.RPL.encode.binary(16)
+  let got = Ether.RLP.encode.read(bin)
+  let exp = "0x10"
+  let name = "2"
+  TestSuite.show.log_string(name, test, exp, got)
+
+// Small int
+RLP.test.encode.3: TestSuite
+  let test = "79"
+  let bin = Ether.RPL.encode.binary(79)
+  let got = Ether.RLP.encode.read(bin)
+  let exp = "0x4f"
+  let name = "3"
+  TestSuite.show.log_string(name, test, exp, got)
+
+// Medium int
+RLP.test.encode.4: TestSuite
+  let test = "100000"
+  let bin = Ether.RPL.encode.binary(100000)
+  let got = Ether.RLP.encode.read(bin)
+  let exp = "0x830186a0"
+  let name = "4"
+  TestSuite.show.log_string(name, test, exp, got)
+
+// Medium int
+RLP.test.encode.5: TestSuite
+  let test = "1000"
+  let bin = Ether.RPL.encode.binary(1000)
+  let got = Ether.RLP.encode.read(bin)
+  let exp = "0x8203e8"
+  let name = "5"
+  TestSuite.show.log_string(name, test, exp, got)
+
+// Empty list
+RLP.test.encode.6: TestSuite
+  let test = "[]"
+  // let bin = Ether.RPL.encode.binary(1000)
+  let got = Ether.RLP.encode.read([])
+  let exp = "0xc0"
+  let name = "6"
+  TestSuite.show.log_string(name, test, exp, got)
+
+// String list
+RLP.test.encode.7: TestSuite
+  let test = "['dog', 'god', 'cat']"
+  let got = Ether.RLP.encode(RLP.test.list_string)
+  let exp = "0xcc83646f6783676f6483636174"
+  let name = "7"
+  TestSuite.show.log_string(name, test, exp, got)
+
+// List of list
+RLP.test.encode.8: TestSuite
+  let test = "[[[], []], []]"
+  let got = Ether.RLP.encode(RLP.test.empty)
+  let exp = "0xc4c2c0c0c0"
+  let name = "8"
+  TestSuite.show.log_string(name, test, exp, got)
+
+// multilist
+RLP.test.encode.9: TestSuite
+  let test = "['zw', [4], 1]"
+  let got = Ether.RLP.encode(RLP.test.multilist)
+  let exp = "0xc6827a77c10401"
+  let name = "9"
+  TestSuite.show.log_string(name, test, exp, got)
+
+RLP.test.encode.10: TestSuite
+  let test = "dictionary example"
+  let got = Ether.RLP.encode(RLP.test.dictionary)
+  let exp = "0xecca846b6579318476616c31ca846b6579328476616c32ca846b6579338476616c33ca846b6579348476616c34"
+  let name = "10"
+  TestSuite.show.log_string(name, test, exp, got)
+
+RLP.test.encode.11: TestSuite
+  let test = "long list"
+  let got = Ether.RLP.encode(RLP.test.long_list)
+  let exp = "0xf840cf84617364668471776572847a786376cf84617364668471776572847a786376cf84617364668471776572847a786376cf84617364668471776572847a786376"
+  let name = "11"
+  TestSuite.show.log_string(name, test, exp, got)
+
+RLP.test.encode.12: TestSuite
+  let test = "long string"
+  let got = Ether.RLP.encode(Ether.RLP.bitify.string(
+    "Lorem ipsum dolor sit amet, consectetur adipisicing elit"
+  ))
+  let exp = "0xb8384c6f72656d20697073756d20646f6c6f722073697420616d65742c20636f6e7365637465747572206164697069736963696e6720656c6974"
+  let name = "12"
+  TestSuite.show.log_string(name, test, exp, got)
+
+RLP.test.encode.12: TestSuite
+  let test = "loooong string"
+  let got = Ether.RLP.encode(Ether.RLP.bitify.string(
+    "Lorem ipsum dolor sit amet, consectetur adipiscing elit. Curabitur mauris magna, suscipit sed vehicula non, iaculis faucibus tortor. Proin suscipit ultricies malesuada. Duis tortor elit, dictum quis tristique eu, ultrices at risus. Morbi a est imperdiet mi ullamcorper aliquet suscipit nec lorem. Aenean quis leo mollis, vulputate elit varius, consequat enim. Nulla ultrices turpis justo, et posuere urna consectetur nec. Proin non convallis metus. Donec tempor ipsum in mauris congue sollicitudin. Vestibulum ante ipsum primis in faucibus orci luctus et ultrices posuere cubilia Curae; Suspendisse convallis sem vel massa faucibus, eget lacinia lacus tempor. Nulla quis ultricies purus. Proin auctor rhoncus nibh condimentum mollis. Aliquam consequat enim at metus luctus, a eleifend purus egestas. Curabitur at nibh metus. Nam bibendum, neque at auctor tristique, lorem libero aliquet arcu, non interdum tellus lectus sit amet eros. Cras rhoncus, metus ac ornare cursus, dolor justo ultrices metus, at ullamcorper volutpat"
+  ))
+  let exp = "0xb904004c6f72656d20697073756d20646f6c6f722073697420616d65742c20636f6e73656374657475722061646970697363696e6720656c69742e20437572616269747572206d6175726973206d61676e612c20737573636970697420736564207665686963756c61206e6f6e2c20696163756c697320666175636962757320746f72746f722e2050726f696e20737573636970697420756c74726963696573206d616c6573756164612e204475697320746f72746f7220656c69742c2064696374756d2071756973207472697374697175652065752c20756c7472696365732061742072697375732e204d6f72626920612065737420696d70657264696574206d6920756c6c616d636f7270657220616c6971756574207375736369706974206e6563206c6f72656d2e2041656e65616e2071756973206c656f206d6f6c6c69732c2076756c70757461746520656c6974207661726975732c20636f6e73657175617420656e696d2e204e756c6c6120756c74726963657320747572706973206a7573746f2c20657420706f73756572652075726e6120636f6e7365637465747572206e65632e2050726f696e206e6f6e20636f6e76616c6c6973206d657475732e20446f6e65632074656d706f7220697073756d20696e206d617572697320636f6e67756520736f6c6c696369747564696e2e20566573746962756c756d20616e746520697073756d207072696d697320696e206661756369627573206f726369206c756374757320657420756c74726963657320706f737565726520637562696c69612043757261653b2053757370656e646973736520636f6e76616c6c69732073656d2076656c206d617373612066617563696275732c2065676574206c6163696e6961206c616375732074656d706f722e204e756c6c61207175697320756c747269636965732070757275732e2050726f696e20617563746f722072686f6e637573206e69626820636f6e64696d656e74756d206d6f6c6c69732e20416c697175616d20636f6e73657175617420656e696d206174206d65747573206c75637475732c206120656c656966656e6420707572757320656765737461732e20437572616269747572206174206e696268206d657475732e204e616d20626962656e64756d2c206e6571756520617420617563746f72207472697374697175652c206c6f72656d206c696265726f20616c697175657420617263752c206e6f6e20696e74657264756d2074656c6c7573206c65637475732073697420616d65742065726f732e20437261732072686f6e6375732c206d65747573206163206f726e617265206375727375732c20646f6c6f72206a7573746f20756c747269636573206d657475732c20617420756c6c616d636f7270657220766f6c7574706174"
+  let name = "12"
+  TestSuite.show.log_string(name, test, exp, got)
+
+
+// -- MOCK -- 
+RLP.test.list_string: Ether.RLP.Tree
+  let bitify_str = (val: String) Ether.RLP.bitify.string(val)
+  let arr = [bitify_str("dog"), bitify_str("god"), bitify_str("cat")]
+  Ether.RLP.Tree.list(arr)
+
+// Tree for: ['zw', [4], 1]
+RLP.test.multilist: Ether.RLP.Tree
+  let bitify_str = (val: String) Ether.RLP.bitify.string(val)
+  let tree_num = (num: Nat) Ether.RLP.Tree.list([Ether.RLP.bifity.nat(num)])
+  Ether.RLP.Tree.list([bitify_str("zw"), tree_num(4), Ether.RLP.bifity.nat(1)])
+
+// [[[], []], []]
+RLP.test.empty: Ether.RLP.Tree
+  Ether.RLP.Tree.list([
+    Ether.RLP.Tree.list([Ether.RLP.bitify.empty, Ether.RLP.bitify.empty]),
+    Ether.RLP.bitify.empty
+  ])
+
+// [["key1", "val1"], ["key2", "val2"], ...]
+RLP.test.dictionary: Ether.RLP.Tree
+  let bitify_str = (val: String) Ether.RLP.bitify.string(val)
+  let entry = (key: String, val: String) Ether.RLP.Tree.list([bitify_str(key), bitify_str(val)])
+  Ether.RLP.Tree.list([
+    entry("key1", "val1"),
+    entry("key2", "val2"),
+    entry("key3", "val3"),
+    entry("key4", "val4")
+  ])
+
+// [["asdf", "qwer", "zxcv"], ["asdf", "qwer", "zxcv"], ...]
+RLP.test.long_list: Ether.RLP.Tree
+  let bitify_str = (val: String) Ether.RLP.bitify.string(val)
+  let entry = (key: String, val1: String, val2: String) Ether.RLP.Tree.list([bitify_str(key), bitify_str(val1), bitify_str(val2)])
+  Ether.RLP.Tree.list([
+    entry("asdf", "qwer", "zxcv"),
+    entry("asdf", "qwer", "zxcv"),
+    entry("asdf", "qwer", "zxcv"),
+    entry("asdf", "qwer", "zxcv")
+  ])
+
+// Reference: https://github.com/ethereumjs/rlp/blob/master/test/fixture/rlptest.json

bin/js/package-lock.json

@@ -1,24 +1,24 @@
 {
   "name": "kind-lang",
-  "version": "1.0.108",
+  "version": "1.0.110",
   "lockfileVersion": 2,
   "requires": true,
   "packages": {
     "": {
       "name": "kind-lang",
-      "version": "1.0.108",
+      "version": "1.0.110",
       "license": "MIT",
       "dependencies": {
-        "formcore-js": "^0.1.93"
+        "formcore-js": "^0.1.95"
       },
       "bin": {
         "kind": "src/main.js"
       }
     },
     "node_modules/formcore-js": {
-      "version": "0.1.93",
-      "resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.93.tgz",
-      "integrity": "sha512-Rkt2eBR/qaDguj01lW8P8jKFExl0+uxJV402Di9rSOnD2YhT64Pd8qFqGx7CqzR83iAnFhQseAgrLkS1Fz85bQ==",
+      "version": "0.1.95",
+      "resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.95.tgz",
+      "integrity": "sha512-6HqawzYO+X/bPGcXuMS8jyhuN2m+J4v9vnqp12QFRCZbGRCaNW5soAc4Md8KO9e5FwK1bRXGVvKHEDgOPDI6Xw==",
       "bin": {
         "fmc": "main.js"
       }
@@ -26,9 +26,9 @@
   },
   "dependencies": {
     "formcore-js": {
-      "version": "0.1.93",
-      "resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.93.tgz",
-      "integrity": "sha512-Rkt2eBR/qaDguj01lW8P8jKFExl0+uxJV402Di9rSOnD2YhT64Pd8qFqGx7CqzR83iAnFhQseAgrLkS1Fz85bQ=="
+      "version": "0.1.95",
+      "resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.95.tgz",
+      "integrity": "sha512-6HqawzYO+X/bPGcXuMS8jyhuN2m+J4v9vnqp12QFRCZbGRCaNW5soAc4Md8KO9e5FwK1bRXGVvKHEDgOPDI6Xw=="
     }
   }
 }

bin/js/package.json

@@ -1,6 +1,6 @@
 {
   "name": "kind-lang",
-  "version": "1.0.109",
+  "version": "1.0.111",
   "description": "Kind-Lang in JavaScript",
   "main": "src/kind.js",
   "scripts": {
@@ -20,6 +20,6 @@
   },
   "homepage": "https://github.com/uwu-tech/kind#readme",
   "dependencies": {
-    "formcore-js": "^0.1.93"
+    "formcore-js": "^0.1.95"
   }
 }

bin/package-lock.json

@@ -9,13 +9,13 @@
       "version": "0.1.0",
       "license": "MIT",
       "dependencies": {
-        "formcore-js": "^0.1.93"
+        "formcore-js": "^0.1.95"
       }
     },
     "node_modules/formcore-js": {
-      "version": "0.1.93",
-      "resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.93.tgz",
-      "integrity": "sha512-Rkt2eBR/qaDguj01lW8P8jKFExl0+uxJV402Di9rSOnD2YhT64Pd8qFqGx7CqzR83iAnFhQseAgrLkS1Fz85bQ==",
+      "version": "0.1.95",
+      "resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.95.tgz",
+      "integrity": "sha512-6HqawzYO+X/bPGcXuMS8jyhuN2m+J4v9vnqp12QFRCZbGRCaNW5soAc4Md8KO9e5FwK1bRXGVvKHEDgOPDI6Xw==",
       "bin": {
         "fmc": "main.js"
       }
@@ -23,9 +23,9 @@
   },
   "dependencies": {
     "formcore-js": {
-      "version": "0.1.93",
-      "resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.93.tgz",
-      "integrity": "sha512-Rkt2eBR/qaDguj01lW8P8jKFExl0+uxJV402Di9rSOnD2YhT64Pd8qFqGx7CqzR83iAnFhQseAgrLkS1Fz85bQ=="
+      "version": "0.1.95",
+      "resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.95.tgz",
+      "integrity": "sha512-6HqawzYO+X/bPGcXuMS8jyhuN2m+J4v9vnqp12QFRCZbGRCaNW5soAc4Md8KO9e5FwK1bRXGVvKHEDgOPDI6Xw=="
     }
   }
 }

bin/package.json

@@ -9,6 +9,6 @@
   "author": "",
   "license": "MIT",
   "dependencies": {
-    "formcore-js": "^0.1.93"
+    "formcore-js": "^0.1.95"
   }
 }