diff --git a/MANIFEST.json b/MANIFEST.json index a3f5fbe..c651be0 100644 --- a/MANIFEST.json +++ b/MANIFEST.json @@ -188,13 +188,13 @@ }, { "path": "audit/ACTIVE_AUDIT_INDEX.json", - "sha256": "sha256:9990eedf03b0b6f95911df34d6cca15e966204abdc12918f62937f07e2be0a18", - "size_bytes": 2781 + "sha256": "sha256:bea24b466c100fd0152f17fb987543534855ca2b89e95af1d25c89ffed3e1773", + "size_bytes": 2887 }, { "path": "audit/ACTIVE_AUDIT_INDEX.md", - "sha256": "sha256:0199cd878c49cba04ea5e49c871d1c4801b7336ea8b7965af731a5bbd44be647", - "size_bytes": 1248 + "sha256": "sha256:e39f20ad45eb4b1d2bc7c7a0b3a95917589d666da9cf405e58af0ae83a7dca24", + "size_bytes": 1363 }, { "path": "audit/FINDING_CLOSURE_MATRIX.json", @@ -226,6 +226,16 @@ "sha256": "sha256:e8b83960c74d002991e2a8f5ae55570a8eee83a0f2115a97e0ed98646973c269", "size_bytes": 903 }, + { + "path": "audit/PDCA-18-SEED-FINAL-SEMANTIC-CLEANUP.json", + "sha256": "sha256:a324d126b6ae9860de5c2a7d89fb55faaace17c4e1d823bbbe47efb45ef14eb0", + "size_bytes": 2140 + }, + { + "path": "audit/PDCA-18-SEED-FINAL-SEMANTIC-CLEANUP.md", + "sha256": "sha256:9d2320b93110c3b8dbd61c956cde68e5b5f45534ad7d28d4363f6fc03fb1fb27", + "size_bytes": 1346 + }, { "path": "audit/PDCA_HISTORY.md", "sha256": "sha256:25ab54577ab863b1d31fcfd34d8c38052381d2822352f2dc35dcbd065679e1c4", @@ -248,8 +258,8 @@ }, { "path": "audit/REFACTORING_LOG.md", - "sha256": "sha256:1957c107f0fc9c71de5bdbd37b96c071742c854e52529ee1bce91b39a920f778", - "size_bytes": 2371 + "sha256": "sha256:80297d41a3e043b14f0bcbcb85cccab17ac1cc6b1347c35fd0a6060450d737f1", + "size_bytes": 3063 }, { "path": "audit/pdca/PDCA-05-RC12-CANON.md", @@ -313,13 +323,13 @@ }, { "path": "docs/architecture/SEED_ROLE.md", - "sha256": "sha256:d5f3f88f91959131304988f264932f1373c7527cda2cbf16c259d3877acd7989", - "size_bytes": 1615 + "sha256": "sha256:a3496eb393c5bc24e8145777f8eab19c2c127067d9425370c5337c1ba5413c34", + "size_bytes": 1742 }, { "path": "docs/architecture/SEED_STATE_MINIMIZATION.md", - "sha256": "sha256:73c0f19ed820dc44e34624f6e4f1829972437ba90a8fc439f563ca7d23e75058", - "size_bytes": 1570 + "sha256": "sha256:2608e9c1e5ef2925983d9735d9c41818fae1b50535cb046b06ee81a067704f24", + "size_bytes": 1674 }, { "path": "docs/architecture/TERMINAL_COMMITMENT_ACCUMULATION.md", @@ -338,13 +348,13 @@ }, { "path": "docs/generated/en/ASET_Seed_Next.md", - "sha256": "sha256:b348604389008b45d1eebcbf93214040c5b18d63614fa62b12f77231d13ee8b2", - "size_bytes": 11273 + "sha256": "sha256:cc8db0a091b1b7065ea50583e2190b0325b59efdc6dfe2e47e1ae64df5e6c656", + "size_bytes": 11789 }, { "path": "docs/generated/en/ASET_Seed_Resolution_0.3-alpha.1.md", - "sha256": "sha256:b348604389008b45d1eebcbf93214040c5b18d63614fa62b12f77231d13ee8b2", - "size_bytes": 11273 + "sha256": "sha256:cc8db0a091b1b7065ea50583e2190b0325b59efdc6dfe2e47e1ae64df5e6c656", + "size_bytes": 11789 }, { "path": "docs/generated/pt-BR/ASET_Seed_0.1-rc12.md", @@ -353,13 +363,13 @@ }, { "path": "docs/generated/pt-BR/ASET_Seed_Next.md", - "sha256": "sha256:1998e820c3144e2303fc0e330a00b489a41f6b83301686f81871334b3dcbf1e7", - "size_bytes": 12022 + "sha256": "sha256:c89f8dfa3303c3d7d7f3626ec9ce55b6a85076786cb6d9ee5f5bca6919c4f5b2", + "size_bytes": 12541 }, { "path": "docs/generated/pt-BR/ASET_Seed_Resolution_0.3-alpha.1.md", - "sha256": "sha256:1998e820c3144e2303fc0e330a00b489a41f6b83301686f81871334b3dcbf1e7", - "size_bytes": 12022 + "sha256": "sha256:c89f8dfa3303c3d7d7f3626ec9ce55b6a85076786cb6d9ee5f5bca6919c4f5b2", + "size_bytes": 12541 }, { "path": "docs/generated/ru/ASET_Seed_0.1-rc12.md", @@ -368,13 +378,13 @@ }, { "path": "docs/generated/ru/ASET_Seed_Next.md", - "sha256": "sha256:f5ee3f5db4a02c6ccd3182af886a6efbe6cbf8c5b531a283c9260cefeda917d0", - "size_bytes": 15982 + "sha256": "sha256:adea55c232c339a2107e4d7c408c8bf85d9fe7dc7e7be2a5a571da341e042dac", + "size_bytes": 16760 }, { "path": "docs/generated/ru/ASET_Seed_Resolution_0.3-alpha.1.md", - "sha256": "sha256:f5ee3f5db4a02c6ccd3182af886a6efbe6cbf8c5b531a283c9260cefeda917d0", - "size_bytes": 15982 + "sha256": "sha256:adea55c232c339a2107e4d7c408c8bf85d9fe7dc7e7be2a5a571da341e042dac", + "size_bytes": 16760 }, { "path": "docs/implementation/CROSS_IMPLEMENTATION_CONFORMANCE_PLAN.md", @@ -383,8 +393,8 @@ }, { "path": "docs/repository/BLACK_BOX_AUDIT_METHOD.md", - "sha256": "sha256:cdfad9ef4666388cae31cc6dff7baa494e79bda6caa4e38805e0083d624b6846", - "size_bytes": 2144 + "sha256": "sha256:3247376ca38a64eeca193c12b27a1ea47d2ccd271599ae528c42f3b5038a726a", + "size_bytes": 2246 }, { "path": "docs/repository/BRANCH_PROTECTION.md", @@ -393,8 +403,8 @@ }, { "path": "docs/repository/CI_ASSURANCE.md", - "sha256": "sha256:e233f5f4ce76e4b156e85d18edba23f70bd785a83f3a08c85f2b747e29c4092e", - "size_bytes": 3304 + "sha256": "sha256:f1d57be6d4f9a27bc8eaac526f605e263be96184d205fd71a277e19d626aa967", + "size_bytes": 3308 }, { "path": "docs/repository/DEPENDENCY_POLICY.md", @@ -468,23 +478,23 @@ }, { "path": "seed/canonical/CANON_PACKAGE.json", - "sha256": "sha256:58455e83e101e7a112a521c66cd68e56312227cfbf2accdbf668eba493d17942", - "size_bytes": 13241 + "sha256": "sha256:b2066da2be27e2f673c97fafebee1bcfc70f92e212b5bbba0c7b39baab505785", + "size_bytes": 13446 }, { "path": "seed/canonical/README.md", - "sha256": "sha256:dd873b7b201da02d7b9ea6f8e1f219b6c6ca31eca1c6c44be42af0d0cf4399cb", - "size_bytes": 2556 + "sha256": "sha256:3f1228ba583b6eef52f4a6ee2c6cf12564f99daae5191f77039453eb6895e4b4", + "size_bytes": 2672 }, { "path": "seed/canonical/assurance/canon-tla-refinement.json", - "sha256": "sha256:2095b62595d056c8a5a3b0700239a0211417979e4d5f2b4a535df0827017371b", - "size_bytes": 6791 + "sha256": "sha256:22884e71f1a484a8a7b00f708188191783505a71d1b2d15ad73cca67510099a5", + "size_bytes": 6876 }, { "path": "seed/canonical/assurance/invariant-coverage.json", - "sha256": "sha256:2d89e21d092bf4d340e271dc3bcba2d7df618c4c4b41e67beb626f518cdb163b", - "size_bytes": 15093 + "sha256": "sha256:0ffed8e2b1351928d9921c96bab4d8225504cf77e7298a0c8a603b66ac71e2c7", + "size_bytes": 15101 }, { "path": "seed/canonical/assurance/limitations.json", @@ -493,8 +503,8 @@ }, { "path": "seed/canonical/assurance/proof-traceability.json", - "sha256": "sha256:043bb3b1717d0c41123d326dc9b1d8dcae1cdde78c7ebf2d2ae26e79d2248eaf", - "size_bytes": 6966 + "sha256": "sha256:eaa97bb7aa9b09554ef4b1624dacac219a8a6ee24fdb8809cf203d1badffb0a2", + "size_bytes": 6972 }, { "path": "seed/canonical/assurance/repository-release-gates.json", @@ -503,8 +513,8 @@ }, { "path": "seed/canonical/assurance/verification-registry.json", - "sha256": "sha256:b4bb28e5a8965e984013ad7408522749cfef3008c913a518f455fefda7136187", - "size_bytes": 9717 + "sha256": "sha256:cc5f2c5b4ce0c9e466bb63779c1199817859e4d65d6df204acfaa3619b1f819c", + "size_bytes": 9722 }, { "path": "seed/canonical/conformance/cases/negative/RES-NEG-001.json", @@ -603,8 +613,8 @@ }, { "path": "seed/canonical/conformance/cases/positive/RES-POS-004.json", - "sha256": "sha256:dcf5f81b0e60f2aa0c157aab5297177d3f082544d64a54081d83e9d7d6093763", - "size_bytes": 2888 + "sha256": "sha256:b7407ed453ab3dd20d36ab3dd540d7c9c0c002df8821c40455b181b425093eef", + "size_bytes": 2906 }, { "path": "seed/canonical/conformance/cases/positive/RES-POS-005.json", @@ -633,7 +643,7 @@ }, { "path": "seed/canonical/conformance/conformance-profile.json", - "sha256": "sha256:aabbf317e0c51a1a1f1021dfbd0b2981c3dcf1142b89eb6a1bbfb1c7e1e9dcd6", + "sha256": "sha256:8b5aaa3b5890315f001ee68257c9a316d1523000db26ddd9b112fd16456f2cf4", "size_bytes": 12423 }, { @@ -643,8 +653,8 @@ }, { "path": "seed/canonical/conformance/model-based-conformance.json", - "sha256": "sha256:db4b3f9e76aff7e8ef3a87f02ae748bb4f718428370306454eb94b9dcc6212b4", - "size_bytes": 1453 + "sha256": "sha256:5cae29741da3488563cf026a04c9918d26d48fcd58db65607c25beb8c8705c08", + "size_bytes": 1577 }, { "path": "seed/canonical/decisions/ADR-001-semantic-canon-authority.md", @@ -691,35 +701,40 @@ "sha256": "sha256:fdb642c8f306d2136345e19c3650c22805f63139ac93d8f81f6773aa249881a0", "size_bytes": 2604 }, + { + "path": "seed/canonical/decisions/ADR-010-unify-authority-conflict-and-operation-semantics.md", + "sha256": "sha256:e9757a2879f7e6ce6c9b087212dbcc4cf2c74085f6b1e09be5fdfd4a7b236078", + "size_bytes": 2609 + }, { "path": "seed/canonical/formal/README.md", - "sha256": "sha256:38ef56c859221204201f3bed365f810bc383ca1fb257328ea6b774a67fe7ff82", - "size_bytes": 2373 + "sha256": "sha256:88d6c9a655bfe61b057bc09af68d7ffa528fa61d7cac4ac6971cd33681a113d4", + "size_bytes": 2492 }, { "path": "seed/canonical/formal/SeedCanonProjection.tla", - "sha256": "sha256:b7265eb707795b592c678842f764a5bfa7ce303bdc66f55f858366e20d64eb4e", - "size_bytes": 4377 + "sha256": "sha256:b3bf0555abba2fc9e817d1c3e97b93d62af933edfb9c7f5e7eec4502445447f5", + "size_bytes": 4246 }, { "path": "seed/canonical/formal/SeedCanonRefinementProofs.tla", - "sha256": "sha256:46ef7336b86d066ee531eb2c43873d9b6e1622dd48632b9af08ea6f412cf6338", - "size_bytes": 3391 + "sha256": "sha256:522338cc774f1f473d20130630e01aec6b66a2ac971ffed113b8a91d654b72ad", + "size_bytes": 3334 }, { "path": "seed/canonical/formal/SeedResolution.cfg", - "sha256": "sha256:b4ee7fb775fbf8909fded4e7b2086b8022e1412e648e21f470c464a625f690c0", - "size_bytes": 706 + "sha256": "sha256:bee70a11c1bde1e0b7aaa0acefbe5a4137bdcd5c3fbea254a3d8a1999086f1b7", + "size_bytes": 657 }, { "path": "seed/canonical/formal/SeedResolution.tla", - "sha256": "sha256:1c53b058d738e074c2a9de96fe27d8d7dd384d3ffa52f3bb95f7732908d66276", - "size_bytes": 7417 + "sha256": "sha256:1c0ebb27ed52da289f0981dcb11b61b6a7fc5c4a030ba434ae0b1d53b286b926", + "size_bytes": 7318 }, { "path": "seed/canonical/formal/SeedResolutionProofs.tla", - "sha256": "sha256:bcb4652249d66cbcb16f7c5a4538ad3bc2c31ef7d37b49fd27328eff6a6725f9", - "size_bytes": 21892 + "sha256": "sha256:3d6bdada8c1c0f93c247eb5c5b4df895e793c174768270138f2d6e6176990ad7", + "size_bytes": 21965 }, { "path": "seed/canonical/migration/ALPHA2_TO_0.3_ALPHA1.md", @@ -733,8 +748,8 @@ }, { "path": "seed/canonical/migration/CANON_CHANGE_DECLARATION.json", - "sha256": "sha256:4eb176ddb006c0957a2bf1d79685fd86b263b89500cc53df919193ec91459bf8", - "size_bytes": 820 + "sha256": "sha256:2bc5d60abed02040dd41c79db86aa23cbf206bf81df8193f771ceb9b8a29541c", + "size_bytes": 824 }, { "path": "seed/canonical/migration/RC11_TO_RC12_SEMANTIC_COVERAGE.json", @@ -873,8 +888,8 @@ }, { "path": "seed/canonical/schemas/canon-tla-refinement.schema.json", - "sha256": "sha256:17b142a998bbc8dd7b82b61c54d75e0c0e735211f35f90312565b78a4e7758e5", - "size_bytes": 6776 + "sha256": "sha256:ccd44d46cd3e9075fd439ead6a08cf3685d62bdea7f76d7ab2a736b579706069", + "size_bytes": 6772 }, { "path": "seed/canonical/schemas/conformance-profile.schema.json", @@ -893,8 +908,8 @@ }, { "path": "seed/canonical/schemas/invariant-coverage.schema.json", - "sha256": "sha256:e7ec1a6577df2519ca49f8c682588d68d767f9d28ab3301a6280221100ddc5b3", - "size_bytes": 3836 + "sha256": "sha256:9831e12343697216eac28a82b29baeb160a360e4e0126fcb356d904227b69ded", + "size_bytes": 4846 }, { "path": "seed/canonical/schemas/proof-traceability.schema.json", @@ -923,8 +938,8 @@ }, { "path": "seed/canonical/schemas/seed-model.schema.json", - "sha256": "sha256:1f1a727764b5d0138951f76fac1ab1155f4ba67c92f21aa8a21f7ef105bf9f94", - "size_bytes": 8807 + "sha256": "sha256:d454d6bc54aa8247ed35ab64d56c8702ba889243bb81f600a8edfbd9ee4fda89", + "size_bytes": 8805 }, { "path": "seed/canonical/shapes/seed.shacl.ttl", @@ -933,8 +948,8 @@ }, { "path": "seed/canonical/source/seed-model.json", - "sha256": "sha256:c43ca7b642a11c3ab140884a6bbff34bbd741f5cb905e6a779c860c813998fcf", - "size_bytes": 40151 + "sha256": "sha256:1fed5dc95045a287b3e9b8b4ea011a7b977729158f3360ed9a8a7e7e6ba1b4b0", + "size_bytes": 41799 }, { "path": "seed/canonical/terminology/foreign-terms.json", @@ -1913,13 +1928,13 @@ }, { "path": "tests/test_canonical_model.py", - "sha256": "sha256:a31ea5918db6c34161996edbe3a1ea11fe664aa311134c13ed92f35a6e25ea4e", - "size_bytes": 1451 + "sha256": "sha256:bfff1d731981bdef1855639d4b946a4f0a53c6217faf901a004e5277c5cb7d3c", + "size_bytes": 1546 }, { "path": "tests/test_ci_assurance.py", - "sha256": "sha256:d9339a902b4c78bf0b2d9d5dce3d705b2dce0a58f51a9c45f7efceaddd87c8f6", - "size_bytes": 9353 + "sha256": "sha256:e6d44a7bf9790e4c99262025ec3f487377760c2928f45d5319729a52456261f3", + "size_bytes": 9410 }, { "path": "tests/test_implementation_conformance_protocol.py", @@ -1928,8 +1943,8 @@ }, { "path": "tests/test_invariant_coverage.py", - "sha256": "sha256:6d5fa8bf5a6affef1b398cf5ac12a77148c3520ba25e11eff8301b89ba9668b9", - "size_bytes": 1744 + "sha256": "sha256:959ff3e0099523719c54a6f621180bb4d40cdc425c8af437e0f6baa0a02cd437", + "size_bytes": 1742 }, { "path": "tests/test_minimal_resolution_kernel.py", @@ -1963,13 +1978,13 @@ }, { "path": "tools/blackbox_documentation_audit.py", - "sha256": "sha256:a8108fcf9241d2c3c419f456439259e6079d76d9994113c493576a9ebd0edc08", - "size_bytes": 4125 + "sha256": "sha256:ac6d7ef36c3114fedad8f5a168a6fb036b763a2190ac0f68dc6fd233ffdc52d2", + "size_bytes": 4181 }, { "path": "tools/build_canon_package.py", - "sha256": "sha256:ec71afc2e51b342694d061e6117360602aebde4ac2c74799b85a9dfda255e2fd", - "size_bytes": 4372 + "sha256": "sha256:f79501e64c6bd95eebad7411e2d487a9c27a2c866b2b54d72ea84a004752ebd0", + "size_bytes": 4464 }, { "path": "tools/build_release.py", @@ -1978,23 +1993,23 @@ }, { "path": "tools/check_assurance_traceability.py", - "sha256": "sha256:7a4076a25b2e73af9244f1bb8e9d57ffede103a454c36dec028a415ed36ecbc6", - "size_bytes": 10419 + "sha256": "sha256:35e94c96b60bb19fd6c872a7d36ff707deca79443463656303a6c9e4ec01df8c", + "size_bytes": 10421 }, { "path": "tools/check_canon_compatibility.py", - "sha256": "sha256:d1130da7274498255176d3a7b637822efb9f94591912309d6146ac45b80e8ce4", - "size_bytes": 5702 + "sha256": "sha256:0961ef11c7ef67fbbc6b90a4529294a12fe80c86269c59236a3add23c8b09d97", + "size_bytes": 5916 }, { "path": "tools/check_canon_tla_refinement.py", - "sha256": "sha256:95a6a771244177f7e4fe83921baadd11170c4b6967fc39d6238a1a87a5e3c02b", - "size_bytes": 8989 + "sha256": "sha256:1e5dcdd478bc88ce1e7b2a972b5d135b3089b12d47f2c626e42def0f95b7d0e9", + "size_bytes": 8977 }, { "path": "tools/check_invariant_coverage.py", - "sha256": "sha256:bc578d83ebe432c16f5649de077fec276ec0f8e0df8239bb9663c03077c1841f", - "size_bytes": 7231 + "sha256": "sha256:c0bb0fc214239214bf1b7c3f472405253b69033122ebe7fe0d3e5e30e8b25d0d", + "size_bytes": 7211 }, { "path": "tools/check_language.py", @@ -2008,13 +2023,13 @@ }, { "path": "tools/generate_canon_tla_projection.py", - "sha256": "sha256:fb0bc3d79d0d8e4c7bffa4a1f5ab6c76b45bb621adae8ef4367958e9a7b16127", - "size_bytes": 9119 + "sha256": "sha256:f92535d146281802918d438169c477f6daeceec29d77142e7bfbfe7eb710d20a", + "size_bytes": 8992 }, { "path": "tools/generate_editions.py", - "sha256": "sha256:0052acde2f7f4855071c424f8ddc3aead530bd2e59ebef0a5213d67a4f1c04a6", - "size_bytes": 5814 + "sha256": "sha256:085e795b3913bcf5cb5be5751292de6a321b6cf6744cd1cdea2f77813024f616", + "size_bytes": 5805 }, { "path": "tools/generate_project_metadata.py", @@ -2043,8 +2058,8 @@ }, { "path": "tools/model_check_seed.py", - "sha256": "sha256:40411d867950450af17bbdf5f4db47c83916c6edb65a45fb565d26d7fbbe67be", - "size_bytes": 9720 + "sha256": "sha256:a5fa0f1808a562d6a774daccbab5a244517f6261a0e8d68f3d5952fe635fcb3d", + "size_bytes": 9693 }, { "path": "tools/production_gate.py", @@ -2128,8 +2143,8 @@ }, { "path": "tools/validate_seed_canon.py", - "sha256": "sha256:39100a61aef4cfed479a9a91a98e7312976bb31970c32aa2fa9e90a093b1d87d", - "size_bytes": 7891 + "sha256": "sha256:d340da0aef7c9f94537dd4a8558e786d90b921b53f58d6544981252726ae777d", + "size_bytes": 8201 }, { "path": "tools/verify_frozen_release.py", @@ -2137,7 +2152,7 @@ "size_bytes": 1035 } ], - "files_count": 427, + "files_count": 430, "manifest_scope": "all repository regular files except MANIFEST.json, Git metadata, virtual environments, caches and dist", "package": "ASET-Seed-0.3.0-alpha.1-Minimal-Strong-Core", "repository_root": "ASET" diff --git a/audit/ACTIVE_AUDIT_INDEX.json b/audit/ACTIVE_AUDIT_INDEX.json index 8f0c17a..c7f4b20 100644 --- a/audit/ACTIVE_AUDIT_INDEX.json +++ b/audit/ACTIVE_AUDIT_INDEX.json @@ -1,6 +1,6 @@ { "active_candidate": { - "canon_package_digest": "sha256:392ff8e36eecb2bf6cfa9a6cbc76117025a4c7d8a170e8ddf562f1ea5df27d38", + "canon_package_digest": "sha256:0e1518c4ff6bd6b0da71089bfe5e1a9802929016c8ec2547024a1a0e2b84a19d", "extension_separation": "COMPLETE", "implementation_precedence": "NONE", "repository_role": "OPEN_IMPLEMENTATION_NEUTRAL_SPECIFICATION", @@ -11,8 +11,8 @@ "audit/PDCA-15-EXTENSION-EXTRACTION-CLOSURE.json", "audit/PDCA-15-EXTENSION-EXTRACTION-CLOSURE.md", "audit/REFACTORING_LOG.md", - "audit/PDCA-17-INVARIANT-CLOSURE.json", - "audit/PDCA-17-INVARIANT-CLOSURE.md" + "audit/PDCA-18-SEED-FINAL-SEMANTIC-CLEANUP.json", + "audit/PDCA-18-SEED-FINAL-SEMANTIC-CLEANUP.md" ], "classification_rules": [ "Only active_controlling_records may support static claims about the current implementation-neutral candidate.", @@ -55,7 +55,9 @@ "audit/pdca/PDCA-11-PREFREEZE-BLOCKER-CLOSURE.md", "audit/pdca/PDCA-12-FINAL-PREFREEZE-ASSURANCE.md", "audit/pdca/PDCA-13-PROJECT-METADATA-AND-DOCUMENTATION-GENERATION.md", - "audit/pdca/PDCA-14-SEED-SEMANTIC-NUCLEUS.md" + "audit/pdca/PDCA-14-SEED-SEMANTIC-NUCLEUS.md", + "audit/PDCA-17-INVARIANT-CLOSURE.json", + "audit/PDCA-17-INVARIANT-CLOSURE.md" ], "index_exclusions": [ "audit/README.md", diff --git a/audit/ACTIVE_AUDIT_INDEX.md b/audit/ACTIVE_AUDIT_INDEX.md index 60beb03..27f0527 100644 --- a/audit/ACTIVE_AUDIT_INDEX.md +++ b/audit/ACTIVE_AUDIT_INDEX.md @@ -6,7 +6,7 @@ This index separates the current implementation-neutral Seed candidate from hist The current candidate is Seed `0.3.0-alpha.1`. Its machine identity is [`seed/canonical/CANON_PACKAGE.json`](../seed/canonical/CANON_PACKAGE.json), and its repository claim boundary is [`REPOSITORY_STATUS.json`](../REPOSITORY_STATUS.json). -Static controlling records are listed in [`ACTIVE_AUDIT_INDEX.json`](ACTIVE_AUDIT_INDEX.json). Candidate-specific executable evidence is generated under `dist/` by [`tools/repository_release_gate.py`](../tools/repository_release_gate.py). The active assurance line additionally requires complete invariant coverage and zero surviving semantic mutations as defined by [`PDCA-17-INVARIANT-CLOSURE.md`](PDCA-17-INVARIANT-CLOSURE.md). +Static controlling records are listed in [`ACTIVE_AUDIT_INDEX.json`](ACTIVE_AUDIT_INDEX.json). Candidate-specific executable evidence is generated under `dist/` by [`tools/repository_release_gate.py`](../tools/repository_release_gate.py). The active assurance line is controlled by [`PDCA-18-SEED-FINAL-SEMANTIC-CLEANUP.md`](PDCA-18-SEED-FINAL-SEMANTIC-CLEANUP.md), which requires role-classified operation coverage, saturated finite-state exploration, zero surviving semantic mutations, TLC/TLAPS closure and standalone canon-to-TLA refinement. ## Historical records diff --git a/audit/PDCA-18-SEED-FINAL-SEMANTIC-CLEANUP.json b/audit/PDCA-18-SEED-FINAL-SEMANTIC-CLEANUP.json new file mode 100644 index 0000000..62dda41 --- /dev/null +++ b/audit/PDCA-18-SEED-FINAL-SEMANTIC-CLEANUP.json @@ -0,0 +1,43 @@ +{ + "act": { + "freeze_rule": "After this cleanup, further Seed changes should strengthen assurance or fix demonstrated semantic defects; new capabilities belong in extensions.", + "release_rule": "The exact candidate must pass canon validation, saturated finite-state exploration, semantic mutations, operation coverage, TLC, TLAPS, standalone canon-to-TLA refinement and the repository release gate." + }, + "candidate": "ASET-SEED-RESOLUTION-CANON-0.3-ALPHA1", + "check": { + "required_results": { + "canon_operations": "3 = 2 state transitions + 1 observer", + "invariants": "12/12", + "requirements": "12/12", + "semantic_mutations": "13/13 killed", + "standalone_projection": "V5 parity + TLAPS refinement proof", + "tlaps": "REQUIRED_BY_RELEASE_GATE", + "tlc": "REQUIRED_BY_RELEASE_GATE" + } + }, + "cycle_id": "PDCA-18", + "do": { + "changes": [ + "unified request and terminal Authority admission under RecognizedAuthorityBindings", + "restricted conflict observation to already accepted terminal resolutions", + "renamed terminal uniqueness to AcceptedTerminalUnique and strengthened conflict semantics as ConflictSound", + "replaced the machine-canon transitions catalogue with a role-classified operations catalogue", + "moved operation identifiers from SEED-TX-* to SEED-OP-*", + "advanced the standalone canon-to-TLA projection profile to V5", + "updated active black-box audit methodology and made that methodology part of the audited documentation surface", + "recorded the cleanup in ADR-010 and the active audit line" + ] + }, + "document_type": "aset-pdca-seed-final-semantic-cleanup", + "plan": { + "constraints": [ + "do not add new Seed capabilities", + "preserve implementation neutrality", + "preserve the wire-level single AuthorityBinding semantics", + "preserve historical RC11/RC12 evidence as non-controlling history" + ], + "objective": "Remove the final formal/wire and terminology mismatches from the Seed 0.3 minimal resolution kernel." + }, + "schema_version": 1, + "verdict": "FINAL_SEMANTIC_CLEANUP_DEFINED" +} diff --git a/audit/PDCA-18-SEED-FINAL-SEMANTIC-CLEANUP.md b/audit/PDCA-18-SEED-FINAL-SEMANTIC-CLEANUP.md new file mode 100644 index 0000000..707b194 --- /dev/null +++ b/audit/PDCA-18-SEED-FINAL-SEMANTIC-CLEANUP.md @@ -0,0 +1,43 @@ +# PDCA-18 — Seed final semantic cleanup + +## Plan + +Remove the remaining mismatches between the active machine canon, wire +semantics and formal model without adding new Seed capabilities. + +## Do + +The candidate: + +- uses one `RecognizedAuthorityBindings` relation for both request and terminal + admission; +- admits conflict observation only for an already accepted terminal resolution; +- distinguishes `AcceptedTerminalUnique` from external conflicting valid + material and expresses the latter through `ConflictSound`; +- publishes three role-classified operations, not three transitions; +- uses `SEED-OP-*` identifiers for two state transitions and one observer; +- advances the standalone canon projection to profile V5; +- replaces the obsolete RC12 runtime black-box methodology with the actual + active specification-repository audit boundary. + +## Check + +The exact candidate is required to close: + +```text +requirements = 12/12 +invariants = 12/12 +operations = 3/3 +semantic mutations killed = 13/13 +finite model saturated = true +TLC = PASS +TLAPS = PASS +canon-to-TLA refinement = PASS +repository release gate = PASS +``` + +## Act + +Once those gates pass, Seed 0.3 should be treated as semantically stabilized. +Further capability growth belongs in extensions; further Seed changes should +be limited to demonstrated defects or assurance strengthening. diff --git a/audit/REFACTORING_LOG.md b/audit/REFACTORING_LOG.md index 47ceee0..c639949 100644 --- a/audit/REFACTORING_LOG.md +++ b/audit/REFACTORING_LOG.md @@ -24,3 +24,11 @@ - Rephrased the active System Composition environment invariant so that it binds an externally committed assurance-toolchain and dependency closure without prescribing Python or any implementation runtime. - Replaced Python-specific environment descriptions in active component and system verification cases with implementation-neutral assurance-toolchain descriptions; frozen rc11 source evidence remains unchanged. - Linked the separate non-normative [`aset-python-sqlite`](https://github.com/attractor-set/aset-python-sqlite) reference implementation from all curated root README editions and the roadmap without granting it semantic precedence. + +## Seed final semantic cleanup + +- Unified request and terminal admission under one `RecognizedAuthorityBindings` relation to match the single wire AuthorityBinding semantics. +- Restricted conflict observation to already accepted terminal resolutions, eliminating impossible pre-terminal conflict states. +- Distinguished accepted terminal uniqueness from external valid conflict material through `AcceptedTerminalUnique` and `ConflictSound`. +- Reclassified the machine-canon catalogue as three operations: two state transitions and one observer, with `SEED-OP-*` identifiers. +- Advanced the standalone canon-to-TLA projection to V5 and updated the active audit methodology and evidence line. diff --git a/docs/architecture/SEED_ROLE.md b/docs/architecture/SEED_ROLE.md index d0ae67a..e228c8f 100644 --- a/docs/architecture/SEED_ROLE.md +++ b/docs/architecture/SEED_ROLE.md @@ -13,8 +13,7 @@ conflict observations, policy results or cryptographic proofs. ## Environment and observers -Conflict is environment state because an independently established conflict -between valid terminal records changes the derived resolution to `UNKNOWN`. +Conflict is environment state because additional distinct valid terminal material for an already accepted terminal resolution changes the derived resolution to `UNKNOWN`. Conflict observation is not admissible before an accepted terminal record exists. `EVALUATE_RESOLUTION` is a pure observer and never mutates Seed-owned state. Invalid, malformed or non-authoritative material has no Seed state slot. It may @@ -23,10 +22,7 @@ Authority, `ALLOW` or a conflict by mere presence. ## Authority boundary -Seed requires an exact-binding Authority to be explicitly recognized by the -local Context. How that recognition is established—signature, certificate, -delegation chain, hardware root, external verifier or another mechanism—is a -profile concern. Opaque evidence references are not Authority by themselves. +Seed consumes one exact-binding Authority-recognition relation for both request registration and terminal submission. How recognition is established—signature, certificate, delegation mechanism, hardware root, external verifier or another mechanism—is a profile concern. Opaque evidence references are not Authority by themselves. ## Outside Seed diff --git a/docs/architecture/SEED_STATE_MINIMIZATION.md b/docs/architecture/SEED_STATE_MINIMIZATION.md index 1275c28..3b1ff79 100644 --- a/docs/architecture/SEED_STATE_MINIMIZATION.md +++ b/docs/architecture/SEED_STATE_MINIMIZATION.md @@ -7,7 +7,7 @@ environment dimension: 1. `requestMeta` — partial map of admitted request metadata; 2. `terminalMeta` — partial map of accepted terminal metadata; -3. `conflicts` — environment observation state. +3. `conflicts` — environment observation state constrained to accepted terminal requests. `seedVars == <>`; conflict is deliberately excluded from Seed-owned state. @@ -34,8 +34,7 @@ separate provenance refinement is specified and proved. Invalid/non-authoritative material has no artificial stutter action. It remains outside the abstract state machine. The executable admission boundary verifies -that it cannot create accepted state. Valid conflict observation is modeled -separately as environment state and is proved not to mutate Seed-owned state. +that it cannot create accepted state. Valid conflict observation is modeled separately as environment state, is admissible only after an accepted terminal record exists, and is proved not to mutate Seed-owned state. No Merkle tree, MMR, signature algorithm or accumulator is introduced into the Seed core. diff --git a/docs/generated/en/ASET_Seed_Next.md b/docs/generated/en/ASET_Seed_Next.md index a9e0495..f0f1c3f 100644 --- a/docs/generated/en/ASET_Seed_Next.md +++ b/docs/generated/en/ASET_Seed_Next.md @@ -4,7 +4,7 @@ **Status:** `MINIMAL_STRONG_CORE_ALPHA` -**Canonical model SHA-256:** `sha256:54c46e46d4e6b5870353bb0ed229310f60583e9acd11798b655bdd837c8dba74` +**Canonical model SHA-256:** `sha256:d8fde8f21b6524b2442151505f8bf4aec29e17be4a17d2409021ad594597b203` > This edition is derived from the machine canon. @@ -98,7 +98,7 @@ Predicate: `resolution_domain` ### `ASET-SEED-REQ-004` -An exact bound effect MUST be permitted if and only if the unique valid terminal ResolutionRecord is ALLOW. +An exact bound effect MUST be permitted if and only if the accepted authoritative terminal ResolutionRecord is ALLOW and no valid terminal conflict is observed. Modality: `MUST` @@ -108,7 +108,7 @@ Predicate: `allow_only` ### `ASET-SEED-REQ-005` -UNKNOWN and BLOCK MUST prohibit the effect. Missing or ambiguous valid terminal state, or failure to establish a valid terminal record, MUST resolve to UNKNOWN. Invalid or non-authoritative material MUST NOT override an otherwise unique valid terminal record. +UNKNOWN and BLOCK MUST prohibit the effect. Missing accepted terminal state, failure to establish an authoritative terminal record, or observation of additional conflicting valid terminal material MUST resolve to UNKNOWN. Invalid or non-authoritative material MUST NOT override an otherwise authoritative accepted terminal record. Modality: `MUST` @@ -148,11 +148,11 @@ Predicate: `inputs_non_authoritative` ### `ASET-SEED-REQ-009` -At most one valid terminal record MAY exist for one resolution_id; conflicting terminal records MUST fail closed as UNKNOWN. +Seed-owned state MUST accept at most one terminal record for one resolution_id. Observation of additional distinct valid terminal material for an already accepted terminal resolution MUST fail closed as UNKNOWN without replacing the accepted record. -Modality: `MAY` +Modality: `MUST` -Predicate: `terminal_unique` +Predicate: `accepted_terminal_unique` `verification`: `ASET-VERIFY-DECLARATIVE-STATE-VALIDATION`, `ASET-VERIFY-PORTABLE-CASES`, `ASET-VERIFY-BOUNDED-MODEL`, `ASET-VERIFY-INVARIANT-COVERAGE`, `ASET-VERIFY-SEMANTIC-MUTATIONS` @@ -189,39 +189,39 @@ Predicate: `implementation_neutral` ## Invariants - `SEED-INV-001` — Every valid derived resolution is UNKNOWN, ALLOW or BLOCK. -- `SEED-INV-002` — Effect permission is true if and only if the unique valid terminal record is ALLOW. +- `SEED-INV-002` — Effect permission is true if and only if the accepted authoritative terminal record is ALLOW and no valid terminal conflict is observed. - `SEED-INV-003` — UNKNOWN and BLOCK never permit an effect. - `SEED-INV-004` — Every request and terminal record preserves one exact binding digest. - `SEED-INV-005` — Every valid terminal record uses an Authority explicitly recognized for the exact local binding. - `SEED-INV-006` — Authority evidence is non-authoritative until exact-binding Authority recognition succeeds; opaque proof material cannot create or expand Authority by itself. - `SEED-INV-007` — External statements and evidence are outside Seed-owned canonical state unless accepted by a recognized Seed transition. -- `SEED-INV-008` — At most one valid terminal record exists for one resolution_id. -- `SEED-INV-009` — Conflicting valid terminal records yield UNKNOWN. Invalid or non-authoritative material cannot create ALLOW, create a conflict, or override an otherwise unique valid terminal record. +- `SEED-INV-008` — Seed-owned state accepts at most one terminal record for one resolution_id. +- `SEED-INV-009` — A conflict observation is valid only for a resolution_id that already has an accepted terminal record. Additional conflicting valid terminal material yields UNKNOWN; invalid or non-authoritative material cannot create ALLOW, create a conflict, or replace the accepted record. - `SEED-INV-010` — Resolution records are append-only, immutable and content-addressed. - `SEED-INV-011` — Only recognized Seed state transitions may change Seed-owned canonical state; environment observations and observer operations do not mutate that state. - `SEED-INV-012` — Reconsideration uses a fresh resolution_id linked by an immutable content-addressed commitment to a previously recognized terminal ResolutionRecord; predecessor object retention is not required. -## Transitions +## Operations -### `SEED-TX-001` — `REGISTER_REQUEST` +### `SEED-OP-001` — `REGISTER_REQUEST` - `payload_schema`: `seed/canonical/protocol/schemas/payload-register-request.schema.json` -- `authority_rule`: The initial Authority binding must be locally rooted and exactly match the request binding. +- `authority_rule`: The Authority must be explicitly recognized for the exact request binding. - `binding_rule`: The request contains one canonical exact binding and a fresh resolution_id. For reconsideration, previous_terminal_record_digest must be a recognized immutable terminal-record commitment; predecessor object presence in retained storage is not required. - `created_artifacts`: `ResolutionRequest` -### `SEED-TX-002` — `SUBMIT_RESOLUTION` +### `SEED-OP-002` — `SUBMIT_RESOLUTION` - `payload_schema`: `seed/canonical/protocol/schemas/payload-submit-resolution.schema.json` -- `authority_rule`: The record Authority must be explicitly recognized for the exact request binding. Concrete signatures, delegation chains and proof construction are external validation mechanisms. +- `authority_rule`: The Authority must be explicitly recognized for the exact request binding. Concrete signatures, credentials, delegation mechanisms and proof construction are external validation mechanisms. - `binding_rule`: The record request_digest and binding_digest must exactly match the registered request. - `created_artifacts`: `ResolutionRecord` -### `SEED-TX-003` — `EVALUATE_RESOLUTION` +### `SEED-OP-003` — `EVALUATE_RESOLUTION` - `payload_schema`: `seed/canonical/protocol/schemas/operation.schema.json` - `authority_rule`: Evaluation creates no Authority and accepts no external statement as a resolution. -- `binding_rule`: Evaluation observes one resolution_id without mutating Seed-owned state. It derives UNKNOWN when no unique valid terminal record is established; invalid or non-authoritative material cannot override a unique valid record. +- `binding_rule`: Evaluation observes one resolution_id without mutating Seed-owned state. It derives UNKNOWN when no authoritative accepted terminal result is established or when additional conflicting valid terminal material is observed; invalid or non-authoritative material cannot override an otherwise authoritative accepted terminal result. - `created_artifacts`: `ResolutionEvaluation` ## Implementation boundary diff --git a/docs/generated/en/ASET_Seed_Resolution_0.3-alpha.1.md b/docs/generated/en/ASET_Seed_Resolution_0.3-alpha.1.md index a9e0495..f0f1c3f 100644 --- a/docs/generated/en/ASET_Seed_Resolution_0.3-alpha.1.md +++ b/docs/generated/en/ASET_Seed_Resolution_0.3-alpha.1.md @@ -4,7 +4,7 @@ **Status:** `MINIMAL_STRONG_CORE_ALPHA` -**Canonical model SHA-256:** `sha256:54c46e46d4e6b5870353bb0ed229310f60583e9acd11798b655bdd837c8dba74` +**Canonical model SHA-256:** `sha256:d8fde8f21b6524b2442151505f8bf4aec29e17be4a17d2409021ad594597b203` > This edition is derived from the machine canon. @@ -98,7 +98,7 @@ Predicate: `resolution_domain` ### `ASET-SEED-REQ-004` -An exact bound effect MUST be permitted if and only if the unique valid terminal ResolutionRecord is ALLOW. +An exact bound effect MUST be permitted if and only if the accepted authoritative terminal ResolutionRecord is ALLOW and no valid terminal conflict is observed. Modality: `MUST` @@ -108,7 +108,7 @@ Predicate: `allow_only` ### `ASET-SEED-REQ-005` -UNKNOWN and BLOCK MUST prohibit the effect. Missing or ambiguous valid terminal state, or failure to establish a valid terminal record, MUST resolve to UNKNOWN. Invalid or non-authoritative material MUST NOT override an otherwise unique valid terminal record. +UNKNOWN and BLOCK MUST prohibit the effect. Missing accepted terminal state, failure to establish an authoritative terminal record, or observation of additional conflicting valid terminal material MUST resolve to UNKNOWN. Invalid or non-authoritative material MUST NOT override an otherwise authoritative accepted terminal record. Modality: `MUST` @@ -148,11 +148,11 @@ Predicate: `inputs_non_authoritative` ### `ASET-SEED-REQ-009` -At most one valid terminal record MAY exist for one resolution_id; conflicting terminal records MUST fail closed as UNKNOWN. +Seed-owned state MUST accept at most one terminal record for one resolution_id. Observation of additional distinct valid terminal material for an already accepted terminal resolution MUST fail closed as UNKNOWN without replacing the accepted record. -Modality: `MAY` +Modality: `MUST` -Predicate: `terminal_unique` +Predicate: `accepted_terminal_unique` `verification`: `ASET-VERIFY-DECLARATIVE-STATE-VALIDATION`, `ASET-VERIFY-PORTABLE-CASES`, `ASET-VERIFY-BOUNDED-MODEL`, `ASET-VERIFY-INVARIANT-COVERAGE`, `ASET-VERIFY-SEMANTIC-MUTATIONS` @@ -189,39 +189,39 @@ Predicate: `implementation_neutral` ## Invariants - `SEED-INV-001` — Every valid derived resolution is UNKNOWN, ALLOW or BLOCK. -- `SEED-INV-002` — Effect permission is true if and only if the unique valid terminal record is ALLOW. +- `SEED-INV-002` — Effect permission is true if and only if the accepted authoritative terminal record is ALLOW and no valid terminal conflict is observed. - `SEED-INV-003` — UNKNOWN and BLOCK never permit an effect. - `SEED-INV-004` — Every request and terminal record preserves one exact binding digest. - `SEED-INV-005` — Every valid terminal record uses an Authority explicitly recognized for the exact local binding. - `SEED-INV-006` — Authority evidence is non-authoritative until exact-binding Authority recognition succeeds; opaque proof material cannot create or expand Authority by itself. - `SEED-INV-007` — External statements and evidence are outside Seed-owned canonical state unless accepted by a recognized Seed transition. -- `SEED-INV-008` — At most one valid terminal record exists for one resolution_id. -- `SEED-INV-009` — Conflicting valid terminal records yield UNKNOWN. Invalid or non-authoritative material cannot create ALLOW, create a conflict, or override an otherwise unique valid terminal record. +- `SEED-INV-008` — Seed-owned state accepts at most one terminal record for one resolution_id. +- `SEED-INV-009` — A conflict observation is valid only for a resolution_id that already has an accepted terminal record. Additional conflicting valid terminal material yields UNKNOWN; invalid or non-authoritative material cannot create ALLOW, create a conflict, or replace the accepted record. - `SEED-INV-010` — Resolution records are append-only, immutable and content-addressed. - `SEED-INV-011` — Only recognized Seed state transitions may change Seed-owned canonical state; environment observations and observer operations do not mutate that state. - `SEED-INV-012` — Reconsideration uses a fresh resolution_id linked by an immutable content-addressed commitment to a previously recognized terminal ResolutionRecord; predecessor object retention is not required. -## Transitions +## Operations -### `SEED-TX-001` — `REGISTER_REQUEST` +### `SEED-OP-001` — `REGISTER_REQUEST` - `payload_schema`: `seed/canonical/protocol/schemas/payload-register-request.schema.json` -- `authority_rule`: The initial Authority binding must be locally rooted and exactly match the request binding. +- `authority_rule`: The Authority must be explicitly recognized for the exact request binding. - `binding_rule`: The request contains one canonical exact binding and a fresh resolution_id. For reconsideration, previous_terminal_record_digest must be a recognized immutable terminal-record commitment; predecessor object presence in retained storage is not required. - `created_artifacts`: `ResolutionRequest` -### `SEED-TX-002` — `SUBMIT_RESOLUTION` +### `SEED-OP-002` — `SUBMIT_RESOLUTION` - `payload_schema`: `seed/canonical/protocol/schemas/payload-submit-resolution.schema.json` -- `authority_rule`: The record Authority must be explicitly recognized for the exact request binding. Concrete signatures, delegation chains and proof construction are external validation mechanisms. +- `authority_rule`: The Authority must be explicitly recognized for the exact request binding. Concrete signatures, credentials, delegation mechanisms and proof construction are external validation mechanisms. - `binding_rule`: The record request_digest and binding_digest must exactly match the registered request. - `created_artifacts`: `ResolutionRecord` -### `SEED-TX-003` — `EVALUATE_RESOLUTION` +### `SEED-OP-003` — `EVALUATE_RESOLUTION` - `payload_schema`: `seed/canonical/protocol/schemas/operation.schema.json` - `authority_rule`: Evaluation creates no Authority and accepts no external statement as a resolution. -- `binding_rule`: Evaluation observes one resolution_id without mutating Seed-owned state. It derives UNKNOWN when no unique valid terminal record is established; invalid or non-authoritative material cannot override a unique valid record. +- `binding_rule`: Evaluation observes one resolution_id without mutating Seed-owned state. It derives UNKNOWN when no authoritative accepted terminal result is established or when additional conflicting valid terminal material is observed; invalid or non-authoritative material cannot override an otherwise authoritative accepted terminal result. - `created_artifacts`: `ResolutionEvaluation` ## Implementation boundary diff --git a/docs/generated/pt-BR/ASET_Seed_Next.md b/docs/generated/pt-BR/ASET_Seed_Next.md index 1d6d520..9d904b3 100644 --- a/docs/generated/pt-BR/ASET_Seed_Next.md +++ b/docs/generated/pt-BR/ASET_Seed_Next.md @@ -4,7 +4,7 @@ **Status:** `MINIMAL_STRONG_CORE_ALPHA` -**SHA-256 do modelo canônico:** `sha256:54c46e46d4e6b5870353bb0ed229310f60583e9acd11798b655bdd837c8dba74` +**SHA-256 do modelo canônico:** `sha256:d8fde8f21b6524b2442151505f8bf4aec29e17be4a17d2409021ad594597b203` > Esta edição é derivada do cânone legível por máquina. @@ -98,7 +98,7 @@ Predicado: `resolution_domain` ### `ASET-SEED-REQ-004` -Um efeito exatamente vinculado DEVE ser permitido se, e somente se, o único ResolutionRecord terminal válido for ALLOW. +Um efeito exatamente vinculado DEVE ser permitido se, e somente se, o ResolutionRecord terminal autoritativo aceito for ALLOW e nenhum conflito terminal válido for observado. Modalidade: `MUST` @@ -108,7 +108,7 @@ Predicado: `allow_only` ### `ASET-SEED-REQ-005` -UNKNOWN e BLOCK DEVEM proibir o efeito. Estado terminal válido ausente ou ambíguo, ou falha em estabelecer um registro terminal válido, DEVE resultar em UNKNOWN. Material inválido ou não autoritativo NÃO DEVE substituir um registro terminal válido e único. +UNKNOWN e BLOCK DEVEM proibir o efeito. Estado terminal aceito ausente, falha em estabelecer um registro terminal autoritativo ou observação de material terminal válido conflitante adicional DEVE resultar em UNKNOWN. Material inválido ou não autoritativo NÃO DEVE substituir um registro terminal autoritativo já aceito. Modalidade: `MUST` @@ -148,11 +148,11 @@ Predicado: `inputs_non_authoritative` ### `ASET-SEED-REQ-009` -No máximo um registro terminal válido PODE existir para um resolution_id; registros terminais conflitantes DEVEM falhar de modo fechado como UNKNOWN. +O estado pertencente ao Seed DEVE aceitar no máximo um registro terminal para um resolution_id. A observação de material terminal válido distinto adicional para uma resolução terminal já aceita DEVE falhar de modo fechado como UNKNOWN sem substituir o registro aceito. -Modalidade: `MAY` +Modalidade: `MUST` -Predicado: `terminal_unique` +Predicado: `accepted_terminal_unique` `verification`: `ASET-VERIFY-DECLARATIVE-STATE-VALIDATION`, `ASET-VERIFY-PORTABLE-CASES`, `ASET-VERIFY-BOUNDED-MODEL`, `ASET-VERIFY-INVARIANT-COVERAGE`, `ASET-VERIFY-SEMANTIC-MUTATIONS` @@ -189,39 +189,39 @@ Predicado: `implementation_neutral` ## Invariantes - `SEED-INV-001` — Toda resolução derivada válida é UNKNOWN, ALLOW ou BLOCK. -- `SEED-INV-002` — A permissão do efeito é verdadeira se, e somente se, o único registro terminal válido for ALLOW. +- `SEED-INV-002` — A permissão de efeito é verdadeira se, e somente se, o registro terminal autoritativo aceito for ALLOW e nenhum conflito terminal válido for observado. - `SEED-INV-003` — UNKNOWN e BLOCK nunca permitem um efeito. - `SEED-INV-004` — Toda solicitação e registro terminal preservam um único digest exato de vinculação. - `SEED-INV-005` — Todo registro terminal válido usa uma Authority explicitamente reconhecida para a vinculação local exata. - `SEED-INV-006` — Evidência de Authority é não autoritativa até que o reconhecimento de Authority com vinculação exata seja bem-sucedido; material de prova opaco não pode criar ou ampliar Authority por si só. - `SEED-INV-007` — Declarações externas e Evidence ficam fora do estado canônico pertencente ao Seed, salvo quando aceitas por uma transição reconhecida do Seed. -- `SEED-INV-008` — Existe no máximo um registro terminal válido para um resolution_id. -- `SEED-INV-009` — Registros terminais válidos conflitantes resultam em UNKNOWN. Material inválido ou não autoritativo não pode criar ALLOW, criar conflito nem substituir um registro terminal válido e único. +- `SEED-INV-008` — O estado pertencente ao Seed aceita no máximo um registro terminal para um resolution_id. +- `SEED-INV-009` — Uma observação de conflito só é válida para um resolution_id que já possua um registro terminal aceito. Material terminal válido conflitante adicional resulta em UNKNOWN; material inválido ou não autoritativo não pode criar ALLOW, criar conflito nem substituir o registro aceito. - `SEED-INV-010` — Registros de resolução são append-only, imutáveis e endereçados por conteúdo. - `SEED-INV-011` — Somente transições de estado reconhecidas do Seed podem alterar o estado canônico pertencente ao Seed; observações do ambiente e operações de observador não alteram esse estado. - `SEED-INV-012` — A reconsideração usa um resolution_id novo vinculado por um compromisso imutável e endereçado por conteúdo a um ResolutionRecord terminal previamente reconhecido; a retenção do objeto predecessor não é obrigatória. -## Transições +## Operações -### `SEED-TX-001` — `REGISTER_REQUEST` +### `SEED-OP-001` — `REGISTER_REQUEST` - `payload_schema`: `seed/canonical/protocol/schemas/payload-register-request.schema.json` -- `authority_rule`: The initial Authority binding must be locally rooted and exactly match the request binding. +- `authority_rule`: The Authority must be explicitly recognized for the exact request binding. - `binding_rule`: The request contains one canonical exact binding and a fresh resolution_id. For reconsideration, previous_terminal_record_digest must be a recognized immutable terminal-record commitment; predecessor object presence in retained storage is not required. - `created_artifacts`: `ResolutionRequest` -### `SEED-TX-002` — `SUBMIT_RESOLUTION` +### `SEED-OP-002` — `SUBMIT_RESOLUTION` - `payload_schema`: `seed/canonical/protocol/schemas/payload-submit-resolution.schema.json` -- `authority_rule`: The record Authority must be explicitly recognized for the exact request binding. Concrete signatures, delegation chains and proof construction are external validation mechanisms. +- `authority_rule`: The Authority must be explicitly recognized for the exact request binding. Concrete signatures, credentials, delegation mechanisms and proof construction are external validation mechanisms. - `binding_rule`: The record request_digest and binding_digest must exactly match the registered request. - `created_artifacts`: `ResolutionRecord` -### `SEED-TX-003` — `EVALUATE_RESOLUTION` +### `SEED-OP-003` — `EVALUATE_RESOLUTION` - `payload_schema`: `seed/canonical/protocol/schemas/operation.schema.json` - `authority_rule`: Evaluation creates no Authority and accepts no external statement as a resolution. -- `binding_rule`: Evaluation observes one resolution_id without mutating Seed-owned state. It derives UNKNOWN when no unique valid terminal record is established; invalid or non-authoritative material cannot override a unique valid record. +- `binding_rule`: Evaluation observes one resolution_id without mutating Seed-owned state. It derives UNKNOWN when no authoritative accepted terminal result is established or when additional conflicting valid terminal material is observed; invalid or non-authoritative material cannot override an otherwise authoritative accepted terminal result. - `created_artifacts`: `ResolutionEvaluation` ## Limite da implementação diff --git a/docs/generated/pt-BR/ASET_Seed_Resolution_0.3-alpha.1.md b/docs/generated/pt-BR/ASET_Seed_Resolution_0.3-alpha.1.md index 1d6d520..9d904b3 100644 --- a/docs/generated/pt-BR/ASET_Seed_Resolution_0.3-alpha.1.md +++ b/docs/generated/pt-BR/ASET_Seed_Resolution_0.3-alpha.1.md @@ -4,7 +4,7 @@ **Status:** `MINIMAL_STRONG_CORE_ALPHA` -**SHA-256 do modelo canônico:** `sha256:54c46e46d4e6b5870353bb0ed229310f60583e9acd11798b655bdd837c8dba74` +**SHA-256 do modelo canônico:** `sha256:d8fde8f21b6524b2442151505f8bf4aec29e17be4a17d2409021ad594597b203` > Esta edição é derivada do cânone legível por máquina. @@ -98,7 +98,7 @@ Predicado: `resolution_domain` ### `ASET-SEED-REQ-004` -Um efeito exatamente vinculado DEVE ser permitido se, e somente se, o único ResolutionRecord terminal válido for ALLOW. +Um efeito exatamente vinculado DEVE ser permitido se, e somente se, o ResolutionRecord terminal autoritativo aceito for ALLOW e nenhum conflito terminal válido for observado. Modalidade: `MUST` @@ -108,7 +108,7 @@ Predicado: `allow_only` ### `ASET-SEED-REQ-005` -UNKNOWN e BLOCK DEVEM proibir o efeito. Estado terminal válido ausente ou ambíguo, ou falha em estabelecer um registro terminal válido, DEVE resultar em UNKNOWN. Material inválido ou não autoritativo NÃO DEVE substituir um registro terminal válido e único. +UNKNOWN e BLOCK DEVEM proibir o efeito. Estado terminal aceito ausente, falha em estabelecer um registro terminal autoritativo ou observação de material terminal válido conflitante adicional DEVE resultar em UNKNOWN. Material inválido ou não autoritativo NÃO DEVE substituir um registro terminal autoritativo já aceito. Modalidade: `MUST` @@ -148,11 +148,11 @@ Predicado: `inputs_non_authoritative` ### `ASET-SEED-REQ-009` -No máximo um registro terminal válido PODE existir para um resolution_id; registros terminais conflitantes DEVEM falhar de modo fechado como UNKNOWN. +O estado pertencente ao Seed DEVE aceitar no máximo um registro terminal para um resolution_id. A observação de material terminal válido distinto adicional para uma resolução terminal já aceita DEVE falhar de modo fechado como UNKNOWN sem substituir o registro aceito. -Modalidade: `MAY` +Modalidade: `MUST` -Predicado: `terminal_unique` +Predicado: `accepted_terminal_unique` `verification`: `ASET-VERIFY-DECLARATIVE-STATE-VALIDATION`, `ASET-VERIFY-PORTABLE-CASES`, `ASET-VERIFY-BOUNDED-MODEL`, `ASET-VERIFY-INVARIANT-COVERAGE`, `ASET-VERIFY-SEMANTIC-MUTATIONS` @@ -189,39 +189,39 @@ Predicado: `implementation_neutral` ## Invariantes - `SEED-INV-001` — Toda resolução derivada válida é UNKNOWN, ALLOW ou BLOCK. -- `SEED-INV-002` — A permissão do efeito é verdadeira se, e somente se, o único registro terminal válido for ALLOW. +- `SEED-INV-002` — A permissão de efeito é verdadeira se, e somente se, o registro terminal autoritativo aceito for ALLOW e nenhum conflito terminal válido for observado. - `SEED-INV-003` — UNKNOWN e BLOCK nunca permitem um efeito. - `SEED-INV-004` — Toda solicitação e registro terminal preservam um único digest exato de vinculação. - `SEED-INV-005` — Todo registro terminal válido usa uma Authority explicitamente reconhecida para a vinculação local exata. - `SEED-INV-006` — Evidência de Authority é não autoritativa até que o reconhecimento de Authority com vinculação exata seja bem-sucedido; material de prova opaco não pode criar ou ampliar Authority por si só. - `SEED-INV-007` — Declarações externas e Evidence ficam fora do estado canônico pertencente ao Seed, salvo quando aceitas por uma transição reconhecida do Seed. -- `SEED-INV-008` — Existe no máximo um registro terminal válido para um resolution_id. -- `SEED-INV-009` — Registros terminais válidos conflitantes resultam em UNKNOWN. Material inválido ou não autoritativo não pode criar ALLOW, criar conflito nem substituir um registro terminal válido e único. +- `SEED-INV-008` — O estado pertencente ao Seed aceita no máximo um registro terminal para um resolution_id. +- `SEED-INV-009` — Uma observação de conflito só é válida para um resolution_id que já possua um registro terminal aceito. Material terminal válido conflitante adicional resulta em UNKNOWN; material inválido ou não autoritativo não pode criar ALLOW, criar conflito nem substituir o registro aceito. - `SEED-INV-010` — Registros de resolução são append-only, imutáveis e endereçados por conteúdo. - `SEED-INV-011` — Somente transições de estado reconhecidas do Seed podem alterar o estado canônico pertencente ao Seed; observações do ambiente e operações de observador não alteram esse estado. - `SEED-INV-012` — A reconsideração usa um resolution_id novo vinculado por um compromisso imutável e endereçado por conteúdo a um ResolutionRecord terminal previamente reconhecido; a retenção do objeto predecessor não é obrigatória. -## Transições +## Operações -### `SEED-TX-001` — `REGISTER_REQUEST` +### `SEED-OP-001` — `REGISTER_REQUEST` - `payload_schema`: `seed/canonical/protocol/schemas/payload-register-request.schema.json` -- `authority_rule`: The initial Authority binding must be locally rooted and exactly match the request binding. +- `authority_rule`: The Authority must be explicitly recognized for the exact request binding. - `binding_rule`: The request contains one canonical exact binding and a fresh resolution_id. For reconsideration, previous_terminal_record_digest must be a recognized immutable terminal-record commitment; predecessor object presence in retained storage is not required. - `created_artifacts`: `ResolutionRequest` -### `SEED-TX-002` — `SUBMIT_RESOLUTION` +### `SEED-OP-002` — `SUBMIT_RESOLUTION` - `payload_schema`: `seed/canonical/protocol/schemas/payload-submit-resolution.schema.json` -- `authority_rule`: The record Authority must be explicitly recognized for the exact request binding. Concrete signatures, delegation chains and proof construction are external validation mechanisms. +- `authority_rule`: The Authority must be explicitly recognized for the exact request binding. Concrete signatures, credentials, delegation mechanisms and proof construction are external validation mechanisms. - `binding_rule`: The record request_digest and binding_digest must exactly match the registered request. - `created_artifacts`: `ResolutionRecord` -### `SEED-TX-003` — `EVALUATE_RESOLUTION` +### `SEED-OP-003` — `EVALUATE_RESOLUTION` - `payload_schema`: `seed/canonical/protocol/schemas/operation.schema.json` - `authority_rule`: Evaluation creates no Authority and accepts no external statement as a resolution. -- `binding_rule`: Evaluation observes one resolution_id without mutating Seed-owned state. It derives UNKNOWN when no unique valid terminal record is established; invalid or non-authoritative material cannot override a unique valid record. +- `binding_rule`: Evaluation observes one resolution_id without mutating Seed-owned state. It derives UNKNOWN when no authoritative accepted terminal result is established or when additional conflicting valid terminal material is observed; invalid or non-authoritative material cannot override an otherwise authoritative accepted terminal result. - `created_artifacts`: `ResolutionEvaluation` ## Limite da implementação diff --git a/docs/generated/ru/ASET_Seed_Next.md b/docs/generated/ru/ASET_Seed_Next.md index 958cbcb..78dcca3 100644 --- a/docs/generated/ru/ASET_Seed_Next.md +++ b/docs/generated/ru/ASET_Seed_Next.md @@ -4,7 +4,7 @@ **Статус:** `MINIMAL_STRONG_CORE_ALPHA` -**SHA-256 канонической модели:** `sha256:54c46e46d4e6b5870353bb0ed229310f60583e9acd11798b655bdd837c8dba74` +**SHA-256 канонической модели:** `sha256:d8fde8f21b6524b2442151505f8bf4aec29e17be4a17d2409021ad594597b203` > Эта редакция выводится из машинного канона. @@ -98,7 +98,7 @@ ResolutionBinding ДОЛЖЕН содержать точные context_id, state ### `ASET-SEED-REQ-004` -Точно связанный эффект ДОЛЖЕН быть разрешён тогда и только тогда, когда единственная действительная терминальная ResolutionRecord имеет значение ALLOW. +Точно связанный эффект ДОЛЖЕН быть разрешён тогда и только тогда, когда принятая авторитетная терминальная ResolutionRecord имеет значение ALLOW и не наблюдается действительный терминальный конфликт. Модальность: `MUST` @@ -108,7 +108,7 @@ ResolutionBinding ДОЛЖЕН содержать точные context_id, state ### `ASET-SEED-REQ-005` -UNKNOWN и BLOCK ДОЛЖНЫ запрещать эффект. Отсутствие или неоднозначность действительного терминального состояния либо невозможность установить действительную терминальную запись ДОЛЖНЫ давать UNKNOWN. Недействительный или неавторитетный материал НЕ ДОЛЖЕН переопределять уже установленную единственную действительную терминальную запись. +UNKNOWN и BLOCK ДОЛЖНЫ запрещать эффект. Отсутствие принятого терминального состояния, невозможность установить авторитетную терминальную запись либо наблюдение дополнительного конфликтующего действительного терминального материала ДОЛЖНЫ давать UNKNOWN. Недействительный или неавторитетный материал НЕ ДОЛЖЕН переопределять уже принятую авторитетную терминальную запись. Модальность: `MUST` @@ -148,11 +148,11 @@ Evidence, результаты проверки, выводы ИИ, резуль ### `ASET-SEED-REQ-009` -Для одного resolution_id МОЖЕТ существовать не более одной действительной терминальной записи; конфликтующие терминальные записи ДОЛЖНЫ давать fail-closed UNKNOWN. +Принадлежащее Seed состояние ДОЛЖНО принимать не более одной терминальной записи для одного resolution_id. Наблюдение дополнительного отличающегося действительного терминального материала для уже принятого терминального разрешения ДОЛЖНО давать fail-closed UNKNOWN без замены принятой записи. -Модальность: `MAY` +Модальность: `MUST` -Предикат: `terminal_unique` +Предикат: `accepted_terminal_unique` `verification`: `ASET-VERIFY-DECLARATIVE-STATE-VALIDATION`, `ASET-VERIFY-PORTABLE-CASES`, `ASET-VERIFY-BOUNDED-MODEL`, `ASET-VERIFY-INVARIANT-COVERAGE`, `ASET-VERIFY-SEMANTIC-MUTATIONS` @@ -189,39 +189,39 @@ Evidence, результаты проверки, выводы ИИ, резуль ## Инварианты - `SEED-INV-001` — Каждое допустимое производное разрешение принадлежит UNKNOWN, ALLOW или BLOCK. -- `SEED-INV-002` — Разрешение эффекта истинно тогда и только тогда, когда единственная действительная терминальная запись равна ALLOW. +- `SEED-INV-002` — Разрешение эффекта истинно тогда и только тогда, когда принятая авторитетная терминальная запись имеет значение ALLOW и не наблюдается действительный терминальный конфликт. - `SEED-INV-003` — UNKNOWN и BLOCK никогда не разрешают эффект. - `SEED-INV-004` — Каждый запрос и терминальная запись сохраняют один точный digest связки. - `SEED-INV-005` — Каждая действительная терминальная запись использует Authority, явно признанную для точной локальной связки. - `SEED-INV-006` — Доказательный материал Authority неавторитетен до успешного точного признания Authority; непрозрачный proof material не может сам по себе создать или расширить полномочие. - `SEED-INV-007` — Внешние утверждения и Evidence находятся вне принадлежащего Seed канонического состояния, пока не приняты признанным переходом Seed. -- `SEED-INV-008` — Для одного resolution_id существует не более одной действительной терминальной записи. -- `SEED-INV-009` — Конфликтующие действительные терминальные записи дают UNKNOWN. Недействительный или неавторитетный материал не может создать ALLOW, создать конфликт или переопределить единственную действительную терминальную запись. +- `SEED-INV-008` — Принадлежащее Seed состояние принимает не более одной терминальной записи для одного resolution_id. +- `SEED-INV-009` — Наблюдение конфликта допустимо только для resolution_id, у которого уже есть принятая терминальная запись. Дополнительный конфликтующий действительный терминальный материал даёт UNKNOWN; недействительный или неавторитетный материал не может создать ALLOW, создать конфликт или заменить принятую запись. - `SEED-INV-010` — Записи разрешения являются append-only, неизменяемыми и контентно-адресуемыми. - `SEED-INV-011` — Только признанные переходы состояния Seed могут изменять принадлежащее Seed каноническое состояние; наблюдения среды и observer-операции его не изменяют. - `SEED-INV-012` — Пересмотр использует свежий resolution_id, связанный неизменяемым контентно-адресуемым коммитментом с ранее признанной терминальной ResolutionRecord; хранение объекта-предшественника не требуется. -## Переходы +## Операции -### `SEED-TX-001` — `REGISTER_REQUEST` +### `SEED-OP-001` — `REGISTER_REQUEST` - `payload_schema`: `seed/canonical/protocol/schemas/payload-register-request.schema.json` -- `authority_rule`: The initial Authority binding must be locally rooted and exactly match the request binding. +- `authority_rule`: The Authority must be explicitly recognized for the exact request binding. - `binding_rule`: The request contains one canonical exact binding and a fresh resolution_id. For reconsideration, previous_terminal_record_digest must be a recognized immutable terminal-record commitment; predecessor object presence in retained storage is not required. - `created_artifacts`: `ResolutionRequest` -### `SEED-TX-002` — `SUBMIT_RESOLUTION` +### `SEED-OP-002` — `SUBMIT_RESOLUTION` - `payload_schema`: `seed/canonical/protocol/schemas/payload-submit-resolution.schema.json` -- `authority_rule`: The record Authority must be explicitly recognized for the exact request binding. Concrete signatures, delegation chains and proof construction are external validation mechanisms. +- `authority_rule`: The Authority must be explicitly recognized for the exact request binding. Concrete signatures, credentials, delegation mechanisms and proof construction are external validation mechanisms. - `binding_rule`: The record request_digest and binding_digest must exactly match the registered request. - `created_artifacts`: `ResolutionRecord` -### `SEED-TX-003` — `EVALUATE_RESOLUTION` +### `SEED-OP-003` — `EVALUATE_RESOLUTION` - `payload_schema`: `seed/canonical/protocol/schemas/operation.schema.json` - `authority_rule`: Evaluation creates no Authority and accepts no external statement as a resolution. -- `binding_rule`: Evaluation observes one resolution_id without mutating Seed-owned state. It derives UNKNOWN when no unique valid terminal record is established; invalid or non-authoritative material cannot override a unique valid record. +- `binding_rule`: Evaluation observes one resolution_id without mutating Seed-owned state. It derives UNKNOWN when no authoritative accepted terminal result is established or when additional conflicting valid terminal material is observed; invalid or non-authoritative material cannot override an otherwise authoritative accepted terminal result. - `created_artifacts`: `ResolutionEvaluation` ## Граница реализации diff --git a/docs/generated/ru/ASET_Seed_Resolution_0.3-alpha.1.md b/docs/generated/ru/ASET_Seed_Resolution_0.3-alpha.1.md index 958cbcb..78dcca3 100644 --- a/docs/generated/ru/ASET_Seed_Resolution_0.3-alpha.1.md +++ b/docs/generated/ru/ASET_Seed_Resolution_0.3-alpha.1.md @@ -4,7 +4,7 @@ **Статус:** `MINIMAL_STRONG_CORE_ALPHA` -**SHA-256 канонической модели:** `sha256:54c46e46d4e6b5870353bb0ed229310f60583e9acd11798b655bdd837c8dba74` +**SHA-256 канонической модели:** `sha256:d8fde8f21b6524b2442151505f8bf4aec29e17be4a17d2409021ad594597b203` > Эта редакция выводится из машинного канона. @@ -98,7 +98,7 @@ ResolutionBinding ДОЛЖЕН содержать точные context_id, state ### `ASET-SEED-REQ-004` -Точно связанный эффект ДОЛЖЕН быть разрешён тогда и только тогда, когда единственная действительная терминальная ResolutionRecord имеет значение ALLOW. +Точно связанный эффект ДОЛЖЕН быть разрешён тогда и только тогда, когда принятая авторитетная терминальная ResolutionRecord имеет значение ALLOW и не наблюдается действительный терминальный конфликт. Модальность: `MUST` @@ -108,7 +108,7 @@ ResolutionBinding ДОЛЖЕН содержать точные context_id, state ### `ASET-SEED-REQ-005` -UNKNOWN и BLOCK ДОЛЖНЫ запрещать эффект. Отсутствие или неоднозначность действительного терминального состояния либо невозможность установить действительную терминальную запись ДОЛЖНЫ давать UNKNOWN. Недействительный или неавторитетный материал НЕ ДОЛЖЕН переопределять уже установленную единственную действительную терминальную запись. +UNKNOWN и BLOCK ДОЛЖНЫ запрещать эффект. Отсутствие принятого терминального состояния, невозможность установить авторитетную терминальную запись либо наблюдение дополнительного конфликтующего действительного терминального материала ДОЛЖНЫ давать UNKNOWN. Недействительный или неавторитетный материал НЕ ДОЛЖЕН переопределять уже принятую авторитетную терминальную запись. Модальность: `MUST` @@ -148,11 +148,11 @@ Evidence, результаты проверки, выводы ИИ, резуль ### `ASET-SEED-REQ-009` -Для одного resolution_id МОЖЕТ существовать не более одной действительной терминальной записи; конфликтующие терминальные записи ДОЛЖНЫ давать fail-closed UNKNOWN. +Принадлежащее Seed состояние ДОЛЖНО принимать не более одной терминальной записи для одного resolution_id. Наблюдение дополнительного отличающегося действительного терминального материала для уже принятого терминального разрешения ДОЛЖНО давать fail-closed UNKNOWN без замены принятой записи. -Модальность: `MAY` +Модальность: `MUST` -Предикат: `terminal_unique` +Предикат: `accepted_terminal_unique` `verification`: `ASET-VERIFY-DECLARATIVE-STATE-VALIDATION`, `ASET-VERIFY-PORTABLE-CASES`, `ASET-VERIFY-BOUNDED-MODEL`, `ASET-VERIFY-INVARIANT-COVERAGE`, `ASET-VERIFY-SEMANTIC-MUTATIONS` @@ -189,39 +189,39 @@ Evidence, результаты проверки, выводы ИИ, резуль ## Инварианты - `SEED-INV-001` — Каждое допустимое производное разрешение принадлежит UNKNOWN, ALLOW или BLOCK. -- `SEED-INV-002` — Разрешение эффекта истинно тогда и только тогда, когда единственная действительная терминальная запись равна ALLOW. +- `SEED-INV-002` — Разрешение эффекта истинно тогда и только тогда, когда принятая авторитетная терминальная запись имеет значение ALLOW и не наблюдается действительный терминальный конфликт. - `SEED-INV-003` — UNKNOWN и BLOCK никогда не разрешают эффект. - `SEED-INV-004` — Каждый запрос и терминальная запись сохраняют один точный digest связки. - `SEED-INV-005` — Каждая действительная терминальная запись использует Authority, явно признанную для точной локальной связки. - `SEED-INV-006` — Доказательный материал Authority неавторитетен до успешного точного признания Authority; непрозрачный proof material не может сам по себе создать или расширить полномочие. - `SEED-INV-007` — Внешние утверждения и Evidence находятся вне принадлежащего Seed канонического состояния, пока не приняты признанным переходом Seed. -- `SEED-INV-008` — Для одного resolution_id существует не более одной действительной терминальной записи. -- `SEED-INV-009` — Конфликтующие действительные терминальные записи дают UNKNOWN. Недействительный или неавторитетный материал не может создать ALLOW, создать конфликт или переопределить единственную действительную терминальную запись. +- `SEED-INV-008` — Принадлежащее Seed состояние принимает не более одной терминальной записи для одного resolution_id. +- `SEED-INV-009` — Наблюдение конфликта допустимо только для resolution_id, у которого уже есть принятая терминальная запись. Дополнительный конфликтующий действительный терминальный материал даёт UNKNOWN; недействительный или неавторитетный материал не может создать ALLOW, создать конфликт или заменить принятую запись. - `SEED-INV-010` — Записи разрешения являются append-only, неизменяемыми и контентно-адресуемыми. - `SEED-INV-011` — Только признанные переходы состояния Seed могут изменять принадлежащее Seed каноническое состояние; наблюдения среды и observer-операции его не изменяют. - `SEED-INV-012` — Пересмотр использует свежий resolution_id, связанный неизменяемым контентно-адресуемым коммитментом с ранее признанной терминальной ResolutionRecord; хранение объекта-предшественника не требуется. -## Переходы +## Операции -### `SEED-TX-001` — `REGISTER_REQUEST` +### `SEED-OP-001` — `REGISTER_REQUEST` - `payload_schema`: `seed/canonical/protocol/schemas/payload-register-request.schema.json` -- `authority_rule`: The initial Authority binding must be locally rooted and exactly match the request binding. +- `authority_rule`: The Authority must be explicitly recognized for the exact request binding. - `binding_rule`: The request contains one canonical exact binding and a fresh resolution_id. For reconsideration, previous_terminal_record_digest must be a recognized immutable terminal-record commitment; predecessor object presence in retained storage is not required. - `created_artifacts`: `ResolutionRequest` -### `SEED-TX-002` — `SUBMIT_RESOLUTION` +### `SEED-OP-002` — `SUBMIT_RESOLUTION` - `payload_schema`: `seed/canonical/protocol/schemas/payload-submit-resolution.schema.json` -- `authority_rule`: The record Authority must be explicitly recognized for the exact request binding. Concrete signatures, delegation chains and proof construction are external validation mechanisms. +- `authority_rule`: The Authority must be explicitly recognized for the exact request binding. Concrete signatures, credentials, delegation mechanisms and proof construction are external validation mechanisms. - `binding_rule`: The record request_digest and binding_digest must exactly match the registered request. - `created_artifacts`: `ResolutionRecord` -### `SEED-TX-003` — `EVALUATE_RESOLUTION` +### `SEED-OP-003` — `EVALUATE_RESOLUTION` - `payload_schema`: `seed/canonical/protocol/schemas/operation.schema.json` - `authority_rule`: Evaluation creates no Authority and accepts no external statement as a resolution. -- `binding_rule`: Evaluation observes one resolution_id without mutating Seed-owned state. It derives UNKNOWN when no unique valid terminal record is established; invalid or non-authoritative material cannot override a unique valid record. +- `binding_rule`: Evaluation observes one resolution_id without mutating Seed-owned state. It derives UNKNOWN when no authoritative accepted terminal result is established or when additional conflicting valid terminal material is observed; invalid or non-authoritative material cannot override an otherwise authoritative accepted terminal result. - `created_artifacts`: `ResolutionEvaluation` ## Граница реализации diff --git a/docs/repository/BLACK_BOX_AUDIT_METHOD.md b/docs/repository/BLACK_BOX_AUDIT_METHOD.md index 4b63ee1..f750ed4 100644 --- a/docs/repository/BLACK_BOX_AUDIT_METHOD.md +++ b/docs/repository/BLACK_BOX_AUDIT_METHOD.md @@ -1,19 +1,52 @@ # Black-box audit method -The final `Check` step of every PDCA cycle evaluates only the deterministic repository snapshot and the public runtime interface. It does not trust internal pass records or import the repository validator. - -## Documentation black-box boundary - -The snapshot auditor performs 28 independent checks: archive safety and CRC; exact manifest scope and hashes; license and citation; claim boundaries; mandatory gates and findings; frozen and expanded rc11 byte identity; requirements, traceability and conformance inventories; strict JSON; Python syntax; generated multilingual parity; migration completeness; required documents and local links; terminology and secret scanning; workflows; Git byte preservation; rc12 canon counts; canonical/runtime schema identity; installable runtime presence; bounded-profile exclusions; formal projection; absence of implicit effect adapters; residual limitations; and complete production-gate registration. - -## Runtime black-box boundary - -The runtime auditor extracts the built snapshot and uses only `python -m aset_seed`. It verifies durable initialization, fail-closed invalid proof handling, accepted signed transition commit, replay idempotency, process-reopen validation, database and audit health, consistent semantic backup, exact-content HMAC binding, invalid identifier handling, corrupt-state isolation, and audit-tampering detection. - -## Adversarial step - -The mutation harness rebuilds a valid manifest after each malicious change. It must still reject removal or drift of required documents, generated editions, frozen rc11 bytes, Git byte policy, migration coverage, runtime files, protocol schemas, formal model, limitation records and release gates; it also rejects a secret marker, readiness overclaim, open blocking finding, and implicit network/effect import. - -Any failed mandatory check forms a finding for the next PDCA cycle. A cycle may close only with zero failed black-box checks and zero open blocking findings. - -The final documentation audit also verifies that technical freeze readiness is explicit while owner approval and exact-byte freeze remain pending. +The active black-box audit evaluates the exact repository snapshot from public +repository artifacts and deterministic commands. It does not treat historical +runtime evidence as controlling evidence for Seed 0.3. + +## Active documentation boundary + +`tools/blackbox_documentation_audit.py` checks the curated active documentation +surface, generated multilingual Seed editions, language navigation, the active +audit classification, implementation-neutrality claims, and prohibited legacy +runtime/readiness claims. Every file under `audit/` must be classified as +active, historical, or explicitly excluded by `ACTIVE_AUDIT_INDEX.json`. + +The method document itself is part of the active documentation surface so that +the description of the gate cannot silently diverge from the gate. + +## Canon and assurance boundary + +The repository release gate independently requires: + +- deterministic repository-view parity; +- machine-canon and canon-package validation; +- exhaustive finite-state saturation for the published finite fixture; +- semantic mutation closure; +- requirement/invariant/operation coverage; +- assurance and proof traceability; +- standalone canon-to-TLA projection parity; +- TLC model checking; +- TLAPS safety proofs; +- TLAPS canon-to-TLA behavioral-equivalence proof; +- specification tests, lint/sanity checks, archive construction and manifest + parity. + +These checks establish consistency and the declared safety properties of the +exact candidate snapshot. They do not establish implementation production +readiness, cryptographic security, factual truth of external evidence, or +correctness of mechanisms intentionally outside the Seed boundary. + +## Historical evidence + +RC11/RC12 runtime, SQLite, HMAC, permit, outcome, membership and related audit +records are preserved as historical evidence. They are non-controlling for the +active Seed 0.3 minimal resolution-recognition semantics unless explicitly +listed as active by `ACTIVE_AUDIT_INDEX.json`. + +## Failure rule + +Any mandatory failing gate or unclassified active audit artifact is a blocking +finding for the candidate snapshot. A candidate may be treated as release-gate +closed only when the aggregate repository release gate passes for that exact +snapshot. diff --git a/docs/repository/CI_ASSURANCE.md b/docs/repository/CI_ASSURANCE.md index c7a856c..2dcdfe7 100644 --- a/docs/repository/CI_ASSURANCE.md +++ b/docs/repository/CI_ASSURANCE.md @@ -86,7 +86,7 @@ The canon-to-TLA theorem is scoped to the declared abstraction profile. It does - equivalence of every natural-language sentence; - concrete Binding/digest construction; -- concrete Authority-recognition evidence, signature or delegation-chain construction; +- concrete Authority-recognition evidence, signature or delegation-mechanism construction; - implementation refinement or production readiness; - liveness; - cryptographic primitive security; diff --git a/seed/canonical/CANON_PACKAGE.json b/seed/canonical/CANON_PACKAGE.json index 54cb356..f28fc64 100644 --- a/seed/canonical/CANON_PACKAGE.json +++ b/seed/canonical/CANON_PACKAGE.json @@ -6,11 +6,11 @@ "files": [ { "path": "seed/canonical/source/seed-model.json", - "sha256": "sha256:c43ca7b642a11c3ab140884a6bbff34bbd741f5cb905e6a779c860c813998fcf" + "sha256": "sha256:1fed5dc95045a287b3e9b8b4ea011a7b977729158f3360ed9a8a7e7e6ba1b4b0" }, { "path": "seed/canonical/schemas/seed-model.schema.json", - "sha256": "sha256:1f1a727764b5d0138951f76fac1ab1155f4ba67c92f21aa8a21f7ef105bf9f94" + "sha256": "sha256:d454d6bc54aa8247ed35ab64d56c8702ba889243bb81f600a8edfbd9ee4fda89" }, { "path": "seed/canonical/protocol/protocol-profile.json", @@ -26,7 +26,7 @@ }, { "path": "seed/canonical/conformance/conformance-profile.json", - "sha256": "sha256:aabbf317e0c51a1a1f1021dfbd0b2981c3dcf1142b89eb6a1bbfb1c7e1e9dcd6" + "sha256": "sha256:8b5aaa3b5890315f001ee68257c9a316d1523000db26ddd9b112fd16456f2cf4" }, { "path": "seed/canonical/schemas/conformance-profile.schema.json", @@ -46,23 +46,23 @@ }, { "path": "seed/canonical/conformance/model-based-conformance.json", - "sha256": "sha256:db4b3f9e76aff7e8ef3a87f02ae748bb4f718428370306454eb94b9dcc6212b4" + "sha256": "sha256:5cae29741da3488563cf026a04c9918d26d48fcd58db65607c25beb8c8705c08" }, { "path": "seed/canonical/assurance/verification-registry.json", - "sha256": "sha256:b4bb28e5a8965e984013ad7408522749cfef3008c913a518f455fefda7136187" + "sha256": "sha256:cc5f2c5b4ce0c9e466bb63779c1199817859e4d65d6df204acfaa3619b1f819c" }, { "path": "seed/canonical/assurance/invariant-coverage.json", - "sha256": "sha256:2d89e21d092bf4d340e271dc3bcba2d7df618c4c4b41e67beb626f518cdb163b" + "sha256": "sha256:0ffed8e2b1351928d9921c96bab4d8225504cf77e7298a0c8a603b66ac71e2c7" }, { "path": "seed/canonical/schemas/invariant-coverage.schema.json", - "sha256": "sha256:e7ec1a6577df2519ca49f8c682588d68d767f9d28ab3301a6280221100ddc5b3" + "sha256": "sha256:9831e12343697216eac28a82b29baeb160a360e4e0126fcb356d904227b69ded" }, { "path": "seed/canonical/assurance/proof-traceability.json", - "sha256": "sha256:043bb3b1717d0c41123d326dc9b1d8dcae1cdde78c7ebf2d2ae26e79d2248eaf" + "sha256": "sha256:eaa97bb7aa9b09554ef4b1624dacac219a8a6ee24fdb8809cf203d1badffb0a2" }, { "path": "seed/canonical/schemas/proof-traceability.schema.json", @@ -70,11 +70,11 @@ }, { "path": "seed/canonical/assurance/canon-tla-refinement.json", - "sha256": "sha256:2095b62595d056c8a5a3b0700239a0211417979e4d5f2b4a535df0827017371b" + "sha256": "sha256:22884e71f1a484a8a7b00f708188191783505a71d1b2d15ad73cca67510099a5" }, { "path": "seed/canonical/schemas/canon-tla-refinement.schema.json", - "sha256": "sha256:17b142a998bbc8dd7b82b61c54d75e0c0e735211f35f90312565b78a4e7758e5" + "sha256": "sha256:ccd44d46cd3e9075fd439ead6a08cf3685d62bdea7f76d7ab2a736b579706069" }, { "path": "seed/canonical/assurance/limitations.json", @@ -98,23 +98,23 @@ }, { "path": "seed/canonical/formal/SeedResolution.tla", - "sha256": "sha256:1c53b058d738e074c2a9de96fe27d8d7dd384d3ffa52f3bb95f7732908d66276" + "sha256": "sha256:1c0ebb27ed52da289f0981dcb11b61b6a7fc5c4a030ba434ae0b1d53b286b926" }, { "path": "seed/canonical/formal/SeedResolutionProofs.tla", - "sha256": "sha256:bcb4652249d66cbcb16f7c5a4538ad3bc2c31ef7d37b49fd27328eff6a6725f9" + "sha256": "sha256:3d6bdada8c1c0f93c247eb5c5b4df895e793c174768270138f2d6e6176990ad7" }, { "path": "seed/canonical/formal/SeedCanonProjection.tla", - "sha256": "sha256:b7265eb707795b592c678842f764a5bfa7ce303bdc66f55f858366e20d64eb4e" + "sha256": "sha256:b3bf0555abba2fc9e817d1c3e97b93d62af933edfb9c7f5e7eec4502445447f5" }, { "path": "seed/canonical/formal/SeedCanonRefinementProofs.tla", - "sha256": "sha256:46ef7336b86d066ee531eb2c43873d9b6e1622dd48632b9af08ea6f412cf6338" + "sha256": "sha256:522338cc774f1f473d20130630e01aec6b66a2ac971ffed113b8a91d654b72ad" }, { "path": "seed/canonical/formal/SeedResolution.cfg", - "sha256": "sha256:b4ee7fb775fbf8909fded4e7b2086b8022e1412e648e21f470c464a625f690c0" + "sha256": "sha256:bee70a11c1bde1e0b7aaa0acefbe5a4137bdcd5c3fbea254a3d8a1999086f1b7" }, { "path": "seed/canonical/migration/ALPHA2_TO_0.3_ALPHA1_CHANGE_DECLARATION.json", @@ -140,9 +140,13 @@ "path": "seed/canonical/decisions/ADR-009-seed-state-environment-observer-and-authority-boundary.md", "sha256": "sha256:fdb642c8f306d2136345e19c3650c22805f63139ac93d8f81f6773aa249881a0" }, + { + "path": "seed/canonical/decisions/ADR-010-unify-authority-conflict-and-operation-semantics.md", + "sha256": "sha256:e9757a2879f7e6ce6c9b087212dbcc4cf2c74085f6b1e09be5fdfd4a7b236078" + }, { "path": "seed/canonical/migration/CANON_CHANGE_DECLARATION.json", - "sha256": "sha256:4eb176ddb006c0957a2bf1d79685fd86b263b89500cc53df919193ec91459bf8" + "sha256": "sha256:2bc5d60abed02040dd41c79db86aa23cbf206bf81df8193f771ceb9b8a29541c" }, { "path": "seed/canonical/migration/WIRE_V2_TO_V3.md", @@ -270,7 +274,7 @@ }, { "path": "seed/canonical/conformance/cases/positive/RES-POS-004.json", - "sha256": "sha256:dcf5f81b0e60f2aa0c157aab5297177d3f082544d64a54081d83e9d7d6093763" + "sha256": "sha256:b7407ed453ab3dd20d36ab3dd540d7c9c0c002df8821c40455b181b425093eef" }, { "path": "seed/canonical/conformance/cases/positive/RES-POS-005.json", @@ -295,6 +299,6 @@ ], "implementation_precedence": "NONE", "normative_source": "seed/canonical/source/seed-model.json", - "package_digest": "sha256:392ff8e36eecb2bf6cfa9a6cbc76117025a4c7d8a170e8ddf562f1ea5df27d38", + "package_digest": "sha256:0e1518c4ff6bd6b0da71089bfe5e1a9802929016c8ec2547024a1a0e2b84a19d", "schema_version": 2 } diff --git a/seed/canonical/README.md b/seed/canonical/README.md index cca6a99..3df3f2e 100644 --- a/seed/canonical/README.md +++ b/seed/canonical/README.md @@ -5,11 +5,12 @@ ASET Seed is a local resolution-recognition kernel. Resolution = UNKNOWN | ALLOW | BLOCK EffectPermitted(r) iff ResolutionOf(r) = ALLOW -A valid terminal `ALLOW` or `BLOCK` is immutable and exact-binding. `UNKNOWN` -is derived when no unique valid terminal record can be established or when -valid terminal material conflicts. Invalid or non-authoritative material cannot -create Authority, create `ALLOW`, create a valid conflict, or override an -otherwise unique valid terminal record. +An accepted terminal `ALLOW` or `BLOCK` is immutable and exact-binding. +`UNKNOWN` is derived when no authoritative accepted terminal record is +established or when additional distinct valid terminal material conflicts with +an accepted terminal resolution. Invalid or non-authoritative material cannot +create Authority, create `ALLOW`, create a valid conflict, or replace an +accepted authoritative terminal record. Seed normatively defines: @@ -17,7 +18,7 @@ Seed normatively defines: - fresh request identity and reconsideration commitment; - exact-binding local Authority recognition as an admission boundary; - immutable content-addressed terminal records; -- terminal uniqueness and fail-closed evaluation; +- accepted-terminal uniqueness, conflict soundness and fail-closed evaluation; - implementation-neutral observable semantics. Concrete policy evaluation, evidence acquisition, signatures, delegation-chain @@ -41,7 +42,7 @@ conflict observation cannot mutate Seed-owned state. The active assurance surface contains: - 12 canonical requirements and 12 canonical invariants; -- 3 canonical operations: two state transitions and one observer; +- 3 canonical operations (`SEED-OP-001..003`): two state transitions and one observer; - 25 portable conformance cases; - 13 semantic mutations; - 14 TLA/TLC properties: 10 state invariants and 4 temporal properties; diff --git a/seed/canonical/assurance/canon-tla-refinement.json b/seed/canonical/assurance/canon-tla-refinement.json index d5df439..6a0fa3a 100644 --- a/seed/canonical/assurance/canon-tla-refinement.json +++ b/seed/canonical/assurance/canon-tla-refinement.json @@ -5,7 +5,7 @@ "id": "OPAQUE_BINDING" }, { - "description": "RequestAuthorityBindings and TerminalAuthorityBindings represent already-recognized exact-binding Authority facts. Concrete signatures, delegation chains, federation proof material and their validation are external to Seed.", + "description": "RecognizedAuthorityBindings represents already-recognized exact-binding Authority facts shared by request registration and terminal submission. Concrete signatures, credentials, delegation mechanisms, federation proof material and their validation are external to Seed.", "id": "AUTHORITY_RECOGNITION_BOUNDARY" }, { @@ -13,11 +13,11 @@ "id": "TERMINAL_COMMITMENT_ORACLE" }, { - "description": "Conflict is modeled separately from Seed-owned state because an independently established conflicting valid terminal record changes the derived resolution while not mutating accepted request or terminal state.", + "description": "Conflict is environment state and may be observed only for a resolution_id with an already accepted terminal record; additional distinct valid terminal material changes the derived resolution to UNKNOWN without mutating accepted Seed state.", "id": "ENVIRONMENT_CONFLICT_STATE" } ], - "claim_boundary": "The proof establishes behavioral equivalence between SeedResolution.tla and a standalone TLA+ projection generated from the exact machine-readable Seed model under ASET-SEED-CANON-TLA-PROJECTION-V4. The generated projection does not import or extend SeedResolution; the proof explicitly instantiates the independent projection onto the target state. Opaque Binding construction, concrete Authority-recognition evidence, terminal-commitment provenance, cryptographic primitives, implementation refinement, liveness and natural-language completeness remain outside this proof boundary. The deterministic generator remains part of the assurance trusted computing base.", + "claim_boundary": "The proof establishes behavioral equivalence between SeedResolution.tla and a standalone TLA+ projection generated from the exact machine-readable Seed model under ASET-SEED-CANON-TLA-PROJECTION-V5. The generated projection does not import or extend SeedResolution; the proof explicitly instantiates the independent projection onto the target state. Opaque Binding construction, concrete Authority-recognition evidence, terminal-commitment provenance, cryptographic primitives, implementation refinement, liveness and natural-language completeness remain outside this proof boundary. The deterministic generator remains part of the assurance trusted computing base.", "document_type": "aset-canon-tla-refinement", "excluded_claims": [ "natural-language-text equivalence", @@ -33,7 +33,7 @@ "generator": "tools/generate_canon_tla_projection.py", "module": "SeedCanonProjection", "path": "seed/canonical/formal/SeedCanonProjection.tla", - "profile": "ASET-SEED-CANON-TLA-PROJECTION-V4" + "profile": "ASET-SEED-CANON-TLA-PROJECTION-V5" }, "invariant_coverage": [ { @@ -85,6 +85,26 @@ "status": "PARTIAL_TERMINAL_COMMITMENT_ABSTRACTION" } ], + "operation_coverage": [ + { + "id": "SEED-OP-001", + "kind": "REGISTER_REQUEST", + "status": "PROVED_IN_DECLARED_PROJECTION", + "tla_action": "RegisterRequest" + }, + { + "id": "SEED-OP-002", + "kind": "SUBMIT_RESOLUTION", + "status": "PROVED_IN_DECLARED_PROJECTION", + "tla_action": "SubmitResolution" + }, + { + "id": "SEED-OP-003", + "kind": "EVALUATE_RESOLUTION", + "status": "OBSERVER_EQUIVALENCE_PROVED", + "tla_action": "EvaluateResolution" + } + ], "proof": { "final_theorem": "SeedResolutionBehaviorallyEquivalentToCanonProjection", "module": "seed/canonical/formal/SeedCanonRefinementProofs.tla", @@ -134,7 +154,7 @@ }, { "id": "ASET-SEED-REQ-009", - "predicate": "terminal_unique", + "predicate": "accepted_terminal_unique", "status": "PROVED_IN_DECLARED_PROJECTION" }, { @@ -167,32 +187,12 @@ "source_model": { "model_id": "ASET-SEED-RESOLUTION-CANON-0.3-ALPHA1", "path": "seed/canonical/source/seed-model.json", - "sha256": "sha256:c43ca7b642a11c3ab140884a6bbff34bbd741f5cb905e6a779c860c813998fcf", + "sha256": "sha256:1fed5dc95045a287b3e9b8b4ea011a7b977729158f3360ed9a8a7e7e6ba1b4b0", "version": "0.3.0-alpha.1" }, "target_model": { "module": "SeedResolution", "path": "seed/canonical/formal/SeedResolution.tla", - "sha256": "sha256:1c53b058d738e074c2a9de96fe27d8d7dd384d3ffa52f3bb95f7732908d66276" - }, - "transition_coverage": [ - { - "id": "SEED-TX-001", - "kind": "REGISTER_REQUEST", - "status": "PROVED_IN_DECLARED_PROJECTION", - "tla_action": "RegisterRequest" - }, - { - "id": "SEED-TX-002", - "kind": "SUBMIT_RESOLUTION", - "status": "PROVED_IN_DECLARED_PROJECTION", - "tla_action": "SubmitResolution" - }, - { - "id": "SEED-TX-003", - "kind": "EVALUATE_RESOLUTION", - "status": "OBSERVER_EQUIVALENCE_PROVED", - "tla_action": "EvaluateResolution" - } - ] + "sha256": "sha256:1c0ebb27ed52da289f0981dcb11b61b6a7fc5c4a030ba434ae0b1d53b286b926" + } } diff --git a/seed/canonical/assurance/invariant-coverage.json b/seed/canonical/assurance/invariant-coverage.json index ac3dc5d..6113c9a 100644 --- a/seed/canonical/assurance/invariant-coverage.json +++ b/seed/canonical/assurance/invariant-coverage.json @@ -23,10 +23,10 @@ "conformance_case_required": true, "formal_property_required": true, "invariants_complete": true, + "operations_complete": true, "orphan_evidence_forbidden": true, "requirements_complete": true, - "semantic_mutation_required": true, - "transitions_complete": true + "semantic_mutation_required": true }, "document_type": "aset-seed-invariant-coverage", "invariants": [ @@ -140,7 +140,7 @@ "RES-NEG-015" ], "formal_properties": [ - "TerminalUnique" + "AcceptedTerminalUnique" ], "id": "SEED-INV-008", "semantic_mutations": [ @@ -156,7 +156,7 @@ ], "formal_properties": [ "FailClosed", - "ConflictUnknown", + "ConflictSound", "ExternalMaterialNonAuthoritative" ], "id": "SEED-INV-009", @@ -392,6 +392,54 @@ } ], "normative": true, + "operations": [ + { + "id": "SEED-OP-001", + "negative_cases": [ + "RES-NEG-001", + "RES-NEG-002", + "RES-NEG-003", + "RES-NEG-004", + "RES-NEG-011", + "RES-NEG-012", + "RES-NEG-013" + ], + "positive_cases": [ + "RES-POS-001", + "RES-POS-008" + ] + }, + { + "id": "SEED-OP-002", + "negative_cases": [ + "RES-NEG-005", + "RES-NEG-006", + "RES-NEG-007", + "RES-NEG-008", + "RES-NEG-009", + "RES-NEG-010", + "RES-NEG-016" + ], + "positive_cases": [ + "RES-POS-002", + "RES-POS-003", + "RES-POS-004", + "RES-POS-005", + "RES-POS-007" + ] + }, + { + "id": "SEED-OP-003", + "negative_cases": [ + "RES-NEG-014", + "RES-NEG-015" + ], + "positive_cases": [ + "RES-POS-006", + "RES-POS-009" + ] + } + ], "requirements": [ { "conformance_cases": [ @@ -474,7 +522,7 @@ ], "formal_properties": [ "FailClosed", - "ConflictUnknown" + "ConflictSound" ], "id": "ASET-SEED-REQ-005", "invariants": [ @@ -547,8 +595,8 @@ "RES-NEG-015" ], "formal_properties": [ - "TerminalUnique", - "ConflictUnknown" + "AcceptedTerminalUnique", + "ConflictSound" ], "id": "ASET-SEED-REQ-009", "invariants": [ @@ -610,53 +658,5 @@ ] } ], - "schema_version": 1, - "transitions": [ - { - "id": "SEED-TX-001", - "negative_cases": [ - "RES-NEG-001", - "RES-NEG-002", - "RES-NEG-003", - "RES-NEG-004", - "RES-NEG-011", - "RES-NEG-012", - "RES-NEG-013" - ], - "positive_cases": [ - "RES-POS-001", - "RES-POS-008" - ] - }, - { - "id": "SEED-TX-002", - "negative_cases": [ - "RES-NEG-005", - "RES-NEG-006", - "RES-NEG-007", - "RES-NEG-008", - "RES-NEG-009", - "RES-NEG-010", - "RES-NEG-016" - ], - "positive_cases": [ - "RES-POS-002", - "RES-POS-003", - "RES-POS-004", - "RES-POS-005", - "RES-POS-007" - ] - }, - { - "id": "SEED-TX-003", - "negative_cases": [ - "RES-NEG-014", - "RES-NEG-015" - ], - "positive_cases": [ - "RES-POS-006", - "RES-POS-009" - ] - } - ] + "schema_version": 1 } diff --git a/seed/canonical/assurance/proof-traceability.json b/seed/canonical/assurance/proof-traceability.json index c545a14..3670c3b 100644 --- a/seed/canonical/assurance/proof-traceability.json +++ b/seed/canonical/assurance/proof-traceability.json @@ -135,7 +135,7 @@ "formal_projection": [ { "kind": "STATE_INVARIANT", - "operator": "TerminalUnique", + "operator": "AcceptedTerminalUnique", "proof_theorem": "SpecImpliesAlwaysSeedStateSafety" } ], @@ -153,7 +153,7 @@ "formal_projection": [ { "kind": "STATE_INVARIANT", - "operator": "ConflictUnknown", + "operator": "ConflictSound", "proof_theorem": "SpecImpliesAlwaysSeedStateSafety" } ], diff --git a/seed/canonical/assurance/verification-registry.json b/seed/canonical/assurance/verification-registry.json index e25cf71..566a917 100644 --- a/seed/canonical/assurance/verification-registry.json +++ b/seed/canonical/assurance/verification-registry.json @@ -91,7 +91,7 @@ { "engine": "TLA_TLC", "kind": "STATE_INVARIANT", - "name": "TerminalUnique", + "name": "AcceptedTerminalUnique", "projection_status": "STRUCTURAL_BY_CONSTRUCTION", "seed_invariants": [ "SEED-INV-008" @@ -103,7 +103,7 @@ { "engine": "TLA_TLC", "kind": "STATE_INVARIANT", - "name": "ConflictUnknown", + "name": "ConflictSound", "projection_status": "BOUNDED_ABSTRACTION", "seed_invariants": [ "SEED-INV-009" @@ -244,12 +244,12 @@ } ], "normative": true, - "schema_version": 4, - "transition_case_policy": { + "operation_case_policy": { "declared_exceptions": [], "require_negative_case": true, "require_positive_case": true }, + "schema_version": 4, "verification_methods": [ { "evidence": "seed/canonical/conformance/conformance-profile.json", diff --git a/seed/canonical/conformance/cases/positive/RES-POS-004.json b/seed/canonical/conformance/cases/positive/RES-POS-004.json index 1a170e8..ad8cbf6 100644 --- a/seed/canonical/conformance/cases/positive/RES-POS-004.json +++ b/seed/canonical/conformance/cases/positive/RES-POS-004.json @@ -19,7 +19,7 @@ } }, "case_id": "RES-POS-004", - "description": "Record ALLOW through one exact-binding Authority grant.", + "description": "Record ALLOW through an independently recognized exact-binding Authority.", "expected": { "accepted": true, "code": "RESOLUTION_RECORDED", diff --git a/seed/canonical/conformance/conformance-profile.json b/seed/canonical/conformance/conformance-profile.json index 90af44d..f9b6626 100644 --- a/seed/canonical/conformance/conformance-profile.json +++ b/seed/canonical/conformance/conformance-profile.json @@ -279,7 +279,7 @@ }, "path": "seed/canonical/conformance/cases/positive/RES-POS-004.json", "polarity": "positive", - "sha256": "sha256:dcf5f81b0e60f2aa0c157aab5297177d3f082544d64a54081d83e9d7d6093763" + "sha256": "sha256:b7407ed453ab3dd20d36ab3dd540d7c9c0c002df8821c40455b181b425093eef" }, { "case_id": "RES-POS-005", diff --git a/seed/canonical/conformance/model-based-conformance.json b/seed/canonical/conformance/model-based-conformance.json index 53abf70..cb5c32b 100644 --- a/seed/canonical/conformance/model-based-conformance.json +++ b/seed/canonical/conformance/model-based-conformance.json @@ -1,14 +1,14 @@ { "document_type": "aset-model-based-conformance", "model": { - "command_set": "REGISTER_REQUEST and SUBMIT_RESOLUTION are state transitions; EVALUATE_RESOLUTION is a pure observer.", + "command_set": "REGISTER_REQUEST and SUBMIT_RESOLUTION are state transitions; EVALUATE_RESOLUTION is a pure observer. Together they form the three-operation Seed interface.", "formal_projection": "seed/canonical/formal/SeedResolution.tla", "state_set": "Seed-owned request/terminal metadata plus separate environment conflict observations satisfying the active minimal Seed invariants.", "transition_relation": "delta(seed_state, environment_state, operation) mutates Seed-owned state only for recognized REGISTER_REQUEST or SUBMIT_RESOLUTION operations; conflict observation changes only environment state; EVALUATE_RESOLUTION observes without mutation." }, "normative": true, "profile_boundary": "Policy evaluation, evidence acquisition, workflow, enforcement, federation, storage and cryptographic mechanisms are extension or implementation responsibilities.", - "resolution_obligation": "UNKNOWN is derived when no unique valid terminal record can be established or valid terminal material conflicts. Invalid/non-authoritative material cannot override an otherwise unique valid record. Only ALLOW permits the effect.", + "resolution_obligation": "UNKNOWN is derived when no authoritative accepted terminal record is established or additional conflicting valid terminal material is observed for an accepted terminal resolution. Invalid/non-authoritative material cannot override an accepted authoritative record. Only ALLOW permits the effect.", "schema_version": 3, - "transition_boundary_obligation": "Only recognized Seed state transitions may change Seed-owned state. Environment conflict observation and observer operations do not mutate Seed-owned state; invalid/unrecognized material cannot become accepted state by mere presence." + "state_change_boundary_obligation": "Only recognized Seed state transitions may change Seed-owned state. Environment conflict observation and observer operations do not mutate Seed-owned state; invalid/unrecognized material cannot become accepted state by mere presence." } diff --git a/seed/canonical/decisions/ADR-010-unify-authority-conflict-and-operation-semantics.md b/seed/canonical/decisions/ADR-010-unify-authority-conflict-and-operation-semantics.md new file mode 100644 index 0000000..c12561e --- /dev/null +++ b/seed/canonical/decisions/ADR-010-unify-authority-conflict-and-operation-semantics.md @@ -0,0 +1,57 @@ +# ADR-010 — Unify Authority recognition, conflict admissibility and operation semantics + +## Status + +Accepted. Refines ADR-009 for the active Seed 0.3 alpha model. Historical +artifacts are not rewritten. + +## Context + +After the deep semantic cleanup, three residual mismatches remained between the +machine canon, wire semantics and formal abstraction: + +1. the formal model exposed separate request and terminal Authority-recognition + relations although the wire model has one exact-binding AuthorityBinding + type and one recognition store; +2. environment conflict observation was allowed before any terminal record had + been accepted, although concrete conflict requires additional distinct valid + terminal material for an existing terminal resolution; +3. `EVALUATE_RESOLUTION` was correctly modeled as an observer but remained + stored under a machine-canon collection named `transitions` with a + `SEED-TX-*` identifier. + +The phrase “at most one valid terminal record exists” also conflated globally +observed valid material with the single terminal record accepted into Seed-owned +state. + +## Decision + +The active Seed model uses: + +- one immutable `RecognizedAuthorityBindings` relation for exact-binding + Authority recognition in both request registration and terminal submission; +- conflict observation only for a `resolution_id` already present in + `TerminalRequests` and not already conflicted; +- `AcceptedTerminalUnique` for the structural single terminal cell in + Seed-owned state; +- `ConflictSound` for the rule that conflict state is a subset of accepted + terminal requests and always derives `UNKNOWN`; +- a machine-canon `operations` catalogue with identifiers `SEED-OP-001` through + `SEED-OP-003`, containing two `STATE_TRANSITION` operations and one + `OBSERVER` operation; +- standalone canon-to-TLA projection profile + `ASET-SEED-CANON-TLA-PROJECTION-V5`. + +## Consequences + +- formal Authority admission now matches the single wire AuthorityBinding + semantics instead of introducing an unexpressed terminal-only privilege; +- impossible pre-request/pre-terminal conflict states are no longer reachable; +- the finite model reports only states reachable under the concrete conflict + boundary; +- accepted terminal uniqueness no longer claims that additional valid external + terminal material cannot exist; such material is represented by conflict; +- generated documentation describes three operations rather than three + transitions; +- this is a breaking machine-canon shape change inside the 0.3 alpha line and + is explicitly declared as such by the canon change declaration. diff --git a/seed/canonical/formal/README.md b/seed/canonical/formal/README.md index 50b4109..27038c2 100644 --- a/seed/canonical/formal/README.md +++ b/seed/canonical/formal/README.md @@ -19,15 +19,11 @@ state dimensions. `Requests` and `TerminalRequests` are partial-map domains. ## Authority and external-material boundary -`RequestAuthorityBindings` and `TerminalAuthorityBindings` are immutable -abstract recognition relations. They mean that Authority recognition has -already succeeded for an exact binding; the formal model does not interpret -signatures, credentials or delegation chains. +`RecognizedAuthorityBindings` is the single immutable abstract recognition relation. It means that Authority recognition has already succeeded for an exact binding and is used consistently by both request registration and terminal submission; the formal model does not interpret signatures, credentials or delegation mechanisms. Invalid or non-authoritative material has no state variable and no artificial transition. It cannot enter accepted state by construction of the admission -boundary. The TLA model covers conflict between valid terminal material as an -environment observation. +boundary. The TLA model covers additional distinct valid terminal material as an environment observation only after a terminal record has already been accepted. ## Checked properties @@ -46,7 +42,7 @@ The final TLAPS theorem surface is: ## Canon-to-TLA relation `SeedCanonProjection.tla` is generated under -`ASET-SEED-CANON-TLA-PROJECTION-V4` as a **standalone module**. It does not +`ASET-SEED-CANON-TLA-PROJECTION-V5` as a **standalone module**. It does not `EXTEND` or instantiate `SeedResolution`. `SeedCanonRefinementProofs.tla` explicitly instantiates the standalone projection onto the handwritten model and proves evaluator and behavioral equivalence. diff --git a/seed/canonical/formal/SeedCanonProjection.tla b/seed/canonical/formal/SeedCanonProjection.tla index a330264..b5b7140 100644 --- a/seed/canonical/formal/SeedCanonProjection.tla +++ b/seed/canonical/formal/SeedCanonProjection.tla @@ -4,10 +4,10 @@ EXTENDS FiniteSets (* GENERATED FILE. DO NOT EDIT. Source: seed/canonical/source/seed-model.json -Source SHA-256: sha256:c43ca7b642a11c3ab140884a6bbff34bbd741f5cb905e6a779c860c813998fcf -Projection profile: ASET-SEED-CANON-TLA-PROJECTION-V4 +Source SHA-256: sha256:1fed5dc95045a287b3e9b8b4ea011a7b977729158f3360ed9a8a7e7e6ba1b4b0 +Projection profile: ASET-SEED-CANON-TLA-PROJECTION-V5 -V4 is a standalone projection. It does not EXTEND or import SeedResolution. +V5 is a standalone projection. It does not EXTEND or import SeedResolution. The refinement proof explicitly instantiates this model onto the target state. Seed-owned state is requestMeta + terminalMeta. Conflict is environment state. EVALUATE_RESOLUTION is a pure observer and is not part of CanonNext. @@ -15,16 +15,14 @@ EVALUATE_RESOLUTION is a pure observer and is not part of CanonNext. CONSTANTS ResolutionIds, Bindings, Authorities, TerminalCommitments, RecognizedTerminalCommitments, NoCommitment, - RequestAuthorityBindings, TerminalAuthorityBindings + RecognizedAuthorityBindings ASSUME ResolutionIds # {} ASSUME Bindings # {} ASSUME Authorities # {} ASSUME RecognizedTerminalCommitments \subseteq TerminalCommitments ASSUME NoCommitment \notin TerminalCommitments -ASSUME RequestAuthorityBindings \subseteq Authorities \X Bindings -ASSUME TerminalAuthorityBindings \subseteq Authorities \X Bindings -ASSUME RequestAuthorityBindings \subseteq TerminalAuthorityBindings +ASSUME RecognizedAuthorityBindings \subseteq Authorities \X Bindings CanonResolutions == {"UNKNOWN", "ALLOW", "BLOCK"} CanonTerminalResolutions == {"ALLOW", "BLOCK"} @@ -63,7 +61,7 @@ CanonRegisterRequest(r, b, a, previous) == /\ r \in ResolutionIds \ CanonRequests /\ b \in Bindings /\ a \in Authorities - /\ <> \in RequestAuthorityBindings + /\ <> \in RecognizedAuthorityBindings /\ \/ previous = NoCommitment \/ previous \in RecognizedTerminalCommitments /\ requestMeta' = @@ -77,7 +75,7 @@ CanonSubmitResolution(r, b, a, value) == /\ r \in CanonRequests /\ b = CanonRequestBinding(r) /\ a \in Authorities - /\ <> \in TerminalAuthorityBindings + /\ <> \in RecognizedAuthorityBindings /\ value \in CanonTerminalResolutions /\ r \notin CanonTerminalRequests /\ r \notin conflicts @@ -89,7 +87,7 @@ CanonSubmitResolution(r, b, a, value) == /\ UNCHANGED <> CanonObserveConflict(r) == - /\ r \in ResolutionIds + /\ r \in CanonTerminalRequests \ conflicts /\ conflicts' = conflicts \cup {r} /\ UNCHANGED CanonSeedVars diff --git a/seed/canonical/formal/SeedCanonRefinementProofs.tla b/seed/canonical/formal/SeedCanonRefinementProofs.tla index eff57bb..e81de5a 100644 --- a/seed/canonical/formal/SeedCanonRefinementProofs.tla +++ b/seed/canonical/formal/SeedCanonRefinementProofs.tla @@ -2,7 +2,7 @@ EXTENDS SeedResolution, TLAPS (* -Behavioral equivalence proof for projection profile V4. +Behavioral equivalence proof for projection profile V5. SeedCanonProjection is standalone and does not import SeedResolution. The instance below explicitly maps the generated projection constants and state @@ -18,8 +18,7 @@ Canon == INSTANCE SeedCanonProjection TerminalCommitments <- TerminalCommitments, RecognizedTerminalCommitments <- RecognizedTerminalCommitments, NoCommitment <- NoCommitment, - RequestAuthorityBindings <- RequestAuthorityBindings, - TerminalAuthorityBindings <- TerminalAuthorityBindings, + RecognizedAuthorityBindings <- RecognizedAuthorityBindings, requestMeta <- requestMeta, terminalMeta <- terminalMeta, conflicts <- conflicts diff --git a/seed/canonical/formal/SeedResolution.cfg b/seed/canonical/formal/SeedResolution.cfg index 2eaa677..436ee6e 100644 --- a/seed/canonical/formal/SeedResolution.cfg +++ b/seed/canonical/formal/SeedResolution.cfg @@ -5,8 +5,7 @@ CONSTANTS TerminalCommitments = {c1, c2} RecognizedTerminalCommitments = {c1, c2} NoCommitment = noCommitment - RequestAuthorityBindings <- TLC_RequestAuthorityBindings - TerminalAuthorityBindings <- TLC_TerminalAuthorityBindings + RecognizedAuthorityBindings <- TLC_RecognizedAuthorityBindings SPECIFICATION Spec INVARIANTS @@ -17,8 +16,8 @@ INVARIANTS TerminalBindingDerived RequestAuthorityRecognized TerminalAuthorityRecognized - TerminalUnique - ConflictUnknown + AcceptedTerminalUnique + ConflictSound FreshReconsideration PROPERTIES RequestsAppendOnly diff --git a/seed/canonical/formal/SeedResolution.tla b/seed/canonical/formal/SeedResolution.tla index 944556a..6fbdbb6 100644 --- a/seed/canonical/formal/SeedResolution.tla +++ b/seed/canonical/formal/SeedResolution.tla @@ -3,16 +3,14 @@ EXTENDS FiniteSets CONSTANTS ResolutionIds, Bindings, Authorities, TerminalCommitments, RecognizedTerminalCommitments, NoCommitment, - RequestAuthorityBindings, TerminalAuthorityBindings + RecognizedAuthorityBindings ASSUME ResolutionIds # {} ASSUME Bindings # {} ASSUME Authorities # {} ASSUME RecognizedTerminalCommitments \subseteq TerminalCommitments ASSUME NoCommitment \notin TerminalCommitments -ASSUME RequestAuthorityBindings \subseteq Authorities \X Bindings -ASSUME TerminalAuthorityBindings \subseteq Authorities \X Bindings -ASSUME RequestAuthorityBindings \subseteq TerminalAuthorityBindings +ASSUME RecognizedAuthorityBindings \subseteq Authorities \X Bindings Resolutions == {"UNKNOWN", "ALLOW", "BLOCK"} TerminalResolutions == {"ALLOW", "BLOCK"} @@ -31,13 +29,10 @@ TLC_Authority2 == CHOOSE a \in Authorities \ {TLC_Authority1} : TRUE TLC_Binding1 == CHOOSE b \in Bindings : TRUE TLC_Binding2 == CHOOSE b \in Bindings \ {TLC_Binding1} : TRUE -TLC_RequestAuthorityBindings == +TLC_RecognizedAuthorityBindings == {<>, - <>} - -TLC_TerminalAuthorityBindings == - TLC_RequestAuthorityBindings \cup - {<>} + <>, + <>} (* Seed-owned state and environment state are deliberately separated. @@ -75,7 +70,7 @@ RegisterRequest(r, b, a, previous) == /\ r \in ResolutionIds \ Requests /\ b \in Bindings /\ a \in Authorities - /\ <> \in RequestAuthorityBindings + /\ <> \in RecognizedAuthorityBindings /\ \/ previous = NoCommitment \/ previous \in RecognizedTerminalCommitments /\ requestMeta' = @@ -89,7 +84,7 @@ SubmitResolution(r, b, a, value) == /\ r \in Requests /\ b = RequestBinding(r) /\ a \in Authorities - /\ <> \in TerminalAuthorityBindings + /\ <> \in RecognizedAuthorityBindings /\ value \in TerminalResolutions /\ r \notin TerminalRequests /\ r \notin conflicts @@ -102,7 +97,7 @@ SubmitResolution(r, b, a, value) == (* Environment transition: it changes only environment state. *) ObserveConflict(r) == - /\ r \in ResolutionIds + /\ r \in TerminalRequests \ conflicts /\ conflicts' = conflicts \cup {r} /\ UNCHANGED seedVars @@ -141,6 +136,7 @@ TypeOK == /\ DOMAIN terminalMeta \subseteq ResolutionIds /\ terminalMeta \in [DOMAIN terminalMeta -> TerminalMetaType] /\ conflicts \subseteq ResolutionIds + /\ conflicts \subseteq TerminalRequests ResolutionDomain == \A r \in ResolutionIds : ResolutionOf(r) \in Resolutions @@ -153,7 +149,7 @@ AllowSoundness == /\ r \in TerminalRequests /\ TerminalResolution(r) = "ALLOW" /\ <> - \in TerminalAuthorityBindings + \in RecognizedAuthorityBindings FailClosed == \A r \in ResolutionIds : @@ -167,20 +163,21 @@ TerminalBindingDerived == RequestAuthorityRecognized == \A r \in Requests : \E a \in Authorities : - <> \in RequestAuthorityBindings + <> \in RecognizedAuthorityBindings TerminalAuthorityRecognized == \A r \in TerminalRequests : /\ r \in Requests /\ <> - \in TerminalAuthorityBindings + \in RecognizedAuthorityBindings (* One keyed terminal metadata cell makes multiple accepted terminals unrepresentable. *) -TerminalUnique == +AcceptedTerminalUnique == terminalMeta \in [DOMAIN terminalMeta -> TerminalMetaType] -ConflictUnknown == - \A r \in conflicts : ResolutionOf(r) = "UNKNOWN" +ConflictSound == + /\ conflicts \subseteq TerminalRequests + /\ \A r \in conflicts : ResolutionOf(r) = "UNKNOWN" FreshReconsideration == \A r \in Requests : @@ -198,8 +195,8 @@ SeedStateSafety == /\ TerminalBindingDerived /\ RequestAuthorityRecognized /\ TerminalAuthorityRecognized - /\ TerminalUnique - /\ ConflictUnknown + /\ AcceptedTerminalUnique + /\ ConflictSound /\ FreshReconsideration InductiveInvariant == diff --git a/seed/canonical/formal/SeedResolutionProofs.tla b/seed/canonical/formal/SeedResolutionProofs.tla index ab4b9a1..77487d0 100644 --- a/seed/canonical/formal/SeedResolutionProofs.tla +++ b/seed/canonical/formal/SeedResolutionProofs.tla @@ -68,11 +68,11 @@ THEOREM FailClosedByEvaluator == PROOF BY DEF FailClosed, EffectPermitted -THEOREM ConflictUnknownFromTypeOK == - TypeOK => ConflictUnknown +THEOREM ConflictSoundFromTypeOK == + TypeOK => ConflictSound PROOF BY ConflictedResolutionIsUnknown - DEF TypeOK, ConflictUnknown + DEF TypeOK, ConflictSound THEOREM ResolutionDomainPointwise == ASSUME TypeOK, @@ -106,10 +106,10 @@ PROOF BY ResolutionDomainPointwise DEF ResolutionDomain -THEOREM TerminalUniqueFromTypeOK == - TypeOK => TerminalUnique +THEOREM AcceptedTerminalUniqueFromTypeOK == + TypeOK => AcceptedTerminalUnique PROOF - BY DEF TypeOK, TerminalUnique + BY DEF TypeOK, AcceptedTerminalUnique THEOREM AllowSoundnessPointwise == ASSUME TerminalBindingDerived, @@ -122,7 +122,7 @@ THEOREM AllowSoundnessPointwise == /\ r \in TerminalRequests /\ TerminalResolution(r) = "ALLOW" /\ <> - \in TerminalAuthorityBindings + \in RecognizedAuthorityBindings PROOF <1>1. /\ r \in Requests @@ -132,7 +132,7 @@ PROOF BY AllowResolutionCharacterization <1>2. <> - \in TerminalAuthorityBindings + \in RecognizedAuthorityBindings BY <1>1 DEF TerminalAuthorityRecognized <1>3. QED BY <1>1, <1>2 @@ -150,8 +150,8 @@ PROOF BY ResolutionDomainFromTypeOK, AllowSoundnessFromStructuralInvariants, FailClosedByEvaluator, - TerminalUniqueFromTypeOK, - ConflictUnknownFromTypeOK + AcceptedTerminalUniqueFromTypeOK, + ConflictSoundFromTypeOK DEF InductiveInvariant, SeedStateSafety THEOREM InitImpliesTypeOK == @@ -220,6 +220,7 @@ PROOF TypeOK, RegisterRequest, Requests, + TerminalRequests, RequestMetaType, TerminalMetaType @@ -423,7 +424,7 @@ THEOREM ObserveConflictPreservesTypeOK == \A r \in ResolutionIds : TypeOK /\ ObserveConflict(r) => TypeOK' PROOF - BY DEF TypeOK, ObserveConflict, seedVars + BY DEF TypeOK, ObserveConflict, seedVars, TerminalRequests THEOREM ObserveConflictPreservesTerminalBindingDerived == \A r \in ResolutionIds : diff --git a/seed/canonical/migration/CANON_CHANGE_DECLARATION.json b/seed/canonical/migration/CANON_CHANGE_DECLARATION.json index 998d023..d6f84dd 100644 --- a/seed/canonical/migration/CANON_CHANGE_DECLARATION.json +++ b/seed/canonical/migration/CANON_CHANGE_DECLARATION.json @@ -1,10 +1,10 @@ { - "candidate_model_sha256": "sha256:c43ca7b642a11c3ab140884a6bbff34bbd741f5cb905e6a779c860c813998fcf", + "candidate_model_sha256": "sha256:1fed5dc95045a287b3e9b8b4ea011a7b977729158f3360ed9a8a7e7e6ba1b4b0", "change_class": "BREAKING", "change_kind": "SEMANTIC_SIMPLIFICATION", - "decision_ref": "seed/canonical/decisions/ADR-009-seed-state-environment-observer-and-authority-boundary.md", + "decision_ref": "seed/canonical/decisions/ADR-010-unify-authority-conflict-and-operation-semantics.md", "document_type": "aset-canon-change-declaration", - "rationale": "Seed 0.3 deep-refactors the active resolution core: exact-binding Authority recognition replaces grant-chain semantics, Seed-owned state is separated from environment conflict state, evaluation is an observer, invalid/non-authoritative material cannot override a unique valid terminal record, and the canon-to-TLA projection is standalone.", + "rationale": "Seed 0.3 final semantic cleanup unifies exact-binding Authority recognition, constrains conflict observation to accepted terminal resolutions, distinguishes accepted-terminal uniqueness from external conflict material, and replaces the legacy transitions catalogue with three role-classified operations under a standalone V5 canon-to-TLA projection.", "schema_version": 1, "supersession_ref": "seed/canonical/migration/ALPHA2_TO_0.3_ALPHA1_CHANGE_DECLARATION.json" } diff --git a/seed/canonical/schemas/canon-tla-refinement.schema.json b/seed/canonical/schemas/canon-tla-refinement.schema.json index 07868da..c8335e9 100644 --- a/seed/canonical/schemas/canon-tla-refinement.schema.json +++ b/seed/canonical/schemas/canon-tla-refinement.schema.json @@ -17,6 +17,42 @@ ], "type": "object" }, + "operationCoverage": { + "additionalProperties": false, + "properties": { + "id": { + "pattern": "^SEED-OP-[0-9]{3}$", + "type": "string" + }, + "kind": { + "enum": [ + "REGISTER_REQUEST", + "SUBMIT_RESOLUTION", + "EVALUATE_RESOLUTION" + ] + }, + "status": { + "enum": [ + "PROVED_IN_DECLARED_PROJECTION", + "OBSERVER_EQUIVALENCE_PROVED" + ] + }, + "tla_action": { + "enum": [ + "RegisterRequest", + "SubmitResolution", + "EvaluateResolution" + ] + } + }, + "required": [ + "id", + "kind", + "tla_action", + "status" + ], + "type": "object" + }, "requirementCoverage": { "additionalProperties": false, "properties": { @@ -69,42 +105,6 @@ "PARTIAL_TERMINAL_COMMITMENT_ABSTRACTION", "META_OUTSIDE_BEHAVIORAL_MODEL" ] - }, - "transitionCoverage": { - "additionalProperties": false, - "properties": { - "id": { - "pattern": "^SEED-TX-[0-9]{3}$", - "type": "string" - }, - "kind": { - "enum": [ - "REGISTER_REQUEST", - "SUBMIT_RESOLUTION", - "EVALUATE_RESOLUTION" - ] - }, - "status": { - "enum": [ - "PROVED_IN_DECLARED_PROJECTION", - "OBSERVER_EQUIVALENCE_PROVED" - ] - }, - "tla_action": { - "enum": [ - "RegisterRequest", - "SubmitResolution", - "EvaluateResolution" - ] - } - }, - "required": [ - "id", - "kind", - "tla_action", - "status" - ], - "type": "object" } }, "$id": "https://github.com/attractor-set/ASET/raw/main/seed/canonical/schemas/canon-tla-refinement.schema.json", @@ -146,7 +146,7 @@ "const": "seed/canonical/formal/SeedCanonProjection.tla" }, "profile": { - "const": "ASET-SEED-CANON-TLA-PROJECTION-V4" + "const": "ASET-SEED-CANON-TLA-PROJECTION-V5" } }, "required": [ @@ -165,6 +165,14 @@ "minItems": 12, "type": "array" }, + "operation_coverage": { + "items": { + "$ref": "#/$defs/operationCoverage" + }, + "maxItems": 3, + "minItems": 3, + "type": "array" + }, "proof": { "additionalProperties": false, "properties": { @@ -266,14 +274,6 @@ "module" ], "type": "object" - }, - "transition_coverage": { - "items": { - "$ref": "#/$defs/transitionCoverage" - }, - "maxItems": 3, - "minItems": 3, - "type": "array" } }, "required": [ @@ -288,7 +288,7 @@ "resolution_algebra_fields", "requirement_coverage", "invariant_coverage", - "transition_coverage", + "operation_coverage", "abstractions", "excluded_claims", "claim_boundary" diff --git a/seed/canonical/schemas/invariant-coverage.schema.json b/seed/canonical/schemas/invariant-coverage.schema.json index 66ad8c1..755e7e0 100644 --- a/seed/canonical/schemas/invariant-coverage.schema.json +++ b/seed/canonical/schemas/invariant-coverage.schema.json @@ -1,113 +1,211 @@ { - "$schema": "https://json-schema.org/draft/2020-12/schema", + "$defs": { + "coverageEntry": { + "additionalProperties": false, + "properties": { + "conformance_cases": { + "$ref": "#/$defs/nonEmptyStrings" + }, + "formal_properties": { + "$ref": "#/$defs/nonEmptyStrings" + }, + "id": { + "minLength": 1, + "type": "string" + }, + "invariants": { + "items": { + "pattern": "^SEED-INV-[0-9]{3}$", + "type": "string" + }, + "type": "array" + }, + "semantic_mutations": { + "$ref": "#/$defs/nonEmptyStrings" + } + }, + "required": [ + "id", + "formal_properties", + "conformance_cases", + "semantic_mutations" + ], + "type": "object" + }, + "nonEmptyStrings": { + "items": { + "minLength": 1, + "type": "string" + }, + "minItems": 1, + "type": "array" + } + }, "$id": "https://github.com/attractor-set/ASET/raw/main/seed/canonical/schemas/invariant-coverage.schema.json", - "type": "object", + "$schema": "https://json-schema.org/draft/2020-12/schema", "additionalProperties": false, - "required": [ - "document_type", - "schema_version", - "normative", - "coverage_policy", - "requirements", - "invariants", - "transitions", - "mutation_catalog", - "claim_boundary" - ], "properties": { - "document_type": {"const": "aset-seed-invariant-coverage"}, - "schema_version": {"const": 1}, - "normative": {"const": true}, + "claim_boundary": { + "additionalProperties": false, + "properties": { + "covered": { + "$ref": "#/$defs/nonEmptyStrings" + }, + "not_claimed": { + "$ref": "#/$defs/nonEmptyStrings" + } + }, + "required": [ + "covered", + "not_claimed" + ], + "type": "object" + }, "coverage_policy": { - "type": "object", "additionalProperties": false, + "properties": { + "conformance_case_required": { + "const": true + }, + "formal_property_required": { + "const": true + }, + "invariants_complete": { + "const": true + }, + "operations_complete": { + "const": true + }, + "orphan_evidence_forbidden": { + "const": true + }, + "requirements_complete": { + "const": true + }, + "semantic_mutation_required": { + "const": true + } + }, "required": [ "requirements_complete", "invariants_complete", - "transitions_complete", + "operations_complete", "formal_property_required", "conformance_case_required", "semantic_mutation_required", "orphan_evidence_forbidden" ], - "properties": { - "requirements_complete": {"const": true}, - "invariants_complete": {"const": true}, - "transitions_complete": {"const": true}, - "formal_property_required": {"const": true}, - "conformance_case_required": {"const": true}, - "semantic_mutation_required": {"const": true}, - "orphan_evidence_forbidden": {"const": true} - } + "type": "object" }, - "requirements": { - "type": "array", - "minItems": 12, - "items": {"$ref": "#/$defs/coverageEntry"} + "document_type": { + "const": "aset-seed-invariant-coverage" }, "invariants": { - "type": "array", + "items": { + "$ref": "#/$defs/coverageEntry" + }, "minItems": 12, - "items": {"$ref": "#/$defs/coverageEntry"} + "type": "array" }, - "transitions": { - "type": "array", - "minItems": 3, + "mutation_catalog": { "items": { - "type": "object", "additionalProperties": false, - "required": ["id", "positive_cases", "negative_cases"], "properties": { - "id": {"pattern": "^SEED-TX-[0-9]{3}$", "type": "string"}, - "positive_cases": {"$ref": "#/$defs/nonEmptyStrings"}, - "negative_cases": {"$ref": "#/$defs/nonEmptyStrings"} - } - } - }, - "mutation_catalog": { - "type": "array", + "case_ids": { + "items": { + "type": "string" + }, + "type": "array" + }, + "description": { + "minLength": 1, + "type": "string" + }, + "id": { + "pattern": "^SEED-MUT-[0-9]{3}$", + "type": "string" + }, + "operator": { + "minLength": 1, + "type": "string" + }, + "seed_invariants": { + "items": { + "pattern": "^SEED-INV-[0-9]{3}$", + "type": "string" + }, + "type": "array" + }, + "seed_requirements": { + "items": { + "pattern": "^ASET-SEED-REQ-[0-9]{3}$", + "type": "string" + }, + "type": "array" + } + }, + "required": [ + "id", + "operator", + "description", + "case_ids", + "seed_invariants", + "seed_requirements" + ], + "type": "object" + }, "minItems": 13, + "type": "array" + }, + "normative": { + "const": true + }, + "operations": { "items": { - "type": "object", "additionalProperties": false, - "required": ["id", "operator", "description", "case_ids", "seed_invariants", "seed_requirements"], "properties": { - "id": {"pattern": "^SEED-MUT-[0-9]{3}$", "type": "string"}, - "operator": {"type": "string", "minLength": 1}, - "description": {"type": "string", "minLength": 1}, - "case_ids": {"type": "array", "items": {"type": "string"}}, - "seed_invariants": {"type": "array", "items": {"pattern": "^SEED-INV-[0-9]{3}$", "type": "string"}}, - "seed_requirements": {"type": "array", "items": {"pattern": "^ASET-SEED-REQ-[0-9]{3}$", "type": "string"}} - } - } + "id": { + "pattern": "^SEED-OP-[0-9]{3}$", + "type": "string" + }, + "negative_cases": { + "$ref": "#/$defs/nonEmptyStrings" + }, + "positive_cases": { + "$ref": "#/$defs/nonEmptyStrings" + } + }, + "required": [ + "id", + "positive_cases", + "negative_cases" + ], + "type": "object" + }, + "minItems": 3, + "type": "array" }, - "claim_boundary": { - "type": "object", - "additionalProperties": false, - "required": ["covered", "not_claimed"], - "properties": { - "covered": {"$ref": "#/$defs/nonEmptyStrings"}, - "not_claimed": {"$ref": "#/$defs/nonEmptyStrings"} - } - } - }, - "$defs": { - "nonEmptyStrings": { - "type": "array", - "minItems": 1, - "items": {"type": "string", "minLength": 1} + "requirements": { + "items": { + "$ref": "#/$defs/coverageEntry" + }, + "minItems": 12, + "type": "array" }, - "coverageEntry": { - "type": "object", - "additionalProperties": false, - "required": ["id", "formal_properties", "conformance_cases", "semantic_mutations"], - "properties": { - "id": {"type": "string", "minLength": 1}, - "invariants": {"type": "array", "items": {"pattern": "^SEED-INV-[0-9]{3}$", "type": "string"}}, - "formal_properties": {"$ref": "#/$defs/nonEmptyStrings"}, - "conformance_cases": {"$ref": "#/$defs/nonEmptyStrings"}, - "semantic_mutations": {"$ref": "#/$defs/nonEmptyStrings"} - } + "schema_version": { + "const": 1 } - } + }, + "required": [ + "document_type", + "schema_version", + "normative", + "coverage_policy", + "requirements", + "invariants", + "operations", + "mutation_catalog", + "claim_boundary" + ], + "type": "object" } diff --git a/seed/canonical/schemas/seed-model.schema.json b/seed/canonical/schemas/seed-model.schema.json index 1b6b44d..d73d410 100644 --- a/seed/canonical/schemas/seed-model.schema.json +++ b/seed/canonical/schemas/seed-model.schema.json @@ -161,6 +161,84 @@ "model_id": { "const": "ASET-SEED-RESOLUTION-CANON-0.3-ALPHA1" }, + "operations": { + "items": { + "additionalProperties": false, + "properties": { + "authority_rule": { + "minLength": 1, + "type": "string" + }, + "binding_rule": { + "minLength": 1, + "type": "string" + }, + "created_artifacts": { + "items": { + "type": "string" + }, + "minItems": 1, + "type": "array" + }, + "from_resolution": { + "enum": [ + null, + "UNKNOWN" + ], + "type": [ + "string", + "null" + ] + }, + "id": { + "pattern": "^SEED-OP-[0-9]{3}$", + "type": "string" + }, + "kind": { + "enum": [ + "REGISTER_REQUEST", + "SUBMIT_RESOLUTION", + "EVALUATE_RESOLUTION" + ] + }, + "payload_schema": { + "type": "string" + }, + "role": { + "enum": [ + "STATE_TRANSITION", + "OBSERVER" + ] + }, + "terminal": { + "type": "boolean" + }, + "to_resolution": { + "enum": [ + "UNKNOWN", + "ALLOW_OR_BLOCK", + "DERIVED" + ] + } + }, + "required": [ + "id", + "kind", + "payload_schema", + "from_resolution", + "to_resolution", + "authority_rule", + "binding_rule", + "created_artifacts", + "role", + "terminal" + ], + "type": "object" + }, + "maxItems": 3, + "minItems": 3, + "type": "array" + }, "predecessor": { "const": "ASET-SEED-RESOLUTION-CANON-0.2-ALPHA2" }, @@ -281,89 +359,11 @@ "type": "object" }, "schema_version": { - "const": 4 + "const": 5 }, "status": { "const": "MINIMAL_STRONG_CORE_ALPHA" }, - "transitions": { - "items": { - "additionalProperties": false, - "properties": { - "authority_rule": { - "minLength": 1, - "type": "string" - }, - "binding_rule": { - "minLength": 1, - "type": "string" - }, - "created_artifacts": { - "items": { - "type": "string" - }, - "minItems": 1, - "type": "array" - }, - "from_resolution": { - "enum": [ - null, - "UNKNOWN" - ], - "type": [ - "string", - "null" - ] - }, - "id": { - "pattern": "^SEED-TX-[0-9]{3}$", - "type": "string" - }, - "kind": { - "enum": [ - "REGISTER_REQUEST", - "SUBMIT_RESOLUTION", - "EVALUATE_RESOLUTION" - ] - }, - "payload_schema": { - "type": "string" - }, - "role": { - "enum": [ - "STATE_TRANSITION", - "OBSERVER" - ] - }, - "terminal": { - "type": "boolean" - }, - "to_resolution": { - "enum": [ - "UNKNOWN", - "ALLOW_OR_BLOCK", - "DERIVED" - ] - } - }, - "required": [ - "id", - "kind", - "payload_schema", - "from_resolution", - "to_resolution", - "authority_rule", - "binding_rule", - "created_artifacts", - "role", - "terminal" - ], - "type": "object" - }, - "maxItems": 3, - "minItems": 3, - "type": "array" - }, "version": { "const": "0.3.0-alpha.1" } @@ -381,7 +381,7 @@ "concepts", "requirements", "invariants", - "transitions", + "operations", "protocol_profile_ref", "conformance_profile_ref", "assurance", diff --git a/seed/canonical/source/seed-model.json b/seed/canonical/source/seed-model.json index e0af6d8..f59c8fb 100644 --- a/seed/canonical/source/seed-model.json +++ b/seed/canonical/source/seed-model.json @@ -194,9 +194,9 @@ ], "id": "SEED-INV-002", "texts": { - "en": "Effect permission is true if and only if the unique valid terminal record is ALLOW.", - "pt-BR": "A permissão do efeito é verdadeira se, e somente se, o único registro terminal válido for ALLOW.", - "ru": "Разрешение эффекта истинно тогда и только тогда, когда единственная действительная терминальная запись равна ALLOW." + "en": "Effect permission is true if and only if the accepted authoritative terminal record is ALLOW and no valid terminal conflict is observed.", + "pt-BR": "A permissão de efeito é verdadeira se, e somente se, o registro terminal autoritativo aceito for ALLOW e nenhum conflito terminal válido for observado.", + "ru": "Разрешение эффекта истинно тогда и только тогда, когда принятая авторитетная терминальная запись имеет значение ALLOW и не наблюдается действительный терминальный конфликт." }, "verification": [ "ASET-VERIFY-DECLARATIVE-STATE-VALIDATION", @@ -302,9 +302,9 @@ ], "id": "SEED-INV-008", "texts": { - "en": "At most one valid terminal record exists for one resolution_id.", - "pt-BR": "Existe no máximo um registro terminal válido para um resolution_id.", - "ru": "Для одного resolution_id существует не более одной действительной терминальной записи." + "en": "Seed-owned state accepts at most one terminal record for one resolution_id.", + "pt-BR": "O estado pertencente ao Seed aceita no máximo um registro terminal para um resolution_id.", + "ru": "Принадлежащее Seed состояние принимает не более одной терминальной записи для одного resolution_id." }, "verification": [ "ASET-VERIFY-DECLARATIVE-STATE-VALIDATION", @@ -320,9 +320,9 @@ ], "id": "SEED-INV-009", "texts": { - "en": "Conflicting valid terminal records yield UNKNOWN. Invalid or non-authoritative material cannot create ALLOW, create a conflict, or override an otherwise unique valid terminal record.", - "pt-BR": "Registros terminais válidos conflitantes resultam em UNKNOWN. Material inválido ou não autoritativo não pode criar ALLOW, criar conflito nem substituir um registro terminal válido e único.", - "ru": "Конфликтующие действительные терминальные записи дают UNKNOWN. Недействительный или неавторитетный материал не может создать ALLOW, создать конфликт или переопределить единственную действительную терминальную запись." + "en": "A conflict observation is valid only for a resolution_id that already has an accepted terminal record. Additional conflicting valid terminal material yields UNKNOWN; invalid or non-authoritative material cannot create ALLOW, create a conflict, or replace the accepted record.", + "pt-BR": "Uma observação de conflito só é válida para um resolution_id que já possua um registro terminal aceito. Material terminal válido conflitante adicional resulta em UNKNOWN; material inválido ou não autoritativo não pode criar ALLOW, criar conflito nem substituir o registro aceito.", + "ru": "Наблюдение конфликта допустимо только для resolution_id, у которого уже есть принятая терминальная запись. Дополнительный конфликтующий действительный терминальный материал даёт UNKNOWN; недействительный или неавторитетный материал не может создать ALLOW, создать конфликт или заменить принятую запись." }, "verification": [ "ASET-VERIFY-DECLARATIVE-STATE-VALIDATION", @@ -393,6 +393,50 @@ "pt-BR" ], "model_id": "ASET-SEED-RESOLUTION-CANON-0.3-ALPHA1", + "operations": [ + { + "authority_rule": "The Authority must be explicitly recognized for the exact request binding.", + "binding_rule": "The request contains one canonical exact binding and a fresh resolution_id. For reconsideration, previous_terminal_record_digest must be a recognized immutable terminal-record commitment; predecessor object presence in retained storage is not required.", + "created_artifacts": [ + "ResolutionRequest" + ], + "from_resolution": null, + "id": "SEED-OP-001", + "kind": "REGISTER_REQUEST", + "payload_schema": "seed/canonical/protocol/schemas/payload-register-request.schema.json", + "role": "STATE_TRANSITION", + "terminal": false, + "to_resolution": "UNKNOWN" + }, + { + "authority_rule": "The Authority must be explicitly recognized for the exact request binding. Concrete signatures, credentials, delegation mechanisms and proof construction are external validation mechanisms.", + "binding_rule": "The record request_digest and binding_digest must exactly match the registered request.", + "created_artifacts": [ + "ResolutionRecord" + ], + "from_resolution": "UNKNOWN", + "id": "SEED-OP-002", + "kind": "SUBMIT_RESOLUTION", + "payload_schema": "seed/canonical/protocol/schemas/payload-submit-resolution.schema.json", + "role": "STATE_TRANSITION", + "terminal": true, + "to_resolution": "ALLOW_OR_BLOCK" + }, + { + "authority_rule": "Evaluation creates no Authority and accepts no external statement as a resolution.", + "binding_rule": "Evaluation observes one resolution_id without mutating Seed-owned state. It derives UNKNOWN when no authoritative accepted terminal result is established or when additional conflicting valid terminal material is observed; invalid or non-authoritative material cannot override an otherwise authoritative accepted terminal result.", + "created_artifacts": [ + "ResolutionEvaluation" + ], + "from_resolution": null, + "id": "SEED-OP-003", + "kind": "EVALUATE_RESOLUTION", + "payload_schema": "seed/canonical/protocol/schemas/operation.schema.json", + "role": "OBSERVER", + "terminal": false, + "to_resolution": "DERIVED" + } + ], "predecessor": "ASET-SEED-RESOLUTION-CANON-0.2-ALPHA2", "protocol_profile_ref": "seed/canonical/protocol/protocol-profile.json", "publication": { @@ -437,6 +481,11 @@ "pt-BR": "Esta edição é derivada do cânone legível por máquina.", "ru": "Эта редакция выводится из машинного канона." }, + "operations": { + "en": "Operations", + "pt-BR": "Operações", + "ru": "Операции" + }, "predicate": { "en": "Predicate", "pt-BR": "Predicado", @@ -452,11 +501,6 @@ "pt-BR": "Status", "ru": "Статус" }, - "transitions": { - "en": "Transitions", - "pt-BR": "Transições", - "ru": "Переходы" - }, "version": { "en": "Version", "pt-BR": "Versão", @@ -538,9 +582,9 @@ "source": "ASET Seed 0.3 minimal strong core", "subject": "ASET Seed", "texts": { - "en": "An exact bound effect MUST be permitted if and only if the unique valid terminal ResolutionRecord is ALLOW.", - "pt-BR": "Um efeito exatamente vinculado DEVE ser permitido se, e somente se, o único ResolutionRecord terminal válido for ALLOW.", - "ru": "Точно связанный эффект ДОЛЖЕН быть разрешён тогда и только тогда, когда единственная действительная терминальная ResolutionRecord имеет значение ALLOW." + "en": "An exact bound effect MUST be permitted if and only if the accepted authoritative terminal ResolutionRecord is ALLOW and no valid terminal conflict is observed.", + "pt-BR": "Um efeito exatamente vinculado DEVE ser permitido se, e somente se, o ResolutionRecord terminal autoritativo aceito for ALLOW e nenhum conflito terminal válido for observado.", + "ru": "Точно связанный эффект ДОЛЖЕН быть разрешён тогда и только тогда, когда принятая авторитетная терминальная ResolutionRecord имеет значение ALLOW и не наблюдается действительный терминальный конфликт." }, "verification": [ "ASET-VERIFY-DECLARATIVE-STATE-VALIDATION", @@ -558,9 +602,9 @@ "source": "ASET Seed 0.3 minimal strong core", "subject": "ASET Seed", "texts": { - "en": "UNKNOWN and BLOCK MUST prohibit the effect. Missing or ambiguous valid terminal state, or failure to establish a valid terminal record, MUST resolve to UNKNOWN. Invalid or non-authoritative material MUST NOT override an otherwise unique valid terminal record.", - "pt-BR": "UNKNOWN e BLOCK DEVEM proibir o efeito. Estado terminal válido ausente ou ambíguo, ou falha em estabelecer um registro terminal válido, DEVE resultar em UNKNOWN. Material inválido ou não autoritativo NÃO DEVE substituir um registro terminal válido e único.", - "ru": "UNKNOWN и BLOCK ДОЛЖНЫ запрещать эффект. Отсутствие или неоднозначность действительного терминального состояния либо невозможность установить действительную терминальную запись ДОЛЖНЫ давать UNKNOWN. Недействительный или неавторитетный материал НЕ ДОЛЖЕН переопределять уже установленную единственную действительную терминальную запись." + "en": "UNKNOWN and BLOCK MUST prohibit the effect. Missing accepted terminal state, failure to establish an authoritative terminal record, or observation of additional conflicting valid terminal material MUST resolve to UNKNOWN. Invalid or non-authoritative material MUST NOT override an otherwise authoritative accepted terminal record.", + "pt-BR": "UNKNOWN e BLOCK DEVEM proibir o efeito. Estado terminal aceito ausente, falha em estabelecer um registro terminal autoritativo ou observação de material terminal válido conflitante adicional DEVE resultar em UNKNOWN. Material inválido ou não autoritativo NÃO DEVE substituir um registro terminal autoritativo já aceito.", + "ru": "UNKNOWN и BLOCK ДОЛЖНЫ запрещать эффект. Отсутствие принятого терминального состояния, невозможность установить авторитетную терминальную запись либо наблюдение дополнительного конфликтующего действительного терминального материала ДОЛЖНЫ давать UNKNOWN. Недействительный или неавторитетный материал НЕ ДОЛЖЕН переопределять уже принятую авторитетную терминальную запись." }, "verification": [ "ASET-VERIFY-DECLARATIVE-STATE-VALIDATION", @@ -633,14 +677,14 @@ { "area": "minimal resolution-recognition kernel", "id": "ASET-SEED-REQ-009", - "modality": "MAY", - "predicate": "terminal_unique", + "modality": "MUST", + "predicate": "accepted_terminal_unique", "source": "ASET Seed 0.3 minimal strong core", "subject": "ASET Seed", "texts": { - "en": "At most one valid terminal record MAY exist for one resolution_id; conflicting terminal records MUST fail closed as UNKNOWN.", - "pt-BR": "No máximo um registro terminal válido PODE existir para um resolution_id; registros terminais conflitantes DEVEM falhar de modo fechado como UNKNOWN.", - "ru": "Для одного resolution_id МОЖЕТ существовать не более одной действительной терминальной записи; конфликтующие терминальные записи ДОЛЖНЫ давать fail-closed UNKNOWN." + "en": "Seed-owned state MUST accept at most one terminal record for one resolution_id. Observation of additional distinct valid terminal material for an already accepted terminal resolution MUST fail closed as UNKNOWN without replacing the accepted record.", + "pt-BR": "O estado pertencente ao Seed DEVE aceitar no máximo um registro terminal para um resolution_id. A observação de material terminal válido distinto adicional para uma resolução terminal já aceita DEVE falhar de modo fechado como UNKNOWN sem substituir o registro aceito.", + "ru": "Принадлежащее Seed состояние ДОЛЖНО принимать не более одной терминальной записи для одного resolution_id. Наблюдение дополнительного отличающегося действительного терминального материала для уже принятого терминального разрешения ДОЛЖНО давать fail-closed UNKNOWN без замены принятой записи." }, "verification": [ "ASET-VERIFY-DECLARATIVE-STATE-VALIDATION", @@ -723,58 +767,14 @@ "ALLOW", "BLOCK" ], - "unknown_semantics": "No unique valid terminal ResolutionRecord is established for the exact request binding, or conflicting valid terminal records are observed.", + "unknown_semantics": "No authoritative accepted terminal ResolutionRecord is established for the exact request binding, or additional conflicting valid terminal material is observed for an accepted terminal resolution.", "values": [ "UNKNOWN", "ALLOW", "BLOCK" ] }, - "schema_version": 4, + "schema_version": 5, "status": "MINIMAL_STRONG_CORE_ALPHA", - "transitions": [ - { - "authority_rule": "The initial Authority binding must be locally rooted and exactly match the request binding.", - "binding_rule": "The request contains one canonical exact binding and a fresh resolution_id. For reconsideration, previous_terminal_record_digest must be a recognized immutable terminal-record commitment; predecessor object presence in retained storage is not required.", - "created_artifacts": [ - "ResolutionRequest" - ], - "from_resolution": null, - "id": "SEED-TX-001", - "kind": "REGISTER_REQUEST", - "payload_schema": "seed/canonical/protocol/schemas/payload-register-request.schema.json", - "role": "STATE_TRANSITION", - "terminal": false, - "to_resolution": "UNKNOWN" - }, - { - "authority_rule": "The record Authority must be explicitly recognized for the exact request binding. Concrete signatures, delegation chains and proof construction are external validation mechanisms.", - "binding_rule": "The record request_digest and binding_digest must exactly match the registered request.", - "created_artifacts": [ - "ResolutionRecord" - ], - "from_resolution": "UNKNOWN", - "id": "SEED-TX-002", - "kind": "SUBMIT_RESOLUTION", - "payload_schema": "seed/canonical/protocol/schemas/payload-submit-resolution.schema.json", - "role": "STATE_TRANSITION", - "terminal": true, - "to_resolution": "ALLOW_OR_BLOCK" - }, - { - "authority_rule": "Evaluation creates no Authority and accepts no external statement as a resolution.", - "binding_rule": "Evaluation observes one resolution_id without mutating Seed-owned state. It derives UNKNOWN when no unique valid terminal record is established; invalid or non-authoritative material cannot override a unique valid record.", - "created_artifacts": [ - "ResolutionEvaluation" - ], - "from_resolution": null, - "id": "SEED-TX-003", - "kind": "EVALUATE_RESOLUTION", - "payload_schema": "seed/canonical/protocol/schemas/operation.schema.json", - "role": "OBSERVER", - "terminal": false, - "to_resolution": "DERIVED" - } - ], "version": "0.3.0-alpha.1" } diff --git a/tests/test_canonical_model.py b/tests/test_canonical_model.py index aade692..70c5efc 100644 --- a/tests/test_canonical_model.py +++ b/tests/test_canonical_model.py @@ -12,9 +12,14 @@ def test_localization_is_complete(): def test_minimal_resolution_algebra_is_exact(): algebra=model()['resolution_algebra']; assert algebra['values']==['UNKNOWN','ALLOW','BLOCK']; assert algebra['stored_terminal']==['ALLOW','BLOCK']; assert algebra['effect_permitted_if']=='ALLOW' def test_operations_are_minimal(): - transitions=model()['transitions'] - assert [item['kind'] for item in transitions]==['REGISTER_REQUEST','SUBMIT_RESOLUTION','EVALUATE_RESOLUTION'] - assert [item['role'] for item in transitions]==['STATE_TRANSITION','STATE_TRANSITION','OBSERVER'] + operations=model()['operations'] + assert [item['kind'] for item in operations]==[ + 'REGISTER_REQUEST','SUBMIT_RESOLUTION','EVALUATE_RESOLUTION' + ] + assert [item['role'] for item in operations]==['STATE_TRANSITION','STATE_TRANSITION','OBSERVER'] + assert [item['id'] for item in operations]==[ + 'SEED-OP-001','SEED-OP-002','SEED-OP-003' + ] def test_protocol_directory_contains_only_active_profile_schemas(): profile=json.loads((ROOT/'seed/canonical/protocol/protocol-profile.json').read_text(encoding='utf-8')) diff --git a/tests/test_ci_assurance.py b/tests/test_ci_assurance.py index 2a7697d..286b5fc 100644 --- a/tests/test_ci_assurance.py +++ b/tests/test_ci_assurance.py @@ -124,8 +124,9 @@ def test_seed_resolution_tla_uses_valid_operator_tokens(): assert r"/\\" not in specification assert "Range(" not in specification assert "VARIABLES\n requestMeta,\n terminalMeta,\n conflicts" in specification - assert "RequestAuthorityBindings" in specification - assert "TerminalAuthorityBindings" in specification + assert "RecognizedAuthorityBindings" in specification + assert "RequestAuthorityBindings" not in specification + assert "TerminalAuthorityBindings" not in specification assert "observedInputs" not in specification assert "invalidMaterial" not in specification assert "terminalBinding," not in specification @@ -144,11 +145,11 @@ def test_seed_resolution_tlc_treats_terminal_states_as_intended_quiescence(): configuration = (ROOT / "seed/canonical/formal/SeedResolution.cfg").read_text( encoding="utf-8" ) - assert "TerminalUnique ==" in specification + assert "AcceptedTerminalUnique ==" in specification + assert r"r \in TerminalRequests \ conflicts" in specification assert "CHECK_DEADLOCK FALSE" in configuration - assert "RequestAuthorityBindings <- TLC_RequestAuthorityBindings" in configuration - assert "TerminalAuthorityBindings <- TLC_TerminalAuthorityBindings" in configuration - assert r"RequestAuthorityBindings \subseteq TerminalAuthorityBindings" in specification + assert "RecognizedAuthorityBindings <- TLC_RecognizedAuthorityBindings" in configuration + assert r"RecognizedAuthorityBindings \subseteq Authorities \X Bindings" in specification def test_active_audit_index_tracks_active_canon_package(): @@ -180,7 +181,7 @@ def test_canon_tla_refinement_relation_is_complete_and_mandatory(): assert len(relation["requirement_coverage"]) == 12 assert len(relation["invariant_coverage"]) == 12 - assert len(relation["transition_coverage"]) == 3 + assert len(relation["operation_coverage"]) == 3 assert len(relation["resolution_algebra_fields"]) == 7 assert relation["proof"]["final_theorem"] == ( "SeedResolutionBehaviorallyEquivalentToCanonProjection" @@ -188,7 +189,7 @@ def test_canon_tla_refinement_relation_is_complete_and_mandatory(): projection = (ROOT / "seed/canonical/formal/SeedCanonProjection.tla").read_text(encoding="utf-8") assert "EXTENDS SeedResolution" not in projection assert "INSTANCE SeedResolution" not in projection - assert "V4 is a standalone projection" in projection + assert "V5 is a standalone projection" in projection assert len(gates["gates"]) >= 26 diff --git a/tests/test_invariant_coverage.py b/tests/test_invariant_coverage.py index f4827da..3df3c92 100644 --- a/tests/test_invariant_coverage.py +++ b/tests/test_invariant_coverage.py @@ -21,8 +21,8 @@ def test_coverage_closes_exact_canonical_sets() -> None: assert {item["id"] for item in coverage["invariants"]} == { item["id"] for item in model["invariants"] } - assert {item["id"] for item in coverage["transitions"]} == { - item["id"] for item in model["transitions"] + assert {item["id"] for item in coverage["operations"]} == { + item["id"] for item in model["operations"] } diff --git a/tools/blackbox_documentation_audit.py b/tools/blackbox_documentation_audit.py index 3909837..40c665f 100755 --- a/tools/blackbox_documentation_audit.py +++ b/tools/blackbox_documentation_audit.py @@ -16,6 +16,7 @@ ROOT / "docs/repository/PRODUCTION_READINESS.md", ROOT / "docs/repository/OPERATIONS_RUNBOOK.md", ROOT / "docs/repository/RELEASE_PROCESS.md", + ROOT / "docs/repository/BLACK_BOX_AUDIT_METHOD.md", ROOT / "audit/README.md", ROOT / "audit/ACTIVE_AUDIT_INDEX.md", ROOT / "EXTENSIONS.md", diff --git a/tools/build_canon_package.py b/tools/build_canon_package.py index a13fe0c..88f126f 100644 --- a/tools/build_canon_package.py +++ b/tools/build_canon_package.py @@ -43,6 +43,7 @@ "seed/canonical/decisions/ADR-007-reconsideration-commitments-and-bounded-retention.md", "seed/canonical/decisions/ADR-008-normalize-seed-state-by-construction.md", "seed/canonical/decisions/ADR-009-seed-state-environment-observer-and-authority-boundary.md", + "seed/canonical/decisions/ADR-010-unify-authority-conflict-and-operation-semantics.md", "seed/canonical/migration/CANON_CHANGE_DECLARATION.json", "seed/canonical/migration/WIRE_V2_TO_V3.md", ] diff --git a/tools/check_assurance_traceability.py b/tools/check_assurance_traceability.py index ca34806..8a09748 100755 --- a/tools/check_assurance_traceability.py +++ b/tools/check_assurance_traceability.py @@ -201,28 +201,29 @@ def main() -> int: f"formal requirement coverage incomplete: missing={sorted(requirement_ids - formal_requirement_coverage)}" ) - transition_counts: dict[str, Counter[str]] = {} + operation_counts: dict[str, Counter[str]] = {} for entry in profile["cases"]: case = load(ROOT / entry["path"]) kind = case.get("candidate", {}).get("kind") if not isinstance(kind, str): errors.append(f"case {entry['case_id']} has no candidate kind") continue - transition_counts.setdefault(kind, Counter())[entry["polarity"]] += 1 + operation_counts.setdefault(kind, Counter())[entry["polarity"]] += 1 - declared_kinds = {item["kind"] for item in model["transitions"]} - if set(transition_counts) - declared_kinds: + declared_kinds = {item["kind"] for item in model["operations"]} + if set(operation_counts) - declared_kinds: errors.append( - f"cases reference undeclared transition kinds: {sorted(set(transition_counts) - declared_kinds)}" + "cases reference undeclared operation kinds: " + f"{sorted(set(operation_counts) - declared_kinds)}" ) - policy = registry["transition_case_policy"] + policy = registry["operation_case_policy"] exceptions = { - (item["transition_kind"], item["missing_polarity"]): item + (item["operation_kind"], item["missing_polarity"]): item for item in policy.get("declared_exceptions", []) } for kind in sorted(declared_kinds): - counts = transition_counts.get(kind, Counter()) + counts = operation_counts.get(kind, Counter()) for polarity, required in ( ("positive", policy.get("require_positive_case", False)), ("negative", policy.get("require_negative_case", False)), @@ -232,7 +233,7 @@ def main() -> int: and counts[polarity] == 0 and (kind, polarity) not in exceptions ): - errors.append(f"transition {kind} has no {polarity} conformance case") + errors.append(f"operation {kind} has no {polarity} conformance case") report = { "document_type": "aset-assurance-traceability-report", @@ -244,11 +245,11 @@ def main() -> int: "tla_temporal_properties": cfg["PROPERTIES"], "formal_seed_requirements_covered": sorted(formal_requirement_coverage), "formal_seed_invariants_covered": sorted(formal_invariant_coverage), - "transition_case_counts": { + "operation_case_counts": { key: dict(sorted(value.items())) - for key, value in sorted(transition_counts.items()) + for key, value in sorted(operation_counts.items()) }, - "declared_transition_coverage_exceptions": list(exceptions.values()), + "declared_operation_coverage_exceptions": list(exceptions.values()), "tlaps_proof_module": ("seed/canonical/formal/SeedResolutionProofs.tla"), "tlaps_final_theorems": list(TLAPS_FINAL_THEOREMS), "errors": errors, diff --git a/tools/check_canon_compatibility.py b/tools/check_canon_compatibility.py index 4a23fa9..9e35044 100755 --- a/tools/check_canon_compatibility.py +++ b/tools/check_canon_compatibility.py @@ -108,7 +108,12 @@ def main() -> int: "concepts": compare_group(approved, candidate, "concepts", "id"), "requirements": compare_group(approved, candidate, "requirements", "id"), "invariants": compare_group(approved, candidate, "invariants", "id"), - "transitions": compare_group(approved, candidate, "transitions", "kind"), + "operations": compare_group( + {"operations": approved.get("operations", approved.get("transitions", []))}, + {"operations": candidate.get("operations", candidate.get("transitions", []))}, + "operations", + "kind", + ), } ignored = { "assurance", @@ -122,7 +127,8 @@ def main() -> int: key for key in set(approved) | set(candidate) if key not in ignored - and key not in {"concepts", "requirements", "invariants", "transitions"} + and key + not in {"concepts", "requirements", "invariants", "operations", "transitions"} and approved.get(key) != candidate.get(key) ) report: dict[str, Any] = { diff --git a/tools/check_canon_tla_refinement.py b/tools/check_canon_tla_refinement.py index a1d49b3..50b5bb5 100755 --- a/tools/check_canon_tla_refinement.py +++ b/tools/check_canon_tla_refinement.py @@ -140,16 +140,16 @@ def main() -> int: "SUBMIT_RESOLUTION": "SubmitResolution", "EVALUATE_RESOLUTION": "EvaluateResolution", } - expected_transitions = [ + expected_operations = [ (item["id"], item["kind"], action_by_kind[item["kind"]]) - for item in model["transitions"] + for item in model["operations"] ] - actual_transitions = [ + actual_operations = [ (item["id"], item["kind"], item["tla_action"]) - for item in relation["transition_coverage"] + for item in relation["operation_coverage"] ] - if actual_transitions != expected_transitions: - errors.append("transition coverage differs from machine canon") + if actual_operations != expected_operations: + errors.append("operation coverage differs from machine canon") if set(relation["resolution_algebra_fields"]) != set(model["resolution_algebra"]): errors.append("resolution algebra field coverage differs from machine canon") @@ -166,7 +166,7 @@ def main() -> int: projection_text = PROJECTION_PATH.read_text(encoding="utf-8") if PROJECTION_PATH.is_file() else "" if "EXTENDS SeedResolution" in projection_text or "INSTANCE SeedResolution" in projection_text: errors.append("generated projection depends on target SeedResolution module") - if "V4 is a standalone projection" not in projection_text: + if "V5 is a standalone projection" not in projection_text: errors.append("standalone projection marker missing") generator = subprocess.run( @@ -195,7 +195,7 @@ def main() -> int: ), "requirements_classified": len(actual_requirements), "invariants_classified": len(actual_invariants), - "transitions_classified": len(actual_transitions), + "operations_classified": len(actual_operations), "resolution_algebra_fields_classified": len( relation["resolution_algebra_fields"] ), @@ -219,7 +219,7 @@ def main() -> int: ) print(f"CANON_TLA_INVARIANTS={len(actual_invariants)}/{len(expected_invariants)}") print( - f"CANON_TLA_TRANSITIONS={len(actual_transitions)}/{len(expected_transitions)}" + f"CANON_TLA_OPERATIONS={len(actual_operations)}/{len(expected_operations)}" ) print( "CANON_TLA_RESOLUTION_ALGEBRA=" diff --git a/tools/check_invariant_coverage.py b/tools/check_invariant_coverage.py index d8024dc..4794fc6 100755 --- a/tools/check_invariant_coverage.py +++ b/tools/check_invariant_coverage.py @@ -34,14 +34,14 @@ def main() -> int: requirement_ids = {item["id"] for item in model["requirements"]} invariant_ids = {item["id"] for item in model["invariants"]} - transition_ids = {item["id"] for item in model["transitions"]} + operation_ids = {item["id"] for item in model["operations"]} case_entries = {item["case_id"]: item for item in profile["cases"]} formal_names = {item["name"] for item in registry["formal_properties"]} mutation_ids = {item["id"] for item in coverage["mutation_catalog"]} covered_requirements = {item["id"] for item in coverage["requirements"]} covered_invariants = {item["id"] for item in coverage["invariants"]} - covered_transitions = {item["id"] for item in coverage["transitions"]} + covered_operations = {item["id"] for item in coverage["operations"]} if covered_requirements != requirement_ids: errors.append( f"requirement coverage mismatch: missing={sorted(requirement_ids-covered_requirements)} " @@ -52,10 +52,10 @@ def main() -> int: f"invariant coverage mismatch: missing={sorted(invariant_ids-covered_invariants)} " f"extra={sorted(covered_invariants-invariant_ids)}" ) - if covered_transitions != transition_ids: + if covered_operations != operation_ids: errors.append( - f"transition coverage mismatch: missing={sorted(transition_ids-covered_transitions)} " - f"extra={sorted(covered_transitions-transition_ids)}" + f"operation coverage mismatch: missing={sorted(operation_ids-covered_operations)} " + f"extra={sorted(covered_operations-operation_ids)}" ) referenced_formal: set[str] = set() @@ -79,7 +79,7 @@ def main() -> int: if invariant_id not in invariant_ids: errors.append(f"{entry['id']} references unknown invariant {invariant_id}") - for entry in coverage["transitions"]: + for entry in coverage["operations"]: for case_id in entry["positive_cases"]: if case_id not in case_entries or case_entries[case_id]["polarity"] != "positive": errors.append(f"{entry['id']} invalid positive case {case_id}") @@ -114,8 +114,8 @@ def main() -> int: "requirements_covered": len(covered_requirements & requirement_ids), "invariants_total": len(invariant_ids), "invariants_covered": len(covered_invariants & invariant_ids), - "transitions_total": len(transition_ids), - "transitions_covered": len(covered_transitions & transition_ids), + "operations_total": len(operation_ids), + "operations_covered": len(covered_operations & operation_ids), "formal_properties": len(formal_names), "conformance_cases": len(case_entries), "semantic_mutations": len(mutation_ids), @@ -129,7 +129,7 @@ def main() -> int: print(f"INVARIANT_COVERAGE_REQUIREMENTS={report['requirements_covered']}/{report['requirements_total']}") print(f"INVARIANT_COVERAGE_INVARIANTS={report['invariants_covered']}/{report['invariants_total']}") - print(f"INVARIANT_COVERAGE_TRANSITIONS={report['transitions_covered']}/{report['transitions_total']}") + print(f"INVARIANT_COVERAGE_OPERATIONS={report['operations_covered']}/{report['operations_total']}") print(f"INVARIANT_COVERAGE_FORMAL_PROPERTIES={report['formal_properties']}") print(f"INVARIANT_COVERAGE_CONFORMANCE_CASES={report['conformance_cases']}") print(f"INVARIANT_COVERAGE_MUTATIONS={report['semantic_mutations_killed']}/{report['semantic_mutations']}") diff --git a/tools/generate_canon_tla_projection.py b/tools/generate_canon_tla_projection.py index 421d0f0..3506837 100755 --- a/tools/generate_canon_tla_projection.py +++ b/tools/generate_canon_tla_projection.py @@ -12,7 +12,7 @@ RELATION_PATH = ROOT / "seed/canonical/assurance/canon-tla-refinement.json" OUTPUT_PATH = ROOT / "seed/canonical/formal/SeedCanonProjection.tla" -EXPECTED_PROFILE = "ASET-SEED-CANON-TLA-PROJECTION-V4" +EXPECTED_PROFILE = "ASET-SEED-CANON-TLA-PROJECTION-V5" EXPECTED_REQUIREMENT_PREDICATES = [ "binding_exact", "request_fresh", @@ -22,15 +22,15 @@ "local_authority", "authority_recognition_boundary", "inputs_non_authoritative", - "terminal_unique", + "accepted_terminal_unique", "record_immutable", "reconsider_fresh", "implementation_neutral", ] -EXPECTED_TRANSITIONS = [ - ("SEED-TX-001", "REGISTER_REQUEST", "STATE_TRANSITION"), - ("SEED-TX-002", "SUBMIT_RESOLUTION", "STATE_TRANSITION"), - ("SEED-TX-003", "EVALUATE_RESOLUTION", "OBSERVER"), +EXPECTED_OPERATIONS = [ + ("SEED-OP-001", "REGISTER_REQUEST", "STATE_TRANSITION"), + ("SEED-OP-002", "SUBMIT_RESOLUTION", "STATE_TRANSITION"), + ("SEED-OP-003", "EVALUATE_RESOLUTION", "OBSERVER"), ] EXPECTED_INVARIANTS = [f"SEED-INV-{index:03d}" for index in range(1, 13)] @@ -73,10 +73,10 @@ def validate_inputs(model: dict[str, Any], relation: dict[str, Any]) -> None: invariants = [item["id"] for item in model["invariants"]] if invariants != EXPECTED_INVARIANTS: errors.append("unsupported invariant catalogue") - transitions = [ - (item["id"], item["kind"], item["role"]) for item in model["transitions"] + operations = [ + (item["id"], item["kind"], item["role"]) for item in model["operations"] ] - if transitions != EXPECTED_TRANSITIONS: + if operations != EXPECTED_OPERATIONS: errors.append("unsupported operation catalogue") algebra = model["resolution_algebra"] @@ -111,7 +111,7 @@ def render(model: dict[str, Any], relation: dict[str, Any]) -> str: Source SHA-256: {source_sha} Projection profile: {profile} -V4 is a standalone projection. It does not EXTEND or import SeedResolution. +V5 is a standalone projection. It does not EXTEND or import SeedResolution. The refinement proof explicitly instantiates this model onto the target state. Seed-owned state is requestMeta + terminalMeta. Conflict is environment state. EVALUATE_RESOLUTION is a pure observer and is not part of CanonNext. @@ -119,16 +119,14 @@ def render(model: dict[str, Any], relation: dict[str, Any]) -> str: CONSTANTS ResolutionIds, Bindings, Authorities, TerminalCommitments, RecognizedTerminalCommitments, NoCommitment, - RequestAuthorityBindings, TerminalAuthorityBindings + RecognizedAuthorityBindings ASSUME ResolutionIds # {{}} ASSUME Bindings # {{}} ASSUME Authorities # {{}} ASSUME RecognizedTerminalCommitments \subseteq TerminalCommitments ASSUME NoCommitment \notin TerminalCommitments -ASSUME RequestAuthorityBindings \subseteq Authorities \X Bindings -ASSUME TerminalAuthorityBindings \subseteq Authorities \X Bindings -ASSUME RequestAuthorityBindings \subseteq TerminalAuthorityBindings +ASSUME RecognizedAuthorityBindings \subseteq Authorities \X Bindings CanonResolutions == {tla_set(algebra["values"])} CanonTerminalResolutions == {tla_set(algebra["stored_terminal"])} @@ -167,7 +165,7 @@ def render(model: dict[str, Any], relation: dict[str, Any]) -> str: /\ r \in ResolutionIds \ CanonRequests /\ b \in Bindings /\ a \in Authorities - /\ <> \in RequestAuthorityBindings + /\ <> \in RecognizedAuthorityBindings /\ \/ previous = NoCommitment \/ previous \in RecognizedTerminalCommitments /\ requestMeta' = @@ -181,7 +179,7 @@ def render(model: dict[str, Any], relation: dict[str, Any]) -> str: /\ r \in CanonRequests /\ b = CanonRequestBinding(r) /\ a \in Authorities - /\ <> \in TerminalAuthorityBindings + /\ <> \in RecognizedAuthorityBindings /\ value \in CanonTerminalResolutions /\ r \notin CanonTerminalRequests /\ r \notin conflicts @@ -193,7 +191,7 @@ def render(model: dict[str, Any], relation: dict[str, Any]) -> str: /\ UNCHANGED <> CanonObserveConflict(r) == - /\ r \in ResolutionIds + /\ r \in CanonTerminalRequests \ conflicts /\ conflicts' = conflicts \cup {{r}} /\ UNCHANGED CanonSeedVars diff --git a/tools/generate_editions.py b/tools/generate_editions.py index 4946444..cf406d7 100644 --- a/tools/generate_editions.py +++ b/tools/generate_editions.py @@ -90,18 +90,18 @@ def render(model: dict, language: str) -> str: lines.extend([f'## {headings["invariants"][language]}', ""]) for invariant in model["invariants"]: lines.append(f'- `{invariant["id"]}` — {invariant["texts"][language]}') - lines.extend(["", f'## {headings["transitions"][language]}', ""]) - for transition in model["transitions"]: + lines.extend(["", f'## {headings["operations"][language]}', ""]) + for operation in model["operations"]: lines.extend( [ - f'### `{transition["id"]}` — `{transition["kind"]}`', + f'### `{operation["id"]}` — `{operation["kind"]}`', "", - f'- `payload_schema`: `{transition["payload_schema"]}`', - f'- `authority_rule`: {transition["authority_rule"]}', - f'- `binding_rule`: {transition["binding_rule"]}', + f'- `payload_schema`: `{operation["payload_schema"]}`', + f'- `authority_rule`: {operation["authority_rule"]}', + f'- `binding_rule`: {operation["binding_rule"]}', "- `created_artifacts`: " + ", ".join( - f"`{item}`" for item in transition["created_artifacts"] + f"`{item}`" for item in operation["created_artifacts"] ), "", ] diff --git a/tools/model_check_seed.py b/tools/model_check_seed.py index a75b19f..420c641 100755 --- a/tools/model_check_seed.py +++ b/tools/model_check_seed.py @@ -14,8 +14,7 @@ TERMINALS = ("ALLOW", "BLOCK") NO_COMMITMENT = -1 RECOGNIZED_TERMINAL_COMMITMENTS = frozenset({0, 1}) -REQUEST_AUTHORITY_BINDINGS = frozenset({(0, 0), (1, 1)}) -TERMINAL_AUTHORITY_BINDINGS = frozenset({(0, 0), (1, 1), (1, 0)}) +RECOGNIZED_AUTHORITY_BINDINGS = frozenset({(0, 0), (1, 1), (1, 0)}) STATE_PROPERTIES = ( "TypeOK", @@ -25,8 +24,8 @@ "TerminalBindingDerived", "RequestAuthorityRecognized", "TerminalAuthorityRecognized", - "TerminalUnique", - "ConflictUnknown", + "AcceptedTerminalUnique", + "ConflictSound", "FreshReconsideration", ) TEMPORAL_PROPERTIES = ( @@ -83,7 +82,7 @@ def successors(state: State) -> Iterable[tuple[str, State]]: for rid in IDS: if rid in requests: continue - for binding, _authority in REQUEST_AUTHORITY_BINDINGS: + for _authority, binding in RECOGNIZED_AUTHORITY_BINDINGS: yield ( "RegisterRequest", State( @@ -105,7 +104,7 @@ def successors(state: State) -> Iterable[tuple[str, State]]: for rid, (binding, _previous) in requests.items(): if rid in records or rid in state.conflicts: continue - for authority, proof_binding in TERMINAL_AUTHORITY_BINDINGS: + for authority, proof_binding in RECOGNIZED_AUTHORITY_BINDINGS: if proof_binding != binding: continue for value in TERMINALS: @@ -118,7 +117,7 @@ def successors(state: State) -> Iterable[tuple[str, State]]: ), ) - for rid in IDS: + for rid in records: if rid not in state.conflicts: yield ( "ObserveConflict", @@ -139,19 +138,19 @@ def state_errors(state: State) -> list[str]: if not set(records).issubset(requests): errors.append("TerminalBindingDerived") if len(records) != len(state.records): - errors.append("TerminalUnique") + errors.append("AcceptedTerminalUnique") for _rid, (binding, _previous) in requests.items(): if not any( authority in AUTHORITIES - and (authority, binding) in REQUEST_AUTHORITY_BINDINGS + and (authority, binding) in RECOGNIZED_AUTHORITY_BINDINGS for authority in AUTHORITIES ): errors.append("RequestAuthorityRecognized") for rid, (authority, _value) in records.items(): request = requests.get(rid) - if request is None or (authority, request[0]) not in TERMINAL_AUTHORITY_BINDINGS: + if request is None or (authority, request[0]) not in RECOGNIZED_AUTHORITY_BINDINGS: errors.append("TerminalAuthorityRecognized") for rid in IDS: @@ -167,7 +166,7 @@ def state_errors(state: State) -> list[str]: or rid in state.conflicts or record is None or record[1] != "ALLOW" - or (record[0], request[0]) not in TERMINAL_AUTHORITY_BINDINGS + or (record[0], request[0]) not in RECOGNIZED_AUTHORITY_BINDINGS ): errors.append("AllowSoundness") @@ -175,7 +174,7 @@ def state_errors(state: State) -> list[str]: errors.append("FailClosed") if rid in state.conflicts and value != "UNKNOWN": - errors.append("ConflictUnknown") + errors.append("ConflictSound") for _rid, (_binding, previous) in requests.items(): if previous == NO_COMMITMENT: diff --git a/tools/validate_seed_canon.py b/tools/validate_seed_canon.py index 14f05e8..a03c8ee 100644 --- a/tools/validate_seed_canon.py +++ b/tools/validate_seed_canon.py @@ -79,17 +79,17 @@ def main() -> int: ids = [item["id"] for item in model[group]] if len(ids) != len(set(ids)): errors.append("duplicate:" + group) - kinds = [item["kind"] for item in model["transitions"]] + kinds = [item["kind"] for item in model["operations"]] expected_kinds = [ "REGISTER_REQUEST", "SUBMIT_RESOLUTION", "EVALUATE_RESOLUTION", ] if kinds != expected_kinds: - errors.append("transition_catalogue") - roles = [item.get("role") for item in model["transitions"]] + errors.append("operation_catalogue") + roles = [item.get("role") for item in model["operations"]] if roles != ["STATE_TRANSITION", "STATE_TRANSITION", "OBSERVER"]: - errors.append("transition_roles") + errors.append("operation_roles") if model["resolution_algebra"] != { "values": ["UNKNOWN", "ALLOW", "BLOCK"], "derived": "UNKNOWN", @@ -210,7 +210,13 @@ def main() -> int: print(f"SEED_CONCEPTS={len(model['concepts'])}") print(f"SEED_REQUIREMENTS={len(model['requirements'])}") print(f"SEED_INVARIANTS={len(model['invariants'])}") - print(f"SEED_TRANSITIONS={len(model['transitions'])}") + print(f"SEED_OPERATIONS={len(model['operations'])}") + state_transition_count = sum( + item.get("role") == "STATE_TRANSITION" for item in model["operations"] + ) + observer_count = sum(item.get("role") == "OBSERVER" for item in model["operations"]) + print(f"SEED_STATE_TRANSITIONS={state_transition_count}") + print(f"SEED_OBSERVERS={observer_count}") print(f"SEED_CONFORMANCE_CASES={profile['case_count']}") print("SEED_CANON_VALIDATION=PASS") return 0