Skip to content

CLAUDE.md

Latest commit

 

History

History
206 lines (186 loc) · 11.1 KB

CLAUDE.md

File metadata and controls

206 lines (186 loc) · 11.1 KB
Raw

CLAUDE.md

This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.

What this is

A TypeScript reference implementation of the LLMbda calculus (Garby, Gordon & Sands, arXiv:2602.20064) — a labeled, dynamically information-flow-tracked lambda calculus for agentic LLM programs. It closely follows the paper's §3/§5/§B big-step operational semantics.

This port carries no formal guarantee. The paper's noninterference theorems (TIPNI, Insulated TIPNI, oracular correctness) are machine-checked only in the paper's Lean 4 development. This repo implements the algorithm and regression-tests it against the paper's own leak examples — it does not prove anything. Keep this distinction in mind when describing what a passing test run means; "the interpreter rejects the Fenton/Denning gadget" is not the same claim as "the interpreter is noninterferent."

Commands

pnpm install
pnpm run build               # tsc -p tsconfig.json — strict build, checks src/ only
pnpm run typecheck            # tsc -p tsconfig.examples.json — typechecks src/+examples/+test/,
                              # the files pnpm run build doesn't (examples/ isn't in tsconfig.json's include)
pnpm test                    # node --import tsx test/run.ts — runs every examples/*.ts as pass/fail
pnpm run coverage             # same suite, instrumented with c8 (text + html report in coverage/)
pnpm run example:postcode
pnpm run example:retry
pnpm run example:leak
pnpm run example:confinement
pnpm run example:quarantine
pnpm run example:robust-endorse
pnpm run example:endorse
pnpm run example:camel-provenance
pnpm run example:dynamic-label
pnpm run example:clear-isolation
pnpm run example:deep-label-confinement
pnpm run example:prim-wrap-values
pnpm run example:recv-scope-isolation
pnpm run example:binop-prim-consistency
pnpm run example:camel-readers-flowsto
pnpm run example:missing-binops
pnpm run example:record-duplicate-field
pnpm run example:index-non-integer
pnpm run example:deep-label-closure-env
pnpm run example:bounded-endorse-boolean-domain
pnpm run example:primeval-error-type
pnpm run example:label-test
pnpm run example:scalar-error-paths
pnpm run example:security-checks-standalone
pnpm run example:endorse-unfactored-lattice
pnpm run example:model-primitives-coverage
pnpm run example:camel-lattice-any-source
pnpm run example:run-program-base-env
pnpm run example:label-lit-decodable

