From 53800b1c713d65c24795f8ecff62dbc0cf06c3d6 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 24 Aug 2026 02:13:20 +0000 Subject: [PATCH 1/4] [ALL] CHORE: full-mode verification manifest at the #81 merge MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit riinac verify --full at a30830e0c: 3318 Rust tests, 0 clippy warnings, 331 .vo compiled, 0 admits, 0 axioms — the tree with the riina back-merge in it. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Uu28z8CdRQ1SLzTv8yszth --- VERIFICATION_MANIFEST.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/VERIFICATION_MANIFEST.md b/VERIFICATION_MANIFEST.md index 46714b14..70d6ee2a 100644 --- a/VERIFICATION_MANIFEST.md +++ b/VERIFICATION_MANIFEST.md @@ -1,6 +1,6 @@ # RIINA Verification Manifest -**Generated:** 2026-08-24T00:40:27Z -**Git SHA:** 07db416aa +**Generated:** 2026-08-24T02:12:25Z +**Git SHA:** a30830e0c **Mode:** full **Status:** PASS @@ -11,7 +11,7 @@ | Rust Tests | PASS | 3318 tests | | Clippy | PASS | 0 warnings | | _CoqProject Completeness | PASS | all 331 .v files listed in _CoqProject | -| Coq Compilation | PASS | 331 .vo files compiled in 225s | +| Coq Compilation | PASS | 331 .vo files compiled in 177s | | Coq Kernel Assumptions | PASS | 5 capstones attested; axioms within reviewed whitelist (1 allowed: funext) | | Coq Admits | PASS | 0 (target: 1) | | Coq Axioms | PASS | 0 (informational; explicit assumptions tracked separately) | @@ -24,7 +24,7 @@ | F* admit Scan | WARN | 12010 admit in 315 files (19 lemmas) | | TLA+ Compilation | PASS | Active spec TelusProcurementProtocol parsed and model checked in 1s (5 theorems, local_active) | | TLA+ Scan | PASS | 317 files (12282 theorems) | -| Alloy Compilation | PASS | Active model TelusProcurementAccessControl executed in 9s (6 checked assertions, local_active) | +| Alloy Compilation | PASS | Active model TelusProcurementAccessControl executed in 7s (6 checked assertions, local_active) | | Alloy Scan | PASS | 306 files (11627 assertions) | | SMT Scan | PASS | 318 files (12431 assertions) | | Verus admit Scan | PASS | 0 admit in 323 files (6395 proof fns) | From ec60368432bddc5dfb69b0525746dc38cc96d88e Mon Sep 17 00:00:00 2001 From: ib823 Date: Mon, 24 Aug 2026 07:58:17 +0800 Subject: [PATCH 2/4] [ALL] FEAT: lower `selagi`/`ulang` to structured WASM control flow (#11) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The WASM backend refused every loop. `emit_structured` knew only forward if/else regions, so a back edge had no structure to map onto; it failed closed (REQ-78) rather than emit the one-shot shape that loops were introduced to fix. It now emits real structured control flow: a `block` wrapping a `loop`, with the condition re-tested INSIDE the `loop` so it observes the body's writes, `br_if` to leave, `br 0` for the back edge and `lanjut`, and `br 1` for `putus`. Depths come from a frame stack, so nesting and loop control from inside an `if` arm resolve to the right label. Back edges are found by DOMINANCE over reachable blocks, not block order. Both parts are load-bearing: the lowerer allocates a loop's exit block BEFORE the body it follows, so `putus` branches to a lower index than the block it leaves; and it leaves an unreachable block behind after a `putus` that branches back into the middle of the loop it was cut out of. Index order accepts both as back edges and invents loops that are not there. Dominators are Cooper/Harvey/Kennedy (immediate-dominator array over reverse postorder) — the set-of-dominators fixpoint was written first and measured 1.8x the cost of all other WASM emission on a ~2,400-block function, worsening quadratically. Also fixes a WASM-only silent wrong answer this uncovered: the lowerer typed every `+` result `Int` unless an operand was in the numeric tower, so string concatenation came out `Ty::Int`. The concat was emitted correctly, but WASM dispatches `cetak`/`cetakln` on the static type (its values are untagged, unlike C's runtime tags), so it sent the result pointer through the integer path — every `cetakln("x=" + ke_teks(x))` printed a heap ADDRESS as a decimal number. `loops_are_refused_by_the_wasm_backend` is replaced by four differential tests asserting the opposite, and the four pre-existing loop tests gain a WASM leg. `untuk` keeps a refusal test, retargeted at the reason that actually blocks it (list literals, REQ-79). corpus_differential: 34 -> 35 dual-backend examples, all byte-equal. --- 03_PROTO/crates/riina-codegen/src/lower.rs | 12 + 03_PROTO/crates/riina-codegen/src/wasm.rs | 393 ++++++++++++++++-- .../crates/riinac/tests/loops_differential.rs | 271 +++++++++++- 07_EXAMPLES/12_kelayakan/README.md | 8 +- docs/guide/MUTABLE_STATE.md | 23 +- 5 files changed, 638 insertions(+), 69 deletions(-) diff --git a/03_PROTO/crates/riina-codegen/src/lower.rs b/03_PROTO/crates/riina-codegen/src/lower.rs index 34da7a9e..d93b88ab 100644 --- a/03_PROTO/crates/riina-codegen/src/lower.rs +++ b/03_PROTO/crates/riina-codegen/src/lower.rs @@ -1183,6 +1183,18 @@ impl Lower { (Ty::Decimal, _) | (_, Ty::Decimal) => Ty::Decimal, (Ty::Fixed, _) | (_, Ty::Fixed) => Ty::Fixed, (Ty::FixedBin, _) | (_, Ty::FixedBin) => Ty::FixedBin, + // `+` on strings is concatenation, not arithmetic. + // Typing the result `Int` made the WASM backend + // print `cetakln("i=" + ke_teks(i))` through its + // integer (itoa) path, so the program emitted the + // heap ADDRESS of the joined string as a decimal + // number. (The concat itself was right; only the + // result's static type was wrong. C dispatches on a + // runtime tag, so it was unaffected — this was a + // WASM-only silent wrong answer.) + (Ty::String, _) | (_, Ty::String) if matches!(op, BinOp::Add) => { + Ty::String + } _ => Ty::Int, } } diff --git a/03_PROTO/crates/riina-codegen/src/wasm.rs b/03_PROTO/crates/riina-codegen/src/wasm.rs index d6d3de57..8a4c070f 100644 --- a/03_PROTO/crates/riina-codegen/src/wasm.rs +++ b/03_PROTO/crates/riina-codegen/src/wasm.rs @@ -54,7 +54,7 @@ use crate::wasm_encode::{ }; use crate::{Error, Result}; -use std::collections::HashMap; +use std::collections::{HashMap, HashSet}; /// Initial heap pointer offset (after data section). /// Aligned to 16 bytes. @@ -4765,7 +4765,10 @@ impl WasmBackend { // Start at the entry block's index (via block_map, since blocks may // share a BlockId and the map keeps the last — e.g. hand-built test IR). let entry_idx = block_map.get(&func.entry).copied().unwrap_or(0); - self.emit_structured(entry_idx, None, func, &ctx, &block_map, &mut code)?; + let mut ctrl = Ctrl::new(func, &block_map); + self.emit_structured( + entry_idx, None, func, &ctx, &block_map, &mut code, &mut ctrl, + )?; if code.is_empty() || !matches!(code.last(), Some(&b) if b == Op::Return as u8) { wasm_i64c(&mut code, 0); @@ -4786,6 +4789,7 @@ impl WasmBackend { /// to the merge `Phi`. This is what makes a *nested* if/else correct: its /// exit is an inner merge block, which is the block the lowerer keys the /// outer `Phi` entry by; the entry block (an inner `CondBranch`) is not. + #[allow(clippy::too_many_arguments)] // an emitter context plus the CFG walk's own state fn emit_structured( &self, entry: usize, @@ -4794,12 +4798,26 @@ impl WasmBackend { ctx: &EmitCtx<'_>, block_map: &HashMap, code: &mut Vec, + ctrl: &mut Ctrl, ) -> Result> { let mut cur = entry; loop { if Some(cur) == stop { return Ok(None); } + + // A loop header we are not already inside: open the `block`/`loop` + // pair and emit the whole loop, then continue at its exit. + if ctrl.headers.contains(&cur) && !ctrl.frames.iter().any(|f| f.header == cur) { + match self.emit_loop(cur, func, ctx, block_map, code, ctrl)? { + Some(next) => { + cur = next; + continue; + } + None => return Ok(None), + } + } + let block = &func.blocks[cur]; self.emit_block_instrs(block, ctx, code)?; match &block.terminator { @@ -4824,21 +4842,33 @@ impl WasmBackend { // merge block, not the region's entry CondBranch). return Ok(Some(cur)); } - // A BACK edge — the CFG of a `selagi`/`ulang` loop. This - // emitter only knows how to structure forward if/else - // regions; following the edge would walk the same blocks - // forever. WASM needs real `loop`/`br_if` nesting, which - // is not built yet, so refuse the module rather than emit - // something that silently runs the body once (which is - // exactly the bug real loops were introduced to fix). - if t <= cur { + // `lanjut` / `putus`: an edge to an enclosing loop's header + // or exit, from somewhere inside it (typically an `if` arm, + // so deeper than the loop body's own top level). Both become + // an unconditional `br` to the right label depth; control + // does not come back, so the region diverges here. + if let Some(depth) = ctrl.br_depth_to_header(t) { + code.push(Op::Br as u8); + wasm_encode::encode_uleb128(depth as u64, code); + return Ok(None); + } + if let Some(depth) = ctrl.br_depth_to_exit(t) { + code.push(Op::Br as u8); + wasm_encode::encode_uleb128(depth as u64, code); + return Ok(None); + } + // A back edge that is NOT to an enclosing loop is a + // CFG shape this emitter cannot structure. Refuse + // rather than walk it forever or emit something wrong. + if ctrl.is_back_edge(cur, t) { return Err(Error::InvalidOperation( - "the WASM backend cannot yet compile `selagi`/`ulang` loops \ - (they need structured loop/br_if lowering). Use `riinac run`, \ - or `riinac build` for a native binary." + "the WASM backend cannot structure this control flow \ + (an irreducible back edge). Build for the native target." .to_string(), )); } + // Every remaining edge is forward, so the walk makes + // progress and terminates. cur = t; } None => return Ok(None), @@ -4854,26 +4884,17 @@ impl WasmBackend { return Ok(None); }; // The merge is where the two branches rejoin: the Branch - // target of the then (or else) branch. - let merge = Self::branch_target(&func.blocks[then_idx], block_map) - .or_else(|| Self::branch_target(&func.blocks[else_idx], block_map)); - - // A "merge" that points BACKWARDS is not a merge — it is the - // back edge of a `selagi`/`ulang` loop, whose header this - // block is. Continuing would re-emit the header forever - // (the emitter's own walk has no visited set). Structuring a - // loop needs real `loop`/`br_if` nesting, which is not built - // yet, so refuse the module: a backend that cannot express a - // construct fails closed rather than emitting something that - // silently runs the body once (REQ-78). - if merge.is_some_and(|m| m <= cur) { - return Err(Error::InvalidOperation( - "the WASM backend cannot yet compile `selagi`/`ulang` loops \ - (they need structured loop/br_if lowering). Use `riinac run`, \ - or `riinac build` for a native binary." - .to_string(), - )); - } + // target of the then (or else) branch. An arm that leaves via + // `putus`/`lanjut` has no merge of its own, so prefer the arm + // that does rejoin forwards. + let merge = [then_idx, else_idx] + .into_iter() + .filter_map(|b| { + let m = Self::branch_target(&func.blocks[b], block_map)?; + (!ctrl.is_back_edge(b, m) && !ctrl.targets_enclosing_loop(m)) + .then_some(m) + }) + .next(); if let Some(local) = ctx.var_map.get(cond) { code.push(Op::LocalGet as u8); @@ -4883,12 +4904,13 @@ impl WasmBackend { code.push(Op::If as u8); // Each branch pushes its i64 phi contribution as the block result. code.push(ValType::I64 as u8); + ctrl.depth += 1; // Emit each branch region, then push its contribution to the // merge phi from the region's EXIT block (its merge // predecessor), falling back to the entry block when the // region diverges (no exit-to-merge). let then_exit = - self.emit_structured(then_idx, merge, func, ctx, block_map, code)?; + self.emit_structured(then_idx, merge, func, ctx, block_map, code, ctrl)?; self.emit_phi_value_for_branch( &func.blocks[then_exit.unwrap_or(then_idx)], &func.blocks, @@ -4898,7 +4920,7 @@ impl WasmBackend { )?; code.push(Op::Else as u8); let else_exit = - self.emit_structured(else_idx, merge, func, ctx, block_map, code)?; + self.emit_structured(else_idx, merge, func, ctx, block_map, code, ctrl)?; self.emit_phi_value_for_branch( &func.blocks[else_exit.unwrap_or(else_idx)], &func.blocks, @@ -4907,6 +4929,7 @@ impl WasmBackend { code, )?; code.push(Op::End as u8); + ctrl.depth -= 1; // Store the if/else result into the merge's phi local. if let Some(m) = merge { for instr in &func.blocks[m].instrs { @@ -4923,10 +4946,10 @@ impl WasmBackend { Some(m) => cur = m, None => { // No merge: BOTH arms diverge (each ends in a - // `return`), so nothing rejoins. The `if` was - // still typed `(result i64)`, so its result is - // sitting on the operand stack with no phi local - // to receive it — wasmtime rejects that as + // `return`, or leaves the enclosing loop), so nothing + // rejoins. The `if` was still typed `(result i64)`, so + // its result is sitting on the operand stack with no + // phi local to receive it — wasmtime rejects that as // "values remaining on stack at end of block". // // Control genuinely cannot reach here, so say so: @@ -4945,6 +4968,102 @@ impl WasmBackend { } } + /// Emit one `selagi`/`ulang` loop as WASM structured control flow, given its + /// header block. Returns the block index to continue at (the loop's exit), or + /// `None` if the loop cannot be left by falling out of it. + /// + /// The CFG the lowerer builds is + /// + /// ```text + /// header: CondBranch(cond, body, exit) + /// body: Branch(header) // the back edge + /// exit: ... + /// ``` + /// + /// and the shape emitted for it is + /// + /// ```wat + /// block ;; br 1 from the loop body == leave (putus) + /// loop ;; br 0 from the loop body == repeat (lanjut) + /// + /// i32.eqz + /// br_if 1 ;; condition false -> leave + /// + /// br 0 ;; back edge + /// end + /// end + /// ``` + /// + /// The condition lives INSIDE the `loop`, so it is re-evaluated every + /// iteration — that is what makes it a loop rather than a guarded block. + fn emit_loop( + &self, + header: usize, + func: &Function, + ctx: &EmitCtx<'_>, + block_map: &HashMap, + code: &mut Vec, + ctrl: &mut Ctrl, + ) -> Result> { + let Some(Terminator::CondBranch { + cond, + then_block, + else_block, + }) = &func.blocks[header].terminator + else { + // A back edge onto a block that does not test a condition is not a + // shape this lowerer produces. Refuse rather than guess. + return Err(Error::InvalidOperation( + "the WASM backend cannot structure a loop whose header does not \ + end in a conditional branch. Build for the native target." + .to_string(), + )); + }; + let (Some(&body_idx), Some(&exit_idx)) = + (block_map.get(then_block), block_map.get(else_block)) + else { + return Ok(None); + }; + + code.push(Op::Block as u8); + code.push(0x40); // void blocktype + code.push(Op::Loop as u8); + code.push(0x40); + ctrl.depth += 2; + ctrl.frames.push(LoopFrame { + header, + exit: exit_idx, + depth_inside: ctrl.depth, + }); + + // The condition is part of the header block's instructions. + self.emit_block_instrs(&func.blocks[header], ctx, code)?; + if let Some(local) = ctx.var_map.get(cond) { + code.push(Op::LocalGet as u8); + wasm_encode::encode_uleb128(*local as u64, code); + code.push(Op::I32WrapI64 as u8); // bool cell -> i32 condition + } + code.push(Op::I32Eqz as u8); // leave when the condition is FALSE + code.push(Op::BrIf as u8); + wasm_encode::encode_uleb128(1, code); // out of the `loop`, to the `block` end + + // The body, up to the back edge. + let body_exit = + self.emit_structured(body_idx, Some(header), func, ctx, block_map, code, ctrl)?; + if body_exit.is_some() { + // Fell through to the back edge: repeat. + code.push(Op::Br as u8); + wasm_encode::encode_uleb128(0, code); + } + + code.push(Op::End as u8); // loop + code.push(Op::End as u8); // block + ctrl.depth -= 2; + ctrl.frames.pop(); + + Ok(Some(exit_idx)) + } + /// The block index a block unconditionally branches to, if any. fn branch_target(block: &BasicBlock, block_map: &HashMap) -> Option { match &block.terminator { @@ -6946,6 +7065,202 @@ struct EmitCtx<'a> { scratch: u32, } +/// One enclosing `selagi`/`ulang` loop, while its body is being emitted. +/// +/// Every loop is emitted as a `block` wrapping a `loop`, so from a point at +/// control depth `d` inside it: +/// +/// - `br (d - depth_inside)` re-enters the `loop` — `lanjut` (continue) +/// - `br (d - depth_inside + 1)` leaves the `block` — `putus` (break) +struct LoopFrame { + /// Block index of the loop header (the block that tests the condition). + header: usize, + /// Block index the loop falls out to when the condition is false. + exit: usize, + /// `Ctrl::depth` immediately after this loop's `block`/`loop` were opened. + depth_inside: u32, +} + +/// Structured-control-flow state threaded through `emit_structured`. +/// +/// WASM has no `goto`: a jump is `br N`, where `N` counts *enclosing control +/// frames* outward from the branch site. So turning the IR's CFG edges back +/// into branches needs two things the CFG does not carry — which blocks are +/// loop headers, and how deeply nested the current emission point is. +struct Ctrl { + /// Blocks that are the target of a back edge, i.e. loop headers. + headers: HashSet, + /// Every back edge, as (source, target) block indices. + back_edges: HashSet<(usize, usize)>, + /// Loops currently open, outermost first. + frames: Vec, + /// Number of control frames (`block`/`loop`/`if`) open right now. + depth: u32, +} + +impl Ctrl { + /// Find the loop headers of a function: the target of every back edge, + /// where a back edge is an edge `u -> v` whose target dominates its source. + /// + /// Dominance, not block order. The lowerer allocates a loop's exit block + /// *before* the body it follows, so `putus` branches to a LOWER index than + /// the block it leaves — index order would call that a back edge and invent + /// a loop around the exit. It also leaves unreachable blocks behind (the + /// one opened after a `putus` for whatever follows it textually), which + /// branch into the middle of the loop they were cut out of. Reachability + /// plus dominance rejects both, and accepts exactly the real back edge. + fn new(func: &Function, block_map: &HashMap) -> Self { + let n = func.blocks.len(); + let entry = block_map.get(&func.entry).copied().unwrap_or(0); + let mut ctrl = Self { + headers: HashSet::new(), + back_edges: HashSet::new(), + frames: Vec::new(), + depth: 0, + }; + if n == 0 || entry >= n { + return ctrl; + } + + let mut succs: Vec> = vec![Vec::new(); n]; + for (i, block) in func.blocks.iter().enumerate() { + let targets: &[&BlockId] = match &block.terminator { + Some(Terminator::Branch(t)) => &[t], + Some(Terminator::CondBranch { + then_block, + else_block, + .. + }) => &[then_block, else_block], + _ => &[], + }; + for t in targets { + if let Some(&idx) = block_map.get(t) { + succs[i].push(idx); + } + } + } + + // Reachable blocks in reverse postorder. Anything unreachable is dead + // code the emitter never walks, so its edges must not shape the output. + let mut postorder = Vec::new(); + let mut seen = vec![false; n]; + let mut stack = vec![(entry, 0usize)]; + seen[entry] = true; + while let Some((b, i)) = stack.pop() { + if i < succs[b].len() { + stack.push((b, i + 1)); + let s = succs[b][i]; + if !seen[s] { + seen[s] = true; + stack.push((s, 0)); + } + } else { + postorder.push(b); + } + } + let rpo: Vec = postorder.iter().rev().copied().collect(); + let mut rpo_num = vec![usize::MAX; n]; + for (i, &b) in rpo.iter().enumerate() { + rpo_num[b] = i; + } + + let mut preds: Vec> = vec![Vec::new(); n]; + for &b in &rpo { + for &s in &succs[b] { + preds[s].push(b); + } + } + + // Cooper/Harvey/Kennedy: keep only the IMMEDIATE dominator of each + // block and walk the tree for the (few) dominance queries below. The + // textbook set-of-dominators fixpoint is quadratic in block count — + // measured 1.8x slower than the rest of WASM emission on a function + // with ~2,400 blocks, and worsening — while this is near-linear. + const NONE: usize = usize::MAX; + fn intersect(mut a: usize, mut b: usize, idom: &[usize], rpo_num: &[usize]) -> usize { + while a != b { + while rpo_num[a] > rpo_num[b] { + a = idom[a]; + } + while rpo_num[b] > rpo_num[a] { + b = idom[b]; + } + } + a + } + let mut idom = vec![NONE; n]; + idom[entry] = entry; + let mut changed = true; + while changed { + changed = false; + for &b in &rpo { + if b == entry { + continue; + } + let mut candidate = NONE; + for &p in &preds[b] { + if idom[p] == NONE { + continue; // not yet processed on this pass + } + candidate = if candidate == NONE { + p + } else { + intersect(p, candidate, &idom, &rpo_num) + }; + } + if candidate != NONE && idom[b] != candidate { + idom[b] = candidate; + changed = true; + } + } + } + let dominates = |v: usize, mut u: usize| loop { + if u == v { + return true; + } + if u == entry || idom[u] == NONE || idom[u] == u { + return false; + } + u = idom[u]; + }; + + for &b in &rpo { + for &s in &succs[b] { + if dominates(s, b) { + ctrl.back_edges.insert((b, s)); + ctrl.headers.insert(s); + } + } + } + ctrl + } + + /// Whether the edge `from -> to` closes a loop. + fn is_back_edge(&self, from: usize, to: usize) -> bool { + self.back_edges.contains(&(from, to)) + } + + /// `br` depth that re-enters the enclosing loop headed by `block`, if any. + fn br_depth_to_header(&self, block: usize) -> Option { + let frame = self.frames.iter().rev().find(|f| f.header == block)?; + Some(self.depth - frame.depth_inside) + } + + /// `br` depth that leaves the enclosing loop whose exit is `block`, if any. + fn br_depth_to_exit(&self, block: usize) -> Option { + let frame = self.frames.iter().rev().find(|f| f.exit == block)?; + Some(self.depth - frame.depth_inside + 1) + } + + /// Whether `block` is an enclosing loop's header or exit — i.e. reaching it + /// is a `lanjut`/`putus`, not an if/else rejoining at a merge. + fn targets_enclosing_loop(&self, block: usize) -> bool { + self.frames + .iter() + .any(|f| f.header == block || f.exit == block) + } +} + impl Backend for WasmBackend { fn emit(&self, program: &Program) -> Result { let module = self.translate(program)?; diff --git a/03_PROTO/crates/riinac/tests/loops_differential.rs b/03_PROTO/crates/riinac/tests/loops_differential.rs index 7e1bd2ed..8d147762 100644 --- a/03_PROTO/crates/riinac/tests/loops_differential.rs +++ b/03_PROTO/crates/riinac/tests/loops_differential.rs @@ -32,11 +32,17 @@ //! //! # The WASM half //! -//! `emit_structured` only knows how to structure FORWARD if/else regions, so a -//! loop's back edge would walk the same blocks forever. It now refuses the -//! module instead, and `loops_are_refused_by_the_wasm_backend` pins that: a -//! backend that cannot express a construct must fail closed, never silently -//! emit something that runs the body once (REQ-78). +//! `emit_structured` used to know only FORWARD if/else regions, so a loop's +//! back edge would have walked the same blocks forever; the backend refused +//! the module instead (REQ-78 fail-closed). It now emits real structured +//! control flow — a `block` wrapping a `loop`, with `br_if` for the exit test, +//! `br 0` for the back edge and `lanjut`, and `br 1` for `putus` — so WASM is +//! a third independent implementation of loop semantics to differ against. +//! +//! Three of the four backends therefore reach a loop by different routes: the +//! interpreter iterates directly, C follows a CFG back edge through `goto`, and +//! WASM re-enters a structured `loop` by label depth. Agreement between those +//! is much stronger evidence than any hand-written expectation. use std::path::PathBuf; use std::process::Command; @@ -158,6 +164,40 @@ fn run_native(sb: &Sandbox, src: &PathBuf) -> String { String::from_utf8_lossy(&run.stdout).into_owned() } +/// Build `src` for `wasm32` and run the module under wasmtime. +/// +/// The WASM backend is the one that has to *reconstruct* structure from the +/// CFG, so a loop shape it gets wrong shows up either as a module wasmtime +/// rejects (a bad `br` depth is a validation error, not a wrong answer) or as +/// output that disagrees with the other two backends. Both are caught here. +fn run_wasm(sb: &Sandbox, src: &PathBuf) -> String { + let build = Command::new(env!("CARGO_BIN_EXE_riinac")) + .args(["build", "--target", "wasm32"]) + .arg(src) + .output() + .expect("riinac build --target wasm32"); + assert!( + build.status.success(), + "wasm build failed: {}{}", + String::from_utf8_lossy(&build.stdout), + String::from_utf8_lossy(&build.stderr) + ); + let wasm = sb.dir.join(format!("{}.wasm", sb.stem)); + let run = Command::new("wasmtime") + .arg("run") + .arg(&wasm) + .output() + .expect("wasmtime run"); + assert!( + run.status.success(), + "wasmtime rejected or trapped on the module (exit {:?}): {}{}", + run.status.code(), + String::from_utf8_lossy(&run.stdout), + String::from_utf8_lossy(&run.stderr) + ); + String::from_utf8_lossy(&run.stdout).into_owned() +} + /// `selagi` runs its body until the condition goes false, and a `biar ubah` /// write inside the body survives the iteration that made it. /// @@ -184,6 +224,9 @@ fungsi utama() -> Nombor kesan Tulis { if require_backend_tools(&["cc"]) { assert_eq!(run_native(&sb, &src), interp, "C backend disagrees"); } + if require_backend_tools(&["wasmtime"]) { + assert_eq!(run_wasm(&sb, &src), interp, "WASM backend disagrees"); + } } /// An accumulator loop. The answer is checked absolutely: 5050 is the sum @@ -216,6 +259,9 @@ fungsi utama() -> Nombor kesan Tulis { if require_backend_tools(&["cc"]) { assert_eq!(run_native(&sb, &src), interp, "C backend disagrees"); } + if require_backend_tools(&["wasmtime"]) { + assert_eq!(run_wasm(&sb, &src), interp, "WASM backend disagrees"); + } } /// A local accumulator keeps the function `kesan Bersih`. @@ -272,6 +318,9 @@ fungsi utama() -> Nombor kesan Tulis { if require_backend_tools(&["cc"]) { assert_eq!(run_native(&sb, &src), interp, "C backend disagrees"); } + if require_backend_tools(&["wasmtime"]) { + assert_eq!(run_wasm(&sb, &src), interp, "WASM backend disagrees"); + } } /// `pulang` inside a loop unwinds to the enclosing FUNCTION, not to the loop. @@ -304,6 +353,9 @@ fungsi utama() -> Nombor kesan Tulis { if require_backend_tools(&["cc"]) { assert_eq!(run_native(&sb, &src), interp, "C backend disagrees"); } + if require_backend_tools(&["wasmtime"]) { + assert_eq!(run_wasm(&sb, &src), interp, "WASM backend disagrees"); + } } /// A parameter named like an enclosing `biar ubah` is an ordinary immutable @@ -424,15 +476,18 @@ fungsi utama() -> Nombor kesan Tulis { } } -/// The WASM backend refuses a loop rather than miscompiling it. +/// The WASM backend compiles a loop, and gets the same answer as the other two. /// -/// `emit_structured` handles forward if/else regions only; a back edge needs -/// real `loop`/`br_if` nesting, which is not built. Failing closed is the -/// standing rule for a backend that cannot express a construct (REQ-78) — the -/// alternative, silently emitting the old one-shot shape, is the bug. +/// This replaces `loops_are_refused_by_the_wasm_backend`. The refusal was +/// honest but temporary: `emit_structured` handled forward if/else regions +/// only, so a back edge had no structure to map onto and the backend failed +/// closed (REQ-78) rather than emit the one-shot shape loops were introduced to +/// fix. It now emits a `block` wrapping a `loop`, so the construct is expressed +/// rather than refused — and the assertion flips from "must fail" to "must +/// agree". #[test] -fn loops_are_refused_by_the_wasm_backend() { - let sb = Sandbox::new("wasmrefuse"); +fn a_loop_compiles_to_wasm_and_agrees() { + let sb = Sandbox::new("wasmloop"); let src = sb.src( r#" fungsi utama() -> Nombor kesan Tulis { @@ -445,25 +500,199 @@ fungsi utama() -> Nombor kesan Tulis { } "#, ); + let interp = run_interp(&src); + assert_eq!(interp, "3\n", "interpreter"); + if require_backend_tools(&["cc"]) { + assert_eq!(run_native(&sb, &src), interp, "C backend disagrees"); + } + if require_backend_tools(&["wasmtime"]) { + assert_eq!(run_wasm(&sb, &src), interp, "WASM backend disagrees"); + } +} + +/// Nested loops, `putus` and `lanjut` from inside an `if` arm, a loop inside an +/// `if` arm, and `selagi betul` left only by `putus` — all in one program. +/// +/// Each of these is a distinct label-depth calculation in the WASM emitter, and +/// an off-by-one in any of them is silent: `br 1` where `br 2` was meant still +/// validates, it just leaves the wrong loop. Only the ANSWER catches that, +/// which is why this is differential rather than a byte-comparison on the +/// emitted module. +#[test] +fn nested_loops_and_loop_control_agree_across_backends() { + let sb = Sandbox::new("wasmnest"); + let src = sb.src( + r#" +fungsi utama() -> Nombor kesan Tulis { + biar ubah i = 0; + biar ubah jum = 0; + selagi i < 5 { + biar ubah j = 0; + selagi j < 4 { + kalau j == 2 { j = j + 1; lanjut; } lain { () }; + jum = jum + (i * 10 + j); + j = j + 1; + }; + i = i + 1; + }; + cetakln(ke_teks(jum)); + + biar ubah k = 0; + kalau jum > 0 { + selagi k < 3 { k = k + 1; }; + () + } lain { + k = 99; + () + }; + cetakln(ke_teks(k)); + + biar ubah m = 0; + selagi betul { + m = m + 1; + kalau m == 7 { putus; } lain { () }; + }; + cetakln(ke_teks(m)); + pulang 0; +} +"#, + ); + // 320 = sum over i in 0..5, j in {0,1,3} of (i*10 + j); k = 3; m = 7. + let interp = run_interp(&src); + assert_eq!(interp, "320\n3\n7\n", "interpreter"); + if require_backend_tools(&["cc"]) { + assert_eq!(run_native(&sb, &src), interp, "C backend disagrees"); + } + if require_backend_tools(&["wasmtime"]) { + assert_eq!(run_wasm(&sb, &src), interp, "WASM backend disagrees"); + } +} + +/// `pulang` from inside a loop, in a callee, on WASM. +/// +/// An early return unwinds past the `block`/`loop` frames the emitter opened. +/// WASM's `return` does that correctly only if the frames were balanced in the +/// first place; an unbalanced one is a validation error, so wasmtime refusing +/// the module is the failure mode this pins. +#[test] +fn pulang_out_of_a_wasm_loop_unwinds_the_function() { + let sb = Sandbox::new("wasmret"); + let src = sb.src( + r#" +fungsi cari(had: Nombor) -> Nombor kesan Bersih { + biar ubah i = 1; + selagi i < 1000 { + kalau i * i > had { pulang i; } lain { () }; + i = i + 1; + }; + 0 - 1 +} + +fungsi gcd(a: Nombor, b: Nombor) -> Nombor kesan Bersih { + biar ubah x = a; + biar ubah y = b; + selagi y != 0 { + biar t = y; + y = x % y; + x = t; + }; + x +} + +fungsi utama() -> Nombor kesan Tulis { + cetakln(ke_teks(cari(50))); + cetakln(ke_teks(cari(10000))); + cetakln(ke_teks(gcd(1071, 462))); + pulang 0; +} +"#, + ); + let interp = run_interp(&src); + assert_eq!(interp, "8\n101\n21\n", "interpreter"); + if require_backend_tools(&["cc"]) { + assert_eq!(run_native(&sb, &src), interp, "C backend disagrees"); + } + if require_backend_tools(&["wasmtime"]) { + assert_eq!(run_wasm(&sb, &src), interp, "WASM backend disagrees"); + } +} + +/// `"..." + ke_teks(n)` prints the JOINED STRING on WASM, not a heap address. +/// +/// The lowerer typed every `+` result `Int` unless an operand was in the +/// numeric tower, so a string concatenation came out `Ty::Int`. The concat +/// itself was emitted correctly — only the static type was wrong — but +/// `cetakln` dispatches on that type in the WASM backend (values are untagged +/// i32 there, unlike C's runtime tags), so it sent the result pointer through +/// the integer path and printed a small decimal number. Every `cetakln("x=" + +/// ...)` in the corpus printed an address, silently, on WASM only. +#[test] +fn string_concatenation_prints_as_a_string_on_wasm() { + let sb = Sandbox::new("wasmconcat"); + let src = sb.src( + r#" +fungsi utama() -> Nombor kesan Tulis { + biar ubah i = 0; + selagi i < 3 { + cetakln("i=" + ke_teks(i) + "!"); + i = i + 1; + }; + cetakln("akhir=" + ke_teks(i)); + pulang 0; +} +"#, + ); + let interp = run_interp(&src); + assert_eq!(interp, "i=0!\ni=1!\ni=2!\nakhir=3\n", "interpreter"); + if require_backend_tools(&["cc"]) { + assert_eq!(run_native(&sb, &src), interp, "C backend disagrees"); + } + if require_backend_tools(&["wasmtime"]) { + assert_eq!(run_wasm(&sb, &src), interp, "WASM backend disagrees"); + } +} + +/// `untuk` is still refused by WASM — for the LIST reason, not a loop reason. +/// +/// `untuk` is sugar for `senarai_peta` over a closure, so it never went through +/// `emit_structured`'s loop path and the loop work does not unblock it. What +/// blocks it is list literals, which the WASM backend declares unsupported +/// (REQ-79) and fails closed on. Pinning the *message* keeps the two gaps from +/// being confused: a future regression that made loops fail again would fail +/// this test with the wrong reason rather than pass by coincidence. +#[test] +fn untuk_is_refused_by_wasm_for_the_list_gap_not_the_loop_gap() { + let sb = Sandbox::new("wasmuntuk"); + let src = sb.src( + r#" +fungsi utama() -> Nombor kesan Tulis { + biar ubah jumlah = 0; + untuk x dalam [1, 2, 3, 4, 5] { + jumlah = jumlah + x; + }; + cetakln(ke_teks(jumlah)); + pulang 0; +} +"#, + ); + assert_eq!(run_interp(&src), "15\n", "interpreter"); let out = Command::new(env!("CARGO_BIN_EXE_riinac")) .args(["build", "--target", "wasm32"]) .arg(&src) .output() .expect("riinac build wasm32"); - assert!( - !out.status.success(), - "the WASM backend must FAIL on a loop, not emit a module that runs the \ - body once: {}{}", - String::from_utf8_lossy(&out.stdout), - String::from_utf8_lossy(&out.stderr) - ); let msg = format!( "{}{}", String::from_utf8_lossy(&out.stdout), String::from_utf8_lossy(&out.stderr) ); assert!( - msg.contains("selagi") || msg.contains("loop"), - "the refusal should name loops as the reason, got: {msg}" + !out.status.success(), + "WASM cannot build list literals yet, so this must fail closed: {msg}" + ); + assert!( + msg.contains("list"), + "the refusal must name LISTS as the reason — a loop-shaped refusal here \ + would be a regression in the loop lowering, got: {msg}" ); } diff --git a/07_EXAMPLES/12_kelayakan/README.md b/07_EXAMPLES/12_kelayakan/README.md index f3605f8e..08a3e7b7 100644 --- a/07_EXAMPLES/12_kelayakan/README.md +++ b/07_EXAMPLES/12_kelayakan/README.md @@ -83,6 +83,8 @@ All of it silently wrong, none of it diagnosed: - `dasar`, `lajur`, `sahkan` and `luaran` are keywords, so they cannot be used as module, variable or function names — hence `peraturan`, `medan` and `semak_rahsia`. -- `riinac build --target wasm32` refuses this program: the WASM emitter cannot - structure a loop's back edge yet, and fails closed rather than emitting the - old one-shot shape. +- `riinac build --target wasm32` still refuses this program, but no longer + because of its loops — those compile now, to a `block`/`loop` pair with + `br_if`. What it refuses is the `panjang` builtin, which that backend has not + implemented; it fails closed rather than emit a stub that returns a wrong + length (REQ-78). diff --git a/docs/guide/MUTABLE_STATE.md b/docs/guide/MUTABLE_STATE.md index 967bdaa3..74377fb0 100644 --- a/docs/guide/MUTABLE_STATE.md +++ b/docs/guide/MUTABLE_STATE.md @@ -121,9 +121,20 @@ Writes to an enclosing `biar ubah` slot from inside a `untuk` body do survive |---|---|---| | Interpreter (`riinac run`) | yes | yes | | C (`riinac build`) | yes | yes | -| WASM (`riinac build --target wasm32`) | **refused** | yes | - -The WASM emitter structures forward `if`/`else` regions only; a loop's back edge -needs real `loop`/`br_if` nesting, which is not built yet. It fails closed with -a message naming loops, rather than emitting the old one-shot shape — a backend -that cannot express a construct must refuse it (REQ-78). +| WASM (`riinac build --target wasm32`) | yes | **refused** | + +The WASM emitter reconstructs structured control flow from the IR's CFG. A +`selagi`/`ulang` loop becomes a `block` wrapping a `loop`: the condition is +re-tested inside the `loop` so it sees the body's writes, `br_if` leaves when it +goes false, `br 0` is the back edge (and `lanjut`), and `br 1` is `putus`. + +Which edges close a loop is decided by **dominance**, not block order. The +lowerer allocates a loop's exit block before the body it follows, so `putus` +branches to a lower-numbered block than the one it leaves; and it leaves an +unreachable block behind after a `putus` for whatever followed it textually. +Index order would read both as back edges and invent loops that are not there. + +`untuk` is refused on WASM, but for an unrelated reason: it desugars to +`senarai_peta` over a list literal, and list literals are not supported by that +backend yet (REQ-79). As always the refusal is explicit — a backend that cannot +express a construct must fail closed rather than emit a stub (REQ-78). From 908de41c98ba0eff8437cd9d9c5a7f8fe34dff85 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 24 Aug 2026 02:28:41 +0000 Subject: [PATCH 3/4] [ALL] CHORE: metrics + banner sync for the #11 back-merge (3318 -> 3322) The four tests riina's #11 adds move the count that 47 doc banners quote. Re-derived by command. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Uu28z8CdRQ1SLzTv8yszth --- 02_FORMAL/coq/DELEGATION_TASKS.md | 2 +- 02_FORMAL/coq/TASK_PROMPTS.md | 2 +- 02_FORMAL/coq/ZERO_AXIOM_ATTACK_PLAN.md | 2 +- .../coq/properties/BRIDGE_ANALYSIS_CONCLUSION.md | 2 +- 04_SPECS/README.md | 2 +- 04_SPECS/RIINA_PRIME_DIRECTIVE_GAP_CLOSURE.md | 2 +- 04_SPECS/cross-cutting/README.md | 2 +- 04_SPECS/industries/README.md | 2 +- .../REGULATORY_COMPLIANCE_MALAYSIA_SINGAPORE_2026.md | 2 +- .../language/RIINA_MATERIALIZATION_PLAN_v1_0_0.md | 2 +- 04_SPECS/language/SYNTAX_IMPROVEMENT_SPEC_v2_0_0.md | 2 +- 04_SPECS/scope/README.md | 2 +- 04_SPECS/scope/RIINA_ARCHITECTURE_CORRECTED.md | 2 +- 04_SPECS/scope/RIINA_DEFINITIVE_SCOPE.md | 2 +- 04_SPECS/scope/RIINA_RESEARCH_EXECUTION_MAP.md | 2 +- 06_COORDINATION/ATTACK_PROOF_MAP.md | 2 +- 06_COORDINATION/AXIOM_ELIMINATION_STRATEGY.md | 2 +- 06_COORDINATION/CLAUDE_AI_WEB_SUPPLEMENT.md | 2 +- 06_COORDINATION/CLAUDE_WEB_DELEGATION_SESSION49.md | 2 +- 06_COORDINATION/COORDINATION_LOG.md | 2 +- 06_COORDINATION/DELEGATION_PROMPT_PHASE0.md | 2 +- 06_COORDINATION/DOMAIN_COVERAGE_MATRIX.md | 2 +- 06_COORDINATION/RESEARCH_INTEGRATION_AUDIT.md | 2 +- .../AXIOM_ELIMINATION_ASSESSMENT.md | 2 +- .../axiom_elimination/EXECUTION_REPORT.md | 2 +- .../axiom_elimination/EXECUTION_REPORT_FINAL.md | 2 +- .../axiom_elimination/EXECUTION_REPORT_v2.md | 2 +- .../axiom_elimination/PHASE2_DEFINITIVE_SUMMARY.md | 2 +- .../PHASE3_INFRASTRUCTURE_SUMMARY.md | 2 +- .../axiom_elimination/PHASE_5_COMPLETE_PROMPT.md | 2 +- .../axiom_elimination/PHASE_5_COMPLETION_REPORT.md | 2 +- 06_COORDINATION/iris_migration_spec.md | 2 +- 06_COORDINATION/llm_proof_pipeline_design.md | 2 +- 07_EXAMPLES/06_ai_context/RIINA_FOR_AI.md | 2 +- CHANGELOG.md | 2 +- CONTRIBUTING.md | 4 ++-- README.md | 2 +- docs/enterprise/CERTIFICATION.md | 2 +- docs/enterprise/COMPLIANCE_GUIDE.md | 2 +- website/public/metrics.json | 12 ++++++------ 40 files changed, 46 insertions(+), 46 deletions(-) diff --git a/02_FORMAL/coq/DELEGATION_TASKS.md b/02_FORMAL/coq/DELEGATION_TASKS.md index 05ad3a51..13aebef4 100644 --- a/02_FORMAL/coq/DELEGATION_TASKS.md +++ b/02_FORMAL/coq/DELEGATION_TASKS.md @@ -1,6 +1,6 @@ # DELEGATION TASKS FOR CLAUDE AI (WEB) -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) ## TASK 1: exp_rel_step1_fst diff --git a/02_FORMAL/coq/TASK_PROMPTS.md b/02_FORMAL/coq/TASK_PROMPTS.md index 13829735..b1a97961 100644 --- a/02_FORMAL/coq/TASK_PROMPTS.md +++ b/02_FORMAL/coq/TASK_PROMPTS.md @@ -1,6 +1,6 @@ # TASK PROMPTS FOR CLAUDE AI (WEB) -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) Use these by copying the CLAUDE_AI_DELEGATION_PROMPT.md first, then appending one of these tasks in Section 4. diff --git a/02_FORMAL/coq/ZERO_AXIOM_ATTACK_PLAN.md b/02_FORMAL/coq/ZERO_AXIOM_ATTACK_PLAN.md index be9f9c06..f4115512 100644 --- a/02_FORMAL/coq/ZERO_AXIOM_ATTACK_PLAN.md +++ b/02_FORMAL/coq/ZERO_AXIOM_ATTACK_PLAN.md @@ -1,6 +1,6 @@ # ZERO AXIOM ATTACK PLAN -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) ## Current State (Session 27) diff --git a/02_FORMAL/coq/properties/BRIDGE_ANALYSIS_CONCLUSION.md b/02_FORMAL/coq/properties/BRIDGE_ANALYSIS_CONCLUSION.md index 8da86379..e180474d 100644 --- a/02_FORMAL/coq/properties/BRIDGE_ANALYSIS_CONCLUSION.md +++ b/02_FORMAL/coq/properties/BRIDGE_ANALYSIS_CONCLUSION.md @@ -1,6 +1,6 @@ # RIINA Bridge Analysis Conclusion -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) ## Worker: WORKER_ζ (Zeta) ## Date: 2026-01-17 diff --git a/04_SPECS/README.md b/04_SPECS/README.md index 2ee687bf..923db93f 100644 --- a/04_SPECS/README.md +++ b/04_SPECS/README.md @@ -1,6 +1,6 @@ # RIINA™ Specifications (Track C) -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) This directory contains formal specifications for RIINA. diff --git a/04_SPECS/RIINA_PRIME_DIRECTIVE_GAP_CLOSURE.md b/04_SPECS/RIINA_PRIME_DIRECTIVE_GAP_CLOSURE.md index 1f4af313..f39e0f82 100644 --- a/04_SPECS/RIINA_PRIME_DIRECTIVE_GAP_CLOSURE.md +++ b/04_SPECS/RIINA_PRIME_DIRECTIVE_GAP_CLOSURE.md @@ -1,6 +1,6 @@ # RIINA PRIME DIRECTIVE GAP CLOSURE SPECIFICATION -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) ## Document Status: AUTHORITATIVE | Version 1.0.0 | 2026-01-22 diff --git a/04_SPECS/cross-cutting/README.md b/04_SPECS/cross-cutting/README.md index ba21b0a1..d1d6482b 100644 --- a/04_SPECS/cross-cutting/README.md +++ b/04_SPECS/cross-cutting/README.md @@ -1,6 +1,6 @@ # RIINA Cross-Cutting Specifications -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) This directory contains cross-cutting concerns that span multiple industries and domains. diff --git a/04_SPECS/industries/README.md b/04_SPECS/industries/README.md index b2a6a432..ee9be1f0 100644 --- a/04_SPECS/industries/README.md +++ b/04_SPECS/industries/README.md @@ -1,6 +1,6 @@ # RIINA Industry Specifications -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) This directory contains industry-specific security requirements and threat models for RIINA. diff --git a/04_SPECS/industries/REGULATORY_COMPLIANCE_MALAYSIA_SINGAPORE_2026.md b/04_SPECS/industries/REGULATORY_COMPLIANCE_MALAYSIA_SINGAPORE_2026.md index 8460b6a1..517b6815 100644 --- a/04_SPECS/industries/REGULATORY_COMPLIANCE_MALAYSIA_SINGAPORE_2026.md +++ b/04_SPECS/industries/REGULATORY_COMPLIANCE_MALAYSIA_SINGAPORE_2026.md @@ -1,6 +1,6 @@ # REGULATORY COMPLIANCE FRAMEWORKS: MALAYSIA & SINGAPORE (2026) -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) ## COMPREHENSIVE GUIDE FOR RIINA SECURITY-FOCUSED PROGRAMMING LANGUAGE diff --git a/04_SPECS/language/RIINA_MATERIALIZATION_PLAN_v1_0_0.md b/04_SPECS/language/RIINA_MATERIALIZATION_PLAN_v1_0_0.md index fff2abb7..8b55f2f7 100644 --- a/04_SPECS/language/RIINA_MATERIALIZATION_PLAN_v1_0_0.md +++ b/04_SPECS/language/RIINA_MATERIALIZATION_PLAN_v1_0_0.md @@ -1,6 +1,6 @@ # RIINA Materialization Plan v1.0.0 -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) **Document ID:** `RIINA_MATERIALIZATION_PLAN_v1_0_0` **Date:** 2026-01-30 diff --git a/04_SPECS/language/SYNTAX_IMPROVEMENT_SPEC_v2_0_0.md b/04_SPECS/language/SYNTAX_IMPROVEMENT_SPEC_v2_0_0.md index 5bfddecc..8cb02a8b 100644 --- a/04_SPECS/language/SYNTAX_IMPROVEMENT_SPEC_v2_0_0.md +++ b/04_SPECS/language/SYNTAX_IMPROVEMENT_SPEC_v2_0_0.md @@ -1,6 +1,6 @@ # RIINA Syntax Improvement Specification v2.0.0 -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) **Document ID:** `SYNTAX_IMPROVEMENT_SPEC_v2_0_0` **Date:** 2026-01-30 diff --git a/04_SPECS/scope/README.md b/04_SPECS/scope/README.md index 6e497ead..896ff08b 100644 --- a/04_SPECS/scope/README.md +++ b/04_SPECS/scope/README.md @@ -1,6 +1,6 @@ # RIINA Scope Specifications -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) This directory contains the definitive scope and architecture documents for the RIINA project. diff --git a/04_SPECS/scope/RIINA_ARCHITECTURE_CORRECTED.md b/04_SPECS/scope/RIINA_ARCHITECTURE_CORRECTED.md index 8cc4f4a6..a03841b2 100644 --- a/04_SPECS/scope/RIINA_ARCHITECTURE_CORRECTED.md +++ b/04_SPECS/scope/RIINA_ARCHITECTURE_CORRECTED.md @@ -1,6 +1,6 @@ # RIINA ARCHITECTURE CORRECTED -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) ## Version 1.0.0 — Proper Framing of Language vs Applications diff --git a/04_SPECS/scope/RIINA_DEFINITIVE_SCOPE.md b/04_SPECS/scope/RIINA_DEFINITIVE_SCOPE.md index 498cd17f..068e5842 100644 --- a/04_SPECS/scope/RIINA_DEFINITIVE_SCOPE.md +++ b/04_SPECS/scope/RIINA_DEFINITIVE_SCOPE.md @@ -1,6 +1,6 @@ # RIINA DEFINITIVE SCOPE DOCUMENT -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) ## Version 1.0.0 — The Single Source of Truth diff --git a/04_SPECS/scope/RIINA_RESEARCH_EXECUTION_MAP.md b/04_SPECS/scope/RIINA_RESEARCH_EXECUTION_MAP.md index a0e4cfd5..f1ca8623 100644 --- a/04_SPECS/scope/RIINA_RESEARCH_EXECUTION_MAP.md +++ b/04_SPECS/scope/RIINA_RESEARCH_EXECUTION_MAP.md @@ -1,6 +1,6 @@ # RIINA RESEARCH-EXECUTION MAP -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) ## Version 1.0.0 — Complete Mapping of 218 Research Tracks to Language Features diff --git a/06_COORDINATION/ATTACK_PROOF_MAP.md b/06_COORDINATION/ATTACK_PROOF_MAP.md index bdc186c8..cbe56d79 100644 --- a/06_COORDINATION/ATTACK_PROOF_MAP.md +++ b/06_COORDINATION/ATTACK_PROOF_MAP.md @@ -6,7 +6,7 @@ > Do not use it as the live execution source of truth. > Use `04_SPECS/execution/RIINA_A_TO_Z_EXECUTION_BOARD.md`, `PROOF_STATUS.md`, and `website/public/metrics.json`. -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) ``` Version: 1.0.0 diff --git a/06_COORDINATION/AXIOM_ELIMINATION_STRATEGY.md b/06_COORDINATION/AXIOM_ELIMINATION_STRATEGY.md index 7b96bcb0..5b7d17bb 100644 --- a/06_COORDINATION/AXIOM_ELIMINATION_STRATEGY.md +++ b/06_COORDINATION/AXIOM_ELIMINATION_STRATEGY.md @@ -5,7 +5,7 @@ > It is not the live execution tracker. > Use `04_SPECS/execution/RIINA_A_TO_Z_EXECUTION_BOARD.md`, `PROOF_STATUS.md`, and `website/public/metrics.json` for current state. -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) ## Comprehensive Analysis & Execution Plan diff --git a/06_COORDINATION/CLAUDE_AI_WEB_SUPPLEMENT.md b/06_COORDINATION/CLAUDE_AI_WEB_SUPPLEMENT.md index 4f8e08ec..ea995f70 100644 --- a/06_COORDINATION/CLAUDE_AI_WEB_SUPPLEMENT.md +++ b/06_COORDINATION/CLAUDE_AI_WEB_SUPPLEMENT.md @@ -1,6 +1,6 @@ # Claude AI Web Integration Supplement -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) ## Purpose This document provides all auxiliary definitions, lemma signatures, and helper functions needed to complete the remaining 18 admits in NonInterference_v2.v with 100% integration compatibility. diff --git a/06_COORDINATION/CLAUDE_WEB_DELEGATION_SESSION49.md b/06_COORDINATION/CLAUDE_WEB_DELEGATION_SESSION49.md index f0da58df..3d825bba 100644 --- a/06_COORDINATION/CLAUDE_WEB_DELEGATION_SESSION49.md +++ b/06_COORDINATION/CLAUDE_WEB_DELEGATION_SESSION49.md @@ -1,6 +1,6 @@ # Claude AI Web Delegation — Session 49 -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) ## Assessment & Limitations diff --git a/06_COORDINATION/COORDINATION_LOG.md b/06_COORDINATION/COORDINATION_LOG.md index c323808d..672fb8b2 100644 --- a/06_COORDINATION/COORDINATION_LOG.md +++ b/06_COORDINATION/COORDINATION_LOG.md @@ -1,6 +1,6 @@ # RIINA Coordination Log -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) ## Version: 3.20.0 ## Last Updated: 2026-02-05 (Session 73: Proof Depth Expansion) diff --git a/06_COORDINATION/DELEGATION_PROMPT_PHASE0.md b/06_COORDINATION/DELEGATION_PROMPT_PHASE0.md index f4bb6aa3..ab59d706 100644 --- a/06_COORDINATION/DELEGATION_PROMPT_PHASE0.md +++ b/06_COORDINATION/DELEGATION_PROMPT_PHASE0.md @@ -1,5 +1,5 @@ # RIINA AXIOM ELIMINATION - PHASE 0 DELEGATION PROMPT -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) ## For Claude AI Web Execution diff --git a/06_COORDINATION/DOMAIN_COVERAGE_MATRIX.md b/06_COORDINATION/DOMAIN_COVERAGE_MATRIX.md index 902d0c81..ee50e5ef 100644 --- a/06_COORDINATION/DOMAIN_COVERAGE_MATRIX.md +++ b/06_COORDINATION/DOMAIN_COVERAGE_MATRIX.md @@ -1,6 +1,6 @@ # Research Track → Coq Proof Coverage Matrix -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) > Auto-generated: 2026-02-02 > Method: `grep -c "^Qed\."` on each .v file; `find -name "*.md"` on each research dir diff --git a/06_COORDINATION/RESEARCH_INTEGRATION_AUDIT.md b/06_COORDINATION/RESEARCH_INTEGRATION_AUDIT.md index 1e038df8..d61f818e 100644 --- a/06_COORDINATION/RESEARCH_INTEGRATION_AUDIT.md +++ b/06_COORDINATION/RESEARCH_INTEGRATION_AUDIT.md @@ -1,6 +1,6 @@ # RESEARCH → CODEBASE INTEGRATION AUDIT -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) ## THE BRUTAL TRUTH diff --git a/06_COORDINATION/axiom_elimination/AXIOM_ELIMINATION_ASSESSMENT.md b/06_COORDINATION/axiom_elimination/AXIOM_ELIMINATION_ASSESSMENT.md index bc071309..767ab7b5 100644 --- a/06_COORDINATION/axiom_elimination/AXIOM_ELIMINATION_ASSESSMENT.md +++ b/06_COORDINATION/axiom_elimination/AXIOM_ELIMINATION_ASSESSMENT.md @@ -1,6 +1,6 @@ # RIINA AXIOM ELIMINATION - COMPREHENSIVE ASSESSMENT REPORT -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) **Generated:** 2026-01-25 **Mode:** ULTRA KIASU | ZERO TRUST | ZERO SHORTCUTS | INFINITE PATIENCE diff --git a/06_COORDINATION/axiom_elimination/EXECUTION_REPORT.md b/06_COORDINATION/axiom_elimination/EXECUTION_REPORT.md index 1ba9fa1c..7f241736 100644 --- a/06_COORDINATION/axiom_elimination/EXECUTION_REPORT.md +++ b/06_COORDINATION/axiom_elimination/EXECUTION_REPORT.md @@ -1,6 +1,6 @@ # RIINA AXIOM ELIMINATION - EXECUTION REPORT -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) **Date:** 2026-01-25 **Mode:** ULTRA KIASU | ZERO TRUST | ZERO SHORTCUTS diff --git a/06_COORDINATION/axiom_elimination/EXECUTION_REPORT_FINAL.md b/06_COORDINATION/axiom_elimination/EXECUTION_REPORT_FINAL.md index c492eedf..6e46832b 100644 --- a/06_COORDINATION/axiom_elimination/EXECUTION_REPORT_FINAL.md +++ b/06_COORDINATION/axiom_elimination/EXECUTION_REPORT_FINAL.md @@ -1,6 +1,6 @@ # RIINA AXIOM ELIMINATION - FINAL EXECUTION REPORT -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) **Date:** 2026-01-25 **Mode:** ULTRA KIASU | ZERO TRUST diff --git a/06_COORDINATION/axiom_elimination/EXECUTION_REPORT_v2.md b/06_COORDINATION/axiom_elimination/EXECUTION_REPORT_v2.md index 6553bae5..d1191eaf 100644 --- a/06_COORDINATION/axiom_elimination/EXECUTION_REPORT_v2.md +++ b/06_COORDINATION/axiom_elimination/EXECUTION_REPORT_v2.md @@ -5,7 +5,7 @@ > It includes stale "remaining admits" state and is not operational truth. > Use `04_SPECS/execution/RIINA_A_TO_Z_EXECUTION_BOARD.md` and `PROOF_STATUS.md` for live status. -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) **Date:** 2026-01-25 **Mode:** ULTRA KIASU | ZERO TRUST | ZERO SHORTCUTS diff --git a/06_COORDINATION/axiom_elimination/PHASE2_DEFINITIVE_SUMMARY.md b/06_COORDINATION/axiom_elimination/PHASE2_DEFINITIVE_SUMMARY.md index a9319134..78e42bee 100644 --- a/06_COORDINATION/axiom_elimination/PHASE2_DEFINITIVE_SUMMARY.md +++ b/06_COORDINATION/axiom_elimination/PHASE2_DEFINITIVE_SUMMARY.md @@ -1,6 +1,6 @@ # RIINA PHASE 2: CASCADE ADMITS - DEFINITIVE PATCH -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) **Date:** 2026-01-25 **Target:** NonInterference_v2.v - 3 admits → 0 diff --git a/06_COORDINATION/axiom_elimination/PHASE3_INFRASTRUCTURE_SUMMARY.md b/06_COORDINATION/axiom_elimination/PHASE3_INFRASTRUCTURE_SUMMARY.md index 5a16c505..165e9166 100644 --- a/06_COORDINATION/axiom_elimination/PHASE3_INFRASTRUCTURE_SUMMARY.md +++ b/06_COORDINATION/axiom_elimination/PHASE3_INFRASTRUCTURE_SUMMARY.md @@ -1,6 +1,6 @@ # RIINA PHASE 3: INFRASTRUCTURE HELPER LEMMAS -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) **Date:** 2026-01-25 **Target:** 6 helper lemmas from Phase 2 patch diff --git a/06_COORDINATION/axiom_elimination/PHASE_5_COMPLETE_PROMPT.md b/06_COORDINATION/axiom_elimination/PHASE_5_COMPLETE_PROMPT.md index aecefdf2..adbade0b 100644 --- a/06_COORDINATION/axiom_elimination/PHASE_5_COMPLETE_PROMPT.md +++ b/06_COORDINATION/axiom_elimination/PHASE_5_COMPLETE_PROMPT.md @@ -1,6 +1,6 @@ # PHASE 5: Store Semantics & Semantic Typing Axioms - COMPLETE PROMPT -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) **Mode:** ULTRA KIASU | ZERO TRUST | QED ETERNUM **Target:** 12 Admits across 5 files diff --git a/06_COORDINATION/axiom_elimination/PHASE_5_COMPLETION_REPORT.md b/06_COORDINATION/axiom_elimination/PHASE_5_COMPLETION_REPORT.md index bf6c9025..992553e9 100644 --- a/06_COORDINATION/axiom_elimination/PHASE_5_COMPLETION_REPORT.md +++ b/06_COORDINATION/axiom_elimination/PHASE_5_COMPLETION_REPORT.md @@ -1,6 +1,6 @@ # PHASE 5: Store Semantics & Semantic Typing Axioms - COMPLETION REPORT -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) **Mode:** ULTRA KIASU | ZERO TRUST | QED ETERNUM **Target:** 12 Admits across 5 files → 0 Admits diff --git a/06_COORDINATION/iris_migration_spec.md b/06_COORDINATION/iris_migration_spec.md index ea9194f5..1e134b8b 100644 --- a/06_COORDINATION/iris_migration_spec.md +++ b/06_COORDINATION/iris_migration_spec.md @@ -1,6 +1,6 @@ # RIINA Iris Migration Specification v1.0.0 -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) **Document ID:** `RIINA_IRIS_MIGRATION_SPEC_v1_0_0` diff --git a/06_COORDINATION/llm_proof_pipeline_design.md b/06_COORDINATION/llm_proof_pipeline_design.md index 7e392b4f..9f376ef2 100644 --- a/06_COORDINATION/llm_proof_pipeline_design.md +++ b/06_COORDINATION/llm_proof_pipeline_design.md @@ -1,6 +1,6 @@ # RIINA LLM-Assisted Proof Pipeline v1.0.0 -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) **Document ID:** RIINA_LLM_PROOF_PIPELINE_v1_0_0 **Version:** 1.0.0 diff --git a/07_EXAMPLES/06_ai_context/RIINA_FOR_AI.md b/07_EXAMPLES/06_ai_context/RIINA_FOR_AI.md index 1d3e18da..aae787b1 100644 --- a/07_EXAMPLES/06_ai_context/RIINA_FOR_AI.md +++ b/07_EXAMPLES/06_ai_context/RIINA_FOR_AI.md @@ -1,6 +1,6 @@ # RIINA for AI Assistants -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) ## What is RIINA? diff --git a/CHANGELOG.md b/CHANGELOG.md index be66a038..8c55d427 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,6 @@ # Changelog -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) All notable changes to RIINA™ will be documented in this file. diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 20e5803b..a532c38a 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,6 +1,6 @@ # Contributing to RIINA™ -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) Thank you for your interest in RIINA. This guide covers how to contribute effectively. @@ -22,7 +22,7 @@ bash 00_SETUP/scripts/verify_setup.sh # Build the compiler cd 03_PROTO && cargo build --release -p riinac && cd .. -# Run all tests (should show 3318 passing) +# Run all tests (should show 3322 passing) cd 03_PROTO && cargo test --all && cd .. # Try it out diff --git a/README.md b/README.md index 88183c96..139a844f 100644 --- a/README.md +++ b/README.md @@ -392,7 +392,7 @@ Every research track in `01_RESEARCH/` (55 domains, A through AJ, plus Greek let ## Current Status **Build:** Passing. -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) | Area | Status | |------|--------| diff --git a/docs/enterprise/CERTIFICATION.md b/docs/enterprise/CERTIFICATION.md index d7fb33dc..287fa06c 100644 --- a/docs/enterprise/CERTIFICATION.md +++ b/docs/enterprise/CERTIFICATION.md @@ -1,6 +1,6 @@ # RIINA Certification Output -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) ## What RIINA Certifies diff --git a/docs/enterprise/COMPLIANCE_GUIDE.md b/docs/enterprise/COMPLIANCE_GUIDE.md index f4ae1ec1..4c3f2c17 100644 --- a/docs/enterprise/COMPLIANCE_GUIDE.md +++ b/docs/enterprise/COMPLIANCE_GUIDE.md @@ -1,6 +1,6 @@ # RIINA Compliance System — User Guide -**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3318 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) +**Verification:** 12,678 Coq Qed (compiled, 0 Admitted, 0 active axioms) — Coq is the only mechanized lane | 3322 Rust tests | the other prover trees are machine-generated (claim-level tracked, not independent verification) ## Overview diff --git a/website/public/metrics.json b/website/public/metrics.json index 86d49dcf..729447be 100644 --- a/website/public/metrics.json +++ b/website/public/metrics.json @@ -1,11 +1,11 @@ { - "generated": "2026-08-24T01:49:04Z", - "generatedHuman": "August 24, 2026 at 01:49 UTC", + "generated": "2026-08-24T02:23:42Z", + "generatedHuman": "August 24, 2026 at 02:23 UTC", "version": "0.4.0", "session": 0, "git": { - "commit": "14c212d29", - "branch": "main" + "commit": "ec6036843", + "branch": "claude/riina-backmerge-11" }, "proofs": { "qedActive": 12678, @@ -195,8 +195,8 @@ "runtimeProofArchitecture": "generated" }, "rust": { - "tests": 3318, - "testsVerified": 3318, + "tests": 3322, + "testsVerified": 3322, "testsEstimated": 0, "testsSource": "full_cargo_test", "crates": 18 From 82b3772b8d695b44d3c2270e81f3bab69dc4161d Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 25 Aug 2026 03:42:17 +0000 Subject: [PATCH 4/4] [ALL] CHORE: full-mode verification manifest at the riina #11 back-merge riinac verify --full on the merged tree: 3322 Rust tests, 0 clippy warnings, 331 .vo compiled, 0 admits, 0 axioms. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Uu28z8CdRQ1SLzTv8yszth --- VERIFICATION_MANIFEST.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/VERIFICATION_MANIFEST.md b/VERIFICATION_MANIFEST.md index 70d6ee2a..2b33769d 100644 --- a/VERIFICATION_MANIFEST.md +++ b/VERIFICATION_MANIFEST.md @@ -1,6 +1,6 @@ # RIINA Verification Manifest -**Generated:** 2026-08-24T02:12:25Z -**Git SHA:** a30830e0c +**Generated:** 2026-08-24T03:45:04Z +**Git SHA:** b7aaaa97a **Mode:** full **Status:** PASS @@ -8,10 +8,10 @@ | Check | Status | Details | |-------|--------|---------| -| Rust Tests | PASS | 3318 tests | +| Rust Tests | PASS | 3322 tests | | Clippy | PASS | 0 warnings | | _CoqProject Completeness | PASS | all 331 .v files listed in _CoqProject | -| Coq Compilation | PASS | 331 .vo files compiled in 177s | +| Coq Compilation | PASS | 331 .vo files compiled in 182s | | Coq Kernel Assumptions | PASS | 5 capstones attested; axioms within reviewed whitelist (1 allowed: funext) | | Coq Admits | PASS | 0 (target: 1) | | Coq Axioms | PASS | 0 (informational; explicit assumptions tracked separately) |