Skip to content

Implementation Status.md

Latest commit

 

History

History
52 lines (44 loc) · 9.71 KB

Implementation Status.md

File metadata and controls

52 lines (44 loc) · 9.71 KB
Raw

Implementation Status

Assessed 2026-09-03 against src/, after the rebuild the Readiness Audit planned. The documents specify the system; this ledger says which parts are built and which gates each passes. Three gates: .NET (dotnet run --project tests/BAREWire.Tests.fsproj, 300 checks), JavaScript (fable src/BAREWire.Fable.fsproj, then node tests/js/roundtrip.mjs and node tests/js/tiers.mjs, the latter dispatching the platform obligations to cvc5 from the JavaScript build), and native (samples/RoundTrip compiled by Composer and run). The native gate passes on the rebuilt Composer (the Composer and clef working trees of 2026-09-03): the sample's transcript is byte-identical to expected.txt. On the Composer snapshot HelloProof pins, it stays blocked by the compiler-surface gaps 12 Intersection Subset records; that rebuild closes them, and HelloProof re-snapshots it next.

Concern Document Status
Substrate reading, the two missions Substrate_Formalism Position. Current; the missions ranked (2026-09-03).
Platform description, the inward reading 11 Platform Description Position and now vocabulary: src/Platform/ implements the description and its three observers; the kernel section (eBPF, wBPF, ThreeBody) is represented and nominally covered.
Evidence for the role 10 The Case from Practice Position. Current.
Compiler-facing rules and gates 12 Intersection Subset Current; every rule verified or documented, with a preferred spelling and a repro. An adversarial review of every tier against the documents and these rules (2026-09-03, 40 confirmed findings) has been applied. The compiler lane closed the rules the rebuilt Composer marks closed; the open ones keep their preferred spellings.
Encoding 02 Encoding and Decoding Engine Built. src/Encoding/: threaded offsets, fault sentinel, full primitive and aggregate coverage, whole-value combinators, per-substrate shims. Gates: .NET (golden vectors), JavaScript (byte-identical), native on the rebuilt Composer (the transcript matches); blocked on the pinned snapshot (array-length).
Framing 05 Network Protocol (envelope adopted) Built. src/Framing/Envelope.fs: kind, correlation, payload; stream length prefix; Hello. Gates: .NET, JavaScript, native on the rebuilt Composer. Transports, RPC, streaming: design.
Schema 03 Schema System Built. src/Schema/: BARE's fixed vocabulary, validation, wire size, packed offsets, compatibility, .bare text emission. Gates: .NET, JavaScript, native on the rebuilt Composer; blocked on the pinned snapshot (recursive-union). Not built: a .bare parser, codec generation.
Hardware descriptors and the validator 08 Hardware Descriptors Built. src/Hardware/: descriptors in fixed widths with counts, ABI profiles, Validator.derive/validate/explain, Layout.isPointerFree, BTF emitter and reader (bpftool btf dump confirms). Gates: .NET, JavaScript, native on the rebuilt Composer; blocked on the pinned snapshot (record-arrays).
Memory mapping 04 Memory Mapping Built (portable byte model). src/Memory/: Region bounded extents, View typed by a descriptor layout. Gates: .NET, JavaScript. Native memref realization, shared memory, mapped files: design over Fidelity.Platform bindings.
Static byte-storage placement StaticStorage.fs Built; .NET gate verified 2026-09-09. StaticStorage.plan assigns concrete relative offsets from a declared fixed, read-only, linker-placed rodata space. It checks allocation alignment, exact endpoints, granularity padding and capacity before returning a plan. Unsupported placement disciplines and overflow return findings. The emitter must allocate the returned pool and use its offsets; applying this plan's proof to independently placed globals is invalid. The source is registered in the .NET, Fable and Clef manifests; registration alone does not establish the other execution gates. Compiler/Composer integration is tracked in Lattice Integration.
Dispatch spatial contract Dispatch Regions Built; .NET and JavaScript gates verified 2026-09-09. DispatchRegions.validate checks canonical allocation/slice relationships, read/write access, complete supplied input including indirect reads, exact partition coverage, exclusive output and target capture-layout agreement. Located checks retain source/worker references for graph consumers. Allocation-free guards reject byte arithmetic overflow. The .NET runner reports 562 passing checks; the Fable dispatch gate exercises exact signed-int64 boundary matrices. The Clef scalar projection passes a native signed-boundary probe and is checked against the hosted equations; full graph-validator native execution is not established. Compiler extraction, native preservation and lifecycle synchronization are separate obligations; SpatiallyValid does not authorize publication or retirement.
Platform description and observers 11 Platform Description Built. src/Platform/: MemorySpace (with map kinds and availability), BoundarySurface/Endpoint (with availability), BufferSchema (fixed, length-prefixed, delimited, capped, ring), Transport, LifecycleFacts, TargetCore, Limits; Check.run/runWithLayouts, Manifest.emit, Obligations.ofDescription/smtLib/ledgerLine. Gates: .NET with cvc5 (unsat on every generated obligation for a Linux x86_64, an eBPF, and a ThreeBody description; sat on the inconsistent ones), native on the rebuilt Composer (Check.run, Obligations.ofDescription, and the manifest run in the sample); blocked on the pinned snapshot (string-constant, string-equality).
IPC 06 IPC Integration, 07 Design. The envelope and the first shared-memory layouts (maps, rings) are declared in the tiers above; the OS bindings are Fidelity.Platform's.
Cache-aware layouts 09 Cache-Aware Layouts Design. The ABI profiles carry natural alignment; cache-line facts and false-sharing analysis are not built.
Arena Arena_Design Design reference; implemented as a compiler intrinsic. The arena space is declared in the platform description.
Eliminating .NET dependencies 99 Historical memo; the shim design in 12 §4 is the current form.

