Record Amendments A2 and A3 to the modeling matrix

docs/adapters.md

@@ -297,10 +297,13 @@ their own. So the runner reads each artifact before the run and refuses it
 unless the default is disabled: a Bifrost modeling policy must set
 `:call-modeling (call-modeling :unmodeled require-model)` and must not name the
 kernel policies' `optimistic`, and a Semgrep modeling rule must set `options:
-taint_assume_safe_functions: true`. Tests pin both strings. CodeQL and Joern
-have no such switch to pin — a `ConfigSig` with no `isAdditionalFlowStep` adds
-no step and a Joern method with no `FlowMapping` propagates nothing — so
-neither is gated.
+taint_assume_safe_functions: true`. Tests pin both strings. CodeQL has no
+such switch to pin — a `ConfigSig` with no `isAdditionalFlowStep` adds no
+step. Joern's equivalent claim ("a method with no `FlowMapping` propagates
+nothing") was measured false by the first wave-M1 run: `FlowSemantic`
+mappings on the pinned 4.0.610 are additive over the engine's default
+pass-through, which is why Amendment A2 moved Joern's propagator and summary
+categories to unsupported activation rather than gating them.
 
 **The execution arm lands with the language.** Today every modeling command
 stops at the population gate, because no fixture exists. The arm that invokes

docs/modeling-matrix.md

@@ -878,6 +878,11 @@ whether the resulting semantics match — which is what the assertions measure.
 
 ### Joern — 4.0.610
 
+> **Amended.** Categories P and O were moved to unsupported activation by
+> Amendment A2 after the first wave-M1 run measured `FlowSemantic` as
+> additive rather than restrictive; Joern's scored set is S, Z, E, B.
+
+
 Verified surface: the OSS data-flow engine ships a flow-semantics loader —
 `io.joern.dataflowengineoss.semanticsloader` with `FlowSemantic`, `FlowMapping`,
 `FlowPath`, `ParamOrRetNode`, `NilSemantics`, `NoCrossTaintSemantics`, and
@@ -904,6 +909,12 @@ scoped to a separate `modeling.sc` so the kernel script is untouched.
 
 ### Semgrep CE — 1.174.0 (`--oss-only`)
 
+> **Amended.** Template 6 (sanitizer-selectivity) was moved to unsupported
+> activation by Amendment A3: the mandated safe-function assumption and
+> selectivity cannot coexist in one invocation. Semgrep's scored set is
+> five templates.
+
+
 This partition is **verified by execution** against the pinned CE binary
 (`semgrep 1.174.0`, `--oss-only`), on small Python probes, before any fixture
 exists. Each cell below states what was run and what came back.
@@ -1138,4 +1149,49 @@ Restating the obligations this tier is most at risk of eroding:
 
 ## Amendments
 
-None yet. This document has not been amended since it merged.
+### A2 — 2026-08-26: Joern's propagator and summary categories are not load-bearing
+
+**What changed.** Joern's cells for category P (`opaque-propagator`,
+`propagator-position`) and category O (`summary-through`, `summary-field`)
+move from scored to **unsupported activation**. Its scored modeling set is
+now the eight templates of categories S, Z, E, and B.
+
+**Why.** The first wave-M1 run (Python) probed the load-bearing contract and
+found that on the pinned 4.0.610, `FlowSemantic` mappings are **additive**
+over the engine's default unmodeled-call pass-through and cannot restrict
+it: removing the propagator declaration leaves the finding standing, and a
+declared positional mapping does not exclude the undeclared position — so a
+P or O result scores the engine's optimism, not the model. A summary's
+field-destination access path is likewise ignored (the whole object is
+tainted), resolving that cell's to-be-verified marker negatively. Category Z
+remains scored: `NilSemantics` was demonstrated genuinely load-bearing
+(removing it restores the flow). The preregistration's stated justification
+for leaving Joern ungated — "a method with no `FlowMapping` propagates
+nothing" — was measured false and is corrected by this amendment.
+
+**Tools, templates, and languages touched.** Joern only; templates 3, 4, 7,
+8; all wave-M1 languages (the limitation is engine-level, verified on
+Python, expected identical elsewhere and to be confirmed by each language's
+retained evidence).
+
+**Freezes invalidated.** None. No modeling report is bound by any freeze.
+
+### A3 — 2026-08-26: Semgrep's sanitizer-selectivity cell is undecidable by construction
+
+**What changed.** Template 6 (`sanitizer-selectivity`) moves from scored to
+**unsupported activation** for Semgrep CE, by a template-level override; its
+category sibling, template 5 (`sanitizer-kill`), remains scored. Semgrep's
+scored modeling set is now five templates.
+
+**Why.** The preregistration mandates `taint_assume_safe_functions: true`
+so that propagator models stay load-bearing — and that same option
+suppresses flow through the *undeclared* sanitizer-lookalike that template
+6's positive requires. Selectivity and the safe-function assumption cannot
+coexist in a single CE invocation, so the cell's positive is undecidable by
+construction rather than by capability: the first wave-M1 run recorded it
+as Semgrep's only false negative before this amendment reclassified it.
+
+**Tools, templates, and languages touched.** Semgrep CE only; template 6;
+all wave-M1 languages.
+
+**Freezes invalidated.** None.

