FEAT-040 (v2.6): machine-readable analysis-gap report

artifacts/roadmap-3.0.yaml

@@ -127,7 +127,7 @@ artifacts:
   - id: FEAT-040
     type: feature
     title: "v2.6 — Machine-readable gap records + aggregated gap report"
-    status: proposed
+    status: accepted
     release: v2.6.0
     description: >
       Stop emitting top as silence. Emit a positive Gap{function, pc, op, kind,

crates/scry-analyze-core/src/lib.rs

@@ -372,6 +372,56 @@ pub struct AnalysisResult {
     /// the frozen v1 JSON contract), like [`AnalysisResult::function_meta`].
     /// Only non-⊤ facts are emitted (a ⊤ fact carries no information).
     pub bit_facts: Vec<BitFact>,
+    /// FEAT-040 (REQ-017): explicit, machine-readable records of the places the
+    /// interval/region interpreter was CONSERVATIVE — every site where it either
+    /// degraded a whole function to ⊤ (an unsupported op, a `br_table`, or a
+    /// non-i32-shaped memory address — the [`FuncCtx::scrub_to_top`] sites,
+    /// enforced complete by that method's signature) OR fell back to write-set
+    /// havoc of an unmodelled control-flow region (a typed `if` / non-empty
+    /// block-type — a partial give-up). Where the rest of the result emits ⊤ as
+    /// *silence* (an unanalyzed point produces no record), this enumerates the
+    /// "scry was conservative here" sites so an assessor (the qualification
+    /// scope/limitation statement) or an AI agent can see them directly. Sorted
+    /// by `(func_index, pc)`. Library-only, emitted regardless of
+    /// `emit_diagnostics`.
+    ///
+    /// SCOPE (honest bounds): this covers the interval/region INTERPRETER. It
+    /// does NOT enumerate (a) ordinary loop widening to ⊤ — that is normal sound
+    /// abstraction, not a give-up; (b) the separate `bit_facts` / taint passes'
+    /// own conservative stops; (c) imported functions (never analyzed). Those
+    /// are sound but out of this report's scope.
+    pub gaps: Vec<Gap>,
+}
+
+/// FEAT-040: one analysis-gap record — a site where scry was conservative.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct Gap {
+    /// Absolute function index where the gap occurred.
+    pub func_index: u32,
+    /// Operator index (pc) of the conservative site.
+    pub pc: u32,
+    /// The operator name that triggered the gap (e.g. `f64.add`, `select`).
+    pub op: String,
+    /// What kind of conservative step this is.
+    pub kind: GapKind,
+}
+
+/// FEAT-040: the category of an analysis [`Gap`].
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum GapKind {
+    /// An operator outside scry's modelled set: the function's abstract state
+    /// is scrubbed to ⊤ (sound, but no further facts are learned in it).
+    UnsupportedOp,
+    /// An unmodelled multi-target branch (`br_table`): control flow scrubbed.
+    UnmodeledBranch,
+    /// A memory access on a non-i32-shaped address operand: region state
+    /// scrubbed to ⊤ (the address could alias anywhere — sound fallback).
+    UnmodeledMemoryAddress,
+    /// An unmodelled control-flow region (a typed `if`, or a non-empty
+    /// block-type `block`) handled by write-set havoc: the locals the region
+    /// writes are widened to ⊤ (the rest stay precise — a PARTIAL give-up,
+    /// unlike the full-function scrubs above). FEAT-016 fallback.
+    UnmodeledControlFlow,
 }
 
 /// FEAT-037: a known-bits / congruence fact about one local at one program
@@ -755,6 +805,10 @@ struct FuncCtx {
     /// become uninformative (all-top) and further records would just
     /// be noise.
     degraded: bool,
+    /// FEAT-040: analysis-gap records collected during this function's walk
+    /// (every unsupported-op fallback), drained by the caller in phase 2.
+    /// Independent of `emit_diagnostics` so the gap report is always available.
+    gaps: Vec<Gap>,
 }
 
 impl FuncCtx {
@@ -765,14 +819,23 @@ impl FuncCtx {
             operand_stack: Vec::new(),
             octagon,
             degraded: false,
+            gaps: Vec::new(),
         }
     }
 
     /// Drop the operand stack and widen every local to top. Used when
     /// we hit any operator outside the v0.2 AC#1 supported set —
     /// soundness over precision (REQ-001 / DD-005). The octagon is reset to
     /// `top` too (all relations forgotten — sound).
