StorageBufferModel.native_content_ready: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_buffer_model.bend as StorageBufferModel
Lines 104-107 of stelliferous@0.0.2.0/proofs/storage_buffer_model.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&start_line=104&end_line=107

import Base
import stelliferous@0.0.2.0/storage_buffer.bend as Storage
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness

def native_content_ready(~Element: Data,buffer: Storage.Buffer<Element>,ready: NativeReady(~Element,buffer)) -> ContentReady<Element,contents(~Element,buffer)>:
  Storage.Buffer{storage,length,Certificate.Certificate{+depth,equation}} = buffer
  Shape.Both{depth_ok,room} = ready
  ContentReady{depth,Witness.balanced(Element,depth,storage,Certificate.witness_at(Element,depth,storage,equation)),depth_ok,room}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&name=ContentReady
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&name=NativeReady
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&name=contents
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_certificate.bend&name=Certificate
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_certificate.bend&name=witness_at
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&name=Both
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=balanced
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/storage_buffer.bend&name=Buffer