src/main.rs

@@ -696,7 +696,16 @@ const MODELING_PARTITION: [ModelingPartitionCell; 24] = [
     ModelingPartitionCell {
         tool: ModelingTool::Joern,
         category: ModelingCategory::Propagators,
-        unsupported_reason: None,
+        // Amendment A2: FlowSemantic mappings on the pinned 4.0.610 are
+        // additive over the engine's default argument pass-through and cannot
+        // restrict it, so a propagator declaration is not load-bearing — the
+        // default decides the cell with or without the model.
+        unsupported_reason: Some(
+            "Joern 4.0.610 FlowSemantic mappings are additive over the \
+             default unmodeled-call pass-through and cannot restrict it; a \
+             propagator model is not load-bearing on the pinned version \
+             (Amendment A2)",
+        ),
     },
     ModelingPartitionCell {
         tool: ModelingTool::Joern,
@@ -706,7 +715,16 @@ const MODELING_PARTITION: [ModelingPartitionCell; 24] = [
     ModelingPartitionCell {
         tool: ModelingTool::Joern,
         category: ModelingCategory::Summaries,
-        unsupported_reason: None,
+        // Amendment A2: same additivity, and the field-destination access
+        // path of a summary (arg -> field of arg) is ignored — the whole
+        // object is tainted — so a summary model is likewise not
+        // load-bearing on the pinned version.
+        unsupported_reason: Some(
+            "Joern 4.0.610 ignores a summary's field-destination access path \
+             and its FlowSemantic cannot restrict the default pass-through; \
+             a summary model is not load-bearing on the pinned version \
+             (Amendment A2)",
+        ),
     },
     ModelingPartitionCell {
         tool: ModelingTool::Joern,
@@ -761,10 +779,33 @@ const MODELING_PARTITION: [ModelingPartitionCell; 24] = [
 /// identity alone: `None` when the category is scored, `Some(reason)` when the
 /// tool declines it. Every cell is present, so an unknown template is a
 /// programming error rather than a silent scored default.
+/// Template-level partition overrides (Amendment A3): consulted before the
+/// category cell, for the cells where a tool's capability splits within a
+/// category. Semgrep CE can score sanitizer-kill (template 5) but not
+/// sanitizer-selectivity (template 6): the mandated
+/// `taint_assume_safe_functions: true` — required to keep propagator models
+/// load-bearing — itself suppresses flow through the undeclared
+/// sanitizer-lookalike, so selectivity's positive is undecidable by
+/// construction in a single CE invocation.
+const MODELING_TEMPLATE_OVERRIDES: [(ModelingTool, &str, &str); 1] = [(
+    ModelingTool::Semgrep,
+    "dfb-template-model-sanitizer-selectivity",
+    "Semgrep CE cannot express sanitizer selectivity and the safe-function \
+     assumption in one invocation: taint_assume_safe_functions suppresses \
+     flow through the undeclared sanitizer-lookalike, so the positive is \
+     undecidable by construction (Amendment A3)",
+)];
+
 fn modeling_partition_reason(tool: ModelingTool, template: &str) -> Result<Option<&'static str>> {
     let category = modeling_category(template).with_context(|| {
         format!("{template:?} is not one of the twelve preregistered modeling templates")
     })?;
+    if let Some((_, _, reason)) = MODELING_TEMPLATE_OVERRIDES
+        .iter()
+        .find(|(t, id, _)| *t == tool && *id == template)
+    {
+        return Ok(Some(reason));
+    }
     MODELING_PARTITION
         .iter()
         .find(|cell| cell.tool == tool && cell.category == category)
@@ -12668,9 +12709,12 @@ mod tests {
     #[test]
     fn modeling_partition_scored_counts_match_the_preregistration() {
         assert_eq!(modeling_supported_templates(ModelingTool::Bifrost).len(), 2);
-        assert_eq!(modeling_supported_templates(ModelingTool::Semgrep).len(), 6);
+        // Amendment A3 moved sanitizer-selectivity out of Semgrep's scored set.
+        assert_eq!(modeling_supported_templates(ModelingTool::Semgrep).len(), 5);
         assert_eq!(modeling_supported_templates(ModelingTool::Codeql).len(), 12);
-        assert_eq!(modeling_supported_templates(ModelingTool::Joern).len(), 12);
+        // Amendment A2 moved Joern's propagator and summary categories to
+        // unsupported: FlowSemantic is additive on the pinned 4.0.610.
+        assert_eq!(modeling_supported_templates(ModelingTool::Joern).len(), 8);
     }
 
     /// Bifrost enters with category S alone — the honest starting position the
@@ -12712,6 +12756,10 @@ mod tests {
         ] {
             expected.extend(category.templates());
         }
+        // Amendment A3: sanitizer-selectivity is template-overridden out of
+        // Semgrep's scored set — the safe-function assumption and selectivity
+        // cannot coexist in one CE invocation.
+        expected.retain(|template| *template != "dfb-template-model-sanitizer-selectivity");
         expected.sort_unstable();
         let mut scored = modeling_supported_templates(ModelingTool::Semgrep);
         scored.sort_unstable();