proofs/storage_allocation_refinement.bend

stelliferous@0.0.2.0 · 64 lines · 4 definitions

1import Base
2import stelliferous@0.0.2.0/storage_buffer.bend as Storage
3import stelliferous@0.0.2.0/storage_allocation.bend as Allocation
4import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
5import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageLaws
6import stelliferous@0.0.2.0/proofs/storage_buffer_model.bend as Buffer
7
8# Dispatch changes neither the initialized array nor its live certificate.
9# This is an unconditional equation for every element type, depth and length.
10def dispatch_same(-Element: Data,-allocator: Nat -> Element -> Nat -> Storage.Buffer<Element>,depth: Nat,+value: Element,+length: Nat) ->
11  {Allocation.dispatch(~Element,~allocator,depth,value,length) == allocator(depth,value,length) : Storage.Buffer<Element>}:
12  match depth:
13    case 0n: {==}
14    case 1n: {==}
15    case 2n: {==}
16    case 3n: {==}
17    case 4n: {==}
18    case 5n: {==}
19    case 6n: {==}
20    case 7n: {==}
21    case 8n: {==}
22    case 9n: {==}
23    case 10n: {==}
24    case 11n: {==}
25    case 12n: {==}
26    case 13n: {==}
27    case 14n: {==}
28    case 15n: {==}
29    case 16n: {==}
30    case 17n: {==}
31    case 18n: {==}
32    case 19n: {==}
33    case 20n: {==}
34    case 21n: {==}
35    case 22n: {==}
36    case 23n: {==}
37    case 24n: {==}
38    case 25n: {==}
39    case 26n: {==}
40    case 27n: {==}
41    case 28n: {==}
42    case 29n: {==}
43    case 30n: {==}
44    case 31n+rest: {==}
45
46def array_same(-Element: Data,+depth: Nat,+value: Element) ->
47  {Allocation.array(~Element,depth,value) == Array.new(Element,depth,value) : Array<Element>}:
48  %Equal.sym(Storage.Buffer<Element>,Allocation.allocate(~Element,depth,value,0n),Storage.allocate(~Element,depth,value,0n),
49    dispatch_same(Element,Allocation.allocated(~Element),depth,value,0n)) :
50    {Allocation.storage(~Element,_) == Array.new(Element,depth,value) : Array<Element>}
51  {==}
52
53def fresh(~Element: Data,+depth: Nat,+value: Element) ->
54  {Allocation.array(~Element,depth,value) == Tree.pack(Element,Tree.fresh(Element,depth,value)) : Array<Element>}:
55  Equal.trans(Array<Element>,Allocation.array(~Element,depth,value),Array.new(Element,depth,value),
56    Tree.pack(Element,Tree.fresh(Element,depth,value)),array_same(Element,depth,value),StorageLaws.fresh(Element,depth,value))
57
58def contents(~Element: Data,+depth: Nat,+value: Element,+length: Nat) ->
59  {Buffer.contents(~Element,Allocation.allocate(~Element,depth,value,length)) == Buffer.Content{Tree.fresh(Element,depth,value),length} : Buffer.Content<Element>}:
60  %Equal.sym(Storage.Buffer<Element>,Allocation.allocate(~Element,depth,value,length),Storage.allocate(~Element,depth,value,length),dispatch_same(Element,Allocation.allocated(~Element),depth,value,length)) :
61    {Buffer.contents(~Element,_) == Buffer.Content{Tree.fresh(Element,depth,value),length} : Buffer.Content<Element>}
62  %Equal.sym(Array<Element>,Array.new(Element,depth,value),Tree.pack(Element,Tree.fresh(Element,depth,value)),StorageLaws.fresh(Element,depth,value)) :
63    {Buffer.Content{Tree.reflect(Element,_),length} == Buffer.Content{Tree.fresh(Element,depth,value),length} : Buffer.Content<Element>}
64  Equal.cong(Tree.Tree<Element>,Buffer.Content<Element>,tree => Buffer.Content{tree,length},Tree.reflect(Element,Tree.pack(Element,Tree.fresh(Element,depth,value))),Tree.fresh(Element,depth,value),StorageLaws.reflect_packed(Element,Tree.fresh(Element,depth,value)))