Fuaran.Core.OpStream 0.33.0

Fuaran.Core

The shared cross-domain substrate for the Fuaran family — the genericity-extracted spine that the domain tiers (UI, Calc, Documents, CAD, Office and the adopters since) consume as a peer dependency, so each domain stops re-implementing the same op-stream / op-algebra / tree / wire / validator / artifact-function machinery for itself.

Apache-2.0. FSharp.Core + Fable.Core only (Fable.Core is a compile-time dependency for the dual .NET/Fable pipeline — no runtime behaviour rides on it). No domain dependency, no native dependency, no host dependency. Every package is a library of generic functions over domain-witness records — the core owns no base node type. Each domain's closed NodeKind DU stays sovereign and exhaustively matched — closed unions + exhaustive total matching are the load-bearing F# constraint the whole pattern rests on.

This repo is the realisation of the rule-of-three extraction: the substrate was extracted only once five artifact-witness spines had shipped (UI, Calc, Documents, CAD, Office), with the string-vs-Guid identity axis resolved as a witness parameter rather than guessed. That is the history, not the current roster: further domains have adopted it since, and the witness-record field freeze in STABILITY.md names the domains whose adoption it rests on.

Packages

Dependency order: Tree → Ops → (OpStream → OpStream.Dag; Wire standalone); Column over Wire; Validator over Tree + Column; Function over Tree/Ops/Wire; Query over Column + Function; Conformance over all of the above. Beside that spine, and all four read by Conformance so they precede it: Observer standalone; Projection over Tree; Propagation over Tree + Ops; AiSurface over Wire + Ops. Then the build-time tier, which nothing above depends on: Idl over Wire → Idl.Codegen over Idl → Idl.Cli over Idl.Codegen.

The compute strand is produced elsewhere (Phase 258, D66). Fuaran.Core.DataFrame, Fuaran.Core.Column.Ops, Fuaran.Core.DataFrame.Conformance and Fuaran.Core.DataFrame.CSharp continue, under the same ids and namespaces, from Fuaran-Core/fuaran-core-compute at 0.33.0; this repository published them up to 0.32.0, and those versions stay on nuget.org. They are built over the packages above and read by none of them, and a test here refuses any project, package reference or built assembly that brings one of the four ids back into this tree.

The C# facade is removed (Phase 231, DECISIONS.md D28). Fuaran.Core.CSharp, the C#-shaped facade over the column layer, the hole-declaration family and the wire JSON model, was published from 0.22.0 to 0.32.0 and is not produced from 0.33.0: the consumer it was shipped for never adopted it. Its one reader, the compute repository's Fuaran.Core.DataFrame.CSharp, is removed by that repository in the release that raises its pin to 0.33.0, so neither half of the facade continues. A C# tier authors through the F# surface; a C# veneer over Core's closed unions returns when the IDL can generate one (D28's second criterion). The published versions stay on nuget.org.

This table is a derived roster, not a hand-kept list. Its rows are held equal to the packable projects under src/ by PackageRosterTests in the suite ./verify.ps1 runs, so a package that ships and is not documented here — or a row for a package that no longer ships — is a red gate rather than a discovery. The purpose column stays hand-written; only the roster is asserted.

The witness pattern

The core never sees a concrete NodeKind. A domain supplies a small record of functions (the witness) and the generic functions operate through it:

let nodew : NodeWitness<MyNode, MyId> =
    { Id = fun n -> n.Id
      KindTag = fun n -> n.Kind
      Children = fun n -> n.Children
      ReplaceChildren = fun n cs -> { n with Children = cs } }

// now the whole skeleton op algebra works over MyNode, with no core change:
Ops.apply nodew idw (InsertChild(parentId, child)) tree

The one genuine cross-domain divergence — id representation — is a witness too: IdWitness<'Id> = { ToString; OfString; Equals }. Doc/Calc keep human-meaningful string ids; UI/Music keep Guids; both over one Core.Tree.

What the witness surface covers — and what stays yours

Every traversal in this library — Tree.ids, Tree.exists, Tree.updateNode, and the whole op algebra built on them — walks NodeWitness.Children and nothing else. That is the witness surface, and it is the exact scope of the one structural invariant the engine enforces for you:

each id occurs at most once over the witness's Children traversal.

That invariant has a name — Tree.WellFormed — and one definition. Tree.wellFormed answers it for a tree and names the first id that breaks it; Tree.graftWellFormed answers it for the tree a graft would produce, without building it. Ops.apply keeps it by reading the second: an InsertChild whose subtree carries an id the tree already holds — or which repeats an id within itself — is refused with DuplicateId, naming the first offender. Diff.toOps reads the first. Asking whether a tree is valid and refusing an op that would invalidate it are therefore the same question, asked of the same function.

