store

Documentation

Overview

Package store holds the content-addressed definition store and is the home of the body-abstraction barrier.

THE BODY BARRIER (a soundness invariant, encoded in package structure — CLAUDE.md): a definition's TYPE is public, but its BODY is sealed inside this package. The Def struct's body field is unexported, so no code outside this package can read a body except through the single gateway Unfold. This makes "no code peeks a body around the barrier" a compile-time fact rather than a future vigilance task.

Unfold is doc-commented as the sole gateway and the proof-cache instrumentation point: in Phase 1 it will log the dependency that the cache's Frame Lemma frames off (see ref_docs/rune-proof-cache-semantics.md). Forcing a glued value's lazy unfolding is the SAME operation; they coincide on purpose.

Index

• func HashDef(ty, body core.Tm) core.Hash
• func HashSCC(group []content) []core.Hash
• func Placeholder(i int) core.Hash
• type Cert
• type DataDecl
• type Def
  • func NewDef(ty, body core.Tm) Def
• type Store
  • func New() *Store
  • func (s *Store) Add(name string, ty, body core.Tm) core.Hash
  • func (s *Store) AddData(d DataDecl) (data core.Hash, ctors []core.Hash, elim core.Hash)
  • func (s *Store) Certified(h core.Hash) bool
  • func (s *Store) Certify(h core.Hash, deps []core.Hash)
  • func (s *Store) CtorOf(h core.Hash) (core.Hash, int, bool)
  • func (s *Store) DataDeclOf(h core.Hash) (DataDecl, []core.Hash, core.Hash, bool)
  • func (s *Store) ElimOf(h core.Hash) (core.ElimSig, bool)
  • func (s *Store) Lookup(name string) (core.Hash, bool)
  • func (s *Store) TypeOf(h core.Hash) (core.Tm, bool)
  • func (s *Store) Unfold(h core.Hash) (core.Tm, bool)

Functions

func HashDef

func HashDef(ty, body core.Tm) core.Hash

HashDef computes the content hash a definition (ty, body) would be stored under, without storing it. Identity is syntax (core.HashTerm); never modulo conversion.

func HashSCC

func HashSCC(group []content) []core.Hash

HashSCC hashes a strongly-connected group of mutually-recursive definitions as a unit (Unison-style), returning one content hash per member in input order.

Mutually-recursive definitions cannot reference each other by content hash — that would be a cycle in the Merkle DAG. The group is therefore hashed together: intra-group references must already be rewritten to the positional placeholder Placeholder(i), so the group's content is self-contained. The group hash digests every member's content in order; each member's hash is then derived from the group hash and its position, so the whole SCC shares one identity yet members stay distinguishable.

A singleton group with no self-reference reduces to hashContent, so the common acyclic case keeps its plain content hash (and alpha-equivalent definitions still hash equal). Phase 0 exercises only that case; the group machinery is laid down so Phase 1's recursive definitions slot in without a redesign.

func Placeholder

func Placeholder(i int) core.Hash

Placeholder is the stand-in content hash for the i-th member of an SCC while the group is being hashed. Intra-group references are rewritten to Placeholder(i) before HashSCC so the group content is self-contained and position-stable.

Types

type Cert

type Cert struct {
	Deps []core.Hash // canonical: sorted
}

Cert is one certificate: the dependency set U the judgment was closed over. Only well-typedness certificates are stored (a failed check is not a reusable fact about immutable content — it is simply not cached).

type DataDecl

type DataDecl struct {
	Name      string
	Ty        core.Tm // the former's type: a parameter telescope ending in U
	NumParams int     // length of that telescope
	CtorNames []string
	CtorTys   []core.Tm      // constructor types, with the former as Placeholder(0)
	Sigs      []core.CtorSig // per-constructor argument arity + recursive positions
	ElimTy    core.Tm        // generated eliminator type, former as Placeholder(0)
}

DataDecl is the elaborated content of one datatype declaration.

type Def

type Def struct {
	Type core.Tm // public: part of the content hash any referencing term already carries
	// contains filtered or unexported fields
}

Def is a stored definition. Type is public; body is sealed. The pair (Type, body) is the definition's content, and its content hash summarizes both.

func NewDef

func NewDef(ty, body core.Tm) Def

NewDef constructs a definition from a public type (optionally nil in Phase 0, since there is no type checker yet) and a body. Construction is the only way to place a body into a Def; thereafter the barrier holds.

type Store

type Store struct {
	// contains filtered or unexported fields
}

Store is the content-addressed definition store plus the mutable name layer.

The definition map is append-only and immutable in spirit: a content hash names a fixed (Type, body) forever. The name map is the only mutable, non-trusted part — it records which immutable object is "current" for a human-facing name, and editing source can only produce cache misses, never wrong hits.

func New

func New() *Store

New returns an empty store.

func (*Store) Add

func (s *Store) Add(name string, ty, body core.Tm) core.Hash

Add stores a single definition under its content hash, binds name to that hash, and returns the hash. Add is the acyclic path: it hashes (Type, body) directly as a singleton with no intra-group references (see HashSCC for the cyclic case).

func (*Store) AddData

func (s *Store) AddData(d DataDecl) (data core.Hash, ctors []core.Hash, elim core.Hash)

AddData stores a datatype declaration group and binds its names. It returns the hashes of the former, the constructors, and the eliminator (bound as Name, the constructor names, and Name+"Elim").

func (*Store) Certified

func (s *Store) Certified(h core.Hash) bool

Certified reports whether a stored certificate for h applies in this store: one whose every recorded dependency hash still resolves here. By immutability that side-condition is a set of lookups, not a validation procedure.

func (*Store) Certify

func (s *Store) Certify(h core.Hash, deps []core.Hash)

Certify records that the definition at h checked under the unfolded-dependency set deps. Append-only: re-certifying is a no-op.

func (*Store) CtorOf

func (s *Store) CtorOf(h core.Hash) (core.Hash, int, bool)

CtorOf implements core.DataInfo: is h a constructor, and of what.

func (*Store) DataDeclOf

func (s *Store) DataDeclOf(h core.Hash) (DataDecl, []core.Hash, core.Hash, bool)

DataDeclOf returns the stored declaration group for a former's hash.

func (*Store) ElimOf

func (s *Store) ElimOf(h core.Hash) (core.ElimSig, bool)

ElimOf implements core.DataInfo: is h an eliminator, and the data it eliminates with its parameter count and constructor signatures.

func (*Store) Lookup

func (s *Store) Lookup(name string) (core.Hash, bool)

Lookup returns the content hash currently bound to a name.

func (*Store) TypeOf

func (s *Store) TypeOf(h core.Hash) (core.Tm, bool)

TypeOf returns a definition's public type. Reading a type logs NO dependency: a referenced definition's type is part of its content hash, already in-band. This is the pure, no-dependency counterpart of Unfold (see the Frame Lemma).

func (*Store) Unfold

func (s *Store) Unfold(h core.Hash) (core.Tm, bool)

Unfold is THE SOLE GATEWAY to a definition's body, and the proof-cache instrumentation point.

Obtaining a body necessarily goes through here. In Phase 1, Unfold runs inside the conversion monad and logs the unfolded definition's hash into the write-only dependency set that keys the proof cache; the same call backs the lazy unfolding of a glued neutral (force == unfold). Phase 0 returns the body without logging, because there is no conversion yet — but the choke point exists now so that the instrumentation is a one-line change behind an already-enforced barrier, not a retrofit.