Repository navigation
Shadow mismatch paths: port to Go, Rust and Python and land the shared observations, vectors and mutants #243
Description
Agent: tracking issue for the work design/2026-10-24-shadow-mismatch-paths.md plans after its TypeScript reference. On 2026-10-24 the maintainer chose to land all of it in #242, which closes this issue, once he is satisfied with the TypeScript reference.
Ports (Plan step 3, in #242)
Each port follows the TypeScript semantics, with its driver and docs.
- Go:
ShadowPolicy.MismatchLogging,Operation.MismatchDiff,MismatchEntry, the warning fields, theshadowMismatchLoggingevent and its exporters,config_unknown_field. - Rust:
ShadowPolicy.mismatch_logging,Operation::mismatch_diff, the warning fields, the event and exporters,config_unknown_field.ShadowPolicygains a public field, so struct literals that list every field stop compiling; the Rustdocs/upgrading.mdentry names it. The pull request carries no!and no breaking-change footer, by the maintainer's choice. - Python:
shadow={"mismatch_logging": ...},shadow_mismatch_diff=, the warning fields, the event,config_unknown_field.
With the last port (Plan step 4, in #242)
- The hand-authored
mismatchPathVectorsgroup informal/catalogs/protocol-vectors.json, mapped insemantic-cases.jsonasprotocol/mismatchPathVectors/*, replayed by every port, and the newCONTRACTS.mdrow. The TypeScript cases intypescript/test/shadow-log-json.test.tsare written as(cached, source) -> { entries, count }pairs so they can move there unchanged. - The observation record:
mismatchWarninggains optionalmismatchPathsJson,mismatchPathCount,diffJsonandloggingOutcome, and ashadowMismatchLoggingevent kind joinsformal/guides/PORTING.mdandformal/replay/protocol.schema.json. Every port compares warning events exactly against the shared scenarios, so until every port emits these fields the TypeScript driver records only the seven shared fields (sharedWarningFieldsintypescript/test/formal/behavior-driver.ts); remove that projection here. - Re-encode the
logPolicychoices informal/replay/features.mjsand the fixed scenarios inbehavioral-scenarios.jsonfor eachdifflevel and forvalue, so the corpus exercises both leaves and the shorthand's expansion. - Mutants for the built-in differ (the array-length rule, the root cases) and for the hook's fail-closed behavior, in
mutations.json(TypeScript and Go) andrust-mutations.json. The catalog requires each mutant to name a semantic case backed by a scheduled Quint check; the differ has no Quint model, so mapping its mutants to the vector group may need the catalog to accept vector-backed cases. - Full validation tier on the final head.
Activity
lan17 commentedon Oct 24, 2026
Agent: two caveats from the review of the TypeScript differ in #242, for whoever designs the
mismatchPathVectorsgroup:diffJsonside over 1 KiB becomes that port's clipped native-JSON text of the subvalue, so its member order and escaping follow each port's renderer (V8 puts integer-like keys first, Go'sjson.Marshalsorts map keys, Python keeps insertion order). C60 keeps exact truncation text as B03/X01, so vectors should assert only that such a side is a string ending in...[truncated], or avoid clipped sides, rather than pin TypeScript's text.[1.0]against[1]and out-of-range exponents yield no entries, whileserde_json::Valuedistinguishes1.0from1. Vectors should stay within integers of magnitude up to 2^53 and canonical number forms unless the record decides how ports compare numbers.feat(shadow): log mismatch paths and diffs in TypeScript confirmed-mi…
docs(shadow): document mismatch paths, the logging leaves and the out…
chore(formal): refresh ledgers for the shadow mismatch paths change
lan17 commentedon Oct 25, 2026
Agent: two model notes for Plan step 4, when the
logPolicychoices and fixed scenarios are re-encoded for eachdifflevel and forvalue. The maintainer chose (2026-10-24) not to model warning content or theshadowMismatchLoggingmetric in Quint; native tests in each port cover them.dialcache-shadow-conformance.qnt(setLogging, the init codes), so adding them is a model edit, not only a driver fixture change.logMismatches: truedefault under a runtime{ diff: "bogus" }), the invariantinvalidLoggingCannotBeCapturedfails as written, becausevaluestays on while a config error is recorded. It would need restating per leaf.Separately, the model records an invalid-logging config error before the capacity check that drops a job (
kernel/shadow.qnt), while TypeScript resolves logging only after that check. No current profile reaches it; it predates this work.feat(python): log mismatch paths and diffs in shadow warnings