"Valid" here means STRUCTURALLY valid and nothing more. Validity is three layers and only the first is this library's: structural (the invariant above), vocabulary (your wire boundary decides whether a kind and its fields are ones you know), and rule families (your own pre-emit lint). A claim that says only "valid" has not said which, and Tree.WellFormed exists so that it can.

A node your domain holds in a keyed, non-structural position is invisible to that traversal — and, since Phase 286, you declare those positions once and the engine walks them. If your node type keeps children anywhere Children does not report them — a case table, a fallback slot, a named alternative, an argument position — supply a KeyedWitness: the nodes each node holds in keyed positions (KeyedChildren), an arity-preserving rebuild of them (ReplaceKeyedChildren), a way to place one there (PlaceKeyedChild), and your own full-walk id check (IdsUnique). Then Tree.traversal nodew keyw is a witness every navigator (tryFind, path, Index.build, updateNode, …) reaches those nodes through; Tree.idsKeyed / wellFormedKeyed / graftWellFormedKeyed are the keyed walks; and Ops.applyContainedKeyed refuses a DuplicateId held in a keyed position on either side of an insert, and addresses nodes below one. The unkeyed Ops.apply / applyContained are unchanged: they see only Children, so a domain that uses them still owes its own check over its own walk.

And certify the declaration rather than assuming it. Conformance.keyedApplyLaws BUILDS the collisions the unkeyed engine is blind to — an id held keyed in the tree against a structural graft, the reverse, and keyed against keyed — and requires applyContainedKeyed to refuse exactly the inserts your own check refuses afterwards; a keyed position your KeyedChildren forgets is the disagreement it reports. Conformance.keyedChildrenLaws certifies your check itself. Building the collisions is the point: your generator mints fresh ids, so a law quantified over what it draws would certify a check that checks nothing. A domain with no keyed position declares the empty list, and the report says it was vacuous by declaration rather than passing quietly.

What stays deliberate is what the engine EDITS through. Children is what it rebuilds through — structural ops append to, filter and permute that list and nothing else — so a keyed position is read and located but never added to, vacated or reordered by a skeleton op; a RemoveNode or MoveNode of a node held directly in one is refused as KeyedPosition. Widening Children itself to reach keyed positions would oblige every domain to re-express them as an ordered list the engine may restructure, which is the change Phase 189 declined and Phase 286 keeps declining. Conformance.opAlgebra certifies the invariant at the structural scope over your own witness, with two laws that say different things: "an accepted insert introduces no id already present" is about the op that can create a duplicate, and "apply's accept path preserves Tree.WellFormed" is about every op, so a MoveNode or a Batch that broke it could not hide behind the first.

Which of this library's assumptions you can discharge, and which you inherit, is one table: the Core-to-domain proof contract. Every assumed row of the claims ladder is classed there as a domain-obligation (a green Conformance law at your witness is the sampled discharge — the invariant above is one of them, and so is the keyed-position obligation beside it), a model-bridge (this repository's own model-to-production gap, which you inherit), or a premise (what nothing discharges — a hash that does not collide, an extractor and a compiler that are correct). The table is checked against proofs.json row for row rather than reviewed.

If you evaluate incrementally with Propagation.evalFrom, your evaluator is one of those obligations (Phase 211). The agreement theorem holds of an evaluator that is a function of what it reads, handed a change set that names every node an edit moved, and a prior that is eval's own output over the same dependency map. The driver enforces none of that, and the first two are properties of YOUR evaluator. Conformance.propagationEvaluatorLaws certifies them at your evaluator, from an EvaluatorWitness: your model generator, your dependency map, your per-node evaluator, and your edits, each with the change set you would name for it. The third is yours in words, because no law can see where a stored Map came from. A prior kept across an edit that moves the dependency map must be re-primed with eval, not replayed.

Compacting an op-stream — verify, then compact

OpStream.compact and compactChainOnly do not walk the chain. They read the boundary record's hash and TRUST it. So the compacted stream verifies exactly when the original does only over a prefix that was verified BEFORE it was discarded — compact_preserves_verify and its corollary compact_verifies_iff_original in proofs/Chain.fst — and a tamper in the prefix of an unverified stream survives compaction, verifies across the new boundary, and once the prefix is gone nothing can find it again. A host that compacts an unverified stream has compacted whatever it was handed. The order is an obligation on every caller: verifyChain (or verifyChainWith cfg) first, then compact.

A stream kept under its own StreamConfig compacts under the same config (Phase 227): compactWith cfg / compactChainOnlyWith cfg (over snapshotAtOptWith cfg) seed the boundary at sequence zero with cfg.Genesis, the value every chain walker starts from, so a compaction at zero verifies across under any genesis (compact_at_zero_verifies_under_any_genesis). The canonical entry points are the empty-genesis instantiation and emit the same bytes they always have.

The container capability — what applyContained enforces, and the one thing it asks of you

Ops.applyContained canHold is the variant for a domain with leaves: canHold answers can this node hold children at all, and a node that cannot earns a typed NotAContainer instead of an op that silently does nothing. Containment legality — which kinds may parent which — stays yours; this is the coarse question only.

