stelliferous

Releases (2)

• 0.0.3.0 invalid

  expected a fresh constructor name (duplicate declaration: Text)

  at checkpoint_pickle.bend:14

  8 files do not load

  • checkpoint_pickle.bend
  • tensor_batch_norm.bend
  • tensor_checkpoint.bend
  • tensor_f32.bend
  • tensor_layer.bend
  • tensor_loss.bend
  • tensor_optimizer.bend
  • tensor_training.bend
• 0.0.2.0 indexed

Definitions (2,086)

proofs/storage_buffer_model.bend

• def fresh
• def fresh_ready
• def packed_contents
• type Observation
• def proposition
• def observe
• def lift

proofs/storage_certificate.bend

• def first
• def left
• def right
• def normalized
• def normalized_witness
• def restored
• type Certificate
• def witness_at
• def witness
• def fresh_equation
• def allocated
• def stored_equation
• def stored
• def family
• def written
• def written_equation
• def write_list

proofs/storage_clone_certificate.bend

• type Copies
• def clone

proofs/storage_readback.bend

• def capacity_node
• def store_capacity
• def write_capacity
• def fetch_node
• def fetch_store
• def read_written
• def other_node
• def fetch_preserved
• def no_wrap
• def read_preserved_full
• def pick_sameEvery address of a fresh tree reads its fill value.
• def fetch_fresh
• def read_fresh
• def read_preserved

proofs/storage_refinement.bend

• def reflect_packedThe tree model covers every native Array owner, including capacities larger than its logical sequence.
• def pack_reflected
• law fresh
• law clone
• law read
• law write
• law size
• law get_nodeBase passes the branch z that the caller computed as i < n/2; each child receives its own comparison against its half.
• law get_go
• law swap_node
• law swap_go
• law swap
• def guarded_read
• def bounded_read
• def bounded_read_is_get
• def write_sequenceSequence transfers preserve native modular addressing for every element type.
• def read_sequence
• def sequence_length
• def sequence_elementAn observed logical prefix has the actual stored element at every valid index.
• def sequence_missing
• def sequence_lookup_case
• def default_after_presence
• def bounded_read_observation_case
• def bounded_read_observationFull logical-read contract, including out-of-range fallback.
• type SequenceEvidenceA fact about an existing storage prefix, not another runtime container.
• def sequence_storage
• def sequence_owner
• def stored_sequence_elementThe unchecked primitive is usable after the caller establishes its logical index bound.
• def read_sequence_evidence
• def read_encoded_sequenceThe logical address conversion is separate from the physical owner.
• def replace_read_ownerUsed only in propositions to compare reads from different physical owners.
• def equivalent_sequence_read
• type ObservationReify an affine owner once for proof consumers that need both its Data model and the relation.
• def observed_node_equation
• def observed_node_reflection
• def observed_node
• def observe
• def lift_observationTransport a concrete owner observation into a proposition checked on trees.
• def lift_pair_observation

proofs/storage_shape.bend

• type Both
• def first
• def second
• law Balanced
• def extent
• def fresh
• def store_node
• def store
• def write
• def capacity
• def unique_depth
• def same_capacityBalanced trees at the same depth expose the same native capacity.
• def transfer_room

proofs/storage_tree_model.bend

• type Tree
• def pack
• def reflectProof observation of an existing owner, not a runtime conversion.
• def capacity
• def fresh
• def fetch
• def store
• def read