Land the Java modeling matrix and complete wave M1 - #80
Merged
Conversation
Twelve modeling templates in six categories — declared sources and sinks, propagators, sanitizers, opaque summaries, framework entry points, and persistence boundaries — each with one positive and one minimally different negative, fixed before any modeling fixture, model file, or run exists. The challenge tier's amendment contract applies verbatim. Each model is defined analyzer-neutrally as entity identity, role, and binding semantics, so the four adapters encode the same declaration in their own native surfaces. Per-tool capability partitions are preregistered from the pinned tools: Semgrep CE 1.174.0 and CodeQL 2.26.3 were probed directly, Joern's flow-semantics surface from a local distribution, and everything unverifiable is recorded as unsupported until shown otherwise. Modeling is a new score tier rather than a fold into core, because it asks a different question from the kernels. Schema groundwork is additive only: score_tier gains "modeling" in the case and freeze schemas and in the result tier ordering. No new negative mechanism was needed — the enum's existing "sanitizer" value already means what the sketch's "sanitizer-kill" would have. No fixtures, no cases, no model files, no runs, no adapter changes. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The twelve preregistered modeling templates, their six categories, and the per-tool capability partition are transcribed from docs/modeling-matrix.md into src/main.rs, ahead of any fixture, model artifact, or run. No fixtures, no model files, no reports: this is the machinery a language pull request fills. MODELING_PARTITION is CHALLENGE_SEMGREP_PARTITION's mechanism generalized to four tools — twenty-four cells, one per tool per category, with the preregistration's "to be verified" cells recorded as unsupported per its own rule. Scored today: Bifrost 2 templates of 12, Semgrep CE 6, CodeQL 12, Joern 12. A declined cell is decided from the template ID before the tool is invoked, retains the document's rationale verbatim, and writes a retained capability decision beside the report; a test asserts the cell does not move when a case's feature_tags are rewritten. Tier isolation is structural rather than a filter to remember: a dfb-template-model- template and score_tier "modeling" imply each other, and smoke_population_case refuses modeling cases the way it already refuses challenge ones, so the frozen 118-case Bifrost slice cannot absorb one. The population validator enforces the balanced twenty-four over exactly the twelve for any language that has modeling cases at all; a language with none has no modeling denominator, which is different from having a zero, so no rollout table is needed — presence is the signal. Four commands, parameterized by language rather than twelve near-identical variants: the per-language kernel commands are separate because each language's kernel differs in real toolchain plumbing, and a modeling run differs from its sibling only in which artifact it loads. Each refuses, before touching the analyzer, when the language has no modeling population or when the tool's modeling artifact is missing — the preregistration's "missing model is a benchmark defect" arm, a hard error that fails the build rather than an outcome. The load-bearing-model gates are wired now so a language pull request cannot forget them: a Bifrost modeling policy must set :unmodeled require-model and may not name the kernel policies' optimistic default, and a Semgrep modeling rule must set taint_assume_safe_functions: true. Tests pin both strings. CodeQL and Joern have no such switch and are not gated. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Wave M1's first language. Twenty-four assertions — the twelve preregistered templates x positive/negative — under cases/taint/java/model-*, four per-adapter artifacts encoding the same analyzer-neutral declarations natively, the scored execution arm for all four modeling runners, and the four runs. No template proved unimplementable as preregistered and no partition cell moved. Where a run disagreed with what docs/modeling-matrix.md expected, the disagreement is published as observed and carried in docs/java-modeling.md as a *proposed* amendment for a separate, dated change: a cell revised from a result is a result being relabelled. Outcomes, on four different denominators that are not comparable to one another and are never pooled with the propagation kernel: Bifrost 4/4 on the one category its partition scores and 20 preregistered `unsupported`; CodeQL 24/24; Joern 20/24; Semgrep CE 11/12 scored and 12 `unsupported`. No `inconclusive` and no `runner-error` anywhere. Load-bearing verification is part of the run contract, and every scored tool has a demonstrated counterfactual: removing one declaration from the committed artifact removes the finding, with a control cell that depends on a different declaration left unchanged. One of them came back negative and is reported that way — Semgrep CE's required `taint_assume_safe_functions: true` also suppresses the flow through the *declared* sanitizer, so on a category-Z fixture the option rather than the declaration decides the cell. A crossed four-run probe is the evidence. Category Z is still scored with the option on, because that is what the preregistration and the runner gate require, and template 6's positive is published as the false negative it is rather than recovered by declaring a propagator this partition does not award CE. Joern's two false positives are separated from "the model was ignored" by their own probes: the `Opaque.select` mapping is acted on but its index is not enforced, and a `FlowPath` access-path destination can be written but does not discriminate the declared field from its sibling. Reconciliation on this tier is source-anchored as well as sink-anchored, because a modeling fixture carries both halves of its pair in one type by construction and category E's handlers need no caller — so the declared handler's flow is present in the negative's fixture. A finding counts only when it lies in the region its case's own source anchor governs and on a callsite of its anchored sink function; an unmatched finding is the pair's other entity, fully attributable, and normalizes to `not-reached` with the count retained rather than to the kernels' `inconclusive`. Two adapter-hygiene points that the freeze depends on. The Semgrep modeling rules share the rules directory but are excluded from the kernel configuration hash, so a modeling wave landing for a new language does not move a hash that describes nothing about the kernel a retained report is evidence for. And Java's CodeQL modeling query joins the adapter's root pack, which is the Java pack; the infra's schematic `adapters/codeql/java/queries/` has no qlpack to resolve `codeql/java-all` from. The eight new report and raw-evidence paths collide with nothing the v0.4.0 freeze binds, no pre-existing case or report is touched, and the smoke population stays 118. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Java is wave M1's last language, and this merge is where its wave meets the Python and JavaScript waves that landed on main in the interval. Main's shapes win wholesale wherever both sides wired the same thing — the four modeling runners, the language dispatch, the `model-*.yaml` exclusion from the Semgrep kernel configuration hash and its pinned eleven-file hash literal, and the shared `adapters/joern/queries/modeling.sc`, which is hash-bound into Python's and JavaScript's committed reports and does not move a byte. Java's artifacts were adapted to main's script rather than the reverse: the `--param` surface, the `DefaultSemantics().plus(declared)` layering, and the empty-parse raise are main's. One value goes the other way, because it is a fact rather than a shape. Java's CodeQL modeling query is `adapters/codeql/queries/JavaModeling.ql`, not `adapters/codeql/java/queries/`. The rule — a modeling query lives inside its language's existing qlpack — is unchanged; Java's pack simply *is* the adapter root, `adapters/codeql/qlpack.yml` declares `dataflowbench/codeql-java`, and no `adapters/codeql/java/` pack exists to descend into. A test now asserts that every modeling query resolves a `qlpack.yml` two directories up. Marker-convention audit. Four of Java's twelve negatives marked the *undeclared sibling* rather than the declared entity — `Audit.discard`, `Config.fetchLocal`, `Handler.onIgnored`, `Handler.onUndeclared` — which is the same authoring slip the JavaScript wave found in four of its own, and it inverts what a negative measures. All four now mark the declared entity, the two entry-point negatives' bodies moved with them (a negative whose declared handler still carries the flow is not a negative), and the corresponding positives were aligned in the same pass. The three rows' fixtures are now shape-for-shape identical, and all twenty-four Java fixtures still compile under `javac -Werror`. Java modeling reconciles under a new `AnchorDialect::JavaMember`, the exact counterpart of main's `EcmaMember`. Java has no free functions, so every declared modeling entity is a member of some type and every callsite of one is written through its receiver; the kernel dialect refuses exactly that spelling, which is right for a kernel and wrong for a declaration that binds a type and a member as one identity. No kernel reconciliation changes. The artifact invariant is applied: `model-java.semantics` drops its category-P and category-O declarations, because Amendment A2 marks those cells unsupported and an artifact never declares a category its partition declines. Three entries remain, and the file stays comment-free — the pinned 4.0.610 parser was measured to return an empty list for a comment-leading file, and `declared_semantic_count: 3` in every retained document is the confirmation that it parses. All four adapters re-run on the merged tree, sequentially, on the amended partition: Bifrost 4/4 scored with 20 preregistered `unsupported`, CodeQL 24/24, Joern 14/16 with 8 `unsupported`, Semgrep CE 10/10 with 14 `unsupported`. No `inconclusive` and no `runner-error` anywhere. That is the Python and JavaScript shape cell for cell, including Joern's two category-B false negatives; the one divergence is that Bifrost decides all four of its category-S cells on Java where JavaScript reported three `inconclusive`, which is that language's engine incompleteness rather than a modeling property. Every scored category has a demonstrated counterfactual in the new `scripts/probe-java-modeling-load-bearing.sh`. Two amendment records, neither of which moves a cell. **A5** confirms that Bifrost v0.10.6 accepts `:call-modeling (call-modeling :unmodeled require-model)` — one of the two facts the preregistration recorded as *to be verified* behind Bifrost's category P, with the other, that a propagator section actually lowers, untouched. It is an evidentiary confirmation and Bifrost's category-S cells were already scored. **A4 gains a dated addendum**: the committed Java semantics declares nothing for category P, and the pinned engine still follows `Opaque.class.getMethod(…).invoke(…)` unaided, so A4's correction is not `jssrc2cpg`-specific. A different reflective construct, an independent measurement, the same conclusion. Pre-amendment observations are retained as evidence rather than deleted: Joern's positional-fidelity and access-path findings and Semgrep's crossed four-run category-Z probe are carried in docs/java-modeling.md, where they now confirm A2 and A3 from a second language instead of proposing amendments of their own. The raw evidence for those declined cells is the partition's own `retained-capability-decision` document, matching the Python and JavaScript rows exactly. Full battery clean: fmt, 136 tests, 816 cases, 54 reports. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Closes #15. The third and final wave-M1 language: Java's 24-assertion modeling population, four hash-bound artifacts (
javac -Werrorclean fixtures; the CodeQL query in the root pack, with a new test asserting every modeling query resolves a qlpack), all four adapters re-run on the amended partition.inconclusiveas that engine-frontend's incompleteness, not a modeling property.AnchorDialect::JavaMemberadded (every Java entity is receiver-qualified).javasrc2cpgwalksClass.getMethod(...).invoke(...)unaided (declared_semantic_count: 3, flow_count: 1retained), an independent measurement on a different reflective construct. A5 records the evidentiary confirmation that Bifrost v0.10.6 accepts:unmodeled require-model(one of the two preregistered to-be-verified facts; the other stays open, so no partition change).scripts/probe-java-modeling-load-bearing.sh); stale raw docs pruned to zero orphans across all four dirs.Issue #15's acceptance criteria are met: balanced pairs per category ✓ · equivalent benchmark-controlled models per analyzer ✓ · modeling scored separately from propagation ✓ · missing-model / unsupported-activation / incomplete-analysis distinguishable in retained evidence ✓ · Java, JavaScript, and Python matrices ✓.
Validation
cargo fmt --check·cargo test(136) ·validate(816 cases) ·validate-reports(54) ·validate-freeze·generate-results --check.🤖 Generated with Claude Code