Record declared u64 classes in the sidecar attestation and prove model/msg slot writes

- 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

@@ -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<Compi
       );
     }
     if (fe.preflight.length > 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<Compi
         // must cover a COMPILED body, never a dead-stripped vacuity — the
         // sidecar advertises the slot's class, so the proof must exist.
         libRoots: [
-          ...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),
+          ...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<Compi
     }
     if (lowered.module === null) return fail(lowered.diagnostics);
     entryInfo = fe.entryExports();
-    contractFacts = profile.sidecar !== null ? fe.entryContract() : null;
     entryText = fe.entryText();
     sourceTexts = fe.sourceTexts();
   } finally {

packages/compiler/src/library/int-infer.ts

@@ -52,7 +52,12 @@
  * class range: i64 ⇒ ±(2^53−1), u64 ⇒ [0, 2^53−1], the u8/u32/i32
  * plumbing classes their C ranges); a call RESULT of a declared integer
  * return is likewise assumed whole-in-range (its own function's returns
- * are checked). External calls of the same slots are the wrapper's
+ * are checked). A declared RECORD FIELD works the same way: every write
+ * into the field (construction or assignment, in any function) is
+ * checked, and a read of the field is assumed whole-in-class-range —
+ * which is what makes `count: model.count + 1` a RANGE refusal (the
+ * unbounded counter may leave ±(2^53 − 1)) rather than a spurious
+ * NaN complaint. External calls of the same slots are the wrapper's
  * business (inbound integer parameters range-check at the marshalled
  * edge — index.ts assembles the host-contract trap). Undeclared function
  * boundaries stay TOP — the obligations are the contract; the strategy
@@ -1329,6 +1334,18 @@ class FnAnalyzer {
         }
         return { ...TOP };
       }
+      case "recordGet": {
+        // A declared record-field slot is an assumption on the read side,
+        // exactly like a declared parameter inside its callee: every write
+        // into the field discharged the class's obligations, so the value
+        // read back is whole and in class range (the read that lets
+        // `model.count + 1` refuse RANGE — the unbounded-counter teaching
+        // — instead of a spurious may-be-NaN wholeness refusal).
+        this.evalExpr(e.obj, env);
+        const slot = this.cfg.records.get(e.shapeId)?.get(e.field);
+        if (slot !== undefined && e.type.kind === "f64") return classSeed(slot.cls);
+        return { ...TOP };
+      }
       default: {
         for (const v of childExprs(e)) this.evalExpr(v, env);
         return { ...TOP };

packages/compiler/src/library/profile.ts

@@ -160,12 +160,14 @@ export interface LibrarySidecarConfig {
    * path grammar (`Msg.count`, `Point.x`, `helpers.clamp.params[0]`,
    * `helpers.clamp.return`). Each named slot must resolve to a NUMBER
    * slot of the projected contract (refused at sidecar build otherwise),
-   * is spelled i64 in the emitted document (the frozen format-1 TypeRef
-   * vocabulary has no u64 — a u64 declaration is the stricter
-   * compile-time obligation over the same wire spelling), joins
-   * `integer_slots`, and obligates every program-side value that can
-   * reach it to the prove-or-refuse check. Empty when the profile
-   * declares none. */
+   * is spelled i64 in the emitted document's TypeRef/descriptor (the
+   * frozen format-1 type vocabulary has no u64 — unsigned-ness is a
+   * boundary-slot refinement, not a type-table concept), joins
+   * `integer_slots` with its DECLARED class ({i64, u64} — the u64
+   * declaration is the stricter obligation, and the attestation records
+   * the class whose proof was discharged), and obligates every
+   * program-side value that can reach it to the prove-or-refuse check.
+   * Empty when the profile declares none. */
   integerSlots: { slot: string; cls: "i64" | "u64" }[];
 }
 

packages/compiler/src/library/sidecar-validate.ts

@@ -464,7 +464,7 @@ export function validateSidecar(doc: unknown): string[] {
   } else {
     const declared = new Set<string>();
     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;
       }

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', '<msg>.arm', '<msg>.arm.numberField', 'helpers.<name>.params[i]', 'helpers.<name>.return')`,
+          `the profile declares integer slot '${slot}' (${cls}), but the projected contract has no number slot at that path (paths: 'Type.field', 'Union.arm', '<msg>.arm', '<msg>.arm.numberField', 'helpers.<name>.params[i]', 'helpers.<name>.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

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));