proofs/storage_buffer_model.bend
stelliferous@0.0.2.0 · 153 lines · 31 definitions
1
2
3import Base
4import stelliferous@0.0.2.0/storage_buffer.bend as Storage
5import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
6import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageLaws
7import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
8import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape
9import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
10import stelliferous@0.0.2.0/proofs/word_power_of_two.bend as Power
11import stelliferous@0.0.2.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
82
83
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
149def lift(~Element: Data,~Context: Data,~Proposition: Context -> @-buffer: Storage.Buffer<Element> -> Type,+context: Context,-buffer: Storage.Buffer<Element>,
150 observation: Observation<Element,buffer>,canonical: @+model: Model<Element> -> Proposition(context,pack(~Element,model))) -> Proposition(context,buffer):
151 Observation{model,equation} = observation
152 %equation : Proposition(context,_)
153 canonical(model)