Skip to content

2026 07 20 phases 0 8

Verification result

FAIL

This is the first recorded verification pass on the SACM library. Phases 0-8 had been marked verified across 28 matrix rows without any verifier having ever reviewed them.

The library is substantially better than its matrix claims are careful. 61 gtest cases and 92 CTest tests pass, no regressions, and attribute/association coverage against the normative inventory is genuinely complete. But two verified rows rest on evidence that does not demonstrate the requirement, and one reproducible silent-data-loss defect falsifies a verified claim outright.

Scope

  • Requirement IDs: all 33 matrix rows; detailed inspection of SACM23-LIB-001, LIB-003, CMD-001, CMD-004/005, XMI-001/002/003/004, RT-001/002, VAL-001, BASE-001, COMPAT-001, ART-001, CLI-001.
  • Library files inspected: libs/sacm/src/metadata/namespaces.cpp, include/sacm/metadata/namespaces.h, src/compare/semantic_compare.cpp, src/io/xmi_reader.cpp, src/io/xmi_writer.cpp, src/validation/validate.cpp, include/sacm/commands/operations.h, include/sacm/validation/codes.h, include/sacm/model/*.h.
  • CLI/tooling files inspected: libs/sacm/tools/sacm_cli.cpp, tools/sacm/check_conformance_matrix.py, tools/sacm/generate_metamodel_inventory.py, cmake/check_layer_gates.cmake, CMakeLists.txt, libs/sacm/CMakeLists.txt, .github/workflows/ci.yml.
  • Adapter files inspected: none exist — Phase 9 correctly not-started.
  • Tests run or reviewed: sacm_tests.exe (61/61 pass), ctest -R "^Sacm" (92/92 pass), check_conformance_matrix.py (5/5 checks OK). All 13 test files reviewed. Targeted CLI probes against the normative ptc/22-03-13 expectations.

Findings

Severity Requirement ID Finding Required fix
High SACM23-XMI-004 Strict save does not refuse all compatibility-only content. Vendor-extension attributes are silently discarded at import — no diagnostic, preserved_content stays empty, so strict save succeeds. Reproduced: acme:owner="alice" on an AssuranceCasePackage → sacm_cli validate prints VALID, exit 0; export emits the document without it. A vendor child element correctly warns SACM-XMI-003 and strict save refuses with SACM-XMI-006. Preserve unknown attributes (or flag the document compat-only) so strict save refuses. Add a negative test using a vendor attribute. Drop row to implemented.
High SACM23-XMI-004 Half the new test cannot fail. SACM23_XMI_004_StrictSaveOmitsLayoutAndRefusesCompatOnlyContent scans output of build_minimal_document(), built through an API with no layout/GSN concept at all (structurally guaranteed by LIB-003). No input can put layout/Goal/Canvas into that output, so the assertion is vacuous. The second half duplicates SACM23_COMPAT_001_VendorContentPreservedAndStrictSaveRefuses. The real XMI-004 risk (Assurance Forge layout reaching the writer) is untestable until Phase 9. Say so in the row and lower the status.
High SACM23-XMI-001 LangString identity is silently dropped. <name xmi:id="ls_name_1" lang="en" content="…"/> loses its id: the reader reads only lang/content/expression, the writer emits none, no diagnostic. LangString generalizes Element in the normative model, so this is standard SACM data, and the row explicitly names "IDs" as in scope. Give LangString an optional ElementId, or record an explicit, tested scope exclusion.
High SACM23-LIB-001 Neither ID-bearing test tests the library boundary. test_version.cpp asserts standard_version()=="2.3"; test_metamodel_coverage.cpp compares class-name sets. Neither touches Assurance Forge independence — that is demonstrated only by the configure-time gate. check_conformance_matrix.py check 1 therefore passes on a false positive, precisely the defect it was written to catch. Retrace both tests to their real requirements; cite only the gate for LIB-001.
Medium (no owning row) The metamodel coverage gate overstates what it proves. Its regex captures only column 1 of the inventory table, so it compares class-name sets and nothing else — attributes, association ends, multiplicities, containment roles are never checked. An ElementKind with zero reader/writer/model support passes. ART-001 cites this test as artifact-model evidence, which it does not supply. (The hand-maintained kAllKinds[] is a lesser risk than it looks: an omitted enumerator still fails the inventory→library direction.) Add a SACM23-META-001 row, rename the test to match, and state that the gate proves name-set parity only.
Medium SACM23-CLI-001 The new negative CLI test cannot distinguish its requirement. SacmCliValidateRejectsDuplicateIds uses WILL_FAIL TRUE, accepting any non-zero exit; sacm_cli validate <nonexistent> also exits 1. The test passes unchanged if the fixture is deleted. Assert the specific diagnostic. SacmCliRoundtripStrict is sound.
Medium SACM23-COMPAT-001 Legacy SACM versions import silently on the default path. is_accepted_sacm_namespace matches any URI containing /spec/SACM/ and any http://omg.sacm/ prefix; check_root_namespace warns only when a namespace is not accepted. The new fixture is SACM 2.2, and data/oasc-ja.xml declares .../spec/SACM/2.2/Argumentation — both load with zero namespace diagnostics under a 2.3 conformance claim. Emit an info/warning naming the detected dialect and version. Keep at implemented.
Medium SACM23-COMPAT-001 Row note claims "Tolerant load preserves unknown vendor content." True for child elements only; unknown attributes are dropped with no preservation and no diagnostic. Correct the note; extend preservation to attributes.
Medium SACM23-VAL-001 Diagnostics catalog does not match behavior. SACM-XMI-002 is documented as a tolerant-mode namespace warning, but a non-pinned-but-accepted URI emits nothing. SACM-XMI-003 is documented as "Unknown element" yet is also emitted at info for multi-language-name→TaggedValue normalization (169 occurrences on data/oasc-ja.xml) — a different condition sharing a code whose meaning the header says must not change. Reconcile catalog and codes.h; give name-normalization its own code.
Medium SACM23-RT-001 Round-trip is not a losslessness proof. semantic_compare reads the library model, so anything dropped at import is absent from both sides and invisible. There is no input-vs-model or byte-level check anywhere in the suite; both High defects above are invisible to every round-trip test. Add an "unconsumed input" assertion for the strict fixtures. Row may stay verified; the note must stop implying losslessness.
Low SACM23-CMD-001 The new test checks operation names for GSN vocabulary and structured results for one create only. Adequate only in combination with the LIB-003 header scan. Record the dependency in the row.
Low SACM23-LIB-003 The scan is a keyword blocklist. Layout could enter under neutral names (Point, Rect, Bounds, x/y) without tripping it. Sufficient for the library-only slice. Revisit at Phase 9.

What held up under scrutiny

  • The namespace-acceptance change is correct and does not weaken strict mode. Verified directly against ptc/22-03-13.xml: zero occurrences of URI=, nsURI, or omg.sacm. The pin genuinely is a project choice. Strict mode uses a separate exact-match predicate and the test asserts strict load rejects the dialect. The only gap is the missing diagnostic, above.
  • No standard SACM element is parked in an untyped blob — measured, not assumed: all six repo fixtures produce zero "unknown element preserved" diagnostics. Attribute and association coverage against the inventory is complete in both directions.
  • Delete preview/apply (CMD-004/005, PKG-003, ARG-003) is the strongest area — reject-by-default policies, explicit opt-in cascades, preview revision expiry, post-delete validation clean, positive and negative cases throughout.
  • Checks 10 and 11 (source-of-truth integrity, adapter layout boundary) are genuinely out of scope and correctly recorded.
  • Check 12: no regressions. 92/92 CTest, 61/61 gtest.

Matrix updates allowed

May keep verified: LIB-003, CMD-001…CMD-006, XMI-002, XMI-003, RT-001, RT-002, VAL-001, VAL-002, BASE-001, BASE-002, PKG-001, PKG-002, PKG-003, TERM-001, ARG-001, ARG-002, ARG-003, ART-001, SEC-001, CLI-001.

LIB-001 may keep verified — the configure-time gate is real, CI-enforced, and a FATAL_ERROR — but its Tests cell must stop citing two tests that do not test it.

Must remain open:

  • SACM23-XMI-001 → implemented until LangString identity is preserved or explicitly scoped out with a test.
  • SACM23-XMI-004 → implemented. Its test is half-vacuous and its core claim is falsified by the vendor-attribute probe.
  • SACM23-COMPAT-001 stays implemented; COMPAT-002 stays not-started; LIB-002 / INT-001 / INT-002 unchanged.

Net: 25 of 28 rows can honestly keep verified.

Follow-up slice suggestions

  1. Unknown-attribute preservation — symmetric with the existing element path. Closes the XMI-004 defect and the COMPAT-001 note overstatement together.
  2. LangString identity — optional ElementId on LangString; unblocks XMI-001.
  3. Losslessness gate — an "unconsumed input" check failing when a source attribute or element is neither mapped nor preserved. This is the missing mechanism behind check 8; nothing in the suite would catch either High defect.
  4. Dialect/version diagnostic — report detected namespace family and SACM version on tolerant load. Prerequisite for COMPAT-001 reaching verified.
  5. Matrix checker hardening — the gate cannot tell whether a test tests its requirement. Consider requiring rows to cite file:TestName pairs.
  6. SACM23-META-001 — give the metamodel coverage gate its own row with an honest scope statement, then extend it beyond class names.