StorageAllocationRefinement.dispatch_same: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_allocation_refinement.bend as StorageAllocationRefinement
Lines 8-44 of stelliferous@0.0.2.0/proofs/storage_allocation_refinement.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_allocation_refinement.bend&start_line=8&end_line=44

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

# Dispatch changes neither the initialized array nor its live certificate.
# This is an unconditional equation for every element type, depth and length.
def dispatch_same(-Element: Data,-allocator: Nat -> Element -> Nat -> Storage.Buffer<Element>,depth: Nat,+value: Element,+length: Nat) ->
  {Allocation.dispatch(~Element,~allocator,depth,value,length) == allocator(depth,value,length) : Storage.Buffer<Element>}:
  match depth:
    case 0n: {==}
    case 1n: {==}
    case 2n: {==}
    case 3n: {==}
    case 4n: {==}
    case 5n: {==}
    case 6n: {==}
    case 7n: {==}
    case 8n: {==}
    case 9n: {==}
    case 10n: {==}
    case 11n: {==}
    case 12n: {==}
    case 13n: {==}
    case 14n: {==}
    case 15n: {==}
    case 16n: {==}
    case 17n: {==}
    case 18n: {==}
    case 19n: {==}
    case 20n: {==}
    case 21n: {==}
    case 22n: {==}
    case 23n: {==}
    case 24n: {==}
    case 25n: {==}
    case 26n: {==}
    case 27n: {==}
    case 28n: {==}
    case 29n: {==}
    case 30n: {==}
    case 31n+rest: {==}

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/storage_allocation.bend&name=dispatch
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/storage_buffer.bend&name=Buffer