split functions in separate files

This commit is contained in:
Rígille S. B. Menezes 2021-12-03 15:06:39 -03:00
parent 802ea59f65
commit 8b0136cc2e
10 changed files with 70 additions and 84 deletions

View File

@ -26,85 +26,3 @@ type Ether.RLP {
data(value: List<U8>)
node(child: List<Ether.RLP>)
}
Ether.RLP.show(r: Ether.RLP): String
case r {
data:
Bytes.to_hex(r.value)
node:
let ret = "["
for child in r.child with ret:
ret|Ether.RLP.show(child)|","
ret|"]"
}
// Length
// ------
Ether.RLP.encode.length(add: Nat, length: Nat): Bytes
if Nat.lte(length, 55) then
[Nat.to_u8(Nat.add(add,length))]
else
let b = Bytes.from_nat(length)
let a = Nat.to_u8(Nat.add(56, Nat.add(add, List.length!(b))))
a & b
Ether.RLP.split.length(add: Nat, bytes: Bytes): Pair<Bytes, Bytes>
case bytes {
nil:
{[], []}
cons:
let fst = Nat.sub(U8.to_nat(bytes.head), add)
if Nat.lte(fst, 55) then
Bytes.split(bytes.tail, fst)
else
let {length, tail} = Bytes.split(bytes.tail, Nat.sub(fst, 56))
Bytes.split(tail, Bytes.to_nat(length))
}
// Repeat
// ------
Ether.RLP.encode.many(trees: List<Ether.RLP>): Bytes
case trees {
nil:
[]
cons:
List.concat!(Ether.RLP.encode(trees.head), Ether.RLP.encode.many(trees.tail))
}
// RLP
// ---
Ether.RLP.encode(tree: Ether.RLP): Bytes
case tree {
data:
if Bool.and(Nat.eql(List.length!(tree.value),1), Nat.lte(U8.to_nat((List.head_with_default!(0#8,tree.value))), 127)) then
tree.value
else
List.concat!(Ether.RLP.encode.length(128, List.length!(tree.value)), tree.value)
node:
let rest = Ether.RLP.encode.many(tree.child)
List.concat!(Ether.RLP.encode.length(192, List.length!(rest)), rest)
}
Ether.RLP.decode.many(bytes: Bytes): List<Ether.RLP>
case bytes {
nil:
[]
cons:
let prefix = U8.to_nat(bytes.head)
if Nat.lte(prefix, 127) then
Ether.RLP.data([bytes.head]) & Ether.RLP.decode.many(bytes.tail)
else if Nat.lte(prefix, 191) then
let {head, tail} = Ether.RLP.split.length(128, bytes)
Ether.RLP.data(head) & Ether.RLP.decode.many(tail)
else
let {head, tail} = Ether.RLP.split.length(192, bytes)
Ether.RLP.node(Ether.RLP.decode.many(head)) & Ether.RLP.decode.many(tail)
}
Ether.RLP.max: Nat
Nat.pred(Nat.pow(256, 7))
Ether.RLP.decode(bytes: Bytes): Ether.RLP
List.head!(Ether.RLP.decode.many(bytes)) <> Ether.RLP.data([])

View File

@ -0,0 +1,2 @@
Ether.RLP.decode(bytes: Bytes): Ether.RLP
List.head!(Ether.RLP.decode.many(bytes)) <> Ether.RLP.data([])

View File

@ -0,0 +1,15 @@
Ether.RLP.decode.many(bytes: Bytes): List<Ether.RLP>
case bytes {
nil:
[]
cons:
let prefix = U8.to_nat(bytes.head)
if Nat.lte(prefix, 127) then
Ether.RLP.data([bytes.head]) & Ether.RLP.decode.many(bytes.tail)
else if Nat.lte(prefix, 191) then
let {head, tail} = Ether.RLP.split.length(128, bytes)
Ether.RLP.data(head) & Ether.RLP.decode.many(tail)
else
let {head, tail} = Ether.RLP.split.length(192, bytes)
Ether.RLP.node(Ether.RLP.decode.many(head)) & Ether.RLP.decode.many(tail)
}

View File

@ -0,0 +1,11 @@
Ether.RLP.encode(tree: Ether.RLP): Bytes
case tree {
data:
if Bool.and(Nat.eql(List.length!(tree.value),1), Nat.lte(U8.to_nat((List.head_with_default!(0#8,tree.value))), 127)) then
tree.value
else
List.concat!(Ether.RLP.encode.length(128, List.length!(tree.value)), tree.value)
node:
let rest = Ether.RLP.encode.many(tree.child)
List.concat!(Ether.RLP.encode.length(192, List.length!(rest)), rest)
}

View File

@ -0,0 +1,7 @@
Ether.RLP.encode.length(add: Nat, length: Nat): Bytes
if Nat.lte(length, 55) then
[Nat.to_u8(Nat.add(add,length))]
else
let b = Bytes.from_nat(length)
let a = Nat.to_u8(Nat.add(56, Nat.add(add, List.length!(b))))
a & b

View File

@ -0,0 +1,7 @@
Ether.RLP.encode.many(trees: List<Ether.RLP>): Bytes
case trees {
nil:
[]
cons:
List.concat!(Ether.RLP.encode(trees.head), Ether.RLP.encode.many(trees.tail))
}

2
base/Ether/RLP/max.kind Normal file
View File

@ -0,0 +1,2 @@
Ether.RLP.max: Nat
Nat.pred(Nat.pow(256, 7))

10
base/Ether/RLP/show.kind Normal file
View File

@ -0,0 +1,10 @@
Ether.RLP.show(r: Ether.RLP): String
case r {
data:
Bytes.to_hex(r.value)
node:
let ret = "["
for child in r.child with ret:
ret|Ether.RLP.show(child)|","
ret|"]"
}

14
base/Ether/RLP/split.kind Normal file
View File

@ -0,0 +1,14 @@
// Length
// ------
Ether.RLP.split.length(add: Nat, bytes: Bytes): Pair<Bytes, Bytes>
case bytes {
nil:
{[], []}
cons:
let fst = Nat.sub(U8.to_nat(bytes.head), add)
if Nat.lte(fst, 55) then
Bytes.split(bytes.tail, fst)
else
let {length, tail} = Bytes.split(bytes.tail, Nat.sub(fst, 56))
Bytes.split(tail, Bytes.to_nat(length))
}

View File

@ -1,2 +1,2 @@
Ether.tests : _
"Ether.tests"
Ether.tests: _
"Ether.tests"