diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index fdd140e..2c6244c 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -138,8 +138,10 @@ jobs: with: # v0.3.0 was too old to parse scry's research-ext schema — # the action's internal `rivet validate` failed on v0.2.0 - # (see issue #10). v0.13.1 matches the rivet release line. - rivet-version: v0.13.1 + # (see issue #10). Bumped to v0.22.0 so the compliance action's + # internal `rivet validate` understands the top-level `release:` + # field (rivet >= 0.21) the roadmap now uses for release planning. + rivet-version: v0.22.0 theme: dark archive: 'true' archive-name: scry-${{ env.BARE_VERSION }}-compliance-evidence diff --git a/artifacts/research-2.yaml b/artifacts/research-2.yaml new file mode 100644 index 0000000..f969fd4 --- /dev/null +++ b/artifacts/research-2.yaml @@ -0,0 +1,671 @@ +artifacts: + + # ══════════════════════════════════════════════════════════════════════ + # Research sweep (v2.5 → v3.0 planning). Captures the gap-driven survey: + # academic literature (classic + 2020-2026 frontier) scry could adopt, + # commercial / notable analyzers we measure against, and the market + # findings that frame the next release. Companion to artifacts/research.yaml + # (AC-001..011, TE-001..010, MF-001..005). Drives roadmap-3.0.yaml. + # ══════════════════════════════════════════════════════════════════════ + + # ── Academic references — numeric domains scry lacks ────────────────── + + - id: AC-012 + type: academic-reference + title: "Automatic Discovery of Linear Restraints Among Variables of a Program (Cousot & Halbwachs, POPL 1978)" + status: draft + tags: [abstract-interpretation, numerical-domain, relational, seminal] + fields: + authors: "Patrick Cousot, Nicolas Halbwachs" + year: 1978 + venue: "POPL 1978" + url: "https://doi.org/10.1145/512760.512770" + key-finding: > + The convex-polyhedra domain: infers arbitrary linear inequalities + sum(a_i x_i) <= c. The most expressive classical linear relational + domain (exponential cost), the precision ceiling above the octagon. + relevance: > + The natural precision step above scry's shipped octagon (limited to + +/-x_i +/-x_j <= c). Would surface true linear memory-index relations + for bounds/trap reasoning. Adopt via ELINA decomposition (TE-012) to + keep it tractable. Backlog domain bet. + links: + - type: traces-to + target: REQ-016 + + - id: AC-013 + type: academic-reference + title: "Affine Relationships Among Variables of a Program (Karr, Acta Informatica 1976)" + status: draft + tags: [abstract-interpretation, numerical-domain, relational, seminal] + fields: + authors: "Michael Karr (+ Müller-Olm & Seidl, ICALP 2004 for complete transfers)" + year: 1976 + venue: "Acta Informatica 6:133-151" + url: "https://doi.org/10.1007/BF00268497" + key-finding: > + Linear-algebra domain computing EXACT affine equalities sum(a_i x_i)=c; + cheaper than polyhedra, fixpoint-complete for affine programs. + relevance: > + A low-cost relational EQUALITY domain to complement the octagon with a + small, mechanizable transfer set — attractive for admit-free Rocq. The + cheapest first step toward surfaced relational invariants (REQ-016). + links: + - type: traces-to + target: REQ-016 + + - id: AC-014 + type: academic-reference + title: "Pentagons: a weakly relational domain for efficient validation of array accesses (Logozzo & Fähndrich, SAC 2008 / SCP 2010)" + status: draft + tags: [abstract-interpretation, numerical-domain, bounds, traps, high-value] + fields: + authors: "Francesco Logozzo, Manuel Fähndrich" + year: 2010 + venue: "SAC 2008; Science of Computer Programming 75(9)" + url: "https://doi.org/10.1016/j.scico.2009.04.004" + key-finding: > + Cheap domain capturing x in [a,b] AND x < y — more precise than + intervals, far cheaper than octagon; built for bytecode/IL + array-bounds validation. + relevance: > + Near-perfect fit for Wasm linear-memory OOB/trap detection: the "x < y" + facts are exactly what prove addr < mem_size. Best effort-to-payoff + ratio of the surveyed domains; the enabler for OOB trap diagnostics. + links: + - type: traces-to + target: REQ-014 + + - id: AC-015 + type: academic-reference + title: "A Parametric Segmentation Functor for Automatic and Scalable Array Content Analysis (Cousot, Cousot & Logozzo, POPL 2011)" + status: draft + tags: [abstract-interpretation, memory, array, seminal] + fields: + authors: "Patrick Cousot, Radhia Cousot, Francesco Logozzo" + year: 2011 + venue: "POPL 2011, pp. 105-118" + url: "https://doi.org/10.1145/1926385.1926399" + key-finding: > + A parametric functor that segments arrays/memory into symbolic + intervals and lifts any element domain over them. + relevance: > + Would give scry's flat linear-memory region CONTENT sensitivity + (per-segment values, not one havoc'd blob) — a new analysis dimension + beyond the current region domain. Backlog memory bet. + links: + - type: traces-to + target: REQ-001 + + - id: AC-016 + type: academic-reference + title: "The Gauge Domain: Scalable Analysis of Linear Inequality Invariants (Venet, CAV 2012)" + status: draft + tags: [abstract-interpretation, numerical-domain, scalability] + fields: + authors: "Arnaud J. Venet" + year: 2012 + venue: "CAV 2012, LNCS 7358" + url: "https://doi.org/10.1007/978-3-642-31424-7_15" + key-finding: > + Expresses each variable as linear relations to in-scope loop counters; + O(kn) operations; scaled to 144 KLOC avionics code. + relevance: > + Scalable linear-inequality invariants tied to loop counters — relational + precision without polyhedra blowup; serves both the scaling (REQ-007) + and relational-surfacing (REQ-016) gaps. + links: + - type: traces-to + target: REQ-016 + + # ── Academic references — precision, termination, methodology ───────── + + - id: AC-017 + type: academic-reference + title: "Trace Partitioning in Abstract-Interpretation-Based Static Analyzers (Mauborgne & Rival, ESOP 2005 / TOPLAS 2007)" + status: draft + tags: [abstract-interpretation, precision, disjunctive, seminal] + fields: + authors: "Laurent Mauborgne, Xavier Rival" + year: 2005 + venue: "ESOP 2005 (LNCS 3444); TOPLAS 29(5) 2007" + url: "https://www.di.ens.fr/~mauborgn/publi/esop05.html" + key-finding: > + Abstract over a PARTITION of traces (by branch history, loop iteration, + call context) rather than the merged state — recovers disjunctive + precision soundly. The canonical path-sensitivity technique (reused by + DeepPoly). + relevance: > + Lets scry avoid joining incompatible branches at merge points — the + standard precision booster, applicable to the loop/guard machinery. + links: + - type: traces-to + target: REQ-001 + + - id: AC-018 + type: academic-reference + title: "The Abstract Domain of Segmented Ranking Functions / FuncTion (Urban, SAS 2013)" + status: draft + tags: [abstract-interpretation, termination, ranking-function, high-value] + fields: + authors: "Caterina Urban (+ Urban & Miné)" + year: 2013 + venue: "SAS 2013, LNCS 7935" + url: "https://caterinaurban.github.io/project/function/" + key-finding: > + A parametric domain synthesizing piecewise ranking functions and sound + sufficient preconditions for termination. + relevance: > + Directly addresses scry's loop-bound/termination gap. A sound ranking + function is what would turn the WCSU stack bound's "Unbounded" (every + recursive SCC) into an actual bound, and extend it to loop-iteration / + fuel bounds (DD-016 slice-3 future). + links: + - type: traces-to + target: DD-016 + + - id: AC-019 + type: academic-reference + title: "SPEED: Precise and Efficient Static Estimation of Program Computational Complexity (Gulwani, Mehra & Chilimbi, POPL 2009)" + status: draft + tags: [abstract-interpretation, cost-analysis, bounds] + fields: + authors: "Sumit Gulwani, Krishna K. Mehra, Trishul Chilimbi" + year: 2009 + venue: "POPL 2009" + url: "https://doi.org/10.1145/1480881.1480898" + key-finding: > + Computes symbolic worst-case iteration/resource bounds via counter + instrumentation plus invariant generation. + relevance: > + Turns scry's reachability/call-graph machinery into a resource/cost + bound estimator — concrete loop-bound numbers and a Wasm fuel/gas bound + (metered Wasm), the analogue of aiT WCET (CA-002). + links: + - type: traces-to + target: DD-016 + + - id: AC-020 + type: academic-reference + title: "A Formally-Verified C Static Analyzer / Verasco (Jourdan, Laporte, Blazy, Leroy, Pichardie, POPL 2015)" + status: draft + tags: [abstract-interpretation, mechanized-soundness, methodology, high-value] + fields: + authors: "Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie" + year: 2015 + venue: "POPL 2015, pp. 247-259" + url: "https://compcert.org/verasco/" + key-finding: > + An abstract interpreter for most of C, machine-checked sound in Coq, + with a modular reduced-product of relational + non-relational domains, + integrated with CompCert so guarantees carry to compiled code. + relevance: > + THE methodological precedent for scry's admit-free Rocq program and for + the reduced-product domain-combinator interface scry needs as its domain + count grows. De-risks REQ-002 (mechanized soundness vs the semantics). + links: + - type: traces-to + target: REQ-002 + + - id: AC-021 + type: academic-reference + title: "Demanded / Interactive Abstract Interpretation with Demanded Summarization (Stein et al., PLDI 2021 / TOPLAS 2024)" + status: draft + tags: [abstract-interpretation, incremental, compositional, scalability, recent] + fields: + authors: "Benno Stein, Bor-Yuh Evan Chang, Manu Sridharan, et al." + year: 2024 + venue: "PLDI 2021; TOPLAS 46(1) 2024" + url: "https://plv.colorado.edu/bec/papers/demanded-summarization-toplas24.pdf" + key-finding: > + First incremental + demand-driven + compositional AI for arbitrary + domains with from-scratch-consistency guarantees; reuses results across + edits and produces composable procedure summaries. + relevance: > + Upgrades scry's function summaries into reusable, edit-incremental + summaries — the scaling story for CI / the dashboard / large fused + modules (REQ-007). + links: + - type: traces-to + target: REQ-007 + + # ── Academic references — floats + recent frontier ──────────────────── + + - id: AC-022 + type: academic-reference + title: "Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors (Miné, ESOP 2004)" + status: draft + tags: [abstract-interpretation, floating-point, relational, high-value] + fields: + authors: "Antoine Miné (+ Chen, Miné, Cousot, APLAS 2008 for FP polyhedra)" + year: 2004 + venue: "ESOP 2004, LNCS 2986" + url: "https://arxiv.org/pdf/cs/0703077" + key-finding: > + Adapts the octagon (later polyhedra) to IEEE-754 by abstracting to + reals-with-rounding-error nondeterminism, then over-approximating + soundly — the first relational floating-point domains. + relevance: > + THE reference for closing scry's IEEE-754 float gap soundly, and it + REUSES scry's already-shipped octagon DBM machinery — the float + capability with the least new machinery (REQ-015). + links: + - type: traces-to + target: REQ-015 + + - id: AC-023 + type: academic-reference + title: "An Abstract Domain for Certifying Neural Networks / DeepPoly (Singh, Gehr, Püschel, Vechev, POPL 2019)" + status: draft + tags: [abstract-interpretation, floating-point, precision, recent] + fields: + authors: "Gagandeep Singh, Timon Gehr, Markus Püschel, Martin Vechev" + year: 2019 + venue: "PACMPL 3(POPL), Art. 41 (ERAN)" + url: "https://ggndpsngh.github.io/files/DeepPoly.pdf" + key-finding: > + A custom polyhedra-lite domain (per-neuron linear upper/lower bounds + + interval concretization) for NN robustness, combined with trace + partitioning for refinement. + relevance: > + A worked example of designing a bespoke, cheap, sound relational domain + with a precise float/affine transformer — informs both the float (REQ-015) + and precision (REQ-001) directions. Also the cross-link to AI-robustness + verification scry's stack could later serve. + links: + - type: traces-to + target: REQ-015 + + - id: AC-024 + type: academic-reference + title: "Hybrid Call Graph Analysis for WebAssembly: AI + Environment Specification (Paccamiccio, Raimondi, Loreti, 2025)" + status: draft + tags: [webassembly, call-graph, component-model, recent] + fields: + authors: "Mattia Paccamiccio, Franco Raimondi, Michele Loreti" + year: 2025 + venue: "2025 preprint (SSRN); follow-on to AC-008" + url: "https://papers.ssrn.com/sol3/papers.cfm?abstract_id=5110464" + key-finding: > + Sound Wasm call-graph construction via abstract interpretation PLUS a + specification mechanism for external/host (import) behavior. + relevance: > + Extends scry's value-domain call graph (FEAT-006) to model host imports + / the Component-Model boundary soundly — the env-specification idea is + what handle/host-call modelling (REQ-003) needs. NOTE: confirm + published-vs-preprint status before promoting past draft. + links: + - type: traces-to + target: REQ-003 + + # ══════════════════════════════════════════════════════════════════════ + # Competitive analysis — the sound-analyzer bar (G-005) + Wasm peers. + # IDs use the prefix CA-. + # ══════════════════════════════════════════════════════════════════════ + + - id: CA-001 + type: competitive-analysis + title: "AbsInt Astrée — sound abstract interpreter (the bar)" + status: draft + tags: [competitor, sound, runtime-error, qualification] + description: > + Deepens TE-001. The reference sound analyzer G-005 targets. + fields: + tool-name: "Astrée" + tool-url: "https://www.absint.com/astree/" + vendor: "AbsInt GmbH" + tool-status: commercial + approach: > + Sound AI for C/C++. Proves ABSENCE of: division by zero, out-of-bounds + indexing, null/uninit/dangling deref, integer AND IEEE-754 overflow, + data races, Spectre, dead code, non-terminating loops. Domains: intervals, + relational octagons (incl. float), congruences, filter domains, trace + partitioning. Ships DO-178C/DO-330, ISO 26262, IEC 61508, EN 50128 QSKs. + limitations: > + C/C++ source only (no Wasm); proprietary; soundness is argued + qualified, + NOT machine-checked against a formal language semantics. + differentiation: > + This is the bar. scry's wedge = mechanized Rocq soundness vs the OFFICIAL + Wasm semantics, which Astrée lacks. BORROW: runtime-error-classes-as- + diagnostics (G1/REQ-014), float octagon (REQ-015), trace partitioning, + and the QSK packaging template for the qualification dossier. + + - id: CA-002 + type: competitive-analysis + title: "AbsInt aiT (WCET) + StackAnalyzer (stack bound)" + status: draft + tags: [competitor, sound, resource-bound] + description: > + Sound binary-level resource-bound analyzers; the comparison point for + scry's worst-case shadow-stack bound. + fields: + tool-name: "aiT / StackAnalyzer" + tool-url: "https://www.absint.com/stackanalyzer/" + vendor: "AbsInt GmbH" + tool-status: commercial + approach: > + Sound AI on binaries. StackAnalyzer proves absence of stack overflow + (worst-case stack usage for all inputs); aiT computes safe WCET upper + bounds via cache/pipeline modelling. Both qualifiable. + limitations: > + Per-target microarchitecture models; proprietary; no Wasm; the bounds + are not mechanized. + differentiation: > + Directly comparable to scry's FEAT-021 WCSU bound — and scry's is + MECHANIZED (StackBound.v) + self-checked via a live kill-criterion, so + scry partly already wins. BORROW: aiT's WCET angle as a future Wasm + fuel/instruction-bound (more tractable than native WCET — no cache), + pairing with termination/ranking functions (AC-018/AC-019). + + - id: CA-003 + type: competitive-analysis + title: "MathWorks Polyspace Code Prover (sound) vs Bug Finder (heuristic)" + status: draft + tags: [competitor, sound, runtime-error, ux] + description: > + The other major commercial sound prover; notable for its per-operation + verdict UX. + fields: + tool-name: "Polyspace Code Prover" + tool-url: "https://www.mathworks.com/products/polyspace-code-prover.html" + vendor: "MathWorks" + tool-status: commercial + approach: > + Code Prover = sound AI proving absence of overflow, div-by-zero, OOB, + and other RTEs over all paths; color-codes EVERY operation + green(proven-safe)/red(unsafe)/orange(unproven). Bug Finder = fast + heuristic, 350+ defect types. Certification via IEC/DO qualification kits. + limitations: > + C/C++/Ada; proprietary; MATLAB ecosystem; orange-noise is the classic + complaint. + differentiation: > + The green/orange/red per-operation verdict is the UX model for scry's + library-only output gap (REQ-016/IDE surface). scry is squarely a "Code + Prover", not a "Bug Finder". + + - id: CA-004 + type: competitive-analysis + title: "Frama-C / Eva — open-source sound abstract interpreter" + status: draft + tags: [competitor, sound, open-source, architecture] + description: > + The closest architectural peer; proof that open-source sound AI reaches + DO-178 / Common Criteria EAL6-7. + fields: + tool-name: "Frama-C / Eva (EVA)" + tool-url: "https://frama-c.com/fc-plugins/eva.html" + vendor: "CEA List" + tool-status: active + approach: > + Sound AI plug-in for C. Proves absence of UB: invalid access, uninit + reads, integer overflow; IEEE-754 float intervals; interval+congruence + integer domain; pluggable communicating domains (gauges, Apron = + octagons/polyhedra). Used for DO-178, IEC 60880, Common Criteria EAL6-7. + limitations: > + C only; LGPL core but qualification is consulting-driven; precision needs + domain tuning. + differentiation: > + Architectural template for scry: its pluggable COMMUNICATING-domain design + is exactly how scry should let interval/octagon/region/bits/taint exchange + info and SURFACE relational invariants (REQ-016) — Eva surfaces them, scry + computes-but-discards. Proof that open-source sound AI can be certified. + + - id: CA-005 + type: competitive-analysis + title: "TrustInSoft Analyzer — commercialized Frama-C lineage" + status: draft + tags: [competitor, sound, qualification] + fields: + tool-name: "TrustInSoft Analyzer" + tool-url: "https://www.trust-in-soft.com/" + vendor: "TrustInSoft" + tool-status: commercial + approach: > + Sound AI (Frama-C lineage). Sound UB detection: buffer overflow, OOB, + null deref, use-after-free, div-by-zero, uninit reads, signed overflow. + C/C++; claims Rust support. ISO 26262 TCL3 qualification. + limitations: > + Proprietary; C/C++ focus; Rust/Wasm not first-class. + differentiation: > + Demonstrates the commercial packaging of sound AI (the business scry's + thesis implies). BORROW: their crisp marketing taxonomy of UB classes + proven absent — the messaging scry needs for its trap/RTE story (REQ-014). + + - id: CA-006 + type: competitive-analysis + title: "VeriWasm — sound SFI/sandbox verifier for compiled Wasm" + status: draft + tags: [competitor, sound, webassembly, closest-peer] + description: > + The closest "sound + Wasm" peer — orthogonal scope, instructive CVE miss. + fields: + tool-name: "VeriWasm" + tool-url: "https://github.com/PLSysSec/veriwasm" + vendor: "UC San Diego (PLSysSec)" + tool-status: maintained + approach: > + Sound static verifier of NATIVE-compiled Wasm (x86-64 from Lucet/ + Wasmtime): proves memory accesses stay in-sandbox, control-flow targets + valid, stack usage bounded — i.e. SFI holds. No false positives by design. + limitations: > + Verifies the compiled output's sandboxing, NOT source-level RTE absence; + missed CVE-2021-32629 (signedness mis-modelling in the spec) — a + cautionary soundness-via-wrong-spec tale; research-grade. + differentiation: > + Orthogonal (SFI of the backend vs AI of the module). scry wins on + domains/RTE reasoning AND mechanized-against-official-semantics — + VeriWasm's CVE miss is the concrete argument FOR scry's WasmCert grounding + (REQ-002). BORROW: control-flow-target-validity + stack-bound verdicts. + + - id: CA-007 + type: competitive-analysis + title: "Wasmati — code-property-graph vulnerability scanner for Wasm" + status: draft + tags: [competitor, heuristic, webassembly, query] + fields: + tool-name: "Wasmati" + tool-url: "https://github.com/wasmati/wasmati" + vendor: "Univ. Lisbon" + tool-status: maintained + approach: > + Builds a Code Property Graph (AST+CFG+PDG) for Wasm; 4 query languages; + ~10 vuln queries (buffer overflow, format string). Scales to large real + binaries. Heuristic pattern-matching, unsound. + limitations: > + Unsound (false neg/pos); detects, does not prove. + differentiation: > + BORROW the CPG + queryable-graph idea. A SOUND CPG — a graph annotated + with scry's proven invariants, queryable — would be genuinely novel + (Wasmati UX + scry soundness). Ties to a query-language surface for + AnalysisResult (agent/REQ-017 + IDE). + + - id: CA-008 + type: competitive-analysis + title: "Wasm symbolic execution (SeeWasm, WASP, Manticore-wasm, WANA)" + status: draft + tags: [competitor, symbolic-execution, webassembly, complementary] + fields: + tool-name: "SeeWasm / WASP / Manticore-wasm / WANA" + tool-url: "https://arxiv.org/abs/2408.08537" + vendor: "various (academic)" + tool-status: research + approach: > + Symbolic / concolic execution of Wasm binaries; find concrete + bug-triggering inputs; path-explosion-bounded (not whole-program sound). + limitations: > + Opposite trade-off to scry: find-a-witness vs prove-absence; bounded + coverage. + differentiation: > + Complementary. BORROW: symbolic execution to generate COUNTEREXAMPLES for + scry's unproven/orange operations — turning "cannot prove safe" into + "input X may trap" (a strong UX pairing for REQ-014). scry wins on + completeness/soundness over all paths. + + - id: CA-009 + type: competitive-analysis + title: "Wasm Component Model verification — uncontested green field" + status: draft + tags: [webassembly, component-model, green-field, moat] + description: > + No sound analyzer occupies handle-state / linear-resource analysis for the + Component Model — scry's biggest novelty opportunity. + fields: + tool-name: "(none — open green field)" + tool-url: "https://component-model.bytecodealliance.org/" + vendor: "Bytecode Alliance (spec)" + tool-status: active + approach: > + The Component Model defines resource handles (own/borrow) with + destructor-on-last-drop. WAW 2025 notes syntactic type soundness is + INSUFFICIENT for interesting Component-Model properties — i.e. no mature + sound analyzer for handle-state exists today. + limitations: > + Nascent; Wasm 3.0 (Sept 2025) also adds 64-bit, multi-memory, GC, + exceptions scry must eventually model. + differentiation: > + Category-defining opportunity: a sound own/borrow handle-state analysis + (use-after-drop, double-drop, leaked handles) extending scry's existing + meld component-provenance boundary. The highest-moat item (REQ-003). + + - id: CA-010 + type: competitive-analysis + title: "CodeQL + Semgrep — heuristic taint at scale (borrow the UX)" + status: draft + tags: [competitor, heuristic, taint, ux, query] + fields: + tool-name: "GitHub CodeQL / Semgrep" + tool-url: "https://codeql.github.com/" + vendor: "GitHub / Semgrep Inc." + tool-status: active + approach: > + CodeQL = semantic code-as-database, whole-program exhaustive taint via a + query language (QL). Semgrep = lightweight pattern + Pro cross-file taint. + Both heuristic (no soundness claim). + limitations: > + Unsound (false neg/pos); not abstract interpretation. + differentiation: > + scry's noninterference/taint is SOUND where theirs is heuristic — a + differentiator to assert. BORROW: (1) a query language over scry's + analysis facts; (2) the SARIF + PR-comment + IDE pipeline (scry's + developer-surface gap); (3) Semgrep's rule-pack distribution model. + + - id: CA-011 + type: competitive-analysis + title: "Tool-qualification ecosystem (DO-330 TQL / ISO 26262-8 TCL / LDRA / QSKs)" + status: draft + tags: [qualification, standard, certification] + description: > + What "qualifiable" (G-005) concretely requires — and where scry's + mechanized proofs are stronger-but-unpackaged evidence. + fields: + tool-name: "DO-330 / ISO 26262-8 §11 qualification kits" + tool-url: "https://www.ldra.com/do-330/" + vendor: "RTCA / ISO; kits from AbsInt, MathWorks, LDRA" + tool-status: standard + approach: > + DO-330 assigns Tool Qualification Levels TQL-1..5; ISO 26262-8 §11 uses + Tool Confidence Level (TCL1-3) = Tool Impact x Tool error Detection. A + sound verification tool like scry typically lands TQL-5 / must justify + TCL. Kits ship: Tool Operational Requirements, Qualification Plan, + qualification test suite + results, life-cycle data (QSLCD). + limitations: > + Kits are test-suite-based; assembling the dossier is substantial effort. + differentiation: > + scry's mechanized Rocq proofs + MC/DC gate + live kill-criteria are + STRONGER evidence than the test-based QSKs — but scry has NO packaged + dossier (TORs, plan, TCL/TQL argument). Producing a DO-330 TQL-5 / + ISO 26262-8 TCL-mapped dossier (with proofs as the differentiating + evidence) is the G-005 capstone. + + # ══════════════════════════════════════════════════════════════════════ + # Technology evaluations (continuing TE- series from research.yaml). + # ══════════════════════════════════════════════════════════════════════ + + - id: TE-011 + type: technology-evaluation + title: "AI-agent gap detection from analysis output (structured-primary, viz-secondary)" + status: draft + tags: [ai-agent, visualization, gap-detection, tooling] + description: > + Evaluation of how an AI agent should consume scry's output (scry-viz + + AnalysisResult) to detect analysis gaps — where the analyzer gave up (top + / unsupported-op fallback). Evidence: LLMs UNDER-read charts/SVG for + precise/numeric queries (CharXiv best-model 47%; SVG fails arithmetic + reads; structured tables score 2.72 vs chart image 1.91), while agentic + triage over STRUCTURED static-analysis findings is production-ready + (AdaTaint cuts FPs 43.7%, ZeroFalse, LLM+SMT invariant loops). scry today + emits top as SILENCE (only non-top facts recorded) with scattered + UnsoundnessFallback diagnostics and no aggregated gap report — the worst + case for an agent. Recommendation: structured side-channel is the + evidentiary basis; the SVG is a human/orientation layer only. + fields: + technology: "Multimodal-LLM / agentic consumption of analysis output" + category: framework + maturity: research + rust-compatible: true + wasm-compatible: true + recommendation: trial + + - id: TE-012 + type: technology-evaluation + title: "Apron / ELINA — numeric abstract-domain libraries" + status: draft + tags: [numerical-domain, library, scalability] + description: > + Apron is the standard interface (intervals/octagons/polyhedra/congruences); + ELINA (ETH) makes polyhedra orders-of-magnitude faster via online constraint + decomposition with no precision loss, and accelerates octagon DBMs. The + engineering answer to "polyhedra is too expensive" (AC-012). Note: C + libraries — scry's pure-Rust no_std ethos means likely re-implementing the + DECOMPOSITION TECHNIQUE rather than linking, but the algorithms are the + reference. + fields: + technology: "Apron / ELINA" + category: library + maturity: production + rust-compatible: false + wasm-compatible: false + license: "LGPL / Apache-2.0" + recommendation: assess + + # ══════════════════════════════════════════════════════════════════════ + # Market findings (continuing MF- series from research.yaml). + # ══════════════════════════════════════════════════════════════════════ + + - id: MF-006 + type: market-finding + title: "Runtime-error / trap detection is the defining capability of the sound-analyzer bar — scry has the domains but emits no verdicts" + status: draft + tags: [runtime-error, positioning, gap] + description: > + Every sound competitor (Astrée, Polyspace Code Prover, Frama-C/Eva, + TrustInSoft, VeriWasm) is fundamentally a "prove absence of run-time + errors" tool. scry's interval/region/pentagon-able domains already compute + the facts (a divisor interval containing 0; an address interval exceeding + the region) but scry classifies NO trap site — div/rem, OOB load/store, + unreachable, overflow, stack-exhaustion all fall to the sound top fallback. + Closing this (REQ-014) is the single biggest credibility gap vs the bar + and the most visible capability for the qualification thesis (G-005). + fields: + domain: "Sound static analysis / safety-critical Wasm" + finding-type: tool-gap + source: "Competitive sweep CA-001/003/004/005/006 (2026-06)" + confidence: high + + - id: MF-007 + type: market-finding + title: "No sound handle-state analyzer exists for the Wasm Component Model — uncontested green field" + status: draft + tags: [component-model, green-field, opportunity, moat] + description: > + The Component Model's resource handles (own/borrow, destructor-on-last-drop) + have no mature sound analyzer; WAW 2025 notes syntactic type soundness is + insufficient for the interesting properties. scry already owns the meld + component-provenance boundary (SCPV v3) — extending it to track handle + lifetimes (use-after-drop, double-drop, leaked handles) would be a + category-defining, uncontested capability (REQ-003 substance / CA-009). + fields: + domain: "WebAssembly Component Model verification" + finding-type: opportunity + source: "Competitive sweep CA-009 + AC-009/AC-024 (2026-06)" + confidence: high diff --git a/artifacts/roadmap-2.0.yaml b/artifacts/roadmap-2.0.yaml index 61cc832..6a06de8 100644 --- a/artifacts/roadmap-2.0.yaml +++ b/artifacts/roadmap-2.0.yaml @@ -1752,7 +1752,8 @@ artifacts: - id: FEAT-034 type: feature title: "v2.x — Independently-verified fusion premises + meld cross-check (FEAT-032 slice-2 consumption)" - status: proposed + status: accepted + release: v2.1.0 description: > Consume the fusion premises (scry#63 / FEAT-032) the SOUND way: VERIFY, don't TRUST. scry parses every op, so it independently determines @@ -1792,6 +1793,7 @@ artifacts: type: feature title: "v2.x — Align wasmparser/wasm-tools to 0.252 (dedup downstream trees, scry#62)" status: accepted + release: v2.1.1 description: > Bump `wasmparser` 0.247 → 0.252 across the workspace so the dependency tree dedups with downstream consumers (meld/synth) that have moved to @@ -1810,6 +1812,7 @@ artifacts: type: feature title: "v2.x — Interprocedural range propagation (synth wishlist, scry#54)" status: accepted + release: v2.2.0 description: > Narrow a callee's parameter invariants from the value ranges at its call sites (a sound, monotone interprocedural pass over the existing @@ -1833,6 +1836,7 @@ artifacts: type: feature title: "v2.x — Known-bits × interval-guarded congruence reduced product (synth#54)" status: accepted + release: v2.3.0 description: > Add a NEW reduced-product abstract domain capturing alignment, low-bit patterns, and induction strides the interval + octagon domains miss — @@ -1880,6 +1884,7 @@ artifacts: type: feature title: "v2.x — Consume verified bounded_memory to tighten the region/memory fixpoint (scry#70)" status: accepted + release: v2.4.0 description: > Make FEAT-034's verified `bounded_memory` premise PAY OFF. INVESTIGATION REFRAME (v2.4.0): the concrete win is the `memory.size` / `memory.grow` @@ -1916,6 +1921,7 @@ artifacts: type: feature title: "v2.x — Sound open-world reachable_from_exports (escaped funcrefs as roots) (scry#71)" status: accepted + release: v2.5.0 description: > INVESTIGATION REFRAME (v2.5.0) — what looked like a `closed_world` precision tweak is actually a SOUNDNESS FIX. A clean-room confirmed that diff --git a/artifacts/roadmap-3.0.yaml b/artifacts/roadmap-3.0.yaml new file mode 100644 index 0000000..865513d --- /dev/null +++ b/artifacts/roadmap-3.0.yaml @@ -0,0 +1,547 @@ +artifacts: + + # ══════════════════════════════════════════════════════════════════════ + # Roadmap 3.0 — release plan distilled from the v2.5→v3.0 research sweep + # (artifacts/research-2.yaml: AC-012..024, CA-001..011, TE-011/012, + # MF-006/007) and the internal gap audit. Theme arc: + # v2.6 "Make the analysis observable" — cash in computed-but-hidden + # facts (relational invariants, gaps); cheap precision; agent/ + # qualification readiness. + # v2.7 "Prove safety" — runtime-error / trap detection, + # the defining capability of the Astrée/Polyspace bar (MF-006). + # v3.0 "Qualifiable + differentiated" — float domain, mechanized + # soundness vs the OFFICIAL Wasm semantics, Component-Model + # handle-state (the moat), and the tool-qualification dossier. + # Release axis = the top-level `release:` field (rivet >= 0.21). Track with + # `rivet release status ` / `rivet list --release `. + # ══════════════════════════════════════════════════════════════════════ + + # ── New requirements from the gap audit ─────────────────────────────── + + - id: REQ-014 + type: requirement + title: "Soundly classify every Wasm trap site as proven-safe or potential-trap" + status: proposed + description: > + scry shall classify each operation that can trap at run time — integer + div/rem (div-by-zero, INT_MIN/-1 overflow), out-of-bounds linear-memory + load/store, `unreachable`, and (where modelled) arithmetic overflow and + stack exhaustion — as PROVEN-SAFE (the domains prove the trap cannot fire + on any run) or POTENTIAL-TRAP (it may), never silently dropping the site. + This is the defining capability of the sound-analyzer bar (MF-006) that + scry's interval/region/pentagon domains already compute the facts for but + do not surface. A new diagnostic category beyond Info/Warning/ + UnsoundnessFallback. Soundness: a site is PROVEN-SAFE only when the + abstract value rules out the trap; otherwise POTENTIAL-TRAP (over-approx). + tags: [runtime-error, trap, soundness, qualification, v2.x] + fields: + priority: must + category: functional + links: + - type: traces-to + target: G-005 + - type: traces-to + target: REQ-001 + + - type: addresses-finding + target: MF-006 + - id: REQ-015 + type: requirement + title: "Sound IEEE-754 floating-point abstract domain" + status: proposed + description: > + scry shall model f32/f64 values soundly (today float arithmetic scrubs to + top, so any float-bearing function is un-analyzed — a hard scope hole vs + the commercial bar). Approach: interval-with-rounding-error / relational + FP domain (Miné ESOP'04, AC-022) reusing the shipped octagon DBM, with + correct NaN/inf/rounding-mode handling. Sound over-approximation of the + IEEE-754 semantics; admit-free Rocq for the core transfers. + tags: [floating-point, numerical-domain, soundness, v3.x] + fields: + priority: should + category: functional + links: + - type: traces-to + target: G-005 + - type: traces-to + target: REQ-001 + + - type: references-paper + target: AC-022 + - id: REQ-016 + type: requirement + title: "Surface relational invariants (octagon / linear) in the analysis output" + status: proposed + description: > + scry computes relational facts (octagon DBM; strong closure since v1.9) + but the output projects them to unary intervals, so the relational + precision is invisible to consumers (the v1.9 non-observability finding). + scry shall expose the relational constraints (difference/sum bounds, and + later linear equalities) in the AnalysisResult so downstream optimizers + (loom, synth) and assessors can use them — the Frama-C/Eva communicating- + domain model (CA-004). Library-only first (like param_ranges/bit_facts); + WIT surfacing is a separate consumer-value item (FEAT-054). + tags: [relational, octagon, output, precision, v2.x] + fields: + priority: should + category: functional + links: + - type: traces-to + target: REQ-004 + - type: traces-to + target: G-005 + + - type: references-paper + target: AC-013 + - id: REQ-017 + type: requirement + title: "Machine-readable analysis-gap reporting for assessor + AI-agent consumption" + status: proposed + description: > + scry shall emit explicit, machine-readable records of every place the + analysis is conservative — a program point degraded to top, an unsupported + op, an empty-on-havoc operand stack, an UnsoundnessFallback — instead of + emitting top as SILENCE (today only non-top facts are recorded). It shall + provide an aggregated gap report (per function, per op-kind, with totals). + This is required both for the qualification dossier's scope/limitation + statement (G-005) and so an AI agent can reliably detect where scry gave + up — the research (TE-011) shows agents must consume the STRUCTURED + side-channel, not the rendered viz, for precise gap claims. + tags: [gap-report, ai-agent, qualification, observability, v2.x] + fields: + priority: must + category: functional + links: + - type: traces-to + target: G-005 + - type: traces-to + target: REQ-013 + + - type: evaluates-tech + target: TE-011 + # ══════════════════════════════════════════════════════════════════════ + # RELEASE v2.6.0 — "Make the analysis observable" + # Cash in computed-but-hidden facts; cheap precision; agent/qual readiness. + # ══════════════════════════════════════════════════════════════════════ + + - id: FEAT-040 + type: feature + title: "v2.6 — Machine-readable gap records + aggregated gap report" + status: proposed + release: v2.6.0 + description: > + Stop emitting top as silence. Emit a positive Gap{function, pc, op, kind, + reason} record whenever a fact degrades to top, an op is unsupported, an + operand stack is havocked, or UnsoundnessFallback/degraded fires; roll + them up into an aggregated gap report (by function, by op-kind, totals). + scry already has the raw signals (UnsoundnessFallback diagnostic, the + `degraded` flag) but scattered and unaggregated. Highest-leverage cheap + win: unlocks both the qualification scope/limitation statement and + AI-agent gap detection (TE-011). Library-only field + a scry-viz gaps + panel (text/table beside the SVG, per TE-011). + tags: [gap-report, observability, ai-agent, qualification, quick-win] + fields: + phase: phase-2 + acceptance-criteria: + - "Given a module with an unsupported op or a top-degraded point, When scry analyzes it, Then AnalysisResult carries an explicit Gap record (function, pc, op, kind) for that site and an aggregated count — no conservative site is silently omitted." + links: + - type: traces-to + target: REQ-017 + + - type: evaluates-tech + target: TE-011 + - id: FEAT-041 + type: feature + title: "v2.6 — Surface relational octagon invariants in AnalysisResult" + status: proposed + release: v2.6.0 + description: > + Expose the octagon's difference/sum bounds (the relational constraints the + analyzer already maintains and strong-closes) on the output, instead of + only the unary interval projection. Cashes in the entire octagon arc + (v1.4-v1.9), whose strong-closure precision is currently non-observable. + Library-only field first; sound by construction (the constraints are the + closed DBM scry already proves). Requires octagon SUM constraints in the + Interp to be non-trivial (the v1.9 note) — couple with that. + tags: [relational, octagon, output, precision] + fields: + phase: phase-2 + acceptance-criteria: + - "Given a function where the octagon holds a relation (e.g. i < n or x + y <= c), When scry analyzes it, Then that relational constraint appears in the AnalysisResult relational-invariants field — not just the unary interval projection." + links: + - type: traces-to + target: REQ-016 + + - id: FEAT-042 + type: feature + title: "v2.6 — Widening with thresholds" + status: proposed + release: v2.6.0 + description: > + Replace the fixed iterate-then-widen at LOOP_WIDEN_THRESHOLD with widening + up to a set of syntactic thresholds (constants and guard bounds in scope), + a standard cheap precision lever that recovers loop bounds the current + widening over-approximates to top. Sound (widening still terminates). + tags: [precision, widening, loop, quick-win] + fields: + phase: phase-2 + acceptance-criteria: + - "Given a counted loop bounded by a constant the current widening loses, When scry analyzes it with threshold widening, Then the loop counter is bounded by (or below) that constant rather than top — and the fixpoint still terminates." + links: + - type: traces-to + target: REQ-001 + + - id: FEAT-043 + type: feature + title: "v2.6 — call_indirect target-set weighting for the shadow-stack bound (FEAT-021 slice-3)" + status: proposed + release: v2.6.0 + description: > + DD-016 slice-3: weight an indirect call in the worst-case shadow-stack + longest-weighted-path by its RESOLVED target set (already computed by + FEAT-006) instead of the whole table — tightening the bound materially + while staying sound (the resolved set is an over-approximation). + tags: [stack-bound, precision, wcsu] + fields: + phase: phase-2 + acceptance-criteria: + - "Given a module whose call_indirect resolves to a small target subset of a large table, When scry computes the stack bound, Then the bound reflects the resolved targets' frames (lower) rather than the whole-table maximum — and never under-counts the true peak." + links: + - type: traces-to + target: DD-016 + + # ══════════════════════════════════════════════════════════════════════ + # RELEASE v2.7.0 — "Prove safety" (the Astrée/Polyspace headline, MF-006) + # ══════════════════════════════════════════════════════════════════════ + + - id: FEAT-044 + type: feature + title: "v2.7 — Pentagons domain (cheap x in [a,b] AND x < y)" + status: proposed + release: v2.7.0 + description: > + Add the Pentagons weakly-relational domain (Logozzo-Fähndrich, AC-014): + intervals + strict-less-than facts, far cheaper than octagon, built for + bounds validation. The enabler for sound out-of-bounds linear-memory trap + detection (the x < mem_size facts). New pure domain crate, admit-free Rocq + for the lattice + transfers, gamma-sweep tests — the scry domain pattern. + tags: [numerical-domain, bounds, traps, pentagons] + fields: + phase: phase-2 + acceptance-criteria: + - "Given an index guarded by a comparison to a length (i < n), When scry analyzes the guarded region, Then the pentagon records i < n soundly, with an admit-free Rocq proof of the lattice + transfer soundness and an exhaustive gamma-sweep." + links: + - type: traces-to + target: REQ-014 + + - type: references-paper + target: AC-014 + - id: FEAT-045 + type: feature + title: "v2.7 — Trap detection: division-by-zero + integer-overflow classification" + status: proposed + release: v2.7.0 + description: > + Classify every i32/i64 div_s/div_u/rem_s/rem_u as PROVEN-SAFE (the divisor + interval excludes 0, and for div_s the dividend/divisor exclude the + INT_MIN/-1 overflow trap) or POTENTIAL-TRAP, as first-class diagnostics — + the first runtime-error class, the bar's headline capability. The interval + domain already computes the divisor range; this surfaces the verdict. + tags: [runtime-error, trap, division, overflow] + fields: + phase: phase-2 + acceptance-criteria: + - "Given a div/rem whose divisor interval excludes 0 (and excludes the INT_MIN/-1 case for div_s), When scry analyzes it, Then it is reported PROVEN-SAFE; given a divisor interval containing 0, it is POTENTIAL-TRAP — never silently dropped." + links: + - type: traces-to + target: REQ-014 + + - type: addresses-finding + target: MF-006 + - id: FEAT-046 + type: feature + title: "v2.7 — Trap detection: out-of-bounds linear-memory access" + status: proposed + release: v2.7.0 + description: > + Classify each load/store as PROVEN-SAFE when the effective address + + access size is provably within the memory's current size (using the region + domain + the pentagon x < mem_size facts + FEAT-038 memory.size bounds), + else POTENTIAL-TRAP. The OOB trap class — the most valuable for Wasm + sandbox-adjacent assurance (cf. VeriWasm, CA-006). + tags: [runtime-error, trap, memory, oob] + fields: + phase: phase-2 + acceptance-criteria: + - "Given a load/store whose address+size is provably < memory size (region/pentagon bounds), When scry analyzes it, Then it is PROVEN-SAFE; given an address that may exceed the memory, it is POTENTIAL-TRAP — soundly (never PROVEN-SAFE when a concrete run could trap)." + links: + - type: traces-to + target: REQ-014 + + - type: addresses-finding + target: MF-006 + # ══════════════════════════════════════════════════════════════════════ + # RELEASE v3.0.0 — "Qualifiable + differentiated" (strategic) + # ══════════════════════════════════════════════════════════════════════ + + - id: FEAT-047 + type: feature + title: "v3.0 — IEEE-754 floating-point domain (FP octagon)" + status: proposed + release: v3.0.0 + description: > + Sound f32/f64 abstraction via interval-with-rounding-error reusing the + octagon DBM (Miné ESOP'04, AC-022), with NaN/inf/rounding handling. + Removes the hard scope hole where any float-bearing function is un-analyzed. + Admit-free Rocq for the core transfers; gamma-sweep over representative + float grids. + tags: [floating-point, numerical-domain, soundness, strategic] + fields: + phase: phase-3 + acceptance-criteria: + - "Given a function performing f32/f64 arithmetic, When scry analyzes it, Then it produces a sound float interval (over-approximating the IEEE-754 result incl. rounding/NaN/inf) instead of degrading the function to top." + links: + - type: traces-to + target: REQ-015 + + - type: references-paper + target: AC-022 + - id: FEAT-048 + type: feature + title: "v3.0 — Mechanized soundness vs WasmCert-Coq + wrap-aware transfers (the differentiator)" + status: proposed + release: v3.0.0 + description: > + Make the G-005 differentiator literally true: prove scry's transfers sound + against the OFFICIAL mechanized Wasm semantics (WasmCert-Coq, TE-004), + not only scry's own concrete model; in particular prove the WRAP-AWARE + i32/i64 add (today proven only on the no-wrap core, widened to top on + possible wrap). Also REPAIR or remove the recorded-false Verus join proof + before any dossier cites mechanized soundness. Methodology template: + Verasco (AC-020). + tags: [mechanized-soundness, rocq, wasmcert, differentiator, strategic] + fields: + phase: phase-3 + acceptance-criteria: + - "Given scry's interval add transfer, When checked against WasmCert-Coq's i32.add semantics, Then an admit-free Rocq theorem establishes soundness INCLUDING the wrapping case — and the false Verus join proof is repaired or removed." + links: + - type: traces-to + target: REQ-002 + - type: traces-to + target: G-005 + + - type: references-paper + target: AC-020 + - type: evaluates-tech + target: TE-004 + - id: FEAT-049 + type: feature + title: "v3.0 — Component-Model handle-state / use-after-drop (the moat)" + status: proposed + release: v3.0.0 + description: > + The uncontested green field (MF-007 / CA-009): a sound affine handle-state + lattice over the Component Model's own/borrow resources (fresh / borrowed / + owned / dropped) detecting use-after-drop, double-drop, and leaked handles, + plus host-call effect sets — extending scry's existing meld component- + provenance boundary (SCPV v3) from plumbing to actual analysis. The + substance of REQ-003 / G-003. Env-specification for host imports per + AC-024. + tags: [component-model, handle-state, use-after-drop, moat, strategic] + fields: + phase: phase-3 + acceptance-criteria: + - "Given a component that drops a resource handle and then uses it, When scry analyzes it, Then a use-after-drop is reported soundly; given a handle correctly owned/borrowed across its lifetime, no false report — with the handle lattice gamma-soundness mechanized." + links: + - type: traces-to + target: REQ-003 + - type: traces-to + target: G-005 + + - type: addresses-finding + target: MF-007 + - id: FEAT-050 + type: feature + title: "v3.0 — Tool-qualification dossier (DO-330 TQL-5 / ISO 26262-8 TCL)" + status: proposed + release: v3.0.0 + description: > + The G-005 capstone (CA-011): assemble the assessor-facing qualification + package — Tool Operational Requirements, Qualification Plan, the scope/ + limitation statement (what scry soundly handles vs falls to top — fed by + FEAT-040's gap report), the operational-verification report, and the + TQL/TCL argument — mapping every objective to a scry artifact, with the + admit-free Rocq proofs + MC/DC gate + live kill-criteria as the + DIFFERENTIATING evidence (stronger than competitors' test-based QSKs). + Depends on the substance landing first (FEAT-045/046/048). + tags: [qualification, dossier, do-330, iso-26262, capstone, strategic] + fields: + phase: phase-3 + acceptance-criteria: + - "Given the qualification dossier, When an assessor reviews it, Then every DO-330 TQL-5 / ISO 26262-8 §11 objective maps to a concrete scry artifact (proof, test, gate, or scope statement) — and the scope/limitation statement enumerates the analysis gaps from FEAT-040." + links: + - type: traces-to + target: G-005 + + # ══════════════════════════════════════════════════════════════════════ + # BACKLOG — researched, valuable, not yet release-scoped (status proposed, + # no `release:`). Promote into a release when picked up. + # ══════════════════════════════════════════════════════════════════════ + + - id: FEAT-051 + type: feature + title: "Backlog — Karr linear-equality domain" + status: proposed + description: > + Exact affine equalities sum(a_i x_i)=c (Karr 1976, AC-013) — a low-cost + relational equality domain complementing the octagon, with a small + mechanizable transfer set. Feeds REQ-016 relational surfacing. + tags: [numerical-domain, relational, backlog] + fields: + phase: future + acceptance-criteria: + - "Given a program with an affine relation among locals, When scry analyzes it, Then the Karr domain infers the exact equality soundly, with admit-free Rocq for join/meet/transfer." + links: + - type: traces-to + target: REQ-016 + + - type: references-paper + target: AC-013 + - id: FEAT-052 + type: feature + title: "Backlog — Termination / loop-bound via segmented ranking functions" + status: proposed + description: > + Synthesize sound ranking functions (Urban FuncTion, AC-018) to turn the + WCSU bound's "Unbounded" (every recursive SCC) into an actual bound for + bounded recursion, and add loop-iteration / Wasm fuel bounds (SPEED-style, + AC-019; the aiT WCET analogue, CA-002). + tags: [termination, ranking-function, resource-bound, backlog] + fields: + phase: future + acceptance-criteria: + - "Given a terminating bounded-recursion or counted loop, When scry analyzes it, Then it reports a sound iteration/depth bound (not Unbounded), backed by a synthesized ranking function." + links: + - type: traces-to + target: DD-016 + + - type: references-paper + target: AC-018 + - id: FEAT-053 + type: feature + title: "Backlog — Incremental / demanded compositional summaries (scaling)" + status: proposed + description: > + Upgrade FEAT-007 function summaries to incremental + demand-driven + + compositional (Stein et al., AC-021): reuse results across edits, compose + procedure summaries — the scaling story for CI, the dashboard, and large + fused modules (REQ-007, whose >=50k-instr scaling claim is still + un-benchmarked). + tags: [scalability, incremental, compositional, backlog] + fields: + phase: future + acceptance-criteria: + - "Given a small edit to one function of a large module, When scry re-analyzes incrementally, Then only the affected summaries recompute and the result matches a from-scratch run (from-scratch consistency)." + links: + - type: traces-to + target: REQ-007 + + - type: references-paper + target: AC-021 + - id: FEAT-054 + type: feature + title: "Backlog — WIT-level surfacing of library-only facts" + status: proposed + description: > + Surface the rich library-only fields (param_ranges, bit_facts, + operand_stack, verified_premises, relational invariants, gaps) through the + WIT/component boundary + the frozen JSON contract, so non-Rust / sandboxed + consumers (loom, assessor tooling) can read them. spar/AADL->WIT regen + + wrapper conversion. Serves REQ-004. + tags: [output, wit, consumer-value, backlog] + fields: + phase: future + acceptance-criteria: + - "Given a non-Rust consumer over the WIT boundary, When scry analyzes a module, Then it can read param_ranges / bit_facts / relational invariants / gaps via WIT — not only the Rust AnalysisResult." + links: + - type: traces-to + target: REQ-004 + + - id: FEAT-055 + type: feature + title: "Backlog — Counterexample generation for POTENTIAL-TRAP sites (symbolic)" + status: proposed + description: > + Couple a SeeWasm-style symbolic engine (CA-008) to scry's POTENTIAL-TRAP + verdicts to turn "cannot prove safe" into "input X may trap" — and the + SeaHorn pattern (AI invariants seeding an SMT/CHC refinement) to shrink + orange->green without losing soundness. + tags: [counterexample, symbolic, ux, backlog] + fields: + phase: future + acceptance-criteria: + - "Given a POTENTIAL-TRAP site, When the symbolic companion runs, Then it either produces a concrete trapping input or refines the site to PROVEN-SAFE — soundness of scry's verdict preserved either way." + links: + - type: traces-to + target: REQ-014 + + - id: FEAT-056 + type: feature + title: "Backlog — Sound queryable CPG + query language over AnalysisResult" + status: proposed + description: > + A queryable graph surface — scry's CFG/call-graph/data-flow annotated with + proven invariants — with a query language (the Wasmati CPG idea, CA-007, + made SOUND; the CodeQL/Semgrep UX, CA-010). Lets an agent or developer ask + "all points where kind=Top and op in (call_indirect, memory.grow)" instead + of scraping HTML (TE-011 structured-channel recommendation). + tags: [query, cpg, ai-agent, ux, backlog] + fields: + phase: future + acceptance-criteria: + - "Given the AnalysisResult, When an agent issues a structured query over the annotated graph, Then it gets the matching nodes/edges with their proven facts and gaps — no HTML scraping." + links: + - type: traces-to + target: REQ-017 + + - id: FEAT-057 + type: feature + title: "Backlog — Polyhedra domain (ELINA-style decomposition)" + status: proposed + description: > + Convex polyhedra (Cousot-Halbwachs, AC-012) for exact linear inequalities + above the octagon, made tractable via ELINA's online constraint + decomposition (TE-012). The precision ceiling; a large domain bet beyond + Karr (FEAT-051). + tags: [numerical-domain, polyhedra, relational, backlog] + fields: + phase: future + acceptance-criteria: + - "Given a program with linear inequality invariants the octagon cannot express, When scry analyzes it, Then the polyhedra domain infers them soundly at acceptable cost (decomposed), with mechanized soundness." + links: + - type: traces-to + target: REQ-016 + + - type: references-paper + target: AC-012 + - type: evaluates-tech + target: TE-012 + - id: FEAT-058 + type: feature + title: "Backlog — Array / linear-memory segmentation (content sensitivity)" + status: proposed + description: > + A parametric segmentation functor (Cousot-Cousot-Logozzo, AC-015) giving + scry's flat linear-memory region per-segment content sensitivity (track + values inside memory ranges, not one havoc'd blob) — a new analysis + dimension extending the region domain (REQ-001). + tags: [memory, array, segmentation, backlog] + fields: + phase: future + acceptance-criteria: + - "Given a loop that fills a memory range with a bounded value, When scry analyzes it, Then the segmentation domain tracks the per-segment content bound instead of widening loaded values to top." + links: + - type: traces-to + target: REQ-001 + - type: references-paper + target: AC-015