From 1a6421e57d7542823a1933ae7cc874d230f78718 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?G=C3=A1bor=20Z=20Sink=C3=B3?= Date: Sun, 9 Aug 2026 19:38:13 +0200 Subject: [PATCH] feat: a gate that asks whether the documentation tells the truth about the tree (audit claim F-06/F-07) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Nothing asked that until an external audit did, and what it found was worse than stale numbers. SPEC.md — the declared authority — said "normative, one implementation" and "executed by one implementation". conformance/README.md said "No implementation exists in this repository yet. Nothing here has passed — it has been authored." Both were in the same commit as a second implementation that runs the whole corpus and produces byte-identical output. docs/spec-vector-map.md said Rust "does not exist yet" and that agreement between implementations was "still an untested claim". The Makefile said mk/rust.mk is NOT present, four lines below including it. Counts: README said 44 invariants against 46, docs/en/architecture.md said 34 invariants and 27 vectors against 46 and 37. None of that was carelessness in the ordinary sense. Every one of those sentences was TRUE WHEN WRITTEN, and nothing connected it to what it described. A count copied into prose is a claim with no owner: it does not fail when it stops being true, it just stops being true. So the gate measures the tree — invariants from the §12 register, vectors from the corpus, implementations from "has sources AND has a conformance runner", because a directory with a .gitkeep is not an implementation — and compares it to what documents say. Two kinds of check, because there are two ways a status claim goes wrong: numbers, which are derived and compared; and situations ("one implementation", "never executed"), which cannot be derived, so they are listed and refused when the measurement contradicts them. Verified it can fail: 46 -> 44 in README fails, "two implementations" -> "one implementation" in SPEC fails, and adding one vector directory fails two claims at once. TWO LIMITS, both stated in the tool's own output rather than left to be discovered. It checks the claims listed in it and nothing else. Prose in a file it does not know about drifts silently, exactly as all of the above did. The lists are explicit rather than clever for that reason: every entry is a claim someone decided was worth binding. And the phrases are deliberately long. "one implementation" also matched "without the corpus and the other implementation noticing" and a sentence about why 0.1's bootstrap rule deadlocked — both correct prose. A check that fires on legitimate text gets switched off, and then it checks nothing. docs/hu/architecture.md is registered for no count at all, because it states none. A document that makes no numeric claim has nothing to go stale, which is the cheapest fix available for this whole class. make ci passes; status-claims runs in ci.gates. --- [signing-metadata] key = cic-my-sign-key signature = vault:v1:MEQCICAbj/Ry1VJTnSIc+dyuPkRLKafhlNMxN1Y6TuCPNtaUAiAwGVRlCMZvqwOI1CUWUmnIh1P9JlrzJ2jT1NStFGg8Hg== hash-algorithm = sha256 digest = 5WQMRx0jTrHcZdQITxbMYn0YX8TRJ/fNPHkTo8RVsvU= [certificate] -----BEGIN CERTIFICATE----- MIICBjCCAaygAwIBAgIUSnRMR6RPnEbg296XWPOqq/u5PCwwCgYIKoZIzj0EAwIw QzELMAkGA1UEBhMCSFUxGTAXBgNVBAoMEENlbnRyYWxJbmZyYUNvcmUxGTAXBgNV BAMMEENJQyBEZXZlbG9wZXIgQ0EwHhcNMjYwMzIwMTMyMjU5WhcNMjYxMjMxMTMy MjU5WjBFMQswCQYDVQQGEwJIVTEZMBcGA1UECgwQQ2VudHJhbEluZnJhQ29yZTEb MBkGA1UEAwwSR2Fib3IgWm9sdGFuIFNpbmtvMFkwEwYHKoZIzj0CAQYIKoZIzj0D AQcDQgAEIG2CVmTfmLB9pLLclj7YmP2eedAjklpy4LGrU2ijoiy6Xqpuybv7OgJe i+ez31s65NEV8+X/ByeX1cstR988z6N8MHowCQYDVR0TBAIwADAdBgNVHQ4EFgQU yZN6AIX/TNnIJ9GwAa/NRN3ujHAwHwYDVR0jBBgwFoAUXn6CHYzPUqU4JVP8g+OS WeDYjhcwDgYDVR0PAQH/BAQDAgeAMB0GA1UdJQQWMBQGCCsGAQUFBwMCBggrBgEF BQcDBDAKBggqhkjOPQQDAgNIADBFAiEA+bFzXRoJ4PCQbhAAtpkcMjt0vNj5rEW0 lOMBGDNyaWkCIB1vmM7PcZzv/c9bIrxF5kqv6QXomouhByUfeNUTbpKW -----END CERTIFICATE----- --- MANIFEST.sha256 | 15 +-- Makefile | 13 ++- SPEC.md | 22 +++-- conformance/README.md | 11 ++- docs/en/architecture.md | 2 +- docs/spec-vector-map.md | 12 ++- mk/ci.mk | 2 +- project.yaml | 2 +- tools/check_status_claims.py | 182 +++++++++++++++++++++++++++++++++++ 9 files changed, 229 insertions(+), 32 deletions(-) create mode 100644 tools/check_status_claims.py diff --git a/MANIFEST.sha256 b/MANIFEST.sha256 index ac54600..a5ce1ec 100644 --- a/MANIFEST.sha256 +++ b/MANIFEST.sha256 @@ -15,7 +15,6 @@ 090194d2cbde04322fd68bed8ce5427b4b0ad5daba1b26017958fed8ef29c964 tools/release_subject.py 0ac298f7c02da6032de189c7931958e6184aa4458e548339e5d4072ce5964717 conformance/validation/004_documentation_member/object.yaml 0ad89412a6fdc0a474993c5a43fc97f6fe74f79e517bdba509301eade72b71ca go/module/version_test.go -0adb6f74bbdb0ed9385dcfe0e27141492c31124bbc02635fae519812bc40e4e5 mk/ci.mk 0bf03d8b25e93057ce99d461372fcb12646f120930ad89cc3ba1f566481bf97e tools/releaselib/__init__.yaml 0c5a65427e75e4640244ec745687f8bae43f1390b4bc7aea6f386365c36d81da conformance/materialization/006_closure_opaque/input.yaml 0cb99237aa09d07543161fdf5a36fdb2d157b873dacdde45f1a5d53991d70823 conformance/invalid/005_origin_in_authoring_input/expected-error.yaml @@ -37,6 +36,7 @@ 168cd37e606cb1646305d512096290e6aeeb612997a8d0200280f821025dc79d go/objectmodel/errors.go 16a0a5ade85c937b51c4a7e5131eb8b0b9b03e4bfb19dd3d0654c9c7b6f44aa0 conformance/materialization/007_normalize_scalar/meta.yaml 171735e8e595777d10212f048329f6d0ca0885b79df841d55ce34adc2466a26c conformance/materialization/010_normalize_empty_object/input.yaml +1774b9631c1cf1b7abdb9a651277bb03dc71454524376a482f63d86def993bb1 Makefile 1b3e25bf2122e2d44a8cfc13620797fd129911c5c74d8e1c1db96cee6994f1ce docs/hu/concept/git-management.meta.yaml 1cbf2e8be1e4909a51180757ab9362abe0b8212025a4ea63d60d1f9a4c15ca6a tests/test_tools/test_compiler.yaml 1d446b9b82e3a4e641645bb34a371dd42063f8732044d88108dd1715e9238a83 conformance/validation/008_origin_terms_out_of_order/meta.yaml @@ -46,9 +46,7 @@ 1fb7dd2afe2b230d7c335db5c5da4e72e0ad271ce2dcd1683f446945e0abb917 conformance/materialization/011_discriminator_envelope/input.yaml 2020cd3da7008987b81055f0ef1bc7481567202da7f8bf49d616b1018f52bc21 mk/infra.mk 2063bf8ac333858a9b5c96de552fc4879ca3c35e5d0e34b0dd4067cec94bb5da Dockerfile -209727f045265edc8fb4149c4edafefdb18779e7dbc4d1377437bf3e35efb1b8 docs/en/architecture.md 20b03084c87f86f2ed3c27cb48ca6d9bc8d55fb53e45ee350687079074520615 docs/hu/workflow.md -210404104fc83339d47136c6f8b5bb564531d0ac5ac12c6a13e030e4ed284274 conformance/README.md 21a2f539315cb8500c9d812776d0e777b2eca73d668b3079b694b651fe8539d8 conformance/materialization/012_discriminator_payload_keywords/input.yaml 21a9994fa283ffca9aa0d063526ba4bc8b7d53d781bfbbee0d0041dcc04d143a conformance/invalid/005_origin_in_authoring_input/schema.yaml 21a9994fa283ffca9aa0d063526ba4bc8b7d53d781bfbbee0d0041dcc04d143a conformance/invalid/006_unknown_primitive/schema.yaml @@ -65,12 +63,14 @@ 2b5c7c2028ce8d8fa9ec385fed586a85d22f30903373b511111011c6e6a34044 go/objectmodel/emit.go 2be51eae75514d81524b44089859b25fa7282a962475cf9bf196b87ebb96cbd9 rust/src/materialize.rs 2bf4423a50b568d1aa9bf938a233f9584e2c6ef19f5dd3ebf458c9a1dd093a30 go/objectmodel/schema.yaml +2cafa2e6c89efdc947b2dc5206041dd3640892c6cdcb8a92f9852eff5f8e9413 docs/spec-vector-map.md 2d28d83b74f3b137a2e2d02d21178ad751b9b59ea81133ec42c9704ca535c986 tools/init_from_template.sh 2d66d76a7399d07f6dc504d64a22e81dfcaa49f6bcee9ab4362c15dcb82b2475 conformance/validation/006_model_version_inside_object/expected-error.yaml 2d763d2e7243d988b6f107432e14f4ac45d10a642ea72abd150ed30d8c3261c2 tools/check_spec_vectors.py 2e19ebdd9db8f56f6dc5fb006f8bb23037595794d0c288e72901b9f628d2d5b5 tools/git_hook_commit-msg.sh 2e83c8f6100c847450f90a1f593db97b7ad2e7cc7798bb762823b61ebcdeff57 go/objectmodel/refs.go 2e85d74791ed8db0bee2e473f3d5906c351c1c962901e12dc4278198a44d07a3 docs/hu/concept/declarative_ecosystem_integration.meta.yaml +2f7e223bf0e58d18a8705d175d0c0845df050c4429e72f22f54eb84e11f4022d docs/en/architecture.md 3057e97eafa5993ad6761b7c1b25076432fc5b1998dc7c4d569926bc37a974b2 tests/test_compiler.yaml 306916d0bc25ffb21038fa8ac7421dddec5dfae2483f3a802d5d0970194ebfbb conformance/materialization/001_origin_yaml/expected.yaml 308a0bc08020a9fe5fc59e2310af16c0aebafcfb3fa9c1b4ac8e585da1967274 conformance/materialization/010_normalize_empty_object/meta.yaml @@ -141,6 +141,7 @@ 66e962cd93fcc33b1dd43760f78d7de6b7e718923536d814d36ff0da8ce10223 conformance/validation/010_primitive_member_is_not_a_node/meta.yaml 688dffd2264877f3a64fca1d3526c57bb34cb1c18f5a01aa906667311831a052 docs/en/workflow.md 68a4754be7f4971ea34eb5277b054692d6582edece24fa50b279682c69380d2f conformance/materialization/003_origin_sealed/meta.yaml +6903a0680e552da4f08e3525e1ff4420458d5829e9b447a98462c5c358910c8e project.yaml 6a9d33a921b501cfea3f229df86d6f26e6cbbfddfd9dde90d66451d1c25ae5f3 conformance/validation/010_primitive_member_is_not_a_node/object.yaml 6b78afd099dcc9b830c51b1da97ab491374167491f3f3b5c0c34129511f73750 go/conformance/conformance_test.go 6d9c5cce2c2ce964f0add1b4aeb97a9bce828ad46dd76b22929e284741273fc4 schemas/index.yaml @@ -189,7 +190,6 @@ 87a06a94138975d7bcee23fd7e8b645f5aadfe728895c71da27d7b25ac2d2b0a go/inv032/testdata/forge/forge.go 8830ee9944b243af220aee813a4348c5435bf3abccdb57c0b9c9ad15ea6dadd1 conformance/invalid/002_sealed_yaml_schema_conflict/expected-error.yaml 885e419c23b97b7558a4f599267ef904a9f059ed3c455d3a95eda787ea7ab117 tools/releaselib/git_service.py -8977c2633b432826d05b367ca50cdaa930994c64b0ad5097a7494f9145ebfead project.yaml 89f1fa5d8a2bcfab9015b51dfe0f60013d92f59595323e74d2cecd24e69962a2 go/objectmodel/branches_test.go 8a3dece67f758da0301a3ea1c5c34e8e7f33a17f41ea518fa016d6d2d386ce52 conformance/invalid/009_yaml_alias/meta.yaml 8ac2a6cb77025dfe7eaf732e15887a28e0563a81a444d465a535372ca115cd6e conformance/invalid/007_sealed_missing_path/input.yaml @@ -222,15 +222,14 @@ 9f61f29a58d467eb8eb1c40fedb3b5e46342b19eed91fd4fd7233d7da83f510d conformance/invalid/005_origin_in_authoring_input/meta.yaml a03b3fccfc1f8eb7f76833fdff8a50ea84c80c039db87bc0e41109e96f64420b docs/en/concept/declarative_ecosystem_integration.md a07ec1b9e98e4813201ab7e9ea8e5f873758e3710ffd5aba692c1f1914cae4b8 conformance/invalid/006_unknown_primitive/input.yaml +a155c1bda117102e5a48969f23835620d528818b057cd98792345a04c5ceb359 conformance/README.md a22ba9af1d65c75475635df964c7c0568417e1d0cd218c46321de4c4dc375041 tools/finalize_release.yaml a3f497092a2fe0fc41467edefff241687affff6f01adbbbf0dadbdefd791bd21 tools/compiler.py a41c7c65df2a47cffb061e4290f333ef26847c8d9d698ac568f8dd67cd3d59da conformance/materialization/013_access_inherit_injection/schema.yaml a49ab35d001c64ab06a9368860224e2c15108c96840f632ff23b6e8b5e262cd8 rust/tests/foundation.rs a6c2baaaf307c0718ecaa43f654742269c3830fd9ff899a000af5e56713e5082 tools/__init__.py -a75656e875924b9ff55f174ecd14e25757736dfe9437df5922a3af2cf1b67e15 Makefile a77d0ec51190a8c5d1b9bcb57482773a68148313de6e4456288d3ac2cdf041d3 conformance/materialization/011_discriminator_envelope/expected.yaml a8ecf9c2551505fd5a4c477c735c88fff9c4627136dade955cdcbfc16d8ca131 docs/en/makefile-cheatsheet.md -a9d0c923d123ed800fb04e2d64443955823b7754219d3d9f08d1bb4051a7a6b8 SPEC.md a9f3d2ed8ade23e7a13e22961e535d83b104b0a91c7ae0b5867d0472ecb8860a rust/src/node.rs aa34e410797cbb287c42042a1724b377896616f7c2d4c3e023fe6d4ae2b762e4 go/objectmodel/defaults.yaml aa44b2b55d2ced16b5fc9072a97f2a0c0c30a34afd4055b8ef95591e77e02bfd reviews/82c05a168c5a20666d1dd5c898e2200ce072f9c47adead5207ebf5cb984d0870.md @@ -250,6 +249,7 @@ b75db4a2182e6ebd8b246deedb6af40900dbc24520eaaec02c4738e9dc98d47a reviews/cbaf92 b78df50dc6d7807172273a4ded207fc85511901446f95b472e4ab26c389b4be7 conformance/validation/002_origin_empty/meta.yaml b7c2102b45f5be699a817f2b0e5010d03dddfb67bb74a471994dcb0c70d1e167 spec/origin.schema.yaml b7cc2d3d36c6fef33a7eaa1d13b35465ab293f7c22b6edeb1a86dd2ca834bc87 go/objectmodel/fuzz_test.go +b92e00b843b3423caab27477ac02305bdd077a1c454a5f0dd142e0a90e8188a4 mk/ci.mk b9325f58a95216b240f3715a773e34fe8cdfa4d5fe48a5e7b32002a40be5cc2e tests/test_tools/test_finalize_release.py b9d89d1f2d541eb9d523bc3f9b3939a0bdebabd5558038b86cb3ec19a8370af0 rust/tests/conformance.rs ba6a2c483d594433ee00f2cc64eec463a68ef2e47babdef5103dff597e3e1773 go/objectmodel/origin.go @@ -288,6 +288,7 @@ d75063538a29c37caad5e4f1ba680c81bc4827ee935e78281ab168b72d5e53a2 tools/check_do d807555962a3e6a0fb6d885537d89e3e93c864e0452511fa4aa8b1c3a6231ff9 conformance/invalid/009_yaml_alias/input.yaml d84bf2b93671212d5ef27baed6eff3a8c7c5431273967d1be762b7141696eccc conformance/validation/005_default_member/expected-error.yaml d90f607cbe23c9f809c121670f33e6d023db0a65f8ce9d7bbf33e2d35655727c go/go.mod +db8324d0f397a43b44fb910586ad1f767ff5056709609a120d4b635b25f2ca67 tools/check_status_claims.py dc1bbc3a438b44ae3cc67725dfa916811d24670d4649211987f973aed48b378a go/objectmodel/doc.go df1a1d134a0917f492882af78775b072430c47dd43008625140ad35e206457e9 tests/test_tools/test_releaselib/test_vault_service.py e0841977943dbbd886d89bdd7b3fdf9a91405608d2a2060453669919c4679d31 go/objectmodel/primitives.go @@ -309,7 +310,6 @@ e63367c6f011417eadf3f26e51dd648f6d85a7086d9db161d616b294e14b6995 tests/test_too e6c3bf74dfd983f1e70a662799cc9e6b99f28b18c7bc330c794f14919589f753 go/cmd/cic-materialize/main.yaml e6e946e141cd9d873d5f1012c9526956e7e22e55345e237aa52863dedcf7a2cd conformance/materialization/005_closure_structured/meta.yaml e7380ef0b0be1345db4c2857c6ba4b1aa8899b8eac78dec32d6ab7e51bdb3bee tests/test_tools/test_releaselib/test_exceptions.py -ea30addfde9489dd8195089b68a3b54633a1d9f3ce97d496da18855a59bcbafc docs/spec-vector-map.md ea3d9182bb0cd8f7601d2e80952adfdc91a0dc91c62ef4c8c53929f2d10641fd tools/releaselib/exceptions.py eb29d58fce2f9a987024ff05ae9dd6d3a8a421c3a0595c05eff3c9997fccfdf6 tools/schemalib/loader.yaml eb8d2d51fed8fb9fa1ad4081c02515942ffb42d830c643e8c8dffae765bee510 tools/schemalib/artifact.py @@ -330,6 +330,7 @@ f8d5eb9a78aad0da576ad083f7345da57620f3ca0c08d317727e353b44e4da49 go/objectmodel fa3d02b5fc0677eb715d676e88b98b94016a76eb13e47abfa1040d0e6f12719f docs/rust-gate-extraction.md fa8afcf490e0b9b1e3ce94789f3233ed73289553ec94f16d2c347afd5e08b367 conformance/invalid/002_sealed_yaml_schema_conflict/input.yaml fd4ba258680da20f4084db2696fa942c09e47de8ec4650104f2b2e18c53980bc go/module/adversarial_test.go +fdd8b8d94d94d9c08aafdc2b0e6f85db5deba627541786a8d72ef99c3eb37049 SPEC.md ff005c27b6c185b065c2121b01fa6f71c9668af920483714c9b137e411cec32c go/objectmodel/emit_test.go ff5d544dc1e253e76844a7c325f7f73d952ac29b284092f0ed2e80b8de3ae0a2 go/objectmodel/materialize.go ffa488df0e6ea07872d7c2b8a7ed0b692e4a998711991e4471cfc134fcbaf0b6 go/objectmodel/api_test.go diff --git a/Makefile b/Makefile index a65401a..b2d574d 100644 --- a/Makefile +++ b/Makefile @@ -1,10 +1,9 @@ # Makefile for cic-object-model — the normative CIC object model spec, # its conformance vectors, and the Go + Rust reference implementations. # -# mk/rust.mk is NOT present yet: the Rust gate is extracted from -# CIC-Relay/Makefile by the cic-object-model-rust sub-job. See -# docs/rust-gate-extraction.md for the line-referenced recipe. Until that -# job lands, `make rust` is unavailable and CI runs the Go gate only. +# mk/rust.mk is present: the Rust gate was extracted from CIC-Relay/Makefile +# per docs/rust-gate-extraction.md. `make rust` runs it, and mk/ci.mk runs both +# implementations' gates. # ---- Includes ---- include mk/infra.mk @@ -13,7 +12,7 @@ include mk/ci.mk -include mk/rust.mk # ---- Phony ---- -.PHONY: verify verify.fuzz verify.mutate release.subject release.verify review.check all help validate release test up down shell build fmt lint check typecheck repo.init manifest-verify manifest-update docs.link-check conformance +.PHONY: verify verify.fuzz verify.mutate release.subject release.verify review.check status-claims all help validate release test up down shell build fmt lint check typecheck repo.init manifest-verify manifest-update docs.link-check conformance # Default to showing help all: help @@ -168,6 +167,10 @@ manifest-update: ##manifest-update # Documentation # ============================================================================= +status-claims: ## Verify the documentation's counts and status match the tree + @echo "--- Status claims ---" + @docker compose exec -T builder python tools/check_status_claims.py + docs.link-check: ## Verify internal markdown links in docs/ and READMEs resolve @echo "--- Checking internal documentation links ---" @docker compose exec -T builder python tools/check_doc_links.py diff --git a/SPEC.md b/SPEC.md index da34857..5f94bc3 100644 --- a/SPEC.md +++ b/SPEC.md @@ -1,10 +1,12 @@ # CIC Object Model — Normative Specification **Model version: 0.2** -**Status: normative, one implementation.** The Go reference implementation in -`go/` executes the conformance corpus. 0.2 is the revision that follows from -running it: eighteen defects were found by implementing 0.1, and the ones that -made 0.1 unsatisfiable are fixed here. See `docs/spec-defects.md` for the full +**Status: normative, two implementations.** The reference implementations in +`go/` and `rust/` both execute the conformance corpus and produce byte-identical +canonical objects. 0.2 is the revision that follows from running it: eighteen +defects were found by implementing 0.1, and the ones that made 0.1 +unsatisfiable are fixed here. The second implementation, and two external +reviews, found the rest. See `docs/spec-defects.md` for the full list and [Conformance](#10-conformance) for what corpus status means for the reader. @@ -1021,12 +1023,12 @@ if an invariant claims a vector that does not exist or a vector claims an invariant that does not exist. The check verifies the *mapping*, not conformance results. -**Status of the corpus as of model 0.2: executed by one implementation.** The Go -reference implementation runs every vector; the Rust implementation does not -exist yet. `make conformance` fails rather than passing vacuously when no -implementation is present. A vector that has never run is a hypothesis, not -evidence — and until a second implementation runs this corpus, agreement between -implementations is still an untested claim. +**Status of the corpus as of model 0.2: executed by both implementations.** +`go/` and `rust/` each run the whole corpus and produce byte-identical +canonical objects. What that establishes is that they agree on THESE +vectors — a bound worth stating, because for thirty-one of them the corpus +contained no wrong-typed input at all, and the two disagreed on every such +case an external review constructed. --- diff --git a/conformance/README.md b/conformance/README.md index bedbbc2..a3c3834 100644 --- a/conformance/README.md +++ b/conformance/README.md @@ -4,11 +4,16 @@ These vectors are the falsifiable part of [`SPEC.md`](../SPEC.md). A normative sentence with no vector behind it is an assertion; a vector is a test that can fail. -**Status: written, never executed.** No implementation exists in this -repository yet. Nothing here has passed — it has been authored. See -[`../docs/spec-vector-map.md`](../docs/spec-vector-map.md) for the full +**Status: executed by both implementations.** `go/` and `rust/` each run the +whole corpus, compare their output to `expected.yaml` byte for byte, and agree. +See [`../docs/spec-vector-map.md`](../docs/spec-vector-map.md) for the full invariant coverage picture. +What that establishes is bounded, and the bound is the interesting part: it says +the two agree on these vectors. It said nothing about wrong-typed input until +the corpus acquired some, because for thirty-one vectors it had none — and the +two implementations disagreed on every such case an external review tried. + ## Format Vectors are implementation-independent: YAML in, YAML out. Go, Rust, and any diff --git a/docs/en/architecture.md b/docs/en/architecture.md index 102b6f5..ed6acf0 100644 --- a/docs/en/architecture.md +++ b/docs/en/architecture.md @@ -8,7 +8,7 @@ model, and everything else here exists to keep that document honest. ```mermaid graph TD - S[SPEC.md — 34 numbered invariants] --> V[conformance/ — 27 vectors] + S[SPEC.md — 46 numbered invariants] --> V[conformance/ — 37 vectors] S --> M[docs/spec-vector-map.md] V --> G[go/ — reference implementation] V --> R[rust/ — reference implementation] diff --git a/docs/spec-vector-map.md b/docs/spec-vector-map.md index 51fc3e5..46f3d5a 100644 --- a/docs/spec-vector-map.md +++ b/docs/spec-vector-map.md @@ -7,10 +7,14 @@ covered nor explicitly excused is a gap, and [`../tools/check_spec_vectors.py`](../tools/check_spec_vectors.py) fails the build when one appears. -**This map records coverage, not results.** As of model 0.2 the Go reference -implementation executes the corpus; the Rust implementation does not exist yet. -A vector that has run in one implementation is evidence about that -implementation. Agreement *between* implementations is still an untested claim. +**This map records coverage, not results.** Both implementations execute the +corpus and agree byte for byte on every vector in it. + +A vector that has run is evidence about the vector. It is not evidence about an +invariant beyond what the vector states, and this map's own history is the +argument: INV-013 says "exactly four forms" and was covered by four vectors, one +per form, every one of them positive — so "these four are accepted" was tested +for months and "nothing else is" never was. ## Coverage diff --git a/mk/ci.mk b/mk/ci.mk index 0269c76..05640e6 100644 --- a/mk/ci.mk +++ b/mk/ci.mk @@ -62,7 +62,7 @@ ci.deps-drift: # ci.gates is everything that holds for this repository whether or not an # implementation exists: integrity, links, code quality, security. -ci.gates: manifest-verify release.verify docs.link-check check ci.security +ci.gates: manifest-verify release.verify status-claims docs.link-check check ci.security # ci.security runs the scanners as their own step rather than hiding inside # `check`. A security finding should be legible as a security finding. diff --git a/project.yaml b/project.yaml index 502058a..e568d84 100644 --- a/project.yaml +++ b/project.yaml @@ -49,7 +49,7 @@ metadata: # # Recompute with `make release.subject`; check with `make release.verify`, # which a third party can run with a clone and a Python and nothing else. - buildHash: 'aa61464bc58ba879adbc4ac276d29ab77884d67297a9d7b729fd151692ebd66d' + buildHash: '388ad2dc8f87f2d6951d2e8fffa0f2ccb843a46c2b07f6dafd11d0c98db124fb' cicSign: 'TBD' cicSignedCA: certificate: "TBD — filled by the release process with the CIC Root CA certificate" diff --git a/tools/check_status_claims.py b/tools/check_status_claims.py new file mode 100644 index 0000000..d1ccef3 --- /dev/null +++ b/tools/check_status_claims.py @@ -0,0 +1,182 @@ +#!/usr/bin/env python3 +"""Does the documentation tell the truth about the tree it ships with? + +Nothing asked that until an external audit did. It found `SPEC.md` — the +declared authority — saying "one implementation" and `conformance/README.md` +saying "No implementation exists in this repository yet. Nothing here has +passed", in the same commit as a second implementation that passes every vector. +It found three different vector counts in three documents and an invariant count +two short. + +None of that was carelessness in the ordinary sense. Every one of those +sentences was true when it was written, and nothing in the repository connected +it to the thing it described. A count copied into prose is a claim with no +owner: it does not fail when it stops being true, it just quietly stops being +true. + +So this gate measures the tree and compares it to what the documents say. Two +kinds of check, because there are two ways a status claim goes wrong: + + NUMBERS a document states a count; the count is measured and compared. + PHRASES a document states a situation — "one implementation", "never + executed" — which the measurement contradicts. These cannot be + derived, so they are listed and refused. + +What this does NOT do is check prose nobody registered here. A sentence that +drifts in a file this tool does not know about drifts silently, exactly as +before. That is a real limit and it is the reason the lists below are explicit +rather than clever: every entry is a claim someone decided was worth binding. +""" + +from __future__ import annotations + +import re +import sys +from pathlib import Path + + +def repo_root() -> Path: + return Path(__file__).resolve().parent.parent + + +# -------------------------------------------------------------------------- +# What is actually true of the tree +# -------------------------------------------------------------------------- + + +def measured(root: Path) -> dict[str, int]: + """Facts, each derived from the artifact rather than from a document.""" + spec = (root / "SPEC.md").read_text(encoding="utf-8") + + # The invariant index of §12 is the register; a token appearing in prose is + # a reference to an invariant, not a declaration of one. + index = spec.split("## 12.", 1)[-1] + invariants = len(set(re.findall(r"^\| (INV-\d+) \|", index, re.M))) + + vectors = len(list((root / "conformance").glob("*/*/meta.yaml"))) + + # An implementation counts when it has BOTH sources and a conformance + # runner. A directory with a .gitkeep is not an implementation, and one + # that cannot run the corpus is not evidence about the model. + implementations = 0 + for lang, runner in ( + ("go", "go/conformance"), + ("rust", "rust/tests/conformance.rs"), + ): + has_sources = any((root / lang).rglob("*.go")) or any( + (root / lang).rglob("*.rs") + ) + has_runner = (root / runner).exists() + if has_sources and has_runner: + implementations += 1 + + return { + "invariants": invariants, + "vectors": vectors, + "implementations": implementations, + } + + +# -------------------------------------------------------------------------- +# Numbers stated in documents +# -------------------------------------------------------------------------- + +# (path, regex with one capturing group, which measured fact it must equal) +NUMBER_CLAIMS: list[tuple[str, str, str]] = [ + ("README.md", r"— (\d+) numbered invariants", "invariants"), + ("README.md", r"— (\d+) vectors", "vectors"), + ("README.md", r"pass all (\d+) vectors", "vectors"), + ("docs/en/architecture.md", r"SPEC\.md — (\d+) numbered invariants", "invariants"), + ("docs/en/architecture.md", r"conformance/ — (\d+) vectors", "vectors"), + # docs/hu/architecture.md states no counts, deliberately: it describes the + # layers and points at the register. A document that does not make a + # numeric claim has nothing here to go stale, which is the cheapest fix + # available for this whole class. +] + +# -------------------------------------------------------------------------- +# Situations stated in documents that a measurement can contradict +# -------------------------------------------------------------------------- + +# (path, phrase, the condition under which the phrase is false) +# The phrases are deliberately long. A short one — "one implementation" — +# also matched "without the corpus and the other implementation noticing" and +# a sentence about why 0.1's bootstrap rule deadlocked, both of which are +# correct prose. A check that fires on legitimate text gets switched off, and +# then it checks nothing. +PHRASE_CLAIMS: list[tuple[str, str, str]] = [ + ("SPEC.md", "normative, one implementation", "implementations > 1"), + ("SPEC.md", "executed by one implementation", "implementations > 1"), + ("conformance/README.md", "never executed", "implementations > 0"), + ("conformance/README.md", "No implementation exists", "implementations > 0"), + ("docs/spec-vector-map.md", "does not exist yet", "implementations > 1"), + ("docs/spec-vector-map.md", "still an untested claim", "implementations > 1"), + ("Makefile", "mk/rust.mk is NOT present", "implementations > 1"), +] + + +def phrase_is_false(condition: str, facts: dict[str, int]) -> bool: + key, op, value = condition.split() + return facts[key] > int(value) if op == ">" else False + + +def main() -> int: + root = repo_root() + facts = measured(root) + failures: list[str] = [] + + print("measured from the tree:") + for name, value in facts.items(): + print(f" {name:16} {value}") + print() + + for path, pattern, fact in NUMBER_CLAIMS: + target = root / path + if not target.is_file(): + failures.append(f"{path}: registered for a claim but the file is missing") + continue + text = target.read_text(encoding="utf-8") + found = re.findall(pattern, text) + if not found: + failures.append( + f"{path}: no claim matched /{pattern}/ — the sentence moved or was " + f"reworded, so it is no longer checked" + ) + continue + for stated in found: + if int(stated) != facts[fact]: + failures.append( + f"{path}: says {stated} {fact}, the tree has {facts[fact]}" + ) + + for path, phrase, condition in PHRASE_CLAIMS: + target = root / path + if not target.is_file(): + continue + if phrase.lower() in target.read_text(encoding="utf-8").lower(): + if phrase_is_false(condition, facts): + failures.append( + f'{path}: says "{phrase}", which is false when {condition} ' + f"(it is {facts[condition.split()[0]]})" + ) + + if failures: + print("FAIL the documentation does not describe this tree:") + for f in failures: + print(f" {f}") + print() + print("A count copied into prose is a claim with no owner. Update the") + print( + "document, or register the claim differently in tools/check_status_claims.py." + ) + return 1 + + print(f"ok {len(NUMBER_CLAIMS)} counts and {len(PHRASE_CLAIMS)} status phrases") + print() + print("This checks the claims listed in this tool and nothing else. Prose in a") + print("file it does not know about drifts silently, as all of this did.") + return 0 + + +if __name__ == "__main__": + sys.exit(main())