def dispatch_same

stelliferous@0.0.2.0 · proofs/storage_allocation_refinement.bend:8

import Base
import stelliferous@0.0.2.0/storage_buffer.bend as Storage
import stelliferous@0.0.2.0/storage_allocation.bend as Allocation

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: {==}