proofs/storage_buffer_model.bend
stelliferous@0.0.3.0 · 253 lines · 0 definitions
1# Proof-only canonical owners retain the actual certificate. They support
2# induction through affine Buffer callers without duplicating native arrays.
3import Base
4import stelliferous@0.0.3.0/storage_buffer.bend as Storage
5import stelliferous@0.0.3.0/proofs/storage_tree_model.bend as Tree
6import stelliferous@0.0.3.0/proofs/storage_refinement.bend as StorageLaws
7import stelliferous@0.0.3.0/proofs/storage_certificate.bend as Certificate
8import stelliferous@0.0.3.0/proofs/storage_shape.bend as Shape
9import stelliferous@0.0.3.0/proofs/storage_witness.bend as Witness
10import stelliferous@0.0.3.0/proofs/word_power_of_two.bend as Power
11import stelliferous@0.0.3.0/proofs/nat_order.bend as Order
12
13type Content<-Element: Data> is Data:
14 Content{tree: Tree.Tree<Element>,length: Nat}
15
16def contents(~Element: Data,buffer: Storage.Buffer<Element>) -> Content<Element>:
17 Storage.Buffer{storage,length,certificate} = buffer
18 Content{Tree.reflect(Element,storage),length}
19
20def value(~Element: Data,index: U32,content: Content<Element>) -> Element:
21 Content{tree,length} = content
22 Tree.read(Element,tree,index)
23
24def content_tree(~Element: Data,content: Content<Element>) -> Tree.Tree<Element>:
25 Content{tree,length} = content
26 tree
27
28def content_length(~Element: Data,content: Content<Element>) -> Nat:
29 Content{tree,length} = content
30 length
31
32type ContentReady<-Element: Data,-content: Content<Element>> is Data:
33 ContentReady{depth: Nat,balanced: Shape.Balanced(Element,depth,content_tree(~Element,content)),
34 depth_ok: {Nat.is_le(depth,30n) == True{} : Bool},
35 room: {Nat.is_le(content_length(~Element,content),U32.to_nat(Tree.capacity(Element,content_tree(~Element,content)))) == True{} : Bool}}
36
37type Model<-Element: Data> is Data:
38 Model{tree: Tree.Tree<Element>,length: Nat,certificate: Certificate.Certificate<Element,Tree.pack(Element,tree)>}
39
40def content(~Element: Data,model: Model<Element>) -> Content<Element>:
41 Model{tree,length,certificate} = model
42 Content{tree,length}
43
44def pack(~Element: Data,model: Model<Element>) -> Storage.Buffer<Element>:
45 Model{tree,length,certificate} = model
46 Storage.Buffer{Tree.pack(Element,tree),length,certificate}
47
48def tree(~Element: Data,model: Model<Element>) -> Tree.Tree<Element>:
49 Model{tree,length,certificate} = model
50 tree
51
52def length(~Element: Data,model: Model<Element>) -> Nat:
53 Model{tree,length,certificate} = model
54 length
55
56def content_length_of(~Element: Data,+model: Model<Element>) -> {content_length(~Element,content(~Element,model)) == length(~Element,model) : Nat}:
57 Model{tree,length,certificate} = model
58 {==}
59
60def depth(~Element: Data,model: Model<Element>) -> Nat:
61 Model{tree,length,Certificate.Certificate{depth,equation}} = model
62 depth
63
64def balanced(~Element: Data,+model: Model<Element>) -> Shape.Balanced(Element,depth(~Element,model),tree(~Element,model)):
65 Model{+tree,length,Certificate.Certificate{+depth,equation}} = model
66 %StorageLaws.reflect_packed(Element,tree) : Shape.Balanced(Element,depth,_)
67 Witness.balanced(Element,depth,Tree.pack(Element,tree),Certificate.witness_at(Element,depth,Tree.pack(Element,tree),equation))
68
69def capacity_bound(~Element: Data,+model: Model<Element>,+depth_ok: {Nat.is_le(depth(~Element,model),30n) == True{} : Bool}) ->
70 {U32.is_le(Tree.capacity(Element,tree(~Element,model)),2147483648) == True{} : Bool}:
71 %Equal.sym(U32,Tree.capacity(Element,tree(~Element,model)),U32.shln(1,depth(~Element,model)),
72 Shape.capacity(Element,depth(~Element,model),tree(~Element,model),balanced(~Element,model))) : {U32.is_le(_,2147483648) == True{} : Bool}
73 Power.native_power_bound(depth(~Element,model),Order.successor(depth(~Element,model),30n,depth_ok))
74
75def capacity_allocatable(~Element: Data,+model: Model<Element>,depth_ok: {Nat.is_le(depth(~Element,model),30n) == True{} : Bool}) ->
76 {U32.is_le(Tree.capacity(Element,tree(~Element,model)),1073741824) == True{} : Bool}:
77 %Equal.sym(U32,Tree.capacity(Element,tree(~Element,model)),U32.shln(1,depth(~Element,model)),
78 Shape.capacity(Element,depth(~Element,model),tree(~Element,model),balanced(~Element,model))) : {U32.is_le(_,1073741824) == True{} : Bool}
79 Power.native_allocatable(depth(~Element,model),depth_ok)
80
81# Logical length and the native machine depth are independent of the stored
82# element values. Allocation establishes them; content-preserving operations
83# carry them with the same owner.
84type Sized<-Element: Data,-model: Model<Element>> is Data:
85 Sized{depth_ok: {Nat.is_le(depth(~Element,model),30n) == True{} : Bool},
86 room: {Nat.is_le(length(~Element,model),U32.to_nat(Tree.capacity(Element,tree(~Element,model)))) == True{} : Bool}}
87
88def ready_content(~Element: Data,+model: Model<Element>,evidence: ContentReady<Element,content(~Element,model)>) -> Sized<Element,model>:
89 Model{+tree,+length,Certificate.Certificate{+depth,+equation}} = model
90 ContentReady{+proved_depth,proved_balanced,depth_ok,room} = evidence
91 Sized{
92 %Equal.sym(Nat,depth,proved_depth,Shape.unique_depth(Element,tree,depth,proved_depth,balanced(~Element,model),proved_balanced)) : {Nat.is_le(_,30n) == True{} : Bool} depth_ok,
93 room}
94
95def content_ready(~Element: Data,+model: Model<Element>,evidence: Sized<Element,model>) -> ContentReady<Element,content(~Element,model)>:
96 Model{+tree,+length,Certificate.Certificate{+depth,+equation}} = model
97 Sized{depth_ok,room} = evidence
98 ContentReady{depth,balanced(~Element,model),depth_ok,room}
99
100def NativeReady(~Element: Data,buffer: Storage.Buffer<Element>) -> Data:
101 Storage.Buffer{storage,length,Certificate.Certificate{depth,equation}} = buffer
102 Shape.Both<{Nat.is_le(depth,30n) == True{} : Bool},{Nat.is_le(length,U32.to_nat(Tree.capacity(Element,Tree.reflect(Element,storage)))) == True{} : Bool}>
103
104def native_content_ready(~Element: Data,buffer: Storage.Buffer<Element>,ready: NativeReady(~Element,buffer)) -> ContentReady<Element,contents(~Element,buffer)>:
105 Storage.Buffer{storage,length,Certificate.Certificate{+depth,equation}} = buffer
106 Shape.Both{depth_ok,room} = ready
107 ContentReady{depth,Witness.balanced(Element,depth,storage,Certificate.witness_at(Element,depth,storage,equation)),depth_ok,room}
108
109def ready_packed(~Element: Data,+model: Model<Element>,ready: NativeReady(~Element,pack(~Element,model))) -> Sized<Element,model>:
110 Model{+tree,+length,Certificate.Certificate{+depth,equation}} = model
111 Shape.Both{depth_ok,room} = ready
112 Sized{depth_ok,
113 %StorageLaws.reflect_packed(Element,tree) : {Nat.is_le(length,U32.to_nat(Tree.capacity(Element,_))) == True{} : Bool} room}
114
115def ready_observed(~Element: Data,-buffer: Storage.Buffer<Element>,+model: Model<Element>,equation: {pack(~Element,model) == buffer : Storage.Buffer<Element>},
116 ready: NativeReady(~Element,buffer)) -> Sized<Element,model>:
117 ready_packed(~Element,model,
118 %Equal.sym(Storage.Buffer<Element>,pack(~Element,model),buffer,equation) : NativeReady(~Element,_) ready)
119
120def fresh_certificate(~Element: Data,+depth: Nat,+fill: Element) -> Certificate.Certificate<Element,Tree.pack(Element,Tree.fresh(Element,depth,fill))>:
121 Certificate.Certificate{depth,
122 %StorageLaws.fresh(Element,depth,fill) : {_ == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,_))) : Array<Element>}
123 Certificate.fresh_equation(Element,depth,fill)}
124
125def fresh(~Element: Data,+depth: Nat,+fill: Element,length: Nat) -> Model<Element>:
126 Model{Tree.fresh(Element,depth,fill),length,fresh_certificate(~Element,depth,fill)}
127
128def fresh_ready(~Element: Data,+depth: Nat,+fill: Element,+length: Nat,depth_ok: {Nat.is_le(depth,30n) == True{} : Bool},
129 room: {Nat.is_le(length,U32.to_nat(U32.shln(1,depth))) == True{} : Bool}) -> Sized<Element,fresh(~Element,depth,fill,length)>:
130 Sized{depth_ok,
131 %Equal.sym(U32,Tree.capacity(Element,Tree.fresh(Element,depth,fill)),U32.shln(1,depth),Shape.capacity(Element,depth,Tree.fresh(Element,depth,fill),Shape.fresh(Element,depth,fill))) :
132 {Nat.is_le(length,U32.to_nat(_)) == True{} : Bool} room}
133
134def packed_contents(~Element: Data,+model: Model<Element>) -> {contents(~Element,pack(~Element,model)) == content(~Element,model) : Content<Element>}:
135 Model{+tree,+length,certificate} = model
136 Equal.cong(Tree.Tree<Element>,Content<Element>,tree => Content{tree,length},Tree.reflect(Element,Tree.pack(Element,tree)),tree,StorageLaws.reflect_packed(Element,tree))
137
138type Observation<-Element: Data,-buffer: Storage.Buffer<Element>> is Data:
139 Observation{model: Model<Element>,equation: {pack(~Element,model) == buffer : Storage.Buffer<Element>}}
140
141def proposition(~Element: Data,length: Nat,-storage: Array<Element>,-tree: Tree.Tree<Element>) -> Type:
142 @certificate: Certificate.Certificate<Element,storage> -> Observation<Element,Storage.Buffer{storage,length,certificate}>
143
144def observe(~Element: Data,buffer: Storage.Buffer<Element>) -> Observation<Element,buffer>:
145 Storage.Buffer{storage,+length,certificate} = buffer
146 StorageLaws.lift_observation(~Element,~Nat,~proposition(~Element),length,storage,StorageLaws.observe(Element,storage),
147 tree => certificate => Observation{Model{tree,length,certificate},{==}})(certificate)
148
149# A model of any buffer.
150def observed_model(~Element: Data,-buffer: Storage.Buffer<Element>,observation: Observation<Element,buffer>) -> Model<Element>:
151 Observation{model,equation} = observation
152 model
153
154def observed_equation(~Element: Data,-buffer: Storage.Buffer<Element>,+observation: Observation<Element,buffer>) ->
155 {pack(~Element,observed_model(~Element,buffer,observation)) == buffer : Storage.Buffer<Element>}:
156 Observation{model,equation} = observation
157 equation
158
159def remodel(~Element: Data,buffer: Storage.Buffer<Element>) -> Model<Element>:
160 observed_model(~Element,buffer,observe(~Element,buffer))
161
162def remodeled(~Element: Data,buffer: Storage.Buffer<Element>) -> {pack(~Element,remodel(~Element,buffer)) == buffer : Storage.Buffer<Element>}:
163 observed_equation(~Element,buffer,observe(~Element,buffer))
164def lift(~Element: Data,~Context: Data,~Proposition: Context -> @-buffer: Storage.Buffer<Element> -> Type,+context: Context,-buffer: Storage.Buffer<Element>,
165 observation: Observation<Element,buffer>,canonical: @+model: Model<Element> -> Proposition(context,pack(~Element,model))) -> Proposition(context,buffer):
166 Observation{model,equation} = observation
167 %equation : Proposition(context,_)
168 canonical(model)
169
170def certificate_equation(~Element: Data,model: Model<Element>) ->
171 {Tree.pack(Element,tree(~Element,model)) == Tree.pack(Element,Certificate.normalized(Element,depth(~Element,model),Tree.reflect(Element,Tree.pack(Element,tree(~Element,model))))) : Array<Element>}:
172 Model{tree,length,Certificate.Certificate{depth,equation}} = model
173 equation
174
175# Certificate transport follows the native read equation at the original depth.
176def read_result(~Element: Data,+model: Model<Element>,-value: Element,-result: Array<Element> & Element,
177 +same: {(Tree.pack(Element,tree(~Element,model)),value) == result : Array<Element> & Element}) ->
178 {Storage.read_result(~Element,length(~Element,model),result,
179 Certificate.retained(~Element,depth(~Element,model),Tree.pack(Element,tree(~Element,model)),value,result,same,
180 certificate_equation(~Element,model))) == (pack(~Element,model),value) : Storage.Buffer<Element> & Element}:
181 Model{+tree,+length,Certificate.Certificate{+depth,+original}} = model
182 %proof@same :
183 {Storage.read_result(~Element,length,_,Certificate.retained(~Element,depth,Tree.pack(Element,tree),value,_,proof,original)) == (pack(~Element,model),value) : Storage.Buffer<Element> & Element}
184 {==}
185
186def read_observed(~Element: Data,+model: Model<Element>,+index: U32,
187 observed: Witness.Read<Element,Tree.pack(Element,tree(~Element,model)),Array.get(Element,Tree.pack(Element,tree(~Element,model)),index)>) ->
188 {Storage.read_result(~Element,length(~Element,model),Array.get(Element,Tree.pack(Element,tree(~Element,model)),index),
189 Certificate.Certificate{depth(~Element,model),Certificate.read_equation(~Element,depth(~Element,model),Tree.pack(Element,tree(~Element,model)),index,certificate_equation(~Element,model),observed)}) ==
190 (pack(~Element,model),Tree.read(Element,tree(~Element,model),index)) : Storage.Buffer<Element> & Element}:
191 Model{+tree,+length,Certificate.Certificate{+depth,+original}} = model
192 Witness.Read{value,+same} = observed
193 Equal.trans(Storage.Buffer<Element> & Element,
194 Storage.read_result(~Element,length,Array.get(Element,Tree.pack(Element,tree),index),Certificate.Certificate{depth,Certificate.read_equation(~Element,depth,Tree.pack(Element,tree),index,original,observed)}),
195 (pack(~Element,model),value),(pack(~Element,model),Tree.read(Element,tree,index)),
196 read_result(~Element,model,value,Array.get(Element,Tree.pack(Element,tree),index),Equal.sym(Array<Element> & Element,Array.get(Element,Tree.pack(Element,tree),index),(Tree.pack(Element,tree),value),same)),
197 Equal.cong(Element,Storage.Buffer<Element> & Element,value => (pack(~Element,model),value),value,Tree.read(Element,tree,index),
198 Equal.cong(Array<Element> & Element,Element,pair => Pair.snd(Array<Element>,Element,pair),(Tree.pack(Element,tree),value),(Tree.pack(Element,tree),Tree.read(Element,tree,index)),
199 Equal.trans(Array<Element> & Element,(Tree.pack(Element,tree),value),Array.get(Element,Tree.pack(Element,tree),index),(Tree.pack(Element,tree),Tree.read(Element,tree,index)),
200 Equal.sym(Array<Element> & Element,Array.get(Element,Tree.pack(Element,tree),index),(Tree.pack(Element,tree),value),same),StorageLaws.read(Element,tree,index)))))
201
202def read(~Element: Data,+model: Model<Element>,+index: U32) ->
203 {Storage.read(~Element,pack(~Element,model),index) == (pack(~Element,model),Tree.read(Element,tree(~Element,model),index)) : Storage.Buffer<Element> & Element}:
204 Model{+tree,+length,Certificate.Certificate{+depth,+equation}} = model
205 read_observed(~Element,model,index,Witness.observed(Element,Tree.pack(Element,tree),index,Witness.ArrayWitness{depth,Certificate.witness_at(Element,depth,Tree.pack(Element,tree),equation)}))
206
207def read_masked(~Element: Data,+fallback: Element,valid: Bool,+model: Model<Element>,+index: U32) ->
208 {Storage.read_masked(~Element,fallback,valid,pack(~Element,model),index) ==
209 (pack(~Element,model),Bool.pick(Element,valid,Tree.read(Element,tree(~Element,model),index),fallback)) : Storage.Buffer<Element> & Element}:
210 match valid:
211 case False{}: {==}
212 case True{}: read(~Element,model,index)
213
214def content_parts(+model: Model<F32>) -> {content(~F32,model) == Content{tree(~F32,model),length(~F32,model)} : Content<F32>}:
215 Model{tree,length,certificate} = model
216 {==}
217
218def model_length(+model: Model<F32>) -> {content_length(~F32,content(~F32,model)) == length(~F32,model) : Nat}:
219 Model{tree,length,certificate} = model
220 {==}
221
222def read_content(+index: U32,+content: Content<F32>) -> {Tree.read(F32,content_tree(~F32,content),index) == value(~F32,index,content) : F32}:
223 Content{tree,length} = content
224 {==}
225
226def buffer_contents(~Element: Data,+model: Model<Element>,-buffer: Storage.Buffer<Element>,equal: {pack(~Element,model) == buffer : Storage.Buffer<Element>}) ->
227 {content(~Element,model) == contents(~Element,buffer) : Content<Element>}:
228 Equal.trans(Content<Element>,content(~Element,model),contents(~Element,pack(~Element,model)),contents(~Element,buffer),
229 Equal.sym(Content<Element>,contents(~Element,pack(~Element,model)),content(~Element,model),packed_contents(~Element,model)),
230 Equal.cong(Storage.Buffer<Element>,Content<Element>,contents(~Element),pack(~Element,model),buffer,equal))
231
232def content_tree_of(~Element: Data,+model: Model<Element>) -> {content_tree(~Element,content(~Element,model)) == tree(~Element,model) : Tree.Tree<Element>}:
233 Model{tree,length,certificate} = model
234 {==}
235
236def observed_content(~Element: Data,-buffer: Storage.Buffer<Element>,observation: Observation<Element,buffer>) ->
237 {content(~Element,observed_model(~Element,buffer,observation)) == contents(~Element,buffer) : Content<Element>}:
238 Observation{+model,equation} = observation
239 buffer_contents(~Element,model,buffer,equation)
240
241def remodel_content(~Element: Data,buffer: Storage.Buffer<Element>) ->
242 {content(~Element,remodel(~Element,buffer)) == contents(~Element,buffer) : Content<Element>}:
243 observed_content(~Element,buffer,observe(~Element,buffer))
244# A value written into a buffer is written into its contents.
245def write_value_packed(~Element: Data,+index: U32,+value: Element,+model: Model<Element>) ->
246 {contents(~Element,Storage.write(~Element,index,value,pack(~Element,model))) ==
247 Content{Tree.write(Element,content_tree(~Element,content(~Element,model)),index,value),content_length(~Element,content(~Element,model))} : Content<Element>}:
248 Model{+tree,+length,certificate} = model
249 %Equal.sym(Array<Element>,Array.set(Element,Tree.pack(Element,tree),index,value),Tree.pack(Element,Tree.write(Element,tree,index,value)),
250 StorageLaws.write(Element,tree,index,value)) :
251 {Content{Tree.reflect(Element,_),length} == Content{Tree.write(Element,tree,index,value),length} : Content<Element>}
252 Equal.cong(Tree.Tree<Element>,Content<Element>,tree => Content{tree,length},Tree.reflect(Element,Tree.pack(Element,Tree.write(Element,tree,index,value))),
253 Tree.write(Element,tree,index,value),StorageLaws.reflect_packed(Element,Tree.write(Element,tree,index,value)))