What lands next (Readiness Audit §4)

Target-aware compiler handoff — planned 2026-09-20

Composer M-01 coordinates operation/profile admission under the existing clef-lang-spec numeric, memory and scheduler contracts. BAREWire's part is to preserve agreed layout, bounds, ownership, publication, transfer and lifecycle facts through Baker's graph and the selected backend handoff. Spatial validation alone does not establish safe publication, retirement, wait ordering or scheduler progress.

For parallel numerical work, transported partial state must preserve the arithmetic construction: rounding a partial before an exact merge requires an exactness proof. Planned oracles cover capacity, partial-state fidelity, contribution identity/multiplicity and lifetime across native and JavaScript boundaries. Zero-copy is admitted only under the actual storage/transport contract. Compiler proof metadata stays in the graph/correspondence carriers; this plan does not add runtime type tags or proof packages to every payload. Any missing shared declaration/schema is coordinated with Fidelity.Platform and CCS before Alex consumes it. No new transport implementation or native gate is claimed by this planning update.

Earlier readiness items

  • Step 11 (landed 2026-09-03 in the Fidelity.Platform working tree): Fidelity.Platform/Environments/Linux/x86_64/Description.clef, with consoleReadln declaring the capacity Console.clef names once as READLINE_CAPACITY; the Arty A7 gains ArtyA7_100T.Description.clef and a rebase plan for its contracts.
  • Steps 10 and 13: the platform description as a coeffect of the program semantic graph, the memory_map.manifest residual, and obligations stated against the declaration in both dispatches (06b for cvc5 at design time, 09 in the smt dialect for cvc5 at build time), replacing the 1024L literals in pSysReadline. Not built: an attempt that minted them in a pass beside the graph was withdrawn on 2026-09-03. The corpus places obligations in the graph itself (Composer docs/Obligation_Residency_Design.md), so this waits on the graph carrying its annotations and edges.
  • The compiler lane (landed 2026-09-03 in the Composer and clef working trees): the surface gaps in 12 closed with regression samples 18 through 23 in Composer's manifest; samples/RoundTrip runs natively and its transcript joins the differential. HelloProof's snapshot of that compiler is the remaining step; the SUBSET(...) sites migrate to their preferred spellings after it.
  • Step 9: Fidelity.Platform's contracts as an alias layer over src/Platform, and the Arty description's memory spaces.
  • Step 14: a .bare parser and codec generation. Step 15: measures on the wire.