0%

Closed AIMS Provenance Schema

Goal

Turn the completed ledger and partition work into one closed, immutable, backend-neutral provenance product embedded in the executable artifact that bytecode-vm established.

Normative Shape

The logical product records truths, not mechanisms. Its vocabulary includes lifetime bounds, extent class, owner bounds, ownership-observation facts, cleanup obligations, thread reachability, external visibility, stable logical events, and proof witnesses. It excludes VM slots, compiled offsets, register classes, raw retain/release calls, atomicity selections, representation tags used as ownership authority, and backend cleanup schedules.

Every function, call site, logical event, retain/drop obligation, user-drop boundary, and relevant aggregate field is addressed by a stable identity owned by the enclosing executable artifact. The product is closed only when all references resolve, all required functions and paths are represented, identities are unique and deterministically ordered, and its fingerprint is bound into the artifact’s validation story.

Proof Order

Calculus changes precede code changes. Extend the existing AIMS theorem family and four-surface synchronization rather than introducing a separate proof vocabulary. The proof must establish that closure preserves T1-T5, that stable keys cannot be rebound after validation, that each logical cleanup obligation has exactly one identity, and that later physical satisfaction cannot create or erase logical ownership truth.

Negative Space

A shared RcStrategy, RcAtomicity, RcInc, RcDec, or ValueRepr field is forbidden when it chooses a physical mechanism. A compatibility adapter may translate a neutral fact at the projection boundary, but it cannot feed back into AIMS or become a second authority. Layout and calling-convention details remain in the bytecode-owned VM/compiled planning structures.

Completion Evidence

Schema construction, closure validation, proof fixtures, deterministic serialization/fingerprinting, and malformed-artifact matrices must all pass the closed-schema probe. No later section may compensate for an under-specified logical roster.

Work Items

  • Define the closed AIMS logical product on the shipped executable-artifact seam, keyed by the bytecode-owned stable identities and containing only backend-neutral facts and events: lifetime bounds, extent class, owner bounds, ownership observations, cleanup obligations, thread reachability, external visibility, and logical retain/drop evidence.
  • Specify the exhaustive event, call-boundary, unwind, user-drop, closure-environment, protocol-witness, loop/back-edge, aggregate-field, and alias-class roster; every logical obligation has a stable key and every key has one producer.
  • Extend the committed Lean calculus before implementation with closure, uniqueness, identity preservation, cleanup totality, and satisfaction-map premises; bridge the new schema to T1-T5 and the existing partition/ledger theorems rather than creating a second ownership calculus.
  • Make the closed product opaque and immutable after validation, with construction restricted to AIMS realization and attachment to the existing closed executable product; prohibit backend mutation, executor-local reanalysis, or layout-derived logical facts.
  • Define versioning, deterministic ordering, fingerprinting, tamper detection, and malformed/partial artifact rejection for the logical product using the bytecode artifact’s existing identity and validation conventions.
  • Add schema matrices and proof fixtures covering normal and unwind paths, branch joins, loops, user destructors, closures, protocols, aggregates, borrowed and owned calls, externally visible values, and non-thread-reachable local values.