proofs/storage_tree_model.bend

stelliferous@0.0.2.0 · 61 lines · 11 definitions

1# Proof-only Data model of native arrays, parameterized by element type.
2# Addresses below intentionally retain the runtime's U32 wrap semantics.
3import Base
4
5type Tree<-T: Data> is Data:
6  Leaf{value: T}
7  Node{left: Tree<T>,right: Tree<T>}
8
9def pack(-T: Data,tree: Tree<T>) -> Array<T>:
10  match tree:
11    case Leaf{v}:
12      ALeaf{v}
13    case Node{l,r}:
14      ANode{pack(T,l),pack(T,r)}
15
16# Proof observation of an existing owner, not a runtime conversion. Callers use
17# it only in erased propositions; numeric code continues to use Array directly.
18def reflect(-Element: Data,storage: Array<Element>) -> Tree<Element>:
19  match storage:
20    case ALeaf{value}: Leaf{value}
21    case ANode{left,right}: Node{reflect(Element,left),reflect(Element,right)}
22def capacity(-T: Data,tree: Tree<T>) -> U32:
23  match tree:
24    case Leaf{v}:
25      1
26    case Node{l,r}:
27      U32.shl(capacity(T,l))
28def fresh(-T: Data,n: Nat,+v: T) -> Tree<T>:
29  match n:
30    case 0n:
31      Leaf{v}
32    case 1n+ +rest:
33      Node{fresh(T,rest,v),fresh(T,rest,v)}
34def fetch(-T: Data,tree: Tree<T>,+n: U32,+i: U32) -> T:
35  match tree:
36    case Leaf{v}:
37      v
38    case Node{l,r}:
39      Bool.pick(T,U32.is_lt(i,U32.shr(n)),fetch(T,l,U32.shr(n),i),fetch(T,r,U32.shr(n),U32.sub(i,U32.shr(n))))
40def store(-T: Data,tree: Tree<T>,+n: U32,+i: U32,+v: T) -> Tree<T>:
41  match tree:
42    case Leaf{old}:
43      Leaf{v}
44    case Node{+l,+r}:
45      Bool.pick(Tree<T>,U32.is_lt(i,U32.shr(n)),Node{store(T,l,U32.shr(n),i,v),r},Node{l,store(T,r,U32.shr(n),U32.sub(i,U32.shr(n)),v)})
46def read(-T: Data,+tree: Tree<T>,i: U32) -> T:
47  fetch(T,tree,capacity(T,tree),U32.and(i,U32.sub(capacity(T,tree),1)))
48def write(-T: Data,+tree: Tree<T>,i: U32,v: T) -> Tree<T>:
49  store(T,tree,capacity(T,tree),U32.and(i,U32.sub(capacity(T,tree),1)),v)
50
51def write_sequence(~Element: Data,values: List<&2,Element>,+offset: U32,tree: Tree<Element>) -> Tree<Element>:
52  match values:
53    case Nil{}: tree
54    case head <> tail:
55      write_sequence(~Element,tail,(offset + 1 : U32),write(Element,tree,offset,head))
56
57def read_sequence(~Element: Data,count: Nat,+offset: U32,+tree: Tree<Element>) -> List<&2,Element>:
58  match count:
59    case 0n: Nil{}
60    case 1n+rest:
61      read(Element,tree,offset) <> read_sequence(~Element,rest,(offset + 1 : U32),tree)