-    fn scrub_to_top(&mut self) {
+    ///
+    /// FEAT-040: every degradation MUST record a [`Gap`] (passed in), so no
+    /// function can silently degrade to ⊤ — the gap report is complete. The
+    /// `degraded` early-return elsewhere means only the FIRST scrub records a
+    /// gap (subsequent ops are skipped), which is the give-up point we want.
+    fn scrub_to_top(&mut self, gap: Gap) {
+        if !self.degraded {
+            self.gaps.push(gap);
+        }
         for slot in self.locals.iter_mut() {
             *slot = AbstractValue::I32Interval(domain::top());
         }
@@ -1538,6 +1601,7 @@ pub fn analyze(
                 &mut sink_edges,
                 /*emit_diagnostics=*/ false,
                 /*depth=*/ 0,
+                /*emit_gaps=*/ None,
             )?;
             extract_results(&defined_funcs[defined].results, &result_state)
         };
@@ -1577,6 +1641,7 @@ pub fn analyze(
 
     let mut points: Vec<ProgramPoint> = Vec::new();
     let mut call_graph: Vec<CallEdge> = Vec::new();
+    let mut gaps: Vec<Gap> = Vec::new();
     for func in &defined_funcs {
         let init_locals = top_input_locals(func);
         run_function_body(
@@ -1588,8 +1653,10 @@ pub fn analyze(
             &mut call_graph,
             config.emit_diagnostics,
             /*depth=*/ 0,
+            /*emit_gaps=*/ Some(&mut gaps),
         )?;
     }
+    gaps.sort_by_key(|g| (g.func_index, g.pc));
 
     // ───────────────────────────────────────────────────────────
     // Assemble the per-function-summary output records (FEAT-007).
@@ -1880,6 +1947,7 @@ pub fn analyze(
         function_meta,
         verified_premises,
         bit_facts,
+        gaps,
     })
 }
 
@@ -2713,7 +2781,12 @@ impl Interp<'_, '_> {
                 }
                 Operator::BrTable { .. } => {
                     // Unmodelled multi-target branch: sound fallback.
-                    ctx.scrub_to_top();
+                    ctx.scrub_to_top(Gap {
+                        func_index: self.func_index,
+                        pc: pc as u32,
+                        op: "br_table".to_string(),
+                        kind: GapKind::UnmodeledBranch,
+                    });
                     return Ok(Flow::Diverged);
                 }
                 _ => {}
@@ -3087,6 +3160,17 @@ impl Interp<'_, '_> {
             let _ = ctx.operand_stack.pop();
         }
         let written = region_write_set(self.ops, opener + 1, end);
+        // FEAT-040: an unmodelled control-flow region that actually widens a
+        // local to ⊤ is a (partial) give-up — record it so the gap report
+        // reflects write-set havoc, not only the full-function scrubs.
+        if !written.is_empty() {
+            ctx.gaps.push(Gap {
+                func_index: self.func_index,
+                pc: opener as u32,
+                op: op_report_name(&self.ops[opener]),
+                kind: GapKind::UnmodeledControlFlow,
+            });
+        }
         for idx in &written {
             if let Some(slot) = ctx.locals.get_mut(*idx as usize) {
                 *slot = AbstractValue::I32Interval(domain::top());
@@ -3138,6 +3222,7 @@ fn run_function_body(
     call_graph: &mut Vec<CallEdge>,
     emit_diagnostics: bool,
     depth: u32,
+    emit_gaps: Option<&mut Vec<Gap>>,
 ) -> Result<Vec<AbstractValue>, AnalyzeError> {
     let mut ctx = FuncCtx::new(init_locals);
     let ops = &func.ops;
@@ -3159,6 +3244,9 @@ fn run_function_body(
     if let Some(out) = emit_points {
         out.extend(interp.points);
     }
+    if let Some(g) = emit_gaps {
+        g.append(&mut ctx.gaps);
+    }
     Ok(ctx.operand_stack)
 }
 
@@ -3899,7 +3987,15 @@ fn interpret_op(
                     ),
                 });
             }
-            ctx.scrub_to_top();
+            // FEAT-040: scrub_to_top records the gap (the function degrades to
+            // ⊤ here). The `degraded` early-return means this fires once per
+            // function — at the first unsupported op, the give-up point.
+            ctx.scrub_to_top(Gap {
+                func_index,
+                pc,
+                op: op_report_name(other),
+                kind: GapKind::UnsupportedOp,
+            });
         }
     }
     Ok(StepOutcome::Continue)
@@ -4036,7 +4132,12 @@ fn handle_memory_load(
                 ),
             });
         }
-        ctx.scrub_to_top();
+        ctx.scrub_to_top(Gap {
+            func_index,
+            pc,
+            op: op_label.to_string(),
+            kind: GapKind::UnmodeledMemoryAddress,
+        });
         return Ok(());
     };
 
@@ -4137,7 +4238,12 @@ fn handle_memory_store(
                 ),
             });
         }
-        ctx.scrub_to_top();
+        ctx.scrub_to_top(Gap {
+            func_index,
+            pc,
+            op: op_label.to_string(),
+            kind: GapKind::UnmodeledMemoryAddress,
+        });
         return Ok(());
     };
 