It is enforced at three places, and the third is worth stating because it is the one a caller authoring a subtree meets: the PARENT of an InsertChild, the NEW PARENT of a MoveNode, and every node of the inserted subtree that holds children. A graft whose own interior places children under a node your predicate refuses is rejected, with NotAContainer naming that node — which is a node of your graft, not of the tree, so look for it there. A MoveNode is deliberately not walked: the subtree is already in the tree, so it carries in no interior the tree did not already hold.

What it asks of you in return: write canHold over the node's own kind (or its own fields), never over its children. The type is 'Node -> bool, so a predicate may read the child list — and one that does can admit a node at the instant the engine checks it and refuse it the instant the very insert that check licensed gives it a child. No check placed anywhere in this library repairs that, because the answer changes under the edit. Conformance.containerLaws perturbs a node's children and requires the predicate to be unchanged, so you meet this as a red law rather than as a tree your own predicate calls invalid. Run it alongside certify; it is opt-in because a domain with no container notion has nothing for it to say.

The artifact-function three laws (Fuaran.Core.Function)

A saved typed tree behaves as a function of its declared holes. The contract bakes in:

1. Totality — bounded iteration only; an unbounded RepeatHole is rejected, never run.
2. Hygiene — holes bind by absolute lexical address (id-path), never bare name, so composition cannot capture.
3. Effect signature — a mandatory two-axis effect/determinism class, joined componentwise through compose (pure ∘ clock = clock; clock ∘ random = clock + random — the determinism axis is a set of factors joined by union).

Build

./run.ps1            # format + build + test
./verify.ps1         # format-check + build + Fable-compile gate + test (the green gate)
./verify.ps1 -Proofs # … plus the proof leg: the F* model of the DAG fold, checked and re-extracted
dotnet build Fuaran.Core.slnx
dotnet run --project tests/Fuaran.Core.Tests

The "Fable-clean on encode and decode" claim is gated, not asserted — in the consumer that owns the Fable toolchain rather than here (Phase 217): fuaran-dotnet's tests/core-fable/ compiles every public package under Fable and runs the ParityVectors table (Fuaran.Core.Conformance) on both pipelines, byte-compared. Every version cut cites a green run of that leg against the candidate packages first. This repository keeps the half that needs no Fable: fable-exclusions.json and the suite hold every packable package to "ships the fable/ sources, or is excluded with a reason", and the .NET side of every parity vector is pinned. See STABILITY.md "Fable cleanliness".

proofs/ carries a machine-checked model of the N-lane DAG fold (Phase 131): DagFold.fst is an F* model of Dag.reconcileMany and the replay with fold confluence proved as a theorem, and proofs/oracle/DagFold.fs is that model extracted to F# and run by the suite beside the production fold as a differential oracle. What the theorem covers, what it assumes and how to run the leg are in proofs/README.md; ./verify.ps1 -Proofs (and CI's proofs job) installs the pinned prover and checks it.

The conformance suite exercises every layer against an in-repo reference witness (a tiny string-id domain) — proving the generics work without depending on any domain workspace. The suite asserts that every law family is exercised, and non-vacuous, at that reference witness; the generated docs/conformance-families.md is the roster. No test count is stated here, because a figure only this paragraph held would be asserted by nothing — PackageRosterTests refuses one. Domain adoption (re-expressing each domain's machinery over Fuaran.Core.*) is deliberately out of scope here; it lands on each domain workspace's own roadmap.

A green law family is not the same claim as an exercised one, and the roster says which it is (Phase 196). A LawResult records that a law HELD; it cannot record how many cases reached it, so a family whose evidence is drawn rather than built reports the same green whether the condition arose two hundred times or never. SampleAdequacy has guarded that inside a run since Phase 121 — and discarded the measurement. It is emitted now: SampleAdequacy.cases reads a family's results through its own census class into a CaseCount, and the generated docs/conformance-families.md carries it as a cases column, per family, measured at this repository's own reference witness. A cell reads vacuous — never a number — when the run certified nothing, naming the starved dimension; unmeasured is the separate state of a rendering handed no run at all. Every family reaches a non-zero, non-starved count here, which is what lets a host read a zero in its own census as a fact about its own witness rather than about the kit. The instance that proves it: attestationLaws at OpStream.noAttestation reports its laws green over zero signed heads, and now says so.

Adopting a domain

Re-expressing a domain spine over Fuaran.Core.*? Start at docs/ADOPTION.md — the four-witness recipe + the caveats a real adoption surfaced — with the runnable template at samples/adoption.

Status

Pre-1.0 — the released version is single-sourced from <Version> in Directory.Build.props. The witness-record contracts (especially IdWitness and NodeWitness) are the stability-critical surfaces — see STABILITY.md. Design log in DECISIONS.md.