1	# Proof-only canonical owners retain the actual certificate. They support
2	# induction through affine Buffer callers without duplicating native arrays.
3	import Base
4	import ../storage_buffer.bend as Storage
5	import ./storage_tree_model.bend as Tree
6	import ./storage_refinement.bend as StorageLaws
7	import ./storage_certificate.bend as Certificate
8	import ./storage_shape.bend as Shape
9	import ./storage_witness.bend as Witness
10	import ./word_power_of_two.bend as Power
11	import ./nat_order.bend as Order
12	
13	type Content<-Element: Data> is Data:
14	  Content{tree: Tree.Tree<Element>,length: Nat}
15	
16	def contents(~Element: Data,buffer: Storage.Buffer<Element>) -> Content<Element>:
17	  Storage.Buffer{storage,length,certificate} = buffer
18	  Content{Tree.reflect(Element,storage),length}
19	
20	def value(~Element: Data,index: U32,content: Content<Element>) -> Element:
21	  Content{tree,length} = content
22	  Tree.read(Element,tree,index)
23	
24	def content_tree(~Element: Data,content: Content<Element>) -> Tree.Tree<Element>:
25	  Content{tree,length} = content
26	  tree
27	
28	def content_length(~Element: Data,content: Content<Element>) -> Nat:
29	  Content{tree,length} = content
30	  length
31	
32	type 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	
37	type Model<-Element: Data> is Data:
38	  Model{tree: Tree.Tree<Element>,length: Nat,certificate: Certificate.Certificate<Element,Tree.pack(Element,tree)>}
39	
40	def content(~Element: Data,model: Model<Element>) -> Content<Element>:
41	  Model{tree,length,certificate} = model
42	  Content{tree,length}
43	
44	def 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	
48	def tree(~Element: Data,model: Model<Element>) -> Tree.Tree<Element>:
49	  Model{tree,length,certificate} = model
50	  tree
51	
52	def length(~Element: Data,model: Model<Element>) -> Nat:
53	  Model{tree,length,certificate} = model
54	  length
55	
56	def 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	
60	def depth(~Element: Data,model: Model<Element>) -> Nat:
61	  Model{tree,length,Certificate.Certificate{depth,equation}} = model
62	  depth
63	
64	def 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	
69	def 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	
75	def 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.
84	type 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	
88	def 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	
95	def 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	
100	def 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	
104	def 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	
109	def 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	
115	def 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	
120	def 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	
125	def 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	
128	def 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	
134	def 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	
138	type Observation<-Element: Data,-buffer: Storage.Buffer<Element>> is Data:
139	  Observation{model: Model<Element>,equation: {pack(~Element,model) == buffer : Storage.Buffer<Element>}}
140	
141	def 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	
144	def 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	def 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)