From 5e5d5bf8a94db296ed35c32bf96ac7bdcd8fa0a3 Mon Sep 17 00:00:00 2001 From: Chris Tate Date: Fri, 24 Jul 2026 17:56:59 -0500 Subject: [PATCH] Record declared u64 classes in the sidecar attestation and prove model/msg slot writes MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - integer_slots now records each slot's DECLARED class ({i64, u64}); the i64 flattening narrows to the frozen format-1 TypeRef/descriptor spellings where unsigned-ness genuinely has no vocabulary, and the V1 self-check accepts both classes - library builds declaring sidecar integer slots force-lower the designated init/update/subscriptions exports and every model-first contract helper, so record-field and msg-arm writes enter the prove-or-refuse boundary check instead of attesting from dead-stripped vacuity - declared record-field reads seed their class shape (whole, class range), the assumption side of the slot contract: an unguarded counter increment now refuses RANGE with the teaching triple rather than a spurious may-be-NaN wholeness complaint - profile-export param/return classes stay out of integer_slots by design — the attestation mirrors the document's own i64-spelled slots (the V10 bijection; abi.exports carries no TypeRefs) while an export's class is attested by the artifact's C signature under the same gate; the unconsumed-path refusal teaches this - regressions added: u64 attests u64 while the TypeRef spells i64, unproven update writes into a declared model field refuse SC4022/SC4023 by slot path, and guarded writes prove and attest --- packages/compiler/src/index.ts | 43 +++++++++-- packages/compiler/src/library/int-infer.ts | 19 ++++- packages/compiler/src/library/profile.ts | 14 ++-- .../compiler/src/library/sidecar-validate.ts | 2 +- packages/compiler/src/library/sidecar.ts | 29 +++++--- tests/harness/library-int.test.ts | 72 ++++++++++++++++++- 6 files changed, 154 insertions(+), 25 deletions(-) diff --git a/packages/compiler/src/index.ts b/packages/compiler/src/index.ts index e13028f76..b0504f200 100644 --- a/packages/compiler/src/index.ts +++ b/packages/compiler/src/index.ts @@ -962,8 +962,10 @@ function libraryIntSlotConfig(profile: LibraryProfile): IntSlotConfig { * slots map onto every interned IR shape whose field-name set matches * the projected record's — shapes intern structurally, so a same-shaped * second type shares the obligation (a sound over-approximation). A - * record fact that matches no shape binds nothing: the program never - * constructs the type, and the attestation holds vacuously. */ + * record fact that matches no shape binds nothing: no compiled code + * constructs the type (the contract surface — init/update/subscriptions + * and every helper — is force-lowered whenever integer slots are + * declared, so this is genuine vacuity, not dead-stripping). */ function mergeSidecarIntSlots(cfg: IntSlotConfig, facts: SidecarIntegerSlotFacts, mod: IrModule): IntSlotConfig { for (const h of facts.helpers) { const fn = mod.functions.find((f) => f.name === h.fnName); @@ -1072,6 +1074,31 @@ export async function compileLibrary(opts: CompileLibraryOptions): Promise 0) return fail(fe.preflight); + contractFacts = profile.sidecar !== null ? fe.entryContract() : null; + // Ask 4, contract-surface reachability: when the sidecar declares ANY + // integer slot, the designated init/update/subscriptions exports and + // every contract helper (model-first exported function) seed lowering + // too. They are attested surface — a declared record-field or msg-arm + // class obligates EVERY write those bodies perform, and a declared + // helper param is checked at their internal call sites — so the + // attestation must cover COMPILED bodies, never a dead-stripped + // vacuity (the bug this closes: a model-slot declaration whose only + // writers were dead-stripped attested without any proof). + const contractSurfaceRoots: string[] = []; + if (profile.sidecar !== null && profile.sidecar.integerSlots.length > 0) { + const sc = profile.sidecar; + const fnNames = new Set(contractFacts!.functions.filter((f) => !f.generic).map((f) => f.name)); + for (const name of [sc.initExport, sc.updateExport, sc.subscriptionsExport]) { + if (fnNames.has(name)) contractSurfaceRoots.push(name); + } + for (const fn of contractFacts!.functions) { + if (fn.generic) continue; + const first = fn.params[0]; + if (first !== undefined && first.shape !== null && first.shape.k === "ref" && first.shape.name === sc.model) { + contractSurfaceRoots.push(fn.name); + } + } + } try { lowered = fe.lower({ dynamic: false, @@ -1083,10 +1110,13 @@ export async function compileLibrary(opts: CompileLibraryOptions): Promise e.export), - ...(profile.sidecar?.integerSlots ?? []) - .map((s) => /^helpers\.([^.]+)\.(?:params\[\d+\]|return)$/.exec(s.slot)?.[1]) - .filter((n): n is string => n !== undefined), + ...new Set([ + ...profile.exports.map((e) => e.export), + ...(profile.sidecar?.integerSlots ?? []) + .map((s) => /^helpers\.([^.]+)\.(?:params\[\d+\]|return)$/.exec(s.slot)?.[1]) + .filter((n): n is string => n !== undefined), + ...contractSurfaceRoots, + ]), ], }); } catch (e) { @@ -1095,7 +1125,6 @@ export async function compileLibrary(opts: CompileLibraryOptions): Promise(); for (const e of integerSlots as unknown[]) { - if (!isDict(e) || typeof e["slot"] !== "string" || e["class"] !== "i64") { + if (!isDict(e) || typeof e["slot"] !== "string" || (e["class"] !== "i64" && e["class"] !== "u64")) { bad("V1", "integer_slots carries a malformed entry"); continue; } diff --git a/packages/compiler/src/library/sidecar.ts b/packages/compiler/src/library/sidecar.ts index 0ad2d83c5..876687780 100644 --- a/packages/compiler/src/library/sidecar.ts +++ b/packages/compiler/src/library/sidecar.ts @@ -34,7 +34,9 @@ * vocabulary — u64 is the stricter compile-time obligation over the same * wire spelling), refuses paths that resolve to no plain number slot, * and emits `integer_slots` as the resolved-decision list, in profile - * declaration order. The list is an ATTESTATION (schema §5's invariant): + * declaration order, each entry recording the DECLARED class ({i64, u64} + * — the flattening is TypeRef-only). The list is an ATTESTATION (schema + * §5's invariant): * compileLibrary runs the integer-boundary inference before writing any * artifact, so a sidecar carrying an entry means every value that can * reach that slot proved whole-in-range. Undeclared numeric slots keep @@ -129,7 +131,7 @@ export interface SidecarDoc { env_msgs: { env: string; msg: string }[]; }; abi: { prefix: string; exports: string[]; snapshot_format: number }; - integer_slots: { slot: string; class: "i64" }[]; + integer_slots: { slot: string; class: "i64" | "u64" }[]; deterministic: boolean; async_free: boolean; } @@ -378,7 +380,7 @@ class Projector { for (const [slot, cls] of this.intDeclared) { if (!this.intConsumed.has(slot)) { throw new SidecarError( - `the profile declares integer slot '${slot}' (${cls}), but the projected contract has no number slot at that path (paths: 'Type.field', 'Union.arm', '.arm', '.arm.numberField', 'helpers..params[i]', 'helpers..return')`, + `the profile declares integer slot '${slot}' (${cls}), but the projected contract has no number slot at that path (paths: 'Type.field', 'Union.arm', '.arm', '.arm.numberField', 'helpers..params[i]', 'helpers..return'; a profile export's integer class is declared on its 'exports' entry — the C signature itself attests it, never integer_slots)`, this.entryLoc, ); } @@ -977,16 +979,27 @@ export function buildSidecar(input: SidecarBuildInput): SidecarBuildResult { }, abi: { prefix: profile.prefix, exports, snapshot_format: config.snapshotFormat }, // Ask 4's resolved integer-class decisions, one entry per declared - // slot in profile declaration order, every one spelled i64 (the - // frozen format-1 vocabulary; a u64 declaration is the stricter - // compile-time obligation over the same wire spelling). The V10 + // slot in profile declaration order, each recording the DECLARED + // class ({i64, u64} — the integer_slots vocabulary; only the + // TypeRef/descriptor spellings above flatten to i64, the frozen + // format-1 type vocabulary, because unsigned-ness is a + // boundary-slot refinement, not a type-table concept). The V10 // bijection with the i64-spelled slots above holds by construction // (intify is the only i64 speller and checkIntConsumed just proved // every declaration was spelled). The list is an ATTESTATION: the // compiler refuses the build before writing any artifact when an // integer-slot proof fails, so a sidecar carrying these entries - // means every listed slot's obligations were discharged (§5). - integer_slots: config.integerSlots.map((e) => ({ slot: e.slot, class: "i64" as const })), + // means every listed slot's obligations — including u64's + // non-negative range — were discharged (§5). Profile-export + // param/return classes are deliberately ABSENT: integer_slots is + // the document-side complement (its entries mirror the document's + // own i64-spelled slots — V10), while an export's class is + // declared on the profile's exports entry and attested by the + // artifact's own C signature (int64_t/uint64_t) under the same + // prove-or-refuse gate; repeating it here would duplicate a fact + // the ABI already states and break the V10 bijection (abi.exports + // is a symbol list carrying no TypeRefs). + integer_slots: config.integerSlots.map((e) => ({ slot: e.slot, class: e.cls })), deterministic: input.deterministic, // Structural in library mode: the SC4005 gate refused any graph // reaching async/timer/event-loop surface before emission, so a diff --git a/tests/harness/library-int.test.ts b/tests/harness/library-int.test.ts index a17cb4851..8777e71d8 100644 --- a/tests/harness/library-int.test.ts +++ b/tests/harness/library-int.test.ts @@ -524,8 +524,9 @@ describe("ask-4 sidecar-declared slots", () => { types: { structs: { name: string; fields: { name: string; type: { kind: string } }[] }[] }; model_helpers: { name: string; returns: { kind: string } }[]; }; - // The resolved-decision list, profile declaration order, every entry - // spelled i64 (the frozen format-1 vocabulary). + // The resolved-decision list, profile declaration order, each entry + // recording its DECLARED class (all i64 here; the TypeRef spellings + // below are the frozen format-1 vocabulary). expect(doc.integer_slots).toEqual([ { slot: "Msg.count", class: "i64" }, { slot: "Model.total", class: "i64" }, @@ -540,6 +541,73 @@ describe("ask-4 sidecar-declared slots", () => { expect(validateSidecar(doc)).toEqual([]); }); + test("a u64 declaration attests u64; the TypeRef still spells i64", async () => { + // The attestation-level class: integer_slots records the DECLARED + // class in its own {i64, u64} vocabulary, while the frozen format-1 + // TypeRef keeps spelling i64 (unsigned-ness is a boundary-slot + // refinement, not a type-table concept). The regression pinned here: + // u64 declarations used to flatten to i64 in the attestation itself, + // misstating the discharged proof's domain. + const r = await buildCase("sidecar-u64-attest", SIDECAR_ENTRY, sidecarProfile([{ slot: "Model.total", class: "u64" }])); + expect(r.ok, r.ok ? "" : r.diagnostics.map((d) => `${d.code}: ${d.message}`).join("\n")).toBe(true); + if (!r.ok) return; + const doc = JSON.parse(readFileSync(r.sidecarPath!, "utf8")) as { + integer_slots: { slot: string; class: string }[]; + types: { structs: { name: string; fields: { name: string; type: { kind: string } }[] }[] }; + }; + expect(doc.integer_slots).toEqual([{ slot: "Model.total", class: "u64" }]); + expect(doc.types.structs.find((s) => s.name === "Model")!.fields.find((f) => f.name === "total")!.type).toEqual({ kind: "i64" }); + expect(validateSidecar(doc)).toEqual([]); + }); + + test("an unproven update write into a declared model field refuses by slot path", async () => { + // The model-slot prove-or-refuse gate: a declared Model field class + // obligates every write the contract surface performs — init and + // update are force-lowered so their record constructions enter the + // boundary check (the regression pinned here: dead-stripped + // init/update bodies let an unprovable write attest). + const broken = SIDECAR_ENTRY.replace( + "export function update(m: Model, msg: Msg): Model { return m; }", + "export function update(m: Model, msg: Msg): Model { return { total: m.total * 0.5, label: m.label }; }", + ); + const r = await buildCase("sidecar-refuse-model-update", broken, sidecarProfile([{ slot: "Model.total", class: "i64" }])); + expect(r.ok).toBe(false); + if (r.ok) return; + expect(r.diagnostics.map((d) => d.code)).toEqual(["SC4022"]); + expect(r.diagnostics[0]!.message).toContain("'Model.total'"); + expect(r.diagnostics[0]!.message).toContain("wholeness failed"); + expect(r.diagnostics[0]!.hint).toBeTruthy(); + }); + + test("an unbounded counter increment into a declared model field refuses range", async () => { + // The read side of the declared-slot contract: m.total reads back + // whole-in-class-range (every write was checked), so the unguarded + // increment fails RANGE — the counter may leave ±(2^53 − 1) — never a + // spurious NaN complaint. A clamped increment proves (next test). + const broken = SIDECAR_ENTRY.replace( + "export function update(m: Model, msg: Msg): Model { return m; }", + "export function update(m: Model, msg: Msg): Model { return { total: m.total + 1, label: m.label }; }", + ); + const r = await buildCase("sidecar-refuse-model-counter", broken, sidecarProfile([{ slot: "Model.total", class: "i64" }])); + expect(r.ok).toBe(false); + if (r.ok) return; + expect(r.diagnostics.map((d) => d.code)).toEqual(["SC4023"]); + expect(r.diagnostics[0]!.message).toContain("'Model.total'"); + expect(r.diagnostics[0]!.message).toContain("range failed"); + }); + + test("guarded model-field writes prove and the build attests them", async () => { + const guarded = SIDECAR_ENTRY.replace( + "export function update(m: Model, msg: Msg): Model { return m; }", + "export function update(m: Model, msg: Msg): Model { return { total: (m.total + 1) % 1000000, label: m.label }; }", + ); + const r = await buildCase("sidecar-prove-model", guarded, sidecarProfile([{ slot: "Model.total", class: "u64" }])); + expect(r.ok, r.ok ? "" : r.diagnostics.map((d) => `${d.code}: ${d.message}`).join("\n")).toBe(true); + if (!r.ok) return; + const doc = JSON.parse(readFileSync(r.sidecarPath!, "utf8")) as { integer_slots: { slot: string; class: string }[] }; + expect(doc.integer_slots).toEqual([{ slot: "Model.total", class: "u64" }]); + }); + test("an unproven write into a declared msg arm refuses by slot path", async () => { const broken = SIDECAR_ENTRY.replace("n: Math.trunc(v)", "n: v * 0.5"); const r = await buildCase("sidecar-refuse-arm", broken, sidecarProfile(DECLARED));