There is no separate lint step and no per-test filtering flag — test/run.ts iterates all of examples/*.ts and reports pass/fail per file. To exercise a single scenario in isolation, run its pnpm run example:* script directly (e.g. pnpm run example:leak), or node --import tsx examples/<file>.ts.

To add a new regression case: add an examples/<name>.ts file (it should assert/throw on failure the way the existing examples do) and it is picked up automatically by test/run.ts — no registration needed.

Verifying constitution compliance

CONSTITUTION.md states this project's non-negotiable principles. Before considering any change to src/ done, run the checks below — they are concrete, not aspirational; several are CI-enforced.

  • Article 1 (paper fidelity). For any evaluator.ts/lattice.ts change: identify the exact paper section/rule it implements and confirm the change matches the rule's text, not just "looks reasonable." If the paper text is ambiguous or the port must diverge, that's Article 4, not silent judgment.
  • Article 2 (no overclaiming). Before committing new prose (README, release notes, code comments, commit messages), grep it for proven, verified, guarantee, sound(ness) and confirm each occurrence is either about the paper's Lean-checked results specifically, or correctly hedged (e.g. "regression-tested against," not "verified").
  • Article 3 (regression test proven to fail first). For any bug fix: copy the pre-fix source with git show HEAD:src/<file>.ts > /tmp/<file>.ts, point the new example's imports at that copy, and confirm it fails; then confirm the same example passes against the actual fix. Don't commit a fix without having done this — a test that would have passed even against the old code proves nothing.
  • Article 4 (documented gaps). If a change introduces or touches a deliberate simplification (see "Design choices" below for the existing list), add an inline comment at the divergence point and check whether README.md/that list needs a matching update.
  • Article 5 (minimalism). Before adding a new abstraction, configuration option, or generalized helper, confirm at least two concrete, current call sites need it. If there's only one, inline it.
  • Article 6 (rigor over velocity). For any change to a Lattice/ FactoredLattice instance, run a lattice-law sanity check before committing — reflexivity, transitivity, antisymmetry, the bottom law (flowsTo(bottom, x) for representative x), and that join is a least upper bound, not just idempotent/commutative. A quick node --import tsx -e "..." script exercising src/lattice.ts directly (see git history around commit 63cff57 for the pattern) is enough — it doesn't need to become a permanent example unless it catches something.
  • Article 7 (100% coverage + full typecheck, enforced). Run pnpm run coverage — it must exit 0 (c8 --check-coverage --statements 100 --functions 100 --lines 100 --branches 99). If it fails: either the change needs a test, or the newly-uncovered code is genuinely unreachable, in which case extend CONSTITUTION.md Article 7's named list with the specific file:line and the reason — never loosen the threshold numbers to make the build pass. Also run pnpm run typecheck — it must exit 0. pnpm run build alone is not enough: it only checks src/, not examples//test/, and a deliberately-injected type error in an example was confirmed to slip past it silently before typecheck existed.
  • Article 8 (honest audit-scope framing). If summarizing an audit pass (to the user, in a commit message, or in docs), state what was specifically checked ("rule-by-rule against §3/§5/§B", "lattice laws for usLattice and camelLattice") — never "no bugs remain" or an unqualified "fully verified."

Architecture

src/
  ast.ts        Expr/Value AST + TS-native builder functions (§3.1, §3.2, §B.1)
  lattice.ts    Lattice<L>/FactoredLattice<L,I,S> + the {U,S}-powerset and
                CaMeL-style Sources×Readers lattice instances (§3.2, §5.2, Appendix D.5)
  model.ts      parse/serialise/primEval/toLabel config (§3.3, §B.1)
  oracle.ts     the Oracle abstraction (§6) — pure evaluator, injectable nondeterminism
  evaluator.ts  the big-step semantics, rule by rule — each rule is commented
                with the paper section it implements, and for the two
                security-critical rules, which of the paper's three named
                leaks (§1) it closes
  prelude.ts    fix/quarantine/robust_endorse/bounded_endorse (§C.5, §5.1,
                §E.2, §E.3) as real object-language closures, not host TS
                functions — see below
  errors.ts     SecurityError vs RuntimeError

examples/       one file per worked scenario/regression test; test/run.ts
                runs all of them as the test suite (see table in README.md
                for what each one exercises)

Substitution semantics, not environments — and the bug that came from conflating them

The paper's semantics is substitution-based (e[x := e′]), not environment-based. This port uses environments (the standard practical way to implement a substitution calculus), which means var lookup and record .field access must actively re-join the ambient pc into the returned value's label — under a substitution-based reading, re-encountering a value inside a pc-raised context implicitly taints it via ⇓-Labelled/⇓-Lam, but a naive environment lookup just returns the stored value unchanged and silently drops that taint.

This exact gap was found and fixed in var/field (⇓-ArrayIndex already did it correctly) — regression test examples/var-pc-confinement.ts — and then found again, independently, in seven more places across three rounds of a rule-by-rule audit against the paper's exact text, spanning evaluator.ts (rule implementations), lattice.ts (a lattice instance's internal correctness), and the completeness of the primitive table against the paper's grammar. Each instance has its own regression test in examples/ and its own commit message with the full writeup — check git log/blame on evaluator.ts/lattice.ts for the details rather than looking for a running list in a doc, which would just drift out of sync.

When touching evaluator.ts, especially any case that reads a value out of an environment/record/array rather than constructing one fresh, or that calls Model.primEval/Model.toLabel, check it against the exact paper rule text — when adding or touching a Lattice/FactoredLattice instance, sanity-check flowsTo(bottom, x) holds for representative x, not just that join is idempotent/commutative — when adding a construct to ast.ts's type surface, confirm it's actually wired through evaluator.ts, not just type-constructible — and when a construct collects entries into a Map/similar keyed structure (records, envs), check the spec's stated tie-breaking rule (e.g. record field lookup is first-wins) rather than assuming whatever the host collection's default overwrite behavior happens to be. There is no guarantee three audit passes were exhaustive.

Design choices worth knowing about (see README.md for full rationale; see docs/adr/ for the individual decision write-ups)

  • quarantine/robust_endorse/bounded_endorse are built as object-language Expr closures in prelude.ts (registered in Model.preludeSource), not host TS functions — they must be callable from agent-generated code that only sees named bindings in the object language's environment. bounded_endorse is a builder rather than a bare Expr because its trust domain must be fixed at construction time (§E.3 — a runtime-computed domain forfeits the log₂n leakage bound).
  • No weight/probability tracking and no "fuel" argument — both are artifacts of the paper's Lean-side proof machinery (probabilistic big-step semantics, termination proofs) that the executable interpreter doesn't need.
  • Labels are homogeneous per run: BareValue's record/array fields store Labeled<unknown> rather than threading L through every data shape, soundness coming from a single asL<L>() cast in evaluator.ts rather than infecting BareValue with a generic parameter.
  • endorse requires Model<L>.lattice to implement FactoredLattice; if it only implements Lattice<L>, endorse throws RuntimeError at evaluation time (a deliberate runtime check, not a type-level one).
  • Default parse/serialise is naive JSON.parse/JSON.stringify with a try/catch — not a grammar-constrained parser. A real deployment should replace defaultParse per §7.3/Appendix C.5.