mirror of
https://github.com/vercel-labs/scriptc.git
synced 2026-10-02 08:35:07 +08:00
The ask-4 conformance corpus end to end, with the sidecar attestation and inbound-trap fixtures
- tests/harness/library-int.test.ts: all 16 reference-corpus cases as library fixtures on both emissions — send/sendU64 are profile-mapped exports with i64/u64 params, PROVE cases pin every crossed value against the Node oracle (the test process runs the same case source), the counter loop crosses 0..9 in order, REFUSE cases name obligation, slot path, and evidence - int-returns fixture: i64/u64 returns cross as real int64_t/uint64_t (9007199254740991, -0 as 0, -7 % 3 as -1, ToUint32 max on a u64 slot) - int-trap fixture: inbound integers past 2^53-1 deliver the structured SC4012 host-contract trap with profile teaching/remediation; in-range extremes convert exactly - Sidecar slots: integer_slots attestation in declaration order, declared slots spelled i64 (V10 bijection validated), unproven writes refused by slot path (Msg.count, helpers.clampIdx.return), unresolvable and non-number declarations refused SC4009, teachings ride SC4022 as attributed notes - Layer-1 differential: no Layer-1 representation exists (trivially unobservable); pinned consequence — f64-declared vs i64-declared builds cross byte-identical values - Integer-declared helpers join libRoots so their attestation covers a compiled body, never a dead-stripped vacuity
This commit is contained in:
Chris Tate
@@ -1077,8 +1077,16 @@ export async function compileLibrary(opts: CompileLibraryOptions): Promise<Compi
|
||||
targetPlatform: buildTargetPlatform(),
|
||||
// The profile-mapped exports are called from OUTSIDE the graph:
|
||||
// they seed reachability beside the entry's top level (an
|
||||
// executable build would dead-strip an uncalled export).
|
||||
libRoots: profile.exports.map((e) => e.export),
|
||||
// executable build would dead-strip an uncalled export). A helper
|
||||
// with a declared integer slot (ask 4) seeds too: its attestation
|
||||
// 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),
|
||||
],
|
||||
});
|
||||
} catch (e) {
|
||||
if (!isCheckerPanic(e)) throw e;
|
||||
|
||||
@@ -0,0 +1,556 @@
|
||||
/* Ask 4 end to end — profile-declared i64/u64 integer boundary slots with
|
||||
* compile-time prove-or-refuse inference, over the REAL pipeline
|
||||
* (frontend lowering, both emissions, real archives, real probes):
|
||||
*
|
||||
* corpus the reference package's §3 conformance corpus, all 16
|
||||
* cases as library fixtures: `send(x)`/`sendU64(x)` are
|
||||
* profile-mapped exports whose parameter the profile
|
||||
* declares i64/u64, so every internal call site is a
|
||||
* declared-slot crossing. PROVE cases compile on both
|
||||
* emissions and every crossed value equals the Node
|
||||
* oracle's number exactly (this test process IS Node — the
|
||||
* oracle runs the same case source); REFUSE cases name the
|
||||
* listed obligation with the slot path and evidence, on
|
||||
* both emissions (the verdict is emission-invariant).
|
||||
* returns the outbound declared-integer edge: i64/u64 RETURNS
|
||||
* cross as real int64_t/uint64_t through the C ABI, pinned
|
||||
* against the oracle's singletons (9007199254740991, 0 for
|
||||
* -0, -1 for -7 % 3, 4294967295).
|
||||
* inbound trap the host-contract edge: an inbound i64/u64 past
|
||||
* ±(2^53 − 1) cannot ride f64 exactly, so the wrapper
|
||||
* delivers the structured SC4012 trap (profile teaching +
|
||||
* remediation riding it) instead of silently rounding;
|
||||
* in-range extremes convert exactly.
|
||||
* sidecar sidecar-declared slots (msg arms, record fields, helper
|
||||
* params/returns): integer_slots emitted as the resolved
|
||||
* attestation in declaration order, the declared slots
|
||||
* spelled i64 in the document (V10 bijection), program-side
|
||||
* writes proven or refused by slot path, and unresolvable
|
||||
* or non-number declarations refused at projection.
|
||||
* layer 1 the unobservability differential: scriptc implements NO
|
||||
* Layer-1 integer representation, so the reference
|
||||
* package's on/off differential is trivially satisfied;
|
||||
* what CAN be pinned is the observable consequence — the
|
||||
* same program compiled with the slot declared f64 vs i64
|
||||
* crosses byte-identical values (declaring a slot adds
|
||||
* proofs and wrapper conversions, never new semantics).
|
||||
*/
|
||||
import { execFileSync, spawnSync } from "node:child_process";
|
||||
import { mkdirSync, readFileSync, writeFileSync } from "node:fs";
|
||||
import { join } from "node:path";
|
||||
import { describe, expect, test } from "vitest";
|
||||
import { compileLibrary, validateSidecar } from "@scriptc/compiler";
|
||||
|
||||
const repoRoot = join(import.meta.dirname, "../..");
|
||||
const fixtureRoot = join(repoRoot, "tests/library-mode");
|
||||
const flavor = process.env["SCRIPTC_SAN"] === "1" ? "san" : "plain";
|
||||
const cacheDir = join(repoRoot, "node_modules/.cache/scriptc-tests/library-int", flavor);
|
||||
|
||||
type Emission = "llvm" | "c";
|
||||
const EMISSIONS: Emission[] = ["llvm", "c"];
|
||||
|
||||
/* ── the corpus (reference package §3, sources verbatim) ─────────────────
|
||||
* `body` is the case's program text: top-level statements, or the body of
|
||||
* `export function f(a: number): void` when `param` is set. The oracle
|
||||
* executes the same text in this Node process. */
|
||||
interface CorpusCase {
|
||||
name: string;
|
||||
body: string;
|
||||
param?: boolean;
|
||||
/** Host-side arguments fed to f through the wrapper (PROVE cases). */
|
||||
args?: string[];
|
||||
expected: "prove" | "refuse";
|
||||
obligation?: "representability" | "wholeness" | "range";
|
||||
code?: string;
|
||||
slot?: string;
|
||||
evidence?: string[];
|
||||
}
|
||||
|
||||
const CORPUS: CorpusCase[] = [
|
||||
{
|
||||
name: "max-safe-integer-exact",
|
||||
body: `send(2 ** 53 - 1);`,
|
||||
expected: "prove",
|
||||
},
|
||||
{
|
||||
name: "literal-not-representable",
|
||||
body: `send(9007199254740993);`,
|
||||
expected: "refuse",
|
||||
obligation: "representability",
|
||||
code: "SC4021",
|
||||
slot: "exports.send.params[0]",
|
||||
// The refusal fires on the SPELLING, and the evidence names both the
|
||||
// author's text and its f64 read-back.
|
||||
evidence: ["9007199254740993", "reads back as 9007199254740992"],
|
||||
},
|
||||
{
|
||||
name: "proven-range-overflow",
|
||||
body: `if (a >= 0 && a <= 2 ** 30) {\n const t = Math.trunc(a);\n send(t * t);\n}`,
|
||||
param: true,
|
||||
expected: "refuse",
|
||||
obligation: "range",
|
||||
code: "SC4023",
|
||||
slot: "exports.send.params[0]",
|
||||
evidence: ["±(2^53 − 1)"],
|
||||
},
|
||||
{
|
||||
name: "negative-zero-crosses-as-zero",
|
||||
body: `send(-0);`,
|
||||
expected: "prove",
|
||||
},
|
||||
{
|
||||
name: "times-half-unprovable",
|
||||
body: `if (a >= 0 && a <= 1000) {\n const t = a * 0.5;\n send(t);\n}`,
|
||||
param: true,
|
||||
expected: "refuse",
|
||||
obligation: "wholeness",
|
||||
code: "SC4022",
|
||||
slot: "exports.send.params[0]",
|
||||
// The guard already proved the range and excluded NaN: the ONLY
|
||||
// failed obligation is wholeness, and the evidence says so.
|
||||
evidence: ["[0, 500]", "non-integers"],
|
||||
},
|
||||
{
|
||||
name: "times-half-with-trunc",
|
||||
body: `if (a >= 0 && a <= 1000) {\n const t = a * 0.5;\n send(Math.trunc(t));\n}`,
|
||||
param: true,
|
||||
args: ["0", "999", "1000", "500.5", "-3"],
|
||||
expected: "prove",
|
||||
},
|
||||
{
|
||||
name: "bounded-counter-loop",
|
||||
body: `for (let n = 0; n < 10; n = n + 1) {\n send(n);\n}`,
|
||||
expected: "prove", // the precision gate: 0..9 in order, pinned below
|
||||
},
|
||||
{
|
||||
name: "division-non-integer",
|
||||
body: `send(7 / 2);`,
|
||||
expected: "refuse",
|
||||
obligation: "wholeness",
|
||||
code: "SC4022",
|
||||
slot: "exports.send.params[0]",
|
||||
},
|
||||
{
|
||||
name: "remainder-negative-dividend",
|
||||
body: `send(-7 % 3);`,
|
||||
expected: "prove",
|
||||
},
|
||||
{
|
||||
name: "bitwise-or-int32",
|
||||
body: `send(a | 0);`,
|
||||
param: true,
|
||||
args: ["3.7", "-2.5", "nan", "1e300", "4294967297"],
|
||||
expected: "prove",
|
||||
},
|
||||
{
|
||||
name: "unsigned-shift-u64",
|
||||
body: `sendU64(a >>> 0);`,
|
||||
param: true,
|
||||
args: ["5.9", "-1", "nan", "4294967295"],
|
||||
expected: "prove",
|
||||
},
|
||||
{
|
||||
name: "u64-negative-proven-range",
|
||||
body: `if (a >= -100 && a <= 100) {\n sendU64(Math.trunc(a));\n}`,
|
||||
param: true,
|
||||
expected: "refuse",
|
||||
obligation: "range",
|
||||
code: "SC4023",
|
||||
slot: "exports.sendU64.params[0]",
|
||||
evidence: ["[-100, 100]", "non-negative"],
|
||||
},
|
||||
{
|
||||
name: "conditional-range-refinement",
|
||||
body: `if (a >= 2 && a <= 6) {\n send(Math.round(a));\n}`,
|
||||
param: true,
|
||||
args: ["2", "5.4", "6", "1", "nan"],
|
||||
expected: "prove",
|
||||
},
|
||||
{
|
||||
name: "data-dependent-loop-bound",
|
||||
body: `for (let n = 0; n < a; n = n + 1) {\n send(n);\n}`,
|
||||
param: true,
|
||||
expected: "refuse",
|
||||
obligation: "range",
|
||||
code: "SC4023",
|
||||
slot: "exports.send.params[0]",
|
||||
},
|
||||
{
|
||||
name: "nan-reaches-slot",
|
||||
body: `send(0 / 0);`,
|
||||
expected: "refuse",
|
||||
obligation: "wholeness",
|
||||
code: "SC4022",
|
||||
slot: "exports.send.params[0]",
|
||||
evidence: ["NaN"],
|
||||
},
|
||||
{
|
||||
name: "infinity-reaches-slot",
|
||||
body: `send(1 / 0);`,
|
||||
expected: "refuse",
|
||||
obligation: "range",
|
||||
code: "SC4023",
|
||||
slot: "exports.send.params[0]",
|
||||
evidence: ["Infinity"],
|
||||
},
|
||||
];
|
||||
|
||||
const PRELUDE = `let crossed: number[] = [];
|
||||
export function send(x: number): void { crossed.push(x); }
|
||||
export function sendU64(x: number): void { crossed.push(x); }
|
||||
export function count(): number { return crossed.length; }
|
||||
export function at(i: number): number { return crossed[i]; }
|
||||
`;
|
||||
|
||||
function corpusSource(c: CorpusCase): string {
|
||||
return c.param === true ? `${PRELUDE}export function f(a: number): void {\n${c.body}\n}\n` : `${PRELUDE}${c.body}\n`;
|
||||
}
|
||||
|
||||
function corpusProfile(c: CorpusCase, emission: Emission, entry: string, sendClass = "i64"): object {
|
||||
return {
|
||||
profile_format: 1,
|
||||
name: "int-corpus",
|
||||
entry,
|
||||
emission,
|
||||
abi: {
|
||||
prefix: "kc_",
|
||||
init_symbol: "kc_init",
|
||||
sink_register_symbol: "kc_set_panic_sink",
|
||||
collect_symbol: null,
|
||||
result_reset_symbol: null,
|
||||
},
|
||||
exports: [
|
||||
{ export: "send", symbol: "kc_send", params: [sendClass], returns: "void" },
|
||||
{ export: "sendU64", symbol: "kc_send_u64", params: ["u64"], returns: "void" },
|
||||
{ export: "count", symbol: "kc_count", params: [], returns: "f64" },
|
||||
{ export: "at", symbol: "kc_at", params: ["f64"], returns: "f64" },
|
||||
...(c.param === true ? [{ export: "f", symbol: "kc_f", params: ["f64"], returns: "void" }] : []),
|
||||
],
|
||||
};
|
||||
}
|
||||
|
||||
/** The Node oracle: this test process runs the SAME case source and
|
||||
* records what crossed. Number(arg) mirrors the probe's strtod. */
|
||||
function nodeOracle(c: CorpusCase): number[] {
|
||||
const crossed: number[] = [];
|
||||
const send = (x: number): void => {
|
||||
crossed.push(x);
|
||||
};
|
||||
// eslint-disable-next-line @typescript-eslint/no-implied-eval
|
||||
const fn = new Function("send", "sendU64", "a", c.body) as (s: unknown, u: unknown, a?: number) => void;
|
||||
if (c.param === true) {
|
||||
for (const a of c.args ?? []) fn(send, send, Number(a));
|
||||
} else {
|
||||
fn(send, send);
|
||||
}
|
||||
return crossed;
|
||||
}
|
||||
|
||||
async function buildCase(tag: string, source: string, profile: object): Promise<
|
||||
| { ok: true; archive: string; outDir: string; sidecarPath?: string }
|
||||
| { ok: false; diagnostics: { code: string; message: string; hint?: string; note?: string }[] }
|
||||
> {
|
||||
const outDir = join(cacheDir, tag);
|
||||
mkdirSync(outDir, { recursive: true });
|
||||
const entry = join(outDir, "lib.ts");
|
||||
writeFileSync(entry, source);
|
||||
const profilePath = join(outDir, "profile.json");
|
||||
writeFileSync(profilePath, JSON.stringify({ ...profile, entry }, null, 2));
|
||||
const result = await compileLibrary({ profilePath, outDir });
|
||||
if (!result.ok) {
|
||||
return {
|
||||
ok: false,
|
||||
diagnostics: result.diagnostics.map((d) => ({
|
||||
code: d.code,
|
||||
message: d.message,
|
||||
...(d.hint !== undefined ? { hint: d.hint } : {}),
|
||||
...(d.note !== undefined ? { note: d.note } : {}),
|
||||
})),
|
||||
};
|
||||
}
|
||||
return {
|
||||
ok: true,
|
||||
archive: result.archivePath,
|
||||
outDir,
|
||||
...(result.sidecarPath !== undefined ? { sidecarPath: result.sidecarPath } : {}),
|
||||
};
|
||||
}
|
||||
|
||||
function buildProbe(probeSrc: string, archive: string, outDir: string, defines: string[] = []): string {
|
||||
const bin = join(outDir, "probe");
|
||||
execFileSync("clang", ["-std=c11", ...defines.map((d) => `-D${d}`), probeSrc, archive, "-lm", "-o", bin]);
|
||||
return bin;
|
||||
}
|
||||
|
||||
function runProbe(bin: string, args: string[] = []): { stdout: string; status: number | null; signal: string | null } {
|
||||
const r = spawnSync(bin, args, { encoding: "utf8", timeout: 60_000 });
|
||||
return { stdout: r.stdout ?? "", status: r.status, signal: r.signal };
|
||||
}
|
||||
|
||||
/* ── the corpus, both emissions ──────────────────────────────────────── */
|
||||
|
||||
describe.each(EMISSIONS)("ask-4 corpus, %s emission", (emission) => {
|
||||
for (const c of CORPUS) {
|
||||
test(`${c.name} — ${c.expected.toUpperCase()}${c.obligation !== undefined ? ` (${c.obligation})` : ""}`, async () => {
|
||||
const r = await buildCase(`corpus-${c.name}-${emission}`, corpusSource(c), corpusProfile(c, emission, "lib.ts"));
|
||||
if (c.expected === "refuse") {
|
||||
expect(r.ok).toBe(false);
|
||||
if (r.ok) return;
|
||||
expect(r.diagnostics.map((d) => d.code)).toEqual([c.code]);
|
||||
const d = r.diagnostics[0]!;
|
||||
// The teaching triple: the slot path, the failed obligation, the
|
||||
// evidence, and (as the hint) the author's fix.
|
||||
expect(d.message).toContain(`'${c.slot}'`);
|
||||
expect(d.message).toContain(`${c.obligation} failed`);
|
||||
for (const ev of c.evidence ?? []) expect(d.message).toContain(ev);
|
||||
expect(d.hint).toBeTruthy();
|
||||
return;
|
||||
}
|
||||
expect(r.ok, r.ok ? "" : r.diagnostics.map((d) => `${d.code}: ${d.message}`).join("\n")).toBe(true);
|
||||
if (!r.ok) return;
|
||||
// The crossing values, pinned against the Node oracle exactly —
|
||||
// this process IS Node, running the same case source.
|
||||
const probe = buildProbe(join(fixtureRoot, "int-corpus/probe.c"), r.archive, r.outDir, c.param === true ? ["HAS_F"] : []);
|
||||
const run = runProbe(probe, c.param === true ? (c.args ?? []) : []);
|
||||
expect(run.signal).toBeNull();
|
||||
expect(run.status).toBe(0);
|
||||
const got = run.stdout.split("\n").filter((l) => l !== "").map(Number);
|
||||
const want = nodeOracle(c);
|
||||
expect(got.length).toBe(want.length);
|
||||
got.forEach((v, i) => {
|
||||
expect(Object.is(v, want[i]), `crossing ${i}: got ${v}, Node says ${want[i]}`).toBe(true);
|
||||
});
|
||||
if (c.name === "bounded-counter-loop") {
|
||||
// The precision gate's runtime half: 0 through 9, in order.
|
||||
expect(got).toEqual([0, 1, 2, 3, 4, 5, 6, 7, 8, 9]);
|
||||
}
|
||||
});
|
||||
}
|
||||
|
||||
/* ── outbound integer returns: real int64_t/uint64_t crossings ─────── */
|
||||
|
||||
test("declared integer returns cross as exact int64_t/uint64_t", async () => {
|
||||
const dir = join(fixtureRoot, "int-returns");
|
||||
const outDir = join(cacheDir, `int-returns-${emission}`);
|
||||
mkdirSync(outDir, { recursive: true });
|
||||
const profile = JSON.parse(readFileSync(join(dir, "profile.json"), "utf8")) as { entry: string; emission: string };
|
||||
profile.emission = emission;
|
||||
profile.entry = join(dir, profile.entry);
|
||||
const profilePath = join(outDir, "profile.json");
|
||||
writeFileSync(profilePath, JSON.stringify(profile));
|
||||
const result = await compileLibrary({ profilePath, outDir });
|
||||
if (!result.ok) throw new Error(result.diagnostics.map((d) => `${d.code}: ${d.message}`).join("\n"));
|
||||
const probe = buildProbe(join(dir, "probe.c"), result.archivePath, outDir);
|
||||
const run = runProbe(probe);
|
||||
expect(run.signal).toBeNull();
|
||||
expect(run.status).toBe(0);
|
||||
// The Node oracle's numbers, converted exactly: 2**53-1, -0 as the
|
||||
// mathematically exact integer 0, JS remainder's -1, ToUint32's max.
|
||||
expect(run.stdout).toBe(`max=9007199254740991\nnegzero=0\nrem=-1\nu32max=4294967295\n`);
|
||||
});
|
||||
|
||||
/* ── the inbound host-contract trap ─────────────────────────────────── */
|
||||
|
||||
test("an inbound integer past 2^53−1 traps SC4012; in-range extremes convert exactly", async () => {
|
||||
const dir = join(fixtureRoot, "int-trap");
|
||||
const outDir = join(cacheDir, `int-trap-${emission}`);
|
||||
mkdirSync(outDir, { recursive: true });
|
||||
const profile = JSON.parse(readFileSync(join(dir, "profile.json"), "utf8")) as { entry: string; emission: string };
|
||||
profile.emission = emission;
|
||||
profile.entry = join(dir, profile.entry);
|
||||
const profilePath = join(outDir, "profile.json");
|
||||
writeFileSync(profilePath, JSON.stringify(profile));
|
||||
const result = await compileLibrary({ profilePath, outDir });
|
||||
if (!result.ok) throw new Error(result.diagnostics.map((d) => `${d.code}: ${d.message}`).join("\n"));
|
||||
const probe = buildProbe(join(dir, "probe.c"), result.archivePath, outDir);
|
||||
|
||||
const ok = runProbe(probe, ["ok"]);
|
||||
expect(ok.signal).toBeNull();
|
||||
expect(ok.status).toBe(0);
|
||||
expect(ok.stdout).toBe(
|
||||
`i64 max: 9007199254740991\ni64 min: -9007199254740991\nu64 max: 9007199254740991\nok, sink_calls=0\n`,
|
||||
);
|
||||
|
||||
for (const mode of ["trap-i64", "trap-u64"] as const) {
|
||||
const run = runProbe(probe, [mode]);
|
||||
expect(run.signal).toBeNull();
|
||||
expect(run.status).toBe(0);
|
||||
// The structured SC4012 message: the profile's teaching as the
|
||||
// text, the code, the trapping export's symbol, the remediation —
|
||||
// and the host survives (nothing was silently rounded).
|
||||
expect(run.stdout).toBe(
|
||||
`sink[1]:
|
||||
text=[this core's integer channel carries at most 2^53 - 1]
|
||||
code=[SC4012]
|
||||
symbol=[${mode === "trap-i64" ? "kt_take" : "kt_take_u"}]
|
||||
remediation=[keep host-side ids within the exact-integer range]
|
||||
fields=4
|
||||
survived, sink_calls=1
|
||||
`,
|
||||
);
|
||||
}
|
||||
});
|
||||
|
||||
/* ── Layer-1 unobservability ────────────────────────────────────────── */
|
||||
|
||||
test("declaring the slot integer changes no program output (Layer 1 differential)", async () => {
|
||||
// scriptc implements NO Layer-1 integer representation (semantics
|
||||
// stay f64, byte-exact to Node), so the reference's on/off flip is
|
||||
// trivially satisfied; the observable consequence pinned here: the
|
||||
// SAME program under an f64-declared and an i64-declared send slot
|
||||
// crosses byte-identical values — the declaration adds proofs and
|
||||
// wrapper conversions, never semantics.
|
||||
const loop = CORPUS.find((c) => c.name === "bounded-counter-loop")!;
|
||||
const outputs: string[] = [];
|
||||
for (const cls of ["f64", "i64"]) {
|
||||
const r = await buildCase(
|
||||
`layer1-${cls}-${emission}`,
|
||||
corpusSource(loop),
|
||||
corpusProfile(loop, emission, "lib.ts", cls),
|
||||
);
|
||||
expect(r.ok).toBe(true);
|
||||
if (!r.ok) return;
|
||||
const probe = buildProbe(join(fixtureRoot, "int-corpus/probe.c"), r.archive, r.outDir);
|
||||
const run = runProbe(probe);
|
||||
expect(run.status).toBe(0);
|
||||
outputs.push(run.stdout);
|
||||
}
|
||||
expect(outputs[1]).toBe(outputs[0]);
|
||||
});
|
||||
});
|
||||
|
||||
/* ── sidecar-declared slots (msg arms, record fields, helpers) ───────────
|
||||
* The projection resolves the profile's sidecar.integer_slots, spells the
|
||||
* declared slots i64, emits the attestation list, and the inference
|
||||
* proves every program-side write. Refusals are pre-emission and pinned
|
||||
* emission-invariant by the corpus above, so one lane suffices here. */
|
||||
|
||||
const SIDECAR_ENTRY = `export interface Model { total: number; label: string; }
|
||||
export type Msg = { kind: "count"; n: number } | { kind: "clear" };
|
||||
export function init(): Model { return { total: 0, label: "" }; }
|
||||
export function update(m: Model, msg: Msg): Model { return m; }
|
||||
let last: Msg = { kind: "clear" };
|
||||
export function poke(v: number): void {
|
||||
if (v >= 0 && v <= 100) { last = { kind: "count", n: Math.trunc(v) }; }
|
||||
}
|
||||
export function lastN(): number { return last.kind === "count" ? last.n : -1; }
|
||||
export function clampIdx(m: Model, i: number): number { return i | 0; }
|
||||
`;
|
||||
|
||||
function sidecarProfile(integerSlots: object[], patch: Record<string, unknown> = {}): object {
|
||||
return {
|
||||
profile_format: 1,
|
||||
name: "int-sidecar",
|
||||
entry: "lib.ts",
|
||||
emission: "c",
|
||||
abi: {
|
||||
prefix: "ks_",
|
||||
init_symbol: "ks_init",
|
||||
sink_register_symbol: "ks_set_panic_sink",
|
||||
collect_symbol: null,
|
||||
result_reset_symbol: null,
|
||||
},
|
||||
exports: [
|
||||
{ export: "poke", symbol: "ks_poke", params: ["f64"], returns: "void" },
|
||||
{ export: "lastN", symbol: "ks_last_n", params: [], returns: "f64" },
|
||||
],
|
||||
sidecar: {
|
||||
wire_version: 3,
|
||||
abi_version: 1,
|
||||
snapshot_format: 1,
|
||||
build_id_symbol: "ks_build_id",
|
||||
abi_version_symbol: "ks_abi_version",
|
||||
model: "Model",
|
||||
msg: "Msg",
|
||||
integer_slots: integerSlots,
|
||||
},
|
||||
...patch,
|
||||
};
|
||||
}
|
||||
|
||||
describe("ask-4 sidecar-declared slots", () => {
|
||||
const DECLARED = [
|
||||
{ slot: "Msg.count", class: "i64" },
|
||||
{ slot: "Model.total", class: "i64" },
|
||||
{ slot: "helpers.clampIdx.return", class: "i64" },
|
||||
];
|
||||
|
||||
test("integer_slots attest the declared classes; declared slots spell i64", async () => {
|
||||
const r = await buildCase("sidecar-ok", SIDECAR_ENTRY, sidecarProfile(DECLARED));
|
||||
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 }[];
|
||||
msg: { arms: { name: string; payload: { kind: string; class?: string } }[] };
|
||||
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).
|
||||
expect(doc.integer_slots).toEqual([
|
||||
{ slot: "Msg.count", class: "i64" },
|
||||
{ slot: "Model.total", class: "i64" },
|
||||
{ slot: "helpers.clampIdx.return", class: "i64" },
|
||||
]);
|
||||
expect(doc.msg.arms.find((a) => a.name === "count")!.payload).toEqual({ kind: "number", class: "i64" });
|
||||
const model = doc.types.structs.find((s) => s.name === "Model")!;
|
||||
expect(model.fields.find((f) => f.name === "total")!.type).toEqual({ kind: "i64" });
|
||||
expect(model.fields.find((f) => f.name === "label")!.type).toEqual({ kind: "bytes" });
|
||||
expect(doc.model_helpers.find((h) => h.name === "clampIdx")!.returns).toEqual({ kind: "i64" });
|
||||
// The document conforms end to end (V10's bijection included).
|
||||
expect(validateSidecar(doc)).toEqual([]);
|
||||
});
|
||||
|
||||
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));
|
||||
expect(r.ok).toBe(false);
|
||||
if (r.ok) return;
|
||||
expect(r.diagnostics.map((d) => d.code)).toEqual(["SC4022"]);
|
||||
expect(r.diagnostics[0]!.message).toContain("'Msg.count'");
|
||||
expect(r.diagnostics[0]!.message).toContain("wholeness failed");
|
||||
});
|
||||
|
||||
test("an unproven declared helper return refuses by slot path", async () => {
|
||||
const broken = SIDECAR_ENTRY.replace("return i | 0;", "return i * 0.5;");
|
||||
const r = await buildCase("sidecar-refuse-helper", broken, sidecarProfile(DECLARED));
|
||||
expect(r.ok).toBe(false);
|
||||
if (r.ok) return;
|
||||
expect(r.diagnostics.map((d) => d.code)).toEqual(["SC4022"]);
|
||||
expect(r.diagnostics[0]!.message).toContain("'helpers.clampIdx.return'");
|
||||
});
|
||||
|
||||
test("a declared path resolving to no slot refuses at projection", async () => {
|
||||
const r = await buildCase("sidecar-refuse-nopath", SIDECAR_ENTRY, sidecarProfile([{ slot: "Msg.nope", class: "i64" }]));
|
||||
expect(r.ok).toBe(false);
|
||||
if (r.ok) return;
|
||||
expect(r.diagnostics.map((d) => d.code)).toEqual(["SC4009"]);
|
||||
expect(r.diagnostics[0]!.message).toContain("'Msg.nope'");
|
||||
expect(r.diagnostics[0]!.message).toContain("no number slot");
|
||||
});
|
||||
|
||||
test("a declared path naming a non-number slot refuses at projection", async () => {
|
||||
const r = await buildCase("sidecar-refuse-nonnum", SIDECAR_ENTRY, sidecarProfile([{ slot: "Model.label", class: "u64" }]));
|
||||
expect(r.ok).toBe(false);
|
||||
if (r.ok) return;
|
||||
expect(r.diagnostics.map((d) => d.code)).toEqual(["SC4009"]);
|
||||
expect(r.diagnostics[0]!.message).toContain("not a plain number slot");
|
||||
});
|
||||
|
||||
test("a profile teaching rides an integer refusal as the attributed note", async () => {
|
||||
const broken = SIDECAR_ENTRY.replace("n: Math.trunc(v)", "n: v * 0.5");
|
||||
const r = await buildCase(
|
||||
"sidecar-refuse-teach",
|
||||
broken,
|
||||
sidecarProfile(DECLARED, {
|
||||
determinism: { teachings: { SC4022: "counters in this core are integral by contract; truncate before posting" } },
|
||||
}),
|
||||
);
|
||||
expect(r.ok).toBe(false);
|
||||
if (r.ok) return;
|
||||
expect(r.diagnostics[0]!.code).toBe("SC4022");
|
||||
expect(r.diagnostics[0]!.note).toBe(
|
||||
"from the 'int-sidecar' profile: counters in this core are integral by contract; truncate before posting",
|
||||
);
|
||||
});
|
||||
});
|
||||
@@ -0,0 +1,46 @@
|
||||
/* Generic driver for the ask-4 conformance corpus (library-int.test.ts):
|
||||
* every corpus fixture records what crossed its declared integer slot in
|
||||
* a module array; the probe replays the host side — optionally feeding
|
||||
* the case's parameter function (compiled with -DHAS_F) the argv values —
|
||||
* and prints each crossed value on its own line with %.17g (exact for
|
||||
* every integer within ±(2^53 − 1)). The suite compares the lines against
|
||||
* the Node oracle's numbers computed from the same case source. */
|
||||
#include <setjmp.h>
|
||||
#include <stddef.h>
|
||||
#include <stdint.h>
|
||||
#include <stdio.h>
|
||||
#include <stdlib.h>
|
||||
|
||||
extern void kc_init(void);
|
||||
extern void kc_set_panic_sink(void (*fn)(void *, const uint8_t *, size_t, uint64_t), void *ctx);
|
||||
extern double kc_count(void);
|
||||
extern double kc_at(double i);
|
||||
#ifdef HAS_F
|
||||
extern void kc_f(double a);
|
||||
#endif
|
||||
|
||||
static jmp_buf trap_jmp;
|
||||
|
||||
static void sink(void *ctx, const uint8_t *msg, size_t len, uint64_t addr) {
|
||||
(void)ctx;
|
||||
(void)addr;
|
||||
printf("sink: %.*s\n", (int)len, (const char *)msg);
|
||||
longjmp(trap_jmp, 1);
|
||||
}
|
||||
|
||||
int main(int argc, char **argv) {
|
||||
(void)argc;
|
||||
(void)argv;
|
||||
kc_set_panic_sink(sink, NULL);
|
||||
if (setjmp(trap_jmp) != 0) {
|
||||
printf("trapped\n");
|
||||
return 1;
|
||||
}
|
||||
kc_init();
|
||||
#ifdef HAS_F
|
||||
for (int i = 1; i < argc; i++) kc_f(strtod(argv[i], NULL));
|
||||
#endif
|
||||
double n = kc_count();
|
||||
for (double i = 0; i < n; i++) printf("%.17g\n", kc_at(i));
|
||||
return 0;
|
||||
}
|
||||
@@ -0,0 +1,29 @@
|
||||
/* Ask 4's outbound declared-integer returns: each export's return slot is
|
||||
* profile-declared i64 (u64 for the unsigned one), so every value below
|
||||
* must PROVE whole-in-range at compile time — and the wrapper's
|
||||
* fp-to-int conversion then carries the mathematically exact integer the
|
||||
* f64 held (the probe reads real int64_t/uint64_t and pins the corpus's
|
||||
* singleton crossing values against the Node oracle). */
|
||||
|
||||
// The largest safe integer crosses exactly (corpus case 1 at the real edge).
|
||||
export function retMax(): number {
|
||||
return 2 ** 53 - 1;
|
||||
}
|
||||
|
||||
// -0 is whole: the sign of zero is f64-interior; the mathematically
|
||||
// exact integer 0 crosses (corpus case 4 at the real edge).
|
||||
export function retNegZero(): number {
|
||||
return -0;
|
||||
}
|
||||
|
||||
// JS remainder: the sign follows the dividend — -7 % 3 is exactly -1,
|
||||
// not 2 (corpus case 9 at the real edge).
|
||||
export function retRem(): number {
|
||||
return -7 % 3;
|
||||
}
|
||||
|
||||
// ToUint32 by the program's own >>> 0: whole, non-negative, uint32 —
|
||||
// satisfies a u64 slot (corpus case 11 at the real edge).
|
||||
export function retU32Max(): number {
|
||||
return 4294967295 >>> 0;
|
||||
}
|
||||
@@ -0,0 +1,31 @@
|
||||
/* The outbound declared-integer crossings, read as REAL int64_t/uint64_t
|
||||
* through the profile's C ABI: each printed value must equal the Node
|
||||
* oracle's number converted exactly (the compile-time proof is what makes
|
||||
* the fp-to-int conversion exact by construction). */
|
||||
#include <inttypes.h>
|
||||
#include <stddef.h>
|
||||
#include <stdint.h>
|
||||
#include <stdio.h>
|
||||
|
||||
extern void kr_init(void);
|
||||
extern void kr_set_panic_sink(void (*fn)(void *, const uint8_t *, size_t, uint64_t), void *ctx);
|
||||
extern int64_t kr_ret_max(void);
|
||||
extern int64_t kr_ret_neg_zero(void);
|
||||
extern int64_t kr_ret_rem(void);
|
||||
extern uint64_t kr_ret_u32_max(void);
|
||||
|
||||
static void sink(void *ctx, const uint8_t *msg, size_t len, uint64_t addr) {
|
||||
(void)ctx;
|
||||
(void)addr;
|
||||
printf("sink: %.*s\n", (int)len, (const char *)msg);
|
||||
}
|
||||
|
||||
int main(void) {
|
||||
kr_set_panic_sink(sink, NULL);
|
||||
kr_init();
|
||||
printf("max=%" PRId64 "\n", kr_ret_max());
|
||||
printf("negzero=%" PRId64 "\n", kr_ret_neg_zero());
|
||||
printf("rem=%" PRId64 "\n", kr_ret_rem());
|
||||
printf("u32max=%" PRIu64 "\n", kr_ret_u32_max());
|
||||
return 0;
|
||||
}
|
||||
@@ -0,0 +1,19 @@
|
||||
{
|
||||
"profile_format": 1,
|
||||
"name": "int-returns",
|
||||
"entry": "lib.ts",
|
||||
"emission": "c",
|
||||
"abi": {
|
||||
"prefix": "kr_",
|
||||
"init_symbol": "kr_init",
|
||||
"sink_register_symbol": "kr_set_panic_sink",
|
||||
"collect_symbol": null,
|
||||
"result_reset_symbol": null
|
||||
},
|
||||
"exports": [
|
||||
{ "export": "retMax", "symbol": "kr_ret_max", "params": [], "returns": "i64" },
|
||||
{ "export": "retNegZero", "symbol": "kr_ret_neg_zero", "params": [], "returns": "i64" },
|
||||
{ "export": "retRem", "symbol": "kr_ret_rem", "params": [], "returns": "i64" },
|
||||
{ "export": "retU32Max", "symbol": "kr_ret_u32_max", "params": [], "returns": "u64" }
|
||||
]
|
||||
}
|
||||
@@ -0,0 +1,19 @@
|
||||
/* Ask 4's inbound declared-integer edge: `take`'s parameter is
|
||||
* profile-declared i64 (takeU's u64), so the generated wrapper
|
||||
* range-checks every HOST call — a value past ±(2^53 − 1) cannot ride
|
||||
* f64 exactly, and silent rounding is a coercion the author never wrote,
|
||||
* so the wrapper delivers the SC4012 host-contract trap instead.
|
||||
* In-range values convert exactly. */
|
||||
let seen: number[] = [];
|
||||
|
||||
export function take(x: number): void {
|
||||
seen.push(x);
|
||||
}
|
||||
|
||||
export function takeU(x: number): void {
|
||||
seen.push(x);
|
||||
}
|
||||
|
||||
export function last(): number {
|
||||
return seen.length === 0 ? -1 : seen[seen.length - 1];
|
||||
}
|
||||
@@ -0,0 +1,86 @@
|
||||
/* The inbound declared-integer host-contract trap, mode-selected by
|
||||
* argv[1]:
|
||||
* ok — in-range int64_t/uint64_t values convert exactly (the
|
||||
* edges: ±(2^53 − 1) for i64, 2^53 − 1 for u64)
|
||||
* trap-i64 — 2^53 + 1 through the i64 parameter: the wrapper's
|
||||
* range-check delivers the structured SC4012 message (the
|
||||
* profile's teaching text and remediation riding it) and
|
||||
* the library poisons — silent rounding never happens
|
||||
* trap-u64 — 2^60 through the u64 parameter, same story
|
||||
* The parse in show() is the spec's rule: split the bytes after the 0x01
|
||||
* marker on 0x1F into text/code/symbol/remediation. */
|
||||
#include <inttypes.h>
|
||||
#include <setjmp.h>
|
||||
#include <stddef.h>
|
||||
#include <stdint.h>
|
||||
#include <stdio.h>
|
||||
#include <string.h>
|
||||
|
||||
extern void kt_init(void);
|
||||
extern void kt_set_panic_sink(void (*fn)(void *, const uint8_t *, size_t, uint64_t), void *ctx);
|
||||
extern void kt_take(int64_t x);
|
||||
extern void kt_take_u(uint64_t x);
|
||||
extern double kt_last(void);
|
||||
|
||||
static jmp_buf trap_jmp;
|
||||
static int sink_calls = 0;
|
||||
|
||||
static void show(const uint8_t *msg, size_t len) {
|
||||
if (len == 0 || msg[0] != 0x01) {
|
||||
printf("baseline text=%.*s", (int)len, (const char *)msg);
|
||||
return;
|
||||
}
|
||||
static const char *names[4] = {"text", "code", "symbol", "remediation"};
|
||||
const uint8_t *p = msg + 1, *end = msg + len;
|
||||
int fields = 0;
|
||||
for (;;) {
|
||||
const uint8_t *sep = memchr(p, 0x1f, (size_t)(end - p));
|
||||
const uint8_t *stop = sep != NULL ? sep : end;
|
||||
if (fields < 4) printf("%s=[%.*s]\n", names[fields], (int)(stop - p), (const char *)p);
|
||||
fields++;
|
||||
if (sep == NULL) break;
|
||||
p = sep + 1;
|
||||
}
|
||||
printf("fields=%d\n", fields);
|
||||
}
|
||||
|
||||
static void sink(void *ctx, const uint8_t *msg, size_t len, uint64_t addr) {
|
||||
(void)ctx;
|
||||
(void)addr;
|
||||
sink_calls++;
|
||||
printf("sink[%d]:\n", sink_calls);
|
||||
show(msg, len);
|
||||
longjmp(trap_jmp, 1);
|
||||
}
|
||||
|
||||
int main(int argc, char **argv) {
|
||||
const char *mode = argc > 1 ? argv[1] : "ok";
|
||||
kt_set_panic_sink(sink, NULL);
|
||||
kt_init();
|
||||
|
||||
if (setjmp(trap_jmp) == 0) {
|
||||
if (strcmp(mode, "ok") == 0) {
|
||||
kt_take(INT64_C(9007199254740991));
|
||||
printf("i64 max: %.17g\n", kt_last());
|
||||
kt_take(INT64_C(-9007199254740991));
|
||||
printf("i64 min: %.17g\n", kt_last());
|
||||
kt_take_u(UINT64_C(9007199254740991));
|
||||
printf("u64 max: %.17g\n", kt_last());
|
||||
printf("ok, sink_calls=%d\n", sink_calls);
|
||||
return 0;
|
||||
} else if (strcmp(mode, "trap-i64") == 0) {
|
||||
kt_take(INT64_C(9007199254740993)); /* 2^53 + 1: cannot ride f64 */
|
||||
} else if (strcmp(mode, "trap-u64") == 0) {
|
||||
kt_take_u(UINT64_C(1) << 60);
|
||||
} else {
|
||||
fprintf(stderr, "unknown mode %s\n", mode);
|
||||
return 2;
|
||||
}
|
||||
printf("UNREACHABLE\n");
|
||||
return 1;
|
||||
}
|
||||
/* Poisoned now: no further entries (kt_last would abort by design) —
|
||||
* the message arrived exactly once and the host survived. */
|
||||
printf("survived, sink_calls=%d\n", sink_calls);
|
||||
return 0;
|
||||
}
|
||||
@@ -0,0 +1,22 @@
|
||||
{
|
||||
"profile_format": 1,
|
||||
"name": "int-trap",
|
||||
"entry": "lib.ts",
|
||||
"emission": "c",
|
||||
"abi": {
|
||||
"prefix": "kt_",
|
||||
"init_symbol": "kt_init",
|
||||
"sink_register_symbol": "kt_set_panic_sink",
|
||||
"collect_symbol": null,
|
||||
"result_reset_symbol": null
|
||||
},
|
||||
"exports": [
|
||||
{ "export": "take", "symbol": "kt_take", "params": ["i64"], "returns": "void" },
|
||||
{ "export": "takeU", "symbol": "kt_take_u", "params": ["u64"], "returns": "void" },
|
||||
{ "export": "last", "symbol": "kt_last", "params": [], "returns": "f64" }
|
||||
],
|
||||
"determinism": {
|
||||
"teachings": { "SC4012": "this core's integer channel carries at most 2^53 - 1" },
|
||||
"remediations": { "SC4012": "keep host-side ids within the exact-integer range" }
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user