storage_buffer.bend
stelliferous@0.0.3.0 · 96 lines · 0 definitions
1# Shared affine storage operations. Shape descriptors do not own another buffer.
2import Base
3import stelliferous@0.0.3.0/traversal_array.bend as Traversal
4import stelliferous@0.0.3.0/proofs/storage_certificate.bend as Certificate
5
6type Buffer<-Element: Data> is Type:
7 Buffer{storage: Array<Element>,length: Nat,certificate: Certificate.Certificate<Element,storage>}
8
9# Construction records evidence once, without visiting the owner or carrying
10# certificates through the elementwise loop.
11def allocate(~Element: Data,+depth: Nat,+value: Element,length: Nat) -> Buffer<Element>:
12 Buffer{Array.new(Element,depth,value),length,Certificate.allocated(Element,depth,value)}
13
14def from_list(~Element: Data,+values: List<&2,Element>,+depth: Nat,+fallback: Element,length: Nat) -> Buffer<Element>:
15 Buffer{Traversal.write_list(~Element,values,0,Array.new(Element,depth,fallback)),length,
16 Certificate.write_list(~Element,values,0,Array.new(Element,depth,fallback),Certificate.allocated(Element,depth,fallback))}
17
18# The values written from the offset on; the certificate follows the storage.
19def write_at(~Element: Data,+values: List<&2,Element>,+offset: U32,buffer: Buffer<Element>) -> Buffer<Element>:
20 Buffer{storage,length,certificate} = buffer
21 Buffer{Traversal.write_list(~Element,values,offset,storage),length,Certificate.write_list(~Element,values,offset,storage,certificate)}
22
23# One value written at index; the certificate follows the storage.
24def write(~Element: Data,+index: U32,value: Element,buffer: Buffer<Element>) -> Buffer<Element>:
25 Buffer{storage,length,certificate} = buffer
26 Buffer{Array.set(Element,storage,index,value),length,Certificate.set(~Element,index,value,storage,certificate)}
27
28def capacity(~Element: Data,-storage: Array<Element>,certificate: Certificate.Certificate<Element,storage>) -> U32:
29 Certificate.Certificate{depth,equation} = certificate
30 U32.shln(1,depth)
31
32def bind_pair(~First: Type,~Second: Type,~Result: Type,pair: First & Second,body: First -> Second -> Result) -> Result:
33 (first,second) = pair
34 body(first,second)
35
36# At most 32 word steps, independent of the allocation length.
37def bit_length(remaining_bits: Nat,+value: U32) -> Nat:
38 match remaining_bits:
39 case 0n: 0n
40 case 1n+rest:
41 Bool.pick(Nat,U32.is_zero(value),0n,1n+bit_length(rest,U32.shr(value)))
42
43# Positive requested lengths round to the next power-of-two capacity.
44# The caller establishes the machine allocation limit before calling Array.new.
45def allocation_depth(length: U32) -> Nat:
46 bit_length(32n,(length - 1 : U32))
47
48# Shared runtime depth calculation. The tail call stops at the significant
49# word bits; allocation_depth remains the arithmetic model used by proofs.
50def significant_bits(remaining: Nat,+value: U32,+bits: Nat,zero: Bool) -> Nat:
51 match remaining zero:
52 case 0n zero: bits
53 case 1n+rest True{}: bits
54 case 1n+rest False{}:
55 +next = U32.shr(value)
56 significant_bits(rest,next,1n+bits,U32.is_zero(next))
57
58def depth_for(+count: U32) -> Nat:
59 +value = (U32.max(count,1) - 1 : U32)
60 significant_bits(32n,value,0n,U32.is_zero(value))
61
62def write_list(~Element: Data,values: List<&2,Element>,+offset: U32,storage: Array<Element>) -> Array<Element>:
63 Traversal.write_list(~Element,values,offset,storage)
64
65def read_list(~Element: Data,count: Nat,+offset: U32,storage: Array<Element>) -> List<&2,Element>:
66 match count:
67 case 0n: []
68 case 1n+rest:
69 bind_pair(Array<Element>,Element,List<&2,Element>,Array.get(Element,storage,offset),storage => value =>
70 value <> read_list(Element,rest,(offset + 1 : U32),storage))
71
72def read_when(~Element: Data,fallback: Element,valid: Bool,storage: Array<Element>,index: U32) -> Array<Element> & Element:
73 match valid:
74 case False{}: (storage,fallback)
75 case True{}: Array.get(Element,storage,index)
76
77def read_sized(~Element: Data,fallback: Element,+index: U32,+logical_length: U32,sized: Array<Element> & U32) -> Array<Element> & Element:
78 (storage,capacity) = sized
79 read_when(Element,fallback,U32.is_lt(index,logical_length) && U32.is_le(logical_length,capacity),storage,index)
80
81def read_or(~Element: Data,fallback: Element,storage: Array<Element>,index: U32,logical_length: U32) -> Array<Element> & Element:
82 read_sized(Element,fallback,index,logical_length,Array.size(Element,storage))
83
84def read_result(~Element: Data,length: Nat,result: Array<Element> & Element,
85 certificate: Certificate.Certificate<Element,Pair.fst(Array<Element>,Element,result)>) -> Buffer<Element> & Element:
86 (storage,value) = result
87 (Buffer{storage,length,certificate},value)
88
89def read(~Element: Data,buffer: Buffer<Element>,+index: U32) -> Buffer<Element> & Element:
90 Buffer{storage,length,certificate} = buffer
91 read_result(~Element,length,Array.get(Element,storage,index),Certificate.read_kept(~Element,storage,index,certificate))
92
93def read_masked(~Element: Data,fallback: Element,valid: Bool,buffer: Buffer<Element>,index: U32) -> Buffer<Element> & Element:
94 match valid:
95 case False{}: (buffer,fallback)
96 case True{}: read(~Element,buffer,index)