@@ -4382,6 +4488,7 @@ fn handle_call(
             &mut sink_edges,
             /*emit_diagnostics=*/ false,
             depth.saturating_add(1),
+            /*emit_gaps=*/ None,
         )?;
         (
             extract_results(&callee.results, &final_stack),
@@ -5102,6 +5209,22 @@ fn run_taint_analysis(
 /// (full payloads) and tends to balloon diagnostic strings. The set
 /// below is the one we expect to see most often via the fallback
 /// path; anything else falls through to a debug-ish label.
+/// FEAT-040: a human-readable name for ANY operator, for gap records. Uses the
+/// curated [`op_name`] when known, else falls back to the operator's Debug
+/// variant name (e.g. `F64Add`, `V128Const`) so an unsupported op is still
+/// identified in the gap report rather than shown as a generic placeholder.
+fn op_report_name(op: &Operator<'_>) -> String {
+    let n = op_name(op);
+    if n != "<unsupported>" {
+        return n.to_string();
+    }
+    let dbg = alloc::format!("{op:?}");
+    dbg.split([' ', '(', '{'])
+        .next()
+        .unwrap_or("<op>")
+        .to_string()
+}
+
 fn op_name(op: &Operator<'_>) -> &'static str {
     match op {
         Operator::Unreachable => "unreachable",
@@ -5188,6 +5311,7 @@ mod tests {
             function_meta: alloc::vec![],
             verified_premises: FusionPremises::default(),
             bit_facts: alloc::vec![],
+            gaps: alloc::vec![],
         };
         assert_eq!(res.invariants.points.len(), 1);
         assert!(matches!(rp, AbstractValue::RegionPointer(_)));
@@ -5985,6 +6109,103 @@ mod tests {
         );
     }
 
+    /// FEAT-040: an unsupported operator that degrades the function to ⊤ is
+    /// recorded as an explicit Gap — not emitted as silence — so an assessor /
+    /// AI agent can enumerate where scry gave up.
+    #[test]
+    fn feat040_unsupported_op_recorded_as_gap() {
+        // f64.add is outside scry's modelled set ⇒ the function degrades to ⊤.
+        let r = analyze_default(
+            "(module (func (param f64 f64) (result f64) \
+               local.get 0 local.get 1 f64.add))",
+        );
+        let g = r
+            .gaps
+            .iter()
+            .find(|g| g.func_index == 0)
+            .expect("a gap for the unsupported f64.add");
+        assert_eq!(g.kind, GapKind::UnsupportedOp);
+        assert!(
+            g.op != "<unsupported>" && g.op.to_lowercase().contains("f64"),
+            "gap should name the unsupported op (f64.*), got {:?}",
+            g.op
+        );
+    }
+
+    /// FEAT-040 completeness: a non-unsupported-op degradation (an unmodelled
+    /// `br_table`) is ALSO recorded — degradation can't be silent (scrub_to_top
+    /// requires a Gap by signature).
+    #[test]
+    fn feat040_br_table_recorded_as_gap() {
+        let r = analyze_default(
+            "(module (func (param i32) (block (block \
+               local.get 0 br_table 0 1 0))))",
+        );
+        let g = r.gaps.iter().find(|g| g.func_index == 0);
+        if let Some(g) = g {
+            assert_eq!(
+                g.kind,
+                GapKind::UnmodeledBranch,
+                "br_table ⇒ UnmodeledBranch gap, got {g:?}"
+            );
+        } else {
+            panic!("br_table must record a gap; gaps={:?}", r.gaps);
+        }
+    }
+
+    /// FEAT-040 completeness (clean-room finding): write-set havoc of an
+    /// unmodelled control-flow region (a typed `if`) is now recorded — it is a
+    /// partial give-up that previously left no gap.
+    #[test]
+    fn feat040_control_flow_havoc_recorded_as_gap() {
+        let r = analyze_default(
+            "(module (func (param i32) (local i32) \
+               i32.const 5 local.set 1 \
+               local.get 0 (if (then i32.const 9 local.set 1))))",
+        );
+        assert!(
+            r.gaps
+                .iter()
+                .any(|g| g.kind == GapKind::UnmodeledControlFlow),
+            "write-set havoc of the if-region must record an UnmodeledControlFlow gap; got {:?}",
+            r.gaps
+        );
+    }
+
+    /// FEAT-040: a fully-modelled function produces NO gaps (no false "gave up").
+    #[test]
+    fn feat040_modelled_function_has_no_gaps() {
+        let r = analyze_default(
+            "(module (func (param i32) (result i32) local.get 0 i32.const 1 i32.add))",
+        );
+        assert!(
+            r.gaps.is_empty(),
+            "a fully-modelled i32 function must report no gaps, got {:?}",
+            r.gaps
+        );
+    }
+
+    /// FEAT-040: gaps are emitted even with the default config
+    /// (emit_diagnostics = false) — the gap report is independent of verbose
+    /// diagnostics.
+    #[test]
+    fn feat040_gaps_independent_of_emit_diagnostics() {
+        let r = analyze(
+            wat::parse_str("(module (func (result f64) f64.const 1 f64.const 2 f64.add))")
+                .expect("assemble"),
+            AnalysisConfig::default(), // emit_diagnostics = false
+        )
+        .expect("analyze");
+        assert!(
+            !r.gaps.is_empty(),
+            "gaps must populate even with default (no-diagnostics) config"
+        );
+        assert!(
+            r.diagnostics.is_empty(),
+            "default config emits no diagnostics"
+        );
+    }
+
     /// FEAT-034: scry determines its OWN fusion premises (verify-not-trust):
     /// bounded_memory = no `memory.grow`; closed_world = no functional imports.
     #[test]