Audit remediation: proof integrity, new core theorems, compiler/runtime soundness, supply chain by ib823 · Pull Request #89 · ib823/proof

ib823 · 2026-10-11T12:44:42Z

Summary

Remediation of a full-codebase audit (2026-10-11). Every finding was reproduced or machine-checked (Rocq 9.1.1, Rust 1.94.1) before it was fixed, and every claim in the docs was re-derived from commands. Beyond fixing the findings, the research-scale gaps the audit opened (REQ-84..87) are now proven for the reference-free, fix-free core, and the model-level limitations were addressed in the compiler.

Changes

Coq kernel integrity (cba3cde)

Two active files let False be proven:
- AlgebraicEffects.v used Unset Positivity Checking. Resumption is now first-order and strictly positive.
- PhysicalSecurity.v had contradictory Parameters. Rebuilt with an in-build satisfiability witness; Parameter TCB 30 → 29.

New theorems (ece2640) — all closed under the global context (no axioms, no section premises):

REQ-87 effect_sound_multi_step_declared: evaluation stays within the declared effect (preservation with ε' ⊑ ε).
REQ-84 well_typed_SN_conclusion_is_false: the old SN statement is false (Landin's knot through a higher-order reference). ref_free_well_typed_SN gives premise-free SN for the reference-free, fix-free core.
REQ-85 ref_free_noninterference and REQ-86 ref_free_constant_time (timing contract: reduction count) for that core, with a non-vacuity witness.
reachable_effects_from_program_text: a set-based effect containment that does not depend on the total effect_level order.
Retraction: BackendComposition.ni_secure concluded f pub = f pub, so "NI preserved through backends" was vacuous. Now real NI over the abstract model, with ni_secure_nonvacuous.
riinac verify: attests 10 kernel capstones, 9 pinned axiom-free.

Gates, CI and release (894a774)

Comment-aware Coq scanners (a hidden Admitted slipped past both).
Kernel-weakening construct gate.
Conditional-capstone tracking.
Real Coq warning budget.
riinac verify --coq in CI.
Commit-accurate hooks.
History-wide secret scan and byte-level bidi scan.
sync-public refuses untracked files.
SHA-pinned actions, checksum-verified installers, non-root Docker.
Committed lockfiles.
VS Code workspace-trust fix.

Compiler (merged branches)

Typechecker (ad98908):
- Labels, taint and CT tags survive erasure into Any.
- Implicit flows through slots, loops and putus.
- Assignment label check.
- Effect charging through Any.
- Top-level capability seeding.
- Linearity across scopes.
- CT through generics and indexing.
Effects (45edbfc):
- Effects are SETS with same-category coverage: kesan Masa no longer authorizes file or network I/O.
- beri may only attenuate inside functions.
- Persistent typing context: 5,000 biar lines 2.7 GB → 36 MiB.
Parser/codegen (50f779d):
- EOF termination and nesting limits.
- Iterative parsing and evaluation (no stack overflow on flat input).
- C string escaping and checked allocations.
- Secret-branch, signed-division and Unicode parity across interpreter, C and WASM.
- CLI hardening.

Runtime, tools, supply chain (e05079b)

CSRF tokens from the OS RNG.
Per-connection TLS-kunci key exchange.
Fail-closed manifest, hash-chain and proof-bundle verifiers.
FIPS 204 pure ML-DSA (OpenSSL-interoperable).
MCP runs Pure programs only by default, under budgets.
HMAC-SHA256-chained, sealed execution receipts.
Ed25519 publisher signatures for remote packages, with lockfile signer pinning.

Docs: README, website, papers, master plan (REQ-84..89, Part 11 entry), CHANGELOG (with retractions) claim only what is attested, with scope stated.

Behaviour changes (see CHANGELOG):

Effect declarations must list every category used.
Old artifact-sign ML-DSA/hybrid signatures no longer verify.
MCP is pure-only unless --allow-effects.
Remote riina.lock files must be re-locked.

Type

Testing

cargo test --all passes: 03_PROTO 3,528, 05_TOOLING 352, with cc and wasmtime present and no opt-out.
cargo clippy --all --all-targets -- -D warnings passes in both workspaces.
Coq: 334/334 .vo, 0 warnings (budget 2, clean single-job build); 10 capstones attested; 0 Admitted / 0 Axiom / 0 Abort; riinac verify --full PASS.
Each agent branch was tested alone and in combination before merging. Conflict resolutions are described in the merge commits.
New tests: scanner negative controls, regression tests for every soundness hole (each fails on the pre-fix code), receipt forgery and splice tests, package-signing end-to-end, context-scaling memory bound, backend differentials.
Example corpus: 98/172 pass riinac check (was 97); 28/28 of 00_basics/.

Checklist

No external dependencies added (SBOM check OK)
No unsafe without justification (two HMAC unsafe blocks removed)
No Admitted in Coq proofs
Examples use Bahasa Melayu keywords (n/a)

Known remaining limitations (tracked in the master plan):

SN/NI/CT are proven for the reference-free, fix-free core only (REQ-89).
Coq's typing effect bound is still a total order; the compiler is finer.
Actor handler effects are not charged to senders.
Package keys have no revocation.
HMAC receipts give no non-repudiation.

🤖 Generated with Claude Code

https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

…d; record well_typed_SN vacuity The 2026-10-11 audit machine-checked (Rocq 9.1.1) that False was provable inside two active-build files, and that the SN capstone is vacuous. domains/AlgebraicEffects.v - `Unset Positivity Checking` admitted a mutual Comp/Handler type with a genuine negative occurrence (HOp's continuation `Val -> Comp` taken as an argument). `Theorem : False` compiled against it, its only assumption being "Comp is assumed to be positive". - Re-encoded resumption first-order: clause bodies are ordinary `Comp`s using a new `CResume r`; `resume_with` plugs the continuation in when a clause fires. Comp/Handler and the typing judgment (now indexed by a resume context) are strictly positive; both positivity bypasses removed. - New `resume_with_typing` (resumption preserves typing; induction proof). EFF_001_12 now states something non-trivial; the always-0 `count_continuation_uses` is replaced by `count_resumes`. - All 23 theorems/lemmas: Print Assumptions = Closed under the global context. domains/PhysicalSecurity.v - The trusted Parameter interface was jointly unsatisfiable: `chip_puf` was a free field of the `Chip` record, so two records with distinct ids and the same response function contradicted `puf_physically_unique`. - `chip_puf` is now an opaque physical function (Parameter); the auxiliary `puf_entropy` / `different_chips_different_entropy` pair is dropped. TCB Parameter count 30 -> 29 (pin updated). - New in-build witness `physical_tcb_satisfiable`: one concrete model satisfies all 13 propositional Parameters at once. Its statement is generated from the declared Parameter types (`type of` + `pattern`), so it cannot drift; it is closed under the global context. termination/ReducibilityFull.v - `well_typed_SN` is exported with four section Hypothesis premises quantified over every store/body/environment; they are refutable, so the theorem is vacuous. Added the honesty record and the machine-checked refutation `well_typed_SN_premise_store_values_are_values_refutable`; corrected the comment that called the store hypothesis an initial-store discipline. Repair tracked as REQ-84. Counts (by command): active Qed 12,678 -> 12,682 (+4), 0 Admitted / Axiom / Abort, 331/331 .vo, zero warnings. Metrics regenerated (generate-metrics.sh --fast, cached verified test count) and synced; proof ledgers regenerated. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

…d supply-chain gaps Every item below was found by the 2026-10-11 audit and verified by a reproducer or control test before and after the fix. Proof gates - coq-source-counts.py and riinac verify lexed comments without the strings Coq lexes inside them: `Proof. (* "(*" *) Admitted.` hid a real Admitted from both. Fixed in both lexers (+ tests). - New hard gate for kernel-weakening constructs the counts never saw: Conjecture, give_up, Admit Obligations, bypass_check, Unset Guard/Positivity/Universe Checking (audit-docs.sh, riinac verify, metrics). - Parameter pin counted with the scanner (grep missed Local/#[local]/plural). - riinac verify: capstones stated under section-Hypothesis premises must be listed as CONDITIONAL with a tracking REQ (well_typed_SN -> REQ-84) or the gate fails; reported as conditional, never as unconditional guarantees. - riinac verify: Coq warning budget enforced on the actual build output (the status-file path only ever warned); clippy now `--all-targets -D warnings`; kernel scratch file in a fresh private dir (fixed /tmp name). - New `riinac verify --coq` (the same shared Coq checks as --full); CI's coq job runs it instead of a bare `make`. - 15 verify.rs tests used hard-coded /workspaces/proof paths behind `if path.exists()` and silently passed elsewhere; now repo-relative and asserting. - "Cross-Prover Validation ... PASS, Grand total" relabelled as a raw corpus inventory (only Coq is mechanized). Doc/metrics gates - audit-docs.sh's README Qed check matched a `**Coq 8.20.1**` row that no longer existed and silently never ran; README carried 12,613 and the website meta description 12,646. Row matcher fixed (missing row = error), prover pin checked, and every current-state Qed figure in public docs must equal the live count. sync-metrics.sh updaters were no-ops for the same reasons and now apply the same rule. - Metrics: axioms via scanner; new parameters / sectionHypotheses / kernelWeakeningConstructs fields; `assumptions` scope documented; recorded negative build evidence downgrades the Coq claim. Security gates - security-gates.sh: Trojan-source scan exited 2 under the C locale and `|| true` made it pass (now byte patterns, errors fail); new-branch pushes diffed against the working tree and scanned nothing; renames skipped; secrets added then deleted were missed. Now scans the added lines of every outgoing commit; `--all-tracked` for releases (release.sh range was empty). - Hooks: pre-commit blocks when verified sources differ between index and working tree; pre-push blocks unless the pushed commit is the clean HEAD (both previously verified the working tree, not what was committed or pushed); pre-commit used a non-existent `coq820` opam switch. Publication / release - sync-public.sh published untracked working-tree files (`git add -A`; the clean check ignored untracked files) — demonstrated with a `.priv` key. Now refuses untracked files and stages tracked changes only; strip list extended (session prompts, proof-attempt logs, patches/). - verify-public.sh path check scans every tracked text file; container paths removed from AGENTS.md and validate_jsonl.py. - build-release.sh fails when a signing key is set but the tool is missing. - deploy-website.sh: no token-in-URL advice; WASM build failure fails the deploy; `npm ci` with committed lockfiles (they were gitignored). Supply chain / packaging - All GitHub Actions pinned by commit SHA; wasmtime download checksum- verified (scripts/ci-install-wasmtime.sh); rust-proto now runs the 14 wasmtime-dependent tests that never ran in CI. - Dockerfile could not build (rust:1.84 vs rust-version 1.94.1): pinned by digest, --locked, non-root. Dockerfile.dev: 1.94.1, checksum-verified rustup-init, dated nightly. install_rust/install_lean: pinned + verified installers, pinned toolchains (were `stable`). - Root rust-toolchain.toml (1.94.1). flake.nix: unfree license (was MPL), no Coq 8.20 in the dev shell. - VS Code extension: riina.riinacPath machine-scoped, restricted in untrusted workspaces, workspace values ignored, no LSP in untrusted workspaces; @types/node added (it did not compile with its declared deps). - Tracked-but-ignored files resolved (Cargo.lock, VERIFICATION_MANIFEST.md); generated Makefile.conf (machine paths) and Lean .lake outputs untracked. Verified: riinac verify --full PASS (3,383 Rust tests, clippy clean, Coq 331/331 .vo, 0 warnings / budget 2, kernel attestation with well_typed_SN CONDITIONAL); riinac verify --coq PASS; audit-docs 0 discrepancies. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

…it flows, assign, effects, caps, linearity, CT) Fixes the verified exploits from the typechecker soundness audit. Every negative regression test in riina-typechecker `tests::audit_soundness` type-checked before this change (verified against bff1d4d) and is rejected now; positive neighbours keep type-checking. H1 (secrecy/taint lost through `Any`): new `Any`-erasure discipline. Every point where a value is viewed at an `Any` type (record literal/field, `Any` parameter, list element, branch join, Any-typed cell) computes what is erased (`erased_info`/`latent_info`: label, taint, CT tag, and a function value's latent effect and result label) and re-attaches it to the `Any` result; a function whose declared (generic/record) result type would hide a label, taint or CT tag is rejected (`erased_result_check`). `[senarai_baru(()), pin]`, `Kotak{isi: pin}.isi`, `buka<T>(..) -> T { s }`, `senarai_peta` over a secret-returning closure and `sql_execute(Kotak{q: read_line(())}.q)` are all rejected. Rust-only gap (Coq has no `Any`). H2 (implicit flows through closures / putus / teruskan / pulang): a closure writing a mutable slot it did not bind gets latent effect `Mut`, so calling it under a secret pc is rejected (writes are attributed to slot identities, so a local helper mutating its function's own slot keeps the function `Bersih`); `putus`/`teruskan`/`pulang` under a secret pc raise the pc for the rest of the loop (re-checked to a fixpoint, covering later iterations) / function; a top-level function writing a global `biar ubah` slot must declare `kesan Ubah`. Calling an `Any`-typed or secret-chosen function under a secret pc is rejected. H3 (assignment dropped the value's label): T_Assign now requires level(value) ⊔ pc ⊑ level(ref). Coq T_Assign types the value at exactly the cell type, so the prototype was less strict than Coq; tightened. H4 (`kesan Bersih` program performing I/O through an `Any` callee): the latent effect of a function value erased into an `Any` position (generic parameter, higher-order builtin, record field, Any-typed cell) is charged at the erasure point — effect discipline, capability gate and pc check — as if called there (Coq T_App joins the callee's latent effect; `Any` is the Rust-only gap). M1a (program-wide capability grants): `check_program` no longer grants the union of every function's declared effects to the whole program. Top-level code holds only explicit `beri` grants (gate always on); a call to a declared top-level function is authorized by its own declaration; a local `fungsi`'s declared effect no longer leaks into the enclosing block. M1b/M1c (unrestricted `beri`, total effect order) match Coq T_Grant and `effect_join`/`effect_level` exactly and are left as model-level limitations. M2 (linear variables used more than once): usage counters are shared across the checker's cloned scopes (Coq `linear_typed` threads its context through T_Let/T_App/T_Pair), so uses in nested `biar` bodies count; a linear/affine variable captured by a closure that is not itself bound `sekali`/`paling` is rejected (a linearly-bound capturing closure is call-only); branches must consume a linear variable consistently; a use inside a loop body is rejected with a clear message (was the misleading "used Zero"). M3 (constant-time bypasses): the CT tag survives `Any`/generic calls (`kalau id(a == 0)` is rejected) and a CT value may not be used as a collection index or lookup key (`senarai_dapat`, `e[i]`, ...), per the documented CT discipline and Coq ConstantTimeCrypto.v CT_007. Also: the large `type_check_full` match arms are moved verbatim into `#[inline(never)]` helpers. In debug builds each recursion level reserved every arm's locals (~104 KiB with this change, ~89 KiB before), which overflowed the fuzz harness's 4 MiB worker stack; a level is now ~28-33 KiB. Corpus: 97 -> 98/172 (`rii_corpus_gate` updated). linear_enforcement.rii now passes (it was a false "used Zero" rejection, M2). closures.rii and tainted_data.rii failed closed and had their declarations corrected rather than the check weakened: stateful closures are `kesan Ubah` (H2), and a record built from `fail_baca` is declared `Tercemar<.., FileSystem>` (H1). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

…SA defaults, key hygiene Security audit findings fixed in 05_TOOLING: H3 build-manifest: manifest "sha256" fields were a 64-bit DefaultHasher value printed four times and `verify` was a stub returning Ok(true). Now real SHA-256 (riina-core), JSON emitted with a real encoder, and `verify` parses the manifest, recomputes every file's SHA-256 + size and exits non-zero on mismatch, missing/unreadable file, unsafe (absolute or `..`) path, malformed or EMPTY manifest; `diff` implemented (non-zero when manifests differ). artifact-sign `sign-manifest`/`verify-manifest` printed "Not yet implemented" and exited 0: now implemented — sign-manifest refuses a stale/empty manifest and signs the exact bytes it checked; verify-manifest checks the signature over the manifest bytes AND every listed file, exiting non-zero on any failure. M1 ML-DSA-65: default sign/verify/sign_hedged (and so the Signature trait, hybrid, artifact-sign and the kripto builtin) used the FIPS 204 INTERNAL interface — non-interoperable, and a standard signature over X verified as one over 0x00||0x00||X. Defaults are now the external "pure" interface with an empty context; the internal interface remains as explicit sign_internal / sign_hedged_internal / verify_internal, which the ACVP internal-vector KATs now call. Interop confirmed both ways against Python `cryptography` (OpenSSL) ML-DSA-65. M2 hash-chain verify --deep passed after a document was deleted (missing and unreadable files were ignored) and after a splice (null predecessor skipped the link check); `signature` was never checked. Now: missing or unreadable documents fail; only the genesis entry may have a null predecessor; documented rule that entries must be unsigned (a present signature fails as unverifiable); document ids must be plain file names; empty chains and malformed hashes fail; output states the chain is unauthenticated. M3 runtime-proof-verify accepted fabricated bundles (unkeyed chain, no expected program identity, empty all-zero bundle printed VALID). riina-effect now rejects empty bundles, unknown versions and out-of-order sequences, adds verify_for_program (expected program hash) and an HMAC-SHA256 authenticated mode (authentication_tag / verify_authenticated). The tool requires --program-hash/--program-identity and an explicit --key-file (authenticated, auth_tag line) or --integrity-only (loud "NOT authenticity" warning); duplicate fields are refused. M5 artifact-sign keygen wrote private keys with umask permissions (0644). Private keys are now created 0600 at open(2) time, public keys 0644; keygen refuses to overwrite either file unless --force (which recreates, not truncates); in-memory private key copies are zeroized. L5 (riina-core part) X25519 all-zero shared-secret check short-circuited on the secret; now a constant-time OR-accumulate via ct_eq. Ed25519SigningKey::from_seed left the expanded secret scalar + prefix on the stack (now scrubbed; sign() also scrubs the nonce r, k*a and the scalar). HmacSha256/HmacSha384 held the keyed inner state in ManuallyDrop, so it was never scrubbed without finalize; it is now a plain field (scrubbed by the hasher's Drop) moved out with mem::take — which also removes both `unsafe` blocks from hmac.rs. No new crates: build-manifest swaps its unused sha2 edge for riina-core, artifact-sign gains an edge to the workspace's existing serde_json. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

…ng and package fetching Security audit findings fixed in 03_PROTO: H1 csrf_generate tokens were fixed-key SipHash of (wall-clock ns, process counter) — recoverable offline. Now 128 bits from the OS CSPRNG (/dev/urandom via riina-tls's fail-closed reader), hex; a missing entropy source is a runtime error. (C backend: csrf_generate is not routed, so compiled programs still fail closed; lower.rs note updated.) H2 jaring_tls_kunci derived keys from the caller secret alone with sequence 0 per connection, so two connections sharing a secret reused the AES-GCM key+nonce sequence (identical keystreams, exposed GHASH key). Both peers now send a fresh 32-byte OS random in-band (one handshake record, "RIINAKN1" tag) and keys are HKDF-Extract(H(ctx), secret) + c/s ap traffic labels over ctx = label || client_random || server_random (role-ordered). Empty secrets, reflected randoms and non-kunci peers are refused; the misleading "open a new connection" error is reworded. Interpreter-only (TLS is not routed to C), so no C counterpart exists. H4 `riinac mcp` ran untrusted riina_run/riina_test source with full host access (inferred effect discarded). Now: programs/tests whose inferred effect is not Pure are refused with a tool error naming the effect; evaluation uses a builtin environment without any host-reaching builtin (file, network, HTTP request, store, VFS, stdin/stdout, clock, random) AND a sandboxed interpreter that refuses them at application time; every tool call runs on its own 256 MiB-stack thread under a step budget, nesting-depth cap and 10 s wall clock (new riina_codegen::ExecLimits / eval_with_limits). `riinac mcp --allow-effects` opts back in (budgets still apply); unknown flags error. Tool descriptions state the policy. M4 csrf_check_referer was a prefix match in both backends ("https://bank.example.attacker.net/" matched "https://bank.example"). Interpreter and C runtime now require the referer to equal the origin or continue it with '/', '?' or '#'; one trailing '/' on the origin ignored. L1 validate_url passed "/\\evil.example/x" and "/\t/evil.example/x". Both backends now reject backslashes and ASCII controls anywhere, refuse a second char of '/' or '\', and trim only ASCII spaces (the old C trim and Rust trim disagreed on controls vs Unicode whitespace). L2 The TLS server reported its peer "authenticated" whenever it had its own identity. ConnectedEvidence.cert_chain_verified now means the PEER proved a pinned credential: false on the server (no client auth), so jaring_tls_disahkan / jaring_tls_jabat_sah return false there. L3 http::message_length overflowed on Content-Length 18446744073709551615 (debug panic / wrong length). Checked arithmetic; over-limit bodies are a TooLarge error. The C runtime's message_complete now refuses them too. L4 riina-receipt: documented that verify() (unkeyed FNV-1a) detects accidental corruption only, not adversarial tampering; a test pins the limit. No dependency added. L5 (riina-tls part) RecordKeys and every key-schedule secret (handshake, master, traffic, finished keys, DH shared secret) are now zeroized on drop via riina-core's Secret/Zeroize. L6 riina-pkg refused nothing: plain-http registries are now rejected unless the host is loopback (localhost, 127.0.0.0/8, [::1]), checked up front; builds from a remote registry require riina.lock (whose sha256-tree checksums were already mandatory). Registry signing remains a gap. Tests asserting the old behaviour were updated: the TLS socket tests now complete the kunci exchange; authenticated_handshake_over_sockets and the riina-tls authenticated-evidence tests now expect the server side to report an unauthenticated peer; pkg http's parse test no longer accepts http://example.com. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

…mpilations and CLI hardening Fixes the parser/codegen/riinac findings of the 2026-10 compiler audit. M4 - parser infinite loops (lexer yields Eof forever, never None): - `jenis T =`, `guna a::b` and `modul m {` skip loops now stop at Eof and report an error (they spun at 100% CPU in check/fmt/LSP/MCP). A missing alias `;`, an unclosed `jenis T<` and an unclosed `bentuk S {` are errors instead of being accepted; `>>` now closes two levels in `jenis T<A<B>>` (it was skipped and the scan swallowed the rest of the file). - Every token loop in the parser and lexer audited; a lexical error is now reported (ParseErrorKind::Lex) instead of being taken for end of file, which silently discarded every declaration after a stray character. - Trailing `guna`/`jenis`/`modul` no longer inject a `()` body that stopped `utama` from running, nor drop a trailing modul's functions; `awam` at EOF is an error. M5 - stack overflow on long flat input: - riinac runs every command on a dedicated 256 MiB thread (4 GiB address space in debug builds, whose frames are ~20x larger), falling back to smaller reservations if refused. - Parser: statement sequences, `lain kalau` chains and runs of skipped declarations are iterative; every recursive path (parse_expr, parse_control_flow, parse_unary, parse_ty, parse_pattern, parse_session_type) is charged to the nesting guard (`[[[[`, `!!!!`, `f(f(`, lambda/match/type/pattern nesting were unbounded). - New riina_parser::limits: programs deeper than MAX_AST_DEPTH (20,000) get a clean P0014 ProgramTooDeep error (also for linked modules); chains are capped while built, rejected trees are dismantled without recursion. - Interpreter: Let/LetMut/If tails loop and BinOp chains fold iteratively; Env is now persistent (each `biar` cloned the whole map: 5,000 bindings took ~5 GB). - Lowering: infer_type(BinOp) inferred each operand twice (exponential: 25 terms took seconds, 40 hours); chains are lowered iteratively. - LSP/MCP JSON parser: nesting bounded (256). M6 - C string literals: fixed-width octal escapes for every non-printable and non-ASCII byte (`\xNN` was parsed greedily: "A\0B|" became "A\v|"); `?` escaped against trigraphs. A literal containing NUL is a clear compile error for C (the C runtime is NUL-terminated throughout: printing, strstr, strcmp, map keys, fopen paths), still supported by interpreter and WASM. M7 - branches on secret booleans: interpreter (if/while) and C (riina_cond unwraps SECRET and checks the tag) now branch on the value; C read the wrapper pointer, so both branches were the same. M8 - signed division: MIN / -1 = MIN and MIN % -1 = 0 at every width (interpreter wrapping semantics = SizedInt.v toSigned/wrapU of the exact quotient); C guards the -1 divisor (was SIGFPE), WASM negates instead of i64.div_s (was a trap). WASM also printed negative i64 as unsigned. L1 - `build --run` executes the artifact by absolute path (no $PATH lookup). L2 - build intermediates go in a private, randomly named 0700 directory created with create_dir; files opened with create_new; removed afterwards. L3 - `test --update` rewrites only the expected literal of the failing `jangkakan` (located by parser span + lexer token span); ambiguity is reported, never guessed. L4 - `riinac doc` HTML-escapes all interpolated text; anchors use a safe, unique alphabet. L5 - C teks_sub/teks_aksara_di index Unicode scalar values (never split a UTF-8 sequence); C case mapping is Rust's str::to_uppercase/to_lowercase (full mapping + final sigma), tables generated from Rust std at emit time, emitted only for programs that use them. L6 - every allocation in the emitted C runtime goes through checked riina_x{malloc,calloc,realloc,strdup} (the sanitizer block owned elsewhere was already checked). Tests: riina-parser robustness_tests + limits, modules depth test, interpreter/env tests, JSON depth test, riina-doc escaping tests, riinac expect_update/private_tmp tests, and integration suites flat_input_robustness, audit_backend_differential, cli_hardening. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

…SN; set-based effect containment The 2026-10-11 audit left four research-scale gaps tracked as REQs. All four are now kernel-checked theorems (Print Assumptions: closed under the global context — no axiom, no section premise), each with its honest scope. REQ-87 dynamic effect soundness (type_system/Preservation.v, effects/EffectGate.v) - preservation_effect / multi_step_preservation_effect add effect_level e' <= effect_level e to preservation (all 38 step cases). - effect_sound_multi_step_declared: every configuration reachable from |- e : T ! eps performs only effects within the DECLARED eps. REQ-84 strong normalization (termination/ReducibilityFull.v, StrongNormRefFree.v) - well_typed_SN_conclusion_is_false: a well-typed, recursion-free program in a well-formed store diverges through a function stored in a higher-order reference (Landin's knot). No premise discharge could repair well_typed_SN. - ref_free_well_typed_SN: premise-free SN for the reference-free, fix-free core (unary Tait relation over closed values + determinism => Acc step_inv). REQ-85 / REQ-86 (properties/NonInterferenceRefFree.v) - Binary logical relation with equal reduction counts. ref_free_noninterference: runs differing only in TSecret inputs return the same observable value. ref_free_constant_time: they take the same number of steps (timing leakage contract over the formal semantics; exec_time_unique makes time well defined). Declassification is handled exactly: declass_ok fixes the released payload in the program text. Non-vacuity witness included. Effect-order limitation (effects/EffectContainment.v) - reachable_effects_from_program_text / absent_effect_never_reachable: for ANY set D, evaluation never produces a perform/require/grant site outside the program text and initial store — independent of the total effect_level order. Retraction (domains/BackendComposition.v) - ni_secure concluded `f pub = f pub`, so "NI preserved through compiled backends" was vacuous. Now real NI over the abstract model, with ni_secure_nonvacuous (a leaking program fails it). Gate (riinac verify) - Ten kernel capstones; AXIOM_FREE_CAPSTONES pins nine as axiom-free (the gate fails if any gains even a whitelisted axiom); Print Assumptions is now fully qualified and attributed per capstone. well_typed_SN stays CONDITIONAL. - riinac verify --coq: 334 .vo, 0 warnings (budget 2), 10 capstones attested. Docs: README, website, UNDERSTANDING_RIINA, the type-safety paper, master plan (REQ-84..87 DONE, REQ-88 remediation record, REQ-89 extension to references/fix, Phase-1 rows, Part 11 entry), CHANGELOG (incl. retractions) state exactly these scoped results. Metrics: 12,819 Qed, 334 active files, 29 Parameter; vacuity 1,318 (a scan of the previous commit gives the same 1,318 — the committed report was stale). Banner scan no longer counts agent worktrees. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

…able FNV-1a chain riina-receipt chained receipts with an unkeyed 64-bit FNV-1a hash over public fields. Anyone could edit a receipt, recompute every id, and `verify()` still passed -- the previous audit pinned exactly that with `rechained_forgery_still_verifies_documented_limit` (audit L4). Receipts are now tamper-evident against anyone without the key: - Every link carries an HMAC-SHA256 tag (first-party riina-core) over an unambiguous length-prefixed encoding, lp(x) = u64_be(len x) || x: tag_i = HMAC(key, lp("RIINA-RECEIPT-LINK-v1") || lp(chain_id) || lp(u64 sequence) || lp(prev_tag) || lp(u64 program_hash) || lp(u64 timestamp) || lp(effect_type)) so each tag covers the previous tag and every field of the receipt, and the chain id stops receipts moving between chains. - A finished chain is sealed: seal = HMAC(key, lp("RIINA-RECEIPT-SEAL-v1") || lp(chain_id) || lp(u64 count) || lp(head_tag)) `verify(&key)` requires the seal, so dropping trailing receipts -- or stripping the seal -- fails. `verify_links` (documented as NOT detecting tail truncation) and `verify_anchored(&key, len, head)` serve chains that are still being written. - Tag, seal and back-link comparisons are constant-time (riina-core ConstantTimeEq). ReceiptKey is exactly 32 bytes, zeroized on drop and redacted in Debug. - The unkeyed mode had no consumers anywhere in 03_PROTO or 05_TOOLING and is removed rather than kept as a forgeable alternative. API change (no in-tree callers): ReceiptChain::new(chain_id), append/append_at(&key, ...) -> Result, seal(&key), verify(&key) -> Result<(), ReceiptError>, from_parts for stored chains; receipts carry sequence, prev_tag and tag ([u8; 32]) instead of u64 ids. Tests 14 -> 18. The re-chained forgery now FAILS keyed verification (`rechained_forgery_fails_keyed_verification` replaces the test that asserted the insecure behaviour). Field edits (every field, chain id, seal), reordering, truncation (tail, head, everything, seal stripped), extension, wrong key and splicing between two same-key chains with identical contents all fail. Known-answer tests pin the encoding and the tags/seal against Python hmac/hashlib (independent implementation). Law 8: the only new edge is the path dependency on first-party riina-core (as riina-tls/riina-codegen); no third-party crate. SBOM unchanged (`scripts/generate-sbom.sh --check` OK). Limits (documented in the crate): HMAC is symmetric, so verifiers can forge (no non-repudiation); rolling back to an older seal of the same chain id needs an external anchor; key management is the embedder's. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

Full-mode riinac verify record produced by the pre-push run of ece2640: 334 .vo, 0 Coq warnings, 10 kernel capstones (9 axiom-free), 3,384 Rust tests, 0 clippy warnings. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

`pkg lock` against a remote registry was trust-on-first-use: whatever tree the registry served first was pinned in riina.lock, and nothing tied a package to its publisher. Packages from a REMOTE registry must now carry an Ed25519 signature (first-party riina-core) by a trusted publisher key, or they are refused before a byte is unpacked. Signed message (unambiguous, lp(x) = u64_be(len x) || x): lp("RIINA-PKG-SIGNATURE-v1") || lp(name) || lp(version) || lp(SHA-256(archive)) The verifier builds it from the name/version it requested and the digest it computed, never from the signature document, so a signature cannot be replayed onto another name, version or archive. - Registry API: GET /api/v1/crates/{name}/{version}/signature serves a strictly parsed text document (header `riina-pkg-signature v1`; nama, versi, arkib-sha256, penandatangan = "ed25519:<hex pubkey>", tandatangan; each key exactly once, <= 4 KiB); 404 = unsigned, any other error status is an error, never a downgrade to "unsigned". `publish` sends sha256/signer/signature query parameters with the archive, after verifying its own signature. - Keys: `riinac pkg keygen [--output <base>] [--force]` (default ~/.riina/keys/publisher, dir created 0700) writes <base>.priv with mode 0600 at open(2) time and <base>.pub 0644; never overwrites without --force (which removes and recreates, never truncates); same file format as artifact-sign Ed25519 keys. Loading a private key readable by group/others is refused. `riinac pkg key-id <file>` prints the key id. - `riinac pkg publish [--key <file.priv>]` signs (default key if present). A remote publish without a key is refused unless --insecure-allow-unsigned; a key inside the package directory is refused (it would be uploaded). - Trust: union of `[registry] trusted-publishers = ["ed25519:<hex>", ...]` in the ROOT riina.toml (dependencies' lists are ignored) and ~/.riina/trusted-publishers (one id per line; refused if group/world writable). Malformed entries are errors. Default: nothing trusted. - `--insecure-allow-unsigned` (global flag, loud banner) accepts unsigned or untrusted-key packages with a WARNING on every use; a malformed or non-verifying signature is refused even then. - riina.lock records `penandatangan` (signer key id, or "unsigned") per remote package; a locked build fails closed (SignerMismatch) if the signer differs -- including a pre-signing lock with no signer, or a local-registry copy of a remotely signed package. - HTTP cache moves to <cache>/<name>/<version>/verified/{package,provenance}, installed by one atomic rename; the recorded signer is re-checked against today's trust list on every use; pre-signing cache entries are ignored. - `pkg lock` now also checks effect escalation against the fetched (signed) package's own manifest, not only the registry's unsigned metadata. - Registry::fetch_verified is a required trait method (no unchecked default for future remote registries). Local filesystem-registry packages are unaffected. Tests: riina-pkg 75 -> 96 (valid signature accepted; tampered archive, relabelled name/version, untrusted key, missing signature, malformed documents, server errors, lockfile signer mismatch all rejected; opt-out accepts and warns; keygen 0600/no-overwrite; Ed25519 KAT against Python cryptography/OpenSSL; loopback-registry fetch and publish round-trips) and a new riinac integration test drives keygen -> publish -> lock -> build through the real binary against a loopback registry, including a registry that later serves tampered bytes. No existing test asserted insecure behaviour; the atomic-cache test was adapted to the new cache layout. Law 8: the only new edge is the path dependency on first-party riina-core; no third-party crate. SBOM unchanged (`scripts/generate-sbom.sh --check` OK). Limits: no key revocation or expiry, no per-package key scoping (any trusted key may sign any name), key distribution is out of band, and the HTTP transport itself is still plain http (loopback only). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

…lity grants Closes audit findings M1c (total-order effect subsumption) and M1b (capability self-grant), which the typechecker hardening left as "model-level limitations". M1c — effects are now checked as a PARTIAL order. `Effect::join` is the Coq total-order `effect_join` (max level), so "performed level <= declared level" let `kesan Masa` (Time, 11) cover `fail_tulis` (FileSystem, 5), `cetak` (Write, 4), sockets (Network, 6), ..., and `join` collapsed `kesan (Masa, SistemFail)` to plain `Masa` in the function's TYPE, so callers lost the other components. * riina-types: new `EffectSet` (a Copy bitset, bit i = the effect of level i). `join` is set union (lossless); `covers(e)` is the partial order: Pure always; Mut (an observable write to an outer `biar ubah`, H2) by any non-pure set (not by `Bersih`, exactly as in the old order); any other e only by a member of the SAME `EffectCategory` with level >= e's. Alloc is NOT local (IO category; `kesan Peruntuk` covers Read, so a local Alloc would let a `Bersih` caller reach Read). `Effect` stays the single label. The order is a strict refinement of Coq's: whatever it accepts, the total order accepts, so the mechanized results still cover accepted programs. * `Ty::Fn`'s latent effect is an `EffectSet`; declared function types use the full declared set (`EffectSet::from_declaration(effect, effect_set)`) at top level, for local `fungsi`, and in `Fn(..) -> R kesan (A, B)` type annotations (the parser kept only the join there). * Typechecker: every judgement yields an `EffectSet`; the declared-effect check (`validate_top_level_decls`), LetRec/LetRecGroup latent checks and `types_compatible` on function types use `covers`; the capability gate checks every gated component of a latent set (it checked only the join); top-level bindings are checked per component (Network used to absorb a Write). `TypeError::EffectViolation.allowed` is the declared set, `found` the first uncovered effect. The LetRecGroup re-check now grants each body exactly its own declared set (the union over-grant, `body_grants`, existed only because the latent type was lossy). * riina-fmt / riina-doc print the whole declared set (fmt used to rewrite `kesan (Masa, SistemFail)` as `kesan Masa`, which no longer type-checks); codegen/riinac/lsp/wasm consumers updated (`total_join` where one label is needed). The capability gate itself stays EXACT membership. M1b — `beri` inside a function may only attenuate. `Expr::Grant` added X to the granted set unconditionally, so any function could `beri` itself Network/Process/... In top-level code `beri` remains the program's capability manifest. Inside any function body — top-level `fungsi`, local `fungsi`, closure — `beri X` is accepted only if X is covered by what the body held on entry (`grant_ceiling`, set by `enter_function`); else CapabilityViolation. A top-level function holds its declared set. A closure or local `fungsi` holds exactly its lexically enclosing grants: a local function's `kesan` now bounds its latent effect but grants nothing, and a local function is no longer "authorized by its own declaration" when called from top-level code (that route let top-level code open a socket with no `beri` by wrapping the call in a local `fungsi`). Tests: 3409 -> 3423 passing, 0 failing (2 ignored, unchanged). New audit_soundness tests m1c_* / m1b_* (15 negative programs, each accepted by the base branch's `riinac check` and rejected now; 13 positive neighbours accepted by both), EffectSet unit tests, a fmt round-trip test. Seven unit tests that asserted the lossy join (e.g. `Random ⊔ Network = Random` for a CSRF-protected POST) now assert the precise set. Test fixtures that relied on the unsound order had their annotations corrected, not the check weakened: end_to_end/wasm_c_differential/wasm_e2e `kesan Sistem` -> `kesan Tulis` (they only print), kripto_runtime `kesan (Kripto, Tulis)`, masa_differential `kesan (Masa, Tulis)`. Corpus: 98/172 -> 98/172, same passing set. The six `07_EXAMPLES/compiler/ *.rii` declared `utama() kesan Sistem` but only print; they failed closed and now declare `kesan Tulis` (run output unchanged). Known residual (not fixed here): an actor handler's latent effect is never charged (`Ty::Actor` does not carry it), so a `kesan (Rangkaian, Proses)` function that sends to an actor whose handler calls `fail_tulis` is accepted (pre-existing; the base branch accepts it too). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

…2, M3) Merges audit-fix/typechecker (4147e5b): labels, taint and constant-time tags survive erasure into Any; closures/loops/putus under a secret pc; assignment requires level(value) join pc <= level(ref); function values erased into Any are charged their latent effect; top-level code holds only explicit grants; linearity counts uses across nested scopes; CT tags survive generic calls and secret indexing. 33 new regression tests (all fail on the pre-fix code). Corpus: 98 of 172 examples pass `riinac check` (re-measured with the merged compiler; 28/28 of 00_basics/). linear_enforcement.rii was a false rejection; closures.rii and tainted_data.rii had their declarations corrected (the checks were right). website/public/metrics.json taken from this branch and regenerated by the hook. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

…ge signing Merges audit-fix/receipts-pkg, which carries audit-fix/runtime-tools: - 583d616 [TRACK_F] fail-closed manifest/hash-chain/proof-bundle verifiers, FIPS 204 pure ML-DSA defaults (interop-tested with OpenSSL), key hygiene, secret scrubbing in X25519/Ed25519/HMAC. - fe69d1d [TRACK_B] CSRF tokens from the OS RNG; per-connection TLS-kunci key exchange; honest server-side authentication flags; MCP runs Pure programs only by default under step/depth/time budgets; strict URL/referer checks in both backends; checked HTTP body arithmetic; http registries loopback-only. - fdf03e5 [TRACK_B] receipts chained with HMAC-SHA256 and sealed; the forgeable unkeyed FNV-1a mode removed. - f9228f7 [TRACK_B] Ed25519 publisher signatures for remote-registry packages with trusted-publisher configuration and lockfile signer pinning. CHANGELOG lists the user-visible behaviour changes (old ML-DSA signatures, MCP defaults, TLS-kunci wire format, re-locking remote packages). SBOM check OK (no third-party crates added). website/public/metrics.json regenerated by the hook. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

…-L6) Merges audit-fix/parser-codegen (46c8cb7): parser termination at EOF, nesting limits and iterative statement/if-chain parsing; persistent interpreter environment; linear operator-chain lowering; C string escaping and checked allocations; secret-boolean branching, signed division and Unicode parity across interpreter/C/WASM; riinac build/test/doc CLI hardening. Conflict resolution (riina-codegen): - interp.rs: runtime-tools' sandbox wrapper `eval_with_env` (step budget, depth cap) stays the entry point; parser-codegen's tail-looping evaluator becomes `eval_with_env_inner`, so every recursive evaluation still pays the MCP budget while long let/if chains no longer recurse. - value.rs: runtime-tools' `Env::without` reimplemented over the new persistent environment (filters the shadowing-resolved bindings). The resolved tree (minus the receipts/pkg crates) passed the full 03_PROTO suite and clippy -D warnings before this commit. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

…ing chains) The typechecker clones its context for every nested scope (each `biar`, each `kalau`/`padan` branch, each lambda) and keeps every clone alive down the recursion, and every clone COPIED its maps — the ~600 builtins included. Checking memory and time were therefore quadratic in the length of a binding chain, and the parser now accepts chains long enough to OOM the checker instead of failing cleanly. * riina-types: new `persistent::PMap` / `PSet`, an immutable, structure-sharing map. Clone is two `Rc` clones; insert/remove affect only the copy they are applied to. The newest entries sit in a short shared list (32); when it fills it is folded into an immutable hash-map level, and equal-weight levels merge like a binary counter (<= ~log2 n levels). Lookup is a bounded list scan plus one probe per level, with HashMap-update semantics (newest insert of a key wins; a removal hides older entries). With every scope alive, total memory is O(n log n). Unit tests compare it against an in-place `HashMap` across 5,000 random operations and forks. * Typechecker: `TypeEnv` (vars + linearity), the legacy `Context`, and the per-scope `slot_ids` / `fn_slot_ids` / `closure_writes` / `declared_fns` of `TypingContext` use them; `Context::to_typing_context` shares the builtin map instead of re-inserting it; the capability-summary environment in `program.rs` (cloned per `biar`, which made closure chains quadratic) too. * `StoreTy` (Σ) is backed by a `PMap` (each `ruj` allocation was copied into every nested scope's context). Lookup/shadowing semantics are unchanged; no typing rule changed. Measured with a release `riinac check` (peak RSS / wall), before -> after: 5,000 sequential `biar` 2,671 MiB / 17.8 s -> 36 MiB / 0.19 s 10,000 sequential `biar` (not run: ~10 GB) -> 69 MiB / 0.48 s 5,000-link `lain kalau` 1,173 MiB / 6.7 s -> 27 MiB / 0.12 s 10,000-link `lain kalau` 2,340 MiB / 13.8 s -> 50 MiB / 0.18 s 19,000-link `lain kalau` (not run: ~4.4 GB) -> 92 MiB / 0.23 s 2,000 `biar ubah` 907 MiB / 3.0 s -> 19 MiB / 0.09 s 2,000 `ruj` 943 MiB / 2.9 s -> 18 MiB / 0.09 s 2,000 closure bindings 1,003 MiB / 6.9 s -> 20 MiB / 0.13 s (Runs used a 1 GiB stack: the recursive parser/checker need more than the default 8 MiB at these depths; that limit is unchanged here.) Regression test `riina-typechecker/tests/context_scaling.rs` (its own test binary, so the process peak RSS is its own) checks 3,000-binding chains of each shape — `biar`, `lain kalau`, `biar ubah`, `ruj`, closures — and asserts each takes < 20 s and the process peak RSS stays < 512 MiB. Against the previous commit it FAILS (peak 2,061 MiB; 7.4 / 3.0 / 12.1 / 10.4 / 41.1 s in a debug build); now ~100 MiB (mostly debug recursion stack) and 0.15-0.28 s each. The riina-typechecker unit suite dropped from ~11 s to ~0.5 s. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

…nts, persistent typing context Merges audit-fix/effects (63cffa0, a1816b7), built on the typechecker fixes: - Declared and latent effects are EffectSets (bitset, join = union); an effect is covered only by a same-category declaration of equal or higher level. `kesan Masa` no longer authorizes file writes or networking, and a compound `kesan (A, B)` survives through function types. Strict refinement of the Coq total order (anything accepted now was accepted before). - `beri X` inside a function/closure/local fungsi requires X to be held already (attenuation only); top-level beri stays the capability manifest. - Persistent typing context: 5,000 sequential biar bindings 2.7 GB/17.8 s -> 36 MiB/0.19 s; long lain-kalau chains linear (context_scaling.rs). Conflict resolution: - riina-parser lib.rs: kept parser-codegen's iterative statement-frame parser and carried the effects change into its local-function frame (EffectSet::from_declaration over the whole declared set). - Semantic conflicts surfaced by the build: a parser-codegen interpreter test built `Ty::Fn(.., Effect::Pure)` (now `.into()`), and runtime-tools' MCP refusal took a single Effect (now EffectSet; the pure-only default is unchanged: an EffectSet equals Pure exactly when empty). Full 03_PROTO suite on the merged tree: 3,528 passed, 0 failed; clippy -D warnings clean; corpus 98/172 unchanged. Docs: CHANGELOG (behaviour change: declarations must list every category), master plan REQ-87 caveat, REQ-88 DONE, Part 11 entry and remaining limits. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

… fresh Coq warning report Counts after merging the four remediation branches, each re-measured: - 03_PROTO: `cargo test --all` 3,528 passed / 0 failed across 18 crates. README said 19 crates and 2,479 / 2,727 tests; the website said 19 crates and 3,002 tests; metrics.json still carried 3,376 from an older full run (fast mode preserves the last verified count, and no full run had happened since). Seeded with the measured 3,528, then regenerated in fast mode so the non-Coq lane levels keep their last full-refresh values. - 05_TOOLING: 352 passed / 0 failed (README said 248). - Coq warning report regenerated by a clean single-job build of all 334 modules: 0 warnings (budget 2); audit-docs now passes with no warnings. - Banners, metrics.json and ledgers synced; website rebuilt locally. Why not a full-mode metrics refresh: in this container the TLA+/Alloy/SMT lane levels come from check-noncoq-mechanized.sh, which needs Lean and Isabelle toolchains that are not installed here. A full run therefore reports those lanes "missing_or_stale" and downgrades SMT from mechanized — an environment fact, not a repository one (CI's SMT scoped set passes on this branch). No non-Coq source changed, so the last full-refresh values stand. Test fix: metrics_doc_consistency walked into .claude/ agent worktrees (other checkouts at other commits) and reported their banners as this tree's; it now skips .claude, matching the audit-docs.sh banner scan. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

Full-mode riinac verify record from the pre-push run of 4cb1ad4 (all four remediation branches merged): 3,528 Rust tests, 0 clippy warnings, 334 .vo, 0 Coq warnings, 10 kernel capstones (9 axiom-free). The TLA+/Alloy smoke jars are now provisioned in this container, so their rows report real runs; Lean and Isabelle remain WARN (toolchains not installed here). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

Regenerated on main after merging the audit remediation (PR #89, d40f538). Counts unchanged from the merge: 3,528 tests (verified by a full cargo test run on the merged tree), 12,819 Qed, 334 active files, 29 Parameter; only provenance moved. Non-Coq lane levels carried from the last full refresh. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

Full-mode riinac verify record from the pre-push run of 166ed50 on main (post-#89 merge chain): PASS; Transpiler Staleness now lists SMT only, since Alloy's claim level is back to generated. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

Merge d40f538, post-merge chain (provenance stamp, non-Coq report refresh and Alloy claim correction, manifest, verify.rs comment fix), public reconcile 5913ba3 -> 952949b. Website/gh-pages and the ib823/riina mirror NOT deployed: outside this session's repository access; owner action recorded. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

…Coq claims With a stale or missing reports/noncoq_mechanized_status.json, `generate-metrics.sh --fast` rebuilt every lane's *_COMPILED and *_MECHANIZED_READY from the previous metrics.json claimLevels and from smoke passes. A smoke pass therefore became a published "compiled" claim, and every later fast run re-read that claim as evidence, so the overclaim reinforced itself. This is what put Alloy at "compiled" during the PR #89 deploy, until the public claim-integrity gate refused it. - The fallback now carries only descriptive fields: pending reasons, with "none" mapped to the stale-report reason; backlogs; and smoke results this run did not observe. Without a fresh report every non-Coq lane is generated, which public-quality-gates.sh already requires. - Smoke checks record whether they actually ran, so a cached pass can no longer mask a smoke check that now fails. - The report-compatibility rule now matches public-quality-gates.sh: content-identical lane paths, .md ignored, no ancestry requirement, and it fails closed on a missing commit or a failing diff. - An Isabelle smoke pass no longer sets isabelleCompiled. The honesty policy that already covered F*, TLA+ and Alloy now covers Isabelle too. This flaw was masked only by the lane's retirement. scripts/test-generate-metrics-fallback.sh runs the generator in a throwaway clone. It fails 32 assertions against the previous generator and passes against this one. Published claims are unchanged, because the current report is fresh. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

Byproducts of scripts/deploy-website.sh: metrics provenance stamp (2fea4f5), the playground WASM rebuilt with the current compiler (1,544,535 -> 1,707,344 bytes; it predated the PR #89 merge), and report timestamps. The Dim1/Dim9 gate re-derived coq_theorem_count 54 -> 58. Derived counts unchanged: 3,528 tests (full cargo test), 12,819 Qed. Chain: gh-pages on ib823/riina 7298dc2 -> 35f41d8 (all public quality gates PASS before and after the build). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E6roGMqnThhqeobMHTkdGG

claude added 17 commits October 11, 2026 11:56

ib823 changed the title ~~Audit remediation: proof-integrity fixes, gate bypasses, supply-chain hardening~~ Audit remediation: proof integrity, new core theorems, compiler/runtime soundness, supply chain Oct 11, 2026

ib823 marked this pull request as ready for review October 12, 2026 01:02

ib823 merged commit d40f538 into main Oct 12, 2026
11 checks passed

ib823 mentioned this pull request Oct 12, 2026

[TRACK_F] FIX: Stop the fast-mode metrics fallback from carrying non-Coq claims #90

Merged

11 of 17 tasks

Navigation Menu

Repository navigation

Audit remediation: proof integrity, new core theorems, compiler/runtime soundness, supply chain - #89

Audit remediation: proof integrity, new core theorems, compiler/runtime soundness, supply chain#89
ib823 merged 18 commits into
mainfrom
ccr-db4b5499-udxc4o

ib823 commented Oct 11, 2026 •

edited

Loading

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

ib823 commented Oct 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Changes

Type

Testing

Checklist

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

ib823 commented Oct 11, 2026 •

edited

Loading