1	# Proof-only Data model of native arrays, parameterized by element type.
2	# Addresses below intentionally retain the runtime's U32 wrap semantics.
3	import Base
4	
5	type Tree<-T: Data> is Data:
6	  Leaf{value: T}
7	  Node{left: Tree<T>,right: Tree<T>}
8	
9	def 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.
18	def 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)}
22	def 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))
28	def 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)}
34	def 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))))
40	def 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)})
46	def 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)))
48	def 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	
51	def 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	
57	def 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)