.{ .{ .id = "test-cli-help", .revision = 3, .suite = .u, .fixture = .{ .id = "fixture-cli-help", .revision = 2, .path = "spec/fixtures/cli/help.md", .sha256 = "dac34b350955f76c1722234763261a48150b3a128ce430ef80d8a963b499668c", }, .claims = .{ .{ .oracle = "INV-HELP-SUCCESS", .kind = .required, .obligations = .{ .{ .id = "obligation-cli-help-success", .revision = 1 }, }, }, .{ .oracle = "INV-HELP-STDOUT", .kind = .required, .obligations = .{ .{ .id = "obligation-cli-help-stdout", .revision = 1 }, }, }, .{ .oracle = "INV-HELP-OPTIONS", .kind = .required, .obligations = .{ .{ .id = "obligation-cli-help-options", .revision = 1 }, .{ .id = "obligation-cli-help-manual-sync", .revision = 1 }, }, }, .{ .oracle = "NO-HELP-STDERR", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-cli-help-stderr-empty", .revision = 1 }, }, }, .{ .oracle = "NO-HELP-FIXTURE-MUTATION", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-cli-help-no-fixture-mutation", .revision = 1 }, }, }, }, .production_boundary = .process, }, .{ .id = "test-cli-version", .revision = 1, .suite = .u, .fixture = .{ .id = "fixture-cli-version", .revision = 1, .path = "spec/fixtures/cli/version.md", .sha256 = "11de7da0aa073e531c9b40fbfbc98d303d9141a5797ead0d6205d13a9fc117cc", }, .claims = .{ .{ .oracle = "INV-VERSION-SUCCESS", .kind = .required, .obligations = .{ .{ .id = "obligation-cli-version-success", .revision = 1 }, }, }, .{ .oracle = "INV-VERSION-STDOUT", .kind = .required, .obligations = .{ .{ .id = "obligation-cli-version-stdout", .revision = 1 }, }, }, .{ .oracle = "INV-VERSION-CHARSET", .kind = .required, .obligations = .{ .{ .id = "obligation-cli-version-charset", .revision = 1 }, }, }, .{ .oracle = "NO-VERSION-STDERR", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-cli-version-stderr-empty", .revision = 1 }, }, }, .{ .oracle = "NO-VERSION-FIXTURE-MUTATION", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-cli-version-no-fixture-mutation", .revision = 1 }, }, }, }, .production_boundary = .process, }, .{ .id = "test-cli-usage", .revision = 1, .suite = .u, .fixture = .{ .id = "fixture-cli-usage", .revision = 1, .path = "spec/fixtures/cli/usage.md", .sha256 = "d3db886e1c7d7e66d7761c716546f0a9ae8f3db6f9cda161dc6313ace9e79d25", }, .claims = .{ .{ .oracle = "INV-USAGE-STATUS", .kind = .required, .obligations = .{ .{ .id = "obligation-cli-usage-status", .revision = 1 }, }, }, .{ .oracle = "INV-USAGE-DIAGNOSTIC", .kind = .required, .obligations = .{ .{ .id = "obligation-cli-usage-diagnostic", .revision = 1 }, }, }, .{ .oracle = "INV-USAGE-ECHO-BOUND", .kind = .required, .obligations = .{ .{ .id = "obligation-cli-usage-echo-bound", .revision = 1 }, }, }, .{ .oracle = "INV-USAGE-ECHO-SANITIZED", .kind = .required, .obligations = .{ .{ .id = "obligation-cli-usage-echo-sanitized", .revision = 1 }, }, }, .{ .oracle = "NO-USAGE-STDOUT", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-cli-usage-no-stdout", .revision = 1 }, }, }, .{ .oracle = "NO-USAGE-FIXTURE-MUTATION", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-cli-usage-no-fixture-mutation", .revision = 1 }, }, }, }, .production_boundary = .process, }, .{ .id = "test-confirm-exact", .revision = 2, .suite = .pty, .fixture = .{ .id = "fixture-confirm-exact", .revision = 1, .path = "spec/fixtures/confirmation/exact.md", .sha256 = "a19811f60ddc3453780fe4896da2ef44c7772acb3d5dcf7cdebd664e14863bf4", }, .claims = .{ .{ .oracle = "INV-CONFIRM-ACCEPTED", .kind = .required, .obligations = .{ .{ .id = "obligation-confirm-accepted", .revision = 1 }, }, }, .{ .oracle = "INV-PLAN-IDENTITY", .kind = .required, .obligations = .{ .{ .id = "obligation-confirm-plan-identity", .revision = 1 }, }, }, .{ .oracle = "NO-MUTATION-BEFORE-ENTER", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-confirm-no-early-mutation", .revision = 1 }, }, }, .{ .oracle = "NO-PLAN-WIDENING", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-confirm-no-plan-widening", .revision = 1 }, }, }, }, .production_boundary = .state_transition, }, .{ .id = "test-cli-terminal", .revision = 1, .suite = .u, .fixture = .{ .id = "fixture-cli-terminal", .revision = 1, .path = "spec/fixtures/cli/terminal.md", .sha256 = "8d61166d80c2c13da1544989fff80d4dc27b7ce94dbe1a211757382b3bd4b4ef", }, .claims = .{ .{ .oracle = "INV-TERM-STATUS", .kind = .required, .obligations = .{ .{ .id = "obligation-cli-term-status", .revision = 1 }, }, }, .{ .oracle = "INV-TERM-DIAGNOSTIC", .kind = .required, .obligations = .{ .{ .id = "obligation-cli-term-diagnostic", .revision = 1 }, }, }, .{ .oracle = "NO-TERM-STDOUT", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-cli-term-no-stdout", .revision = 1 }, }, }, .{ .oracle = "NO-TERM-FIXTURE-MUTATION", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-cli-term-no-fixture-mutation", .revision = 1 }, }, }, }, .production_boundary = .process, }, .{ .id = "test-android-allowlist", .revision = 1, .suite = .u, .fixture = .{ .id = "fixture-android-allowlist", .revision = 1, .path = "spec/fixtures/adapters/android_allowlist.md", .sha256 = "b90e991e21d4d02570848fffa8425033ce6a4f2f61da6add6250c13f3dd97039", }, .claims = .{ .{ .oracle = "INV-ANDROID-ALLOWLIST-IDENTITIES", .kind = .required, .obligations = .{ .{ .id = "obligation-android-allowlist-identities", .revision = 1 }, }, }, .{ .oracle = "INV-ANDROID-ALLOWLIST-ROLES", .kind = .required, .obligations = .{ .{ .id = "obligation-android-allowlist-roles", .revision = 1 }, }, }, .{ .oracle = "NO-ANDROID-ALLOWLIST-BASE-ADDON", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-android-allowlist-no-base-addon", .revision = 1 }, }, }, }, .production_boundary = .state_transition, }, .{ .id = "test-classification-catalogs", .revision = 1, .suite = .u, .fixture = .{ .id = "fixture-classification-catalogs", .revision = 1, .path = "spec/fixtures/classification/catalogs.md", .sha256 = "7936337b30f09d9b64d8c142f9aca47afb52ca952422d591d5fec70a24ce7189", }, .claims = .{ .{ .oracle = "INV-CLASSIFICATION-BASENAMES", .kind = .required, .obligations = .{ .{ .id = "obligation-classification-basenames", .revision = 1 }, }, }, .{ .oracle = "INV-CLASSIFICATION-SUFFIXES", .kind = .required, .obligations = .{ .{ .id = "obligation-classification-suffixes", .revision = 1 }, }, }, .{ .oracle = "INV-CLASSIFICATION-DOCUMENT-ROOTS", .kind = .required, .obligations = .{ .{ .id = "obligation-classification-document-roots", .revision = 1 }, }, }, .{ .oracle = "NO-CLASSIFICATION-DUPLICATES", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-classification-no-duplicates", .revision = 1 }, }, }, }, .production_boundary = .state_transition, }, .{ .id = "test-classification-thresholds", .revision = 2, .suite = .u, .fixture = .{ .id = "fixture-classification-thresholds", .revision = 2, .path = "spec/fixtures/classification/thresholds.md", .sha256 = "fd49d5dd656290a39ab94b109a5ff791ea8547a162f0a0b73a0062e79a9677a2", }, .claims = .{ .{ .oracle = "INV-THRESHOLD-VALUES", .kind = .required, .obligations = .{ .{ .id = "obligation-threshold-values", .revision = 1 }, }, }, .{ .oracle = "INV-THRESHOLD-ORDER", .kind = .required, .obligations = .{ .{ .id = "obligation-threshold-order", .revision = 1 }, }, }, .{ .oracle = "INV-THRESHOLD-BOUNDARY-SETS", .kind = .required, .obligations = .{ .{ .id = "obligation-threshold-boundary-sets", .revision = 1 }, }, }, .{ .oracle = "NO-THRESHOLD-DUPLICATES", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-threshold-no-duplicates", .revision = 1 }, }, }, }, .production_boundary = .state_transition, }, .{ .id = "test-requirement-manifest-u", .revision = 4, .suite = .u, .fixture = .{ .id = "fixture-requirement-manifest-u", .revision = 4, .path = "spec/fixtures/requirements/manifest_u.md", .sha256 = "d43dea3b9464202a32efa7d63a9a7624a58c0fb317ff7c2fc29477b91e4a412b", }, .claims = .{ .{ .oracle = "INV-REQ-TJ-GOV-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-gov-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-GOV-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-gov-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-GOV-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-gov-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-GOV-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-gov-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-GOV-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-gov-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-GOV-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-gov-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-GOV-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-gov-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-GOV-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-gov-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-GOV-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-gov-09", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-GOV-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-gov-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-GOV-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-gov-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-GOV-12", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-gov-12", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-GOV-13", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-gov-13", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-GOV-14", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-gov-14", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-09", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CONCEPT-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-concept-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CONCEPT-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-concept-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CONCEPT-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-concept-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-09", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-09", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-09", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-12", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-12", .revision = 1 }, }, }, .{ .oracle = "INV-REVIEW-LIST-SET-SHAPES", .kind = .required, .obligations = .{ .{ .id = "obligation-review-list-set-shapes", .revision = 1 }, }, }, .{ .oracle = "INV-REVIEW-LIST-EQUAL-RANK", .kind = .required, .obligations = .{ .{ .id = "obligation-review-list-equal-rank", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-13", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-13", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-15", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-15", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-16", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-16", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LINK-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-link-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LINK-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-link-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LINK-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-link-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-11", .revision = 1 }, }, }, .{ .oracle = "INV-CONFIRM-BUFFERED-DISCARDED", .kind = .required, .obligations = .{ .{ .id = "obligation-confirm-buffered-input", .revision = 1 }, }, }, .{ .oracle = "INV-CONFIRM-PASTE-NEVER-CONFIRMS", .kind = .required, .obligations = .{ .{ .id = "obligation-confirm-paste-no-confirm", .revision = 1 }, }, }, .{ .oracle = "INV-CONFIRM-AUTO-REPEAT", .kind = .required, .obligations = .{ .{ .id = "obligation-confirm-auto-repeat", .revision = 1 }, }, }, .{ .oracle = "INV-CONFIRM-LEGACY-DISCLOSURE", .kind = .required, .obligations = .{ .{ .id = "obligation-confirm-legacy-disclosure", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-FAIL-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-fail-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LOG-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-log-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LOG-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-log-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LOG-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-log-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-04", .revision = 1 }, }, }, .{ .oracle = "INV-UI-ALL-HIDDEN-STATE", .kind = .required, .obligations = .{ .{ .id = "obligation-ui-all-hidden-state", .revision = 1 }, }, }, .{ .oracle = "INV-UI-ALL-HIDDEN-BULK", .kind = .required, .obligations = .{ .{ .id = "obligation-ui-all-hidden-bulk", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-12", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-12", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TERM-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-term-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TERM-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-term-07", .revision = 1 }, }, }, .{ .oracle = "INV-TERM-FRAGMENTED-INPUT", .kind = .required, .obligations = .{ .{ .id = "obligation-term-fragmented-input", .revision = 1 }, }, }, .{ .oracle = "INV-TERM-MALFORMED-MOUSE", .kind = .required, .obligations = .{ .{ .id = "obligation-term-malformed-mouse", .revision = 1 }, }, }, .{ .oracle = "INV-TERM-KEYBOARD-RECOVERY", .kind = .required, .obligations = .{ .{ .id = "obligation-term-keyboard-recovery", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TERM-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-term-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CONFIG-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-config-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CONFIG-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-config-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CONFIG-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-config-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CONFIG-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-config-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CONFIG-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-config-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CONFIG-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-config-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CONFIG-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-config-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-09", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-12", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-12", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-MAN-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-man-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-MAN-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-man-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-MAN-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-man-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-MAN-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-man-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-MAN-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-man-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-MAN-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-man-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-12", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-12", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-STYLE-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-style-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PERF-01", .kind = .required, .obligations = .{ .{ .id = "obligation-perf-resource-model", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PERF-02", .kind = .required, .obligations = .{ .{ .id = "obligation-perf-budgets", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PERF-03", .kind = .required, .obligations = .{ .{ .id = "obligation-perf-bottlenecks", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PERF-04", .kind = .required, .obligations = .{ .{ .id = "obligation-perf-measurement", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PERF-05", .kind = .required, .obligations = .{ .{ .id = "obligation-perf-benchmarks", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PERF-07", .kind = .required, .obligations = .{ .{ .id = "obligation-perf-regression-criteria", .revision = 1 }, }, }, .{ .oracle = "NO-REQ-MANIFEST-UNBOUND-U", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-requirement-manifest-no-unbound-pass-u", .revision = 1 }, }, }, .{ .oracle = "NO-REVIEW-LIST-UNKNOWN-FILL", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-review-list-no-unknown-fill", .revision = 1 }, }, }, .{ .oracle = "NO-UI-BULK-HIDDEN-SELECTION", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-ui-no-bulk-hidden-selection", .revision = 1 }, }, }, .{ .oracle = "NO-CONFIRM-STALE-ADMISSION", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-confirm-no-stale-admission", .revision = 1 }, }, }, .{ .oracle = "NO-TERM-KEYMAP-CORRUPTION", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-term-no-keymap-corruption", .revision = 1 }, }, }, }, .production_boundary = .state_transition, }, .{ .id = "test-requirement-manifest-sm", .revision = 3, .suite = .sm, .fixture = .{ .id = "fixture-requirement-manifest-sm", .revision = 3, .path = "spec/fixtures/requirements/manifest_sm.md", .sha256 = "51a499a369b949bcdd811a4bbf42c82d6c2cee9b7ec1ed8788984044686b932e", }, .claims = .{ .{ .oracle = "INV-REQ-TJ-CORE-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-09", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-13", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-13", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-12", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-12", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-13", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-13", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-FAIL-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-fail-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-FAIL-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-fail-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LOG-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-log-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LOG-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-log-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LOG-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-log-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-04", .revision = 1 }, }, }, .{ .oracle = "INV-UI-ALL-HIDDEN-STATE", .kind = .required, .obligations = .{ .{ .id = "obligation-ui-all-hidden-state", .revision = 1 }, }, }, .{ .oracle = "INV-UI-ALL-HIDDEN-BULK", .kind = .required, .obligations = .{ .{ .id = "obligation-ui-all-hidden-bulk", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-05", .revision = 1 }, }, }, .{ .oracle = "INV-PLAN-REORDER-MATERIAL", .kind = .required, .obligations = .{ .{ .id = "obligation-plan-reorder-material", .revision = 1 }, }, }, .{ .oracle = "INV-PLAN-REORDER-EQUIVALENT", .kind = .required, .obligations = .{ .{ .id = "obligation-plan-reorder-equivalent", .revision = 1 }, }, }, .{ .oracle = "NO-PLAN-REORDER-CONFIRMATION", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-plan-reorder-no-confirmation", .revision = 1 }, }, }, .{ .oracle = "NO-UI-BULK-HIDDEN-SELECTION", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-ui-no-bulk-hidden-selection", .revision = 1 }, }, }, .{ .oracle = "NO-REQ-MANIFEST-UNBOUND-SM", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-requirement-manifest-no-unbound-pass-sm", .revision = 1 }, }, }, }, .production_boundary = .state_transition, }, .{ .id = "test-requirement-manifest-r", .revision = 4, .suite = .r, .fixture = .{ .id = "fixture-requirement-manifest-r", .revision = 4, .path = "spec/fixtures/requirements/manifest_r.md", .sha256 = "381b7b7296a05e00baf7908cf672d197db865487a989fffd3d9968355e5f1e30", }, .claims = .{ .{ .oracle = "INV-REQ-TJ-CORE-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-09", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CONCEPT-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-concept-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-09", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-13", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-13", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-12", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-12", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-09", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-EXEC-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-exec-05", .revision = 1 }, }, }, .{ .oracle = "INV-EXEC-EXPECTED-PRIOR-EFFECTS", .kind = .required, .obligations = .{ .{ .id = "obligation-exec-expected-prior-effects", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LOG-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-log-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-03", .revision = 1 }, }, }, .{ .oracle = "INV-UI-ALL-HIDDEN-STATE", .kind = .required, .obligations = .{ .{ .id = "obligation-ui-all-hidden-state", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-09", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-12", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-12", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TERM-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-term-02", .revision = 1 }, }, }, .{ .oracle = "INV-TERM-RESIZE-BELOW-MINIMUM", .kind = .required, .obligations = .{ .{ .id = "obligation-term-resize-below-minimum", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TERM-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-term-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TERM-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-term-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TERM-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-term-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TERM-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-term-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TERM-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-term-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-MAN-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-man-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-MAN-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-man-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-05", .revision = 1 }, }, }, .{ .oracle = "NO-REQ-MANIFEST-UNBOUND-R", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-requirement-manifest-no-unbound-pass-r", .revision = 1 }, }, }, .{ .oracle = "NO-EXEC-EXPECTED-EFFECT-MISMATCH", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-exec-expected-prior-effects-no-mismatch", .revision = 1 }, }, }, }, .production_boundary = .state_transition, }, .{ .id = "test-requirement-manifest-a", .revision = 3, .suite = .a, .fixture = .{ .id = "fixture-requirement-manifest-a", .revision = 3, .path = "spec/fixtures/requirements/manifest_a.md", .sha256 = "f9bde9440ca4965742a3a1fd2d41a3eb412eae51378566d0564e3fcb0a81276c", }, .claims = .{ .{ .oracle = "INV-REQ-TJ-CORE-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-09", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-12", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-12", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-15", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-15", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-16", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-16", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LINK-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-link-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LINK-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-link-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LINK-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-link-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LINK-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-link-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-12", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-12", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-13", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-13", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-EXEC-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-exec-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-EXEC-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-exec-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-EXEC-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-exec-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-EXEC-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-exec-04", .revision = 1 }, }, }, .{ .oracle = "INV-EXEC-ANCESTOR-REPLACEMENT", .kind = .required, .obligations = .{ .{ .id = "obligation-exec-drift-ancestor-replacement", .revision = 1 }, }, }, .{ .oracle = "INV-EXEC-LEAF-REPLACEMENT", .kind = .required, .obligations = .{ .{ .id = "obligation-exec-drift-leaf-replacement", .revision = 1 }, }, }, .{ .oracle = "INV-EXEC-MOUNT-CHANGE", .kind = .required, .obligations = .{ .{ .id = "obligation-exec-drift-mount-change", .revision = 1 }, }, }, .{ .oracle = "INV-EXEC-LINK-COUNT-CHANGE", .kind = .required, .obligations = .{ .{ .id = "obligation-exec-drift-link-count-change", .revision = 1 }, }, }, .{ .oracle = "INV-EXEC-CHILD-SET-DELTA", .kind = .required, .obligations = .{ .{ .id = "obligation-exec-drift-child-set-delta", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-FAIL-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-fail-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LOG-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-log-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LOG-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-log-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LOG-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-log-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LOG-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-log-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CONFIG-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-config-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CONFIG-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-config-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CONFIG-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-config-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-09", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-MAN-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-man-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-MAN-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-man-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-MAN-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-man-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-STYLE-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-style-01", .revision = 1 }, }, }, .{ .oracle = "INV-ADAPT-EFFECT-CHANGE-MEMBERSHIP", .kind = .required, .obligations = .{ .{ .id = "obligation-adapt-effect-change-membership", .revision = 1 }, }, }, .{ .oracle = "INV-ADAPT-EFFECT-CHANGE-HOOKS", .kind = .required, .obligations = .{ .{ .id = "obligation-adapt-effect-change-hooks", .revision = 1 }, }, }, .{ .oracle = "INV-ADAPT-EFFECT-CHANGE-CACHE-SCOPE", .kind = .required, .obligations = .{ .{ .id = "obligation-adapt-effect-change-cache-scope", .revision = 1 }, }, }, .{ .oracle = "INV-ADAPT-TUPLE-CHANGE-MANAGER-VERSION", .kind = .required, .obligations = .{ .{ .id = "obligation-adapt-tuple-change-manager-version", .revision = 1 }, }, }, .{ .oracle = "INV-ADAPT-TUPLE-CHANGE-RUNTIME-VERSION", .kind = .required, .obligations = .{ .{ .id = "obligation-adapt-tuple-change-runtime-version", .revision = 1 }, }, }, .{ .oracle = "INV-ADAPT-TUPLE-CHANGE-CONFIGURATION", .kind = .required, .obligations = .{ .{ .id = "obligation-adapt-tuple-change-configuration", .revision = 1 }, }, }, .{ .oracle = "NO-ADAPT-EFFECT-CHANGE-ADMISSION", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-adapt-effect-change-no-admission", .revision = 1 }, }, }, .{ .oracle = "NO-ADAPT-TUPLE-CHANGE-SUPPORTED", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-adapt-tuple-change-no-supported", .revision = 1 }, }, }, .{ .oracle = "NO-EXEC-MISMATCH-MUTATION", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-exec-drift-no-mismatch-mutation", .revision = 1 }, }, }, .{ .oracle = "NO-REQ-MANIFEST-UNBOUND-A", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-requirement-manifest-no-unbound-pass-a", .revision = 1 }, }, }, }, .production_boundary = .state_transition, }, .{ .id = "test-requirement-manifest-pty", .revision = 3, .suite = .pty, .fixture = .{ .id = "fixture-requirement-manifest-pty", .revision = 3, .path = "spec/fixtures/requirements/manifest_pty.md", .sha256 = "532933313389e19faaad79afe224195a1f86afd845a8b4499fbe1b3fc14eab83", }, .claims = .{ .{ .oracle = "INV-REQ-TJ-CORE-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-09", .revision = 1 }, }, }, .{ .oracle = "INV-CONFIRM-BUFFERED-DISCARDED", .kind = .required, .obligations = .{ .{ .id = "obligation-confirm-buffered-input", .revision = 1 }, }, }, .{ .oracle = "INV-CONFIRM-PASTE-NEVER-CONFIRMS", .kind = .required, .obligations = .{ .{ .id = "obligation-confirm-paste-no-confirm", .revision = 1 }, }, }, .{ .oracle = "INV-CONFIRM-AUTO-REPEAT", .kind = .required, .obligations = .{ .{ .id = "obligation-confirm-auto-repeat", .revision = 1 }, }, }, .{ .oracle = "INV-CONFIRM-LEGACY-DISCLOSURE", .kind = .required, .obligations = .{ .{ .id = "obligation-confirm-legacy-disclosure", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-FAIL-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-fail-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-09", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TERM-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-term-02", .revision = 1 }, }, }, .{ .oracle = "INV-TERM-RESIZE-BELOW-MINIMUM", .kind = .required, .obligations = .{ .{ .id = "obligation-term-resize-below-minimum", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TERM-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-term-07", .revision = 1 }, }, }, .{ .oracle = "INV-TERM-FRAGMENTED-INPUT", .kind = .required, .obligations = .{ .{ .id = "obligation-term-fragmented-input", .revision = 1 }, }, }, .{ .oracle = "INV-TERM-MALFORMED-MOUSE", .kind = .required, .obligations = .{ .{ .id = "obligation-term-malformed-mouse", .revision = 1 }, }, }, .{ .oracle = "INV-TERM-KEYBOARD-RECOVERY", .kind = .required, .obligations = .{ .{ .id = "obligation-term-keyboard-recovery", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TERM-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-term-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TERM-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-term-09", .revision = 1 }, }, }, .{ .oracle = "INV-TERM-RESTORE-NORMAL-EXIT", .kind = .required, .obligations = .{ .{ .id = "obligation-term-exit-restore-normal", .revision = 1 }, }, }, .{ .oracle = "INV-TERM-STARTUP-ERROR", .kind = .required, .obligations = .{ .{ .id = "obligation-term-startup-error", .revision = 1 }, }, }, .{ .oracle = "INV-TERM-RESTORE-RUNTIME-ERROR", .kind = .required, .obligations = .{ .{ .id = "obligation-term-exit-restore-runtime-error", .revision = 1 }, }, }, .{ .oracle = "INV-TERM-RESTORE-HANDLED-SIGNALS", .kind = .required, .obligations = .{ .{ .id = "obligation-term-restore-signals", .revision = 1 }, }, }, .{ .oracle = "INV-TERM-SUSPEND-RESUME", .kind = .required, .obligations = .{ .{ .id = "obligation-term-suspend-resume", .revision = 1 }, }, }, .{ .oracle = "INV-TERM-DISCONNECT-RESTORE", .kind = .required, .obligations = .{ .{ .id = "obligation-term-disconnect-restore", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TERM-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-term-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CONFIG-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-config-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-05", .revision = 1 }, }, }, .{ .oracle = "NO-REQ-MANIFEST-UNBOUND-PTY", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-requirement-manifest-no-unbound-pass-pty", .revision = 1 }, }, }, .{ .oracle = "NO-TERM-UNRESTORED-EXIT", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-term-no-unrestored-exit", .revision = 1 }, }, }, .{ .oracle = "NO-CONFIRM-STALE-ADMISSION", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-confirm-no-stale-admission", .revision = 1 }, }, }, .{ .oracle = "NO-TERM-KEYMAP-CORRUPTION", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-term-no-keymap-corruption", .revision = 1 }, }, }, }, .production_boundary = .state_transition, }, .{ .id = "test-requirement-manifest-sim", .revision = 4, .suite = .sim, .fixture = .{ .id = "fixture-requirement-manifest-sim", .revision = 4, .path = "spec/fixtures/requirements/manifest_sim.md", .sha256 = "ce5a52c57064a2b4667577499e343c26688fb9be9646415728fe720a7a4a1db3", }, .claims = .{ .{ .oracle = "INV-REQ-TJ-CORE-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-09", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CLASS-12", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-class-12", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LINK-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-link-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LINK-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-link-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-EXEC-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-exec-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-EXEC-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-exec-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-EXEC-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-exec-04", .revision = 1 }, }, }, .{ .oracle = "INV-EXEC-ANCESTOR-REPLACEMENT", .kind = .required, .obligations = .{ .{ .id = "obligation-exec-drift-ancestor-replacement", .revision = 1 }, }, }, .{ .oracle = "INV-EXEC-LEAF-REPLACEMENT", .kind = .required, .obligations = .{ .{ .id = "obligation-exec-drift-leaf-replacement", .revision = 1 }, }, }, .{ .oracle = "INV-EXEC-MOUNT-CHANGE", .kind = .required, .obligations = .{ .{ .id = "obligation-exec-drift-mount-change", .revision = 1 }, }, }, .{ .oracle = "INV-EXEC-LINK-COUNT-CHANGE", .kind = .required, .obligations = .{ .{ .id = "obligation-exec-drift-link-count-change", .revision = 1 }, }, }, .{ .oracle = "INV-EXEC-CHILD-SET-DELTA", .kind = .required, .obligations = .{ .{ .id = "obligation-exec-drift-child-set-delta", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-FAIL-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-fail-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-FAIL-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-fail-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LOG-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-log-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-UI-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-ui-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PERF-02", .kind = .required, .obligations = .{ .{ .id = "obligation-perf-budgets", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PERF-04", .kind = .required, .obligations = .{ .{ .id = "obligation-perf-measurement", .revision = 1 }, }, }, .{ .oracle = "INV-ADAPT-EFFECT-CHANGE-MEMBERSHIP", .kind = .required, .obligations = .{ .{ .id = "obligation-adapt-effect-change-membership", .revision = 1 }, }, }, .{ .oracle = "INV-ADAPT-EFFECT-CHANGE-HOOKS", .kind = .required, .obligations = .{ .{ .id = "obligation-adapt-effect-change-hooks", .revision = 1 }, }, }, .{ .oracle = "INV-ADAPT-EFFECT-CHANGE-CACHE-SCOPE", .kind = .required, .obligations = .{ .{ .id = "obligation-adapt-effect-change-cache-scope", .revision = 1 }, }, }, .{ .oracle = "NO-ADAPT-EFFECT-CHANGE-ADMISSION", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-adapt-effect-change-no-admission", .revision = 1 }, }, }, .{ .oracle = "NO-EXEC-MISMATCH-MUTATION", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-exec-drift-no-mismatch-mutation", .revision = 1 }, }, }, .{ .oracle = "NO-REQ-MANIFEST-UNBOUND-SIM", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-requirement-manifest-no-unbound-pass-sim", .revision = 1 }, }, }, }, .production_boundary = .state_transition, }, .{ .id = "test-requirement-manifest-m", .revision = 4, .suite = .m, .fixture = .{ .id = "fixture-requirement-manifest-m", .revision = 4, .path = "spec/fixtures/requirements/manifest_m.md", .sha256 = "cc859bcee79eb7e00033419d130115f7141f70d538fb8d47a3d62d691d82a54f", }, .claims = .{ .{ .oracle = "INV-REQ-TJ-GOAL-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-goal-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-CORE-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-core-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SCAN-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-scan-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LIMIT-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-limit-09", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-SIZE-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-size-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ADAPT-13", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-adapt-13", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PLAN-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-plan-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-EXEC-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-exec-01", .revision = 1 }, }, }, .{ .oracle = "INV-EXEC-ANCESTOR-REPLACEMENT", .kind = .required, .obligations = .{ .{ .id = "obligation-exec-drift-ancestor-replacement", .revision = 1 }, }, }, .{ .oracle = "INV-EXEC-LEAF-REPLACEMENT", .kind = .required, .obligations = .{ .{ .id = "obligation-exec-drift-leaf-replacement", .revision = 1 }, }, }, .{ .oracle = "INV-EXEC-MOUNT-CHANGE", .kind = .required, .obligations = .{ .{ .id = "obligation-exec-drift-mount-change", .revision = 1 }, }, }, .{ .oracle = "INV-EXEC-LINK-COUNT-CHANGE", .kind = .required, .obligations = .{ .{ .id = "obligation-exec-drift-link-count-change", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-EXEC-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-exec-05", .revision = 1 }, }, }, .{ .oracle = "INV-EXEC-EXPECTED-PRIOR-EFFECTS", .kind = .required, .obligations = .{ .{ .id = "obligation-exec-expected-prior-effects", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-LOG-03", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-log-03", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TERM-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-term-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-09", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-ART-12", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-art-12", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-MAN-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-man-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-01", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-01", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-06", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-06", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-07", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-07", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-08", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-08", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-09", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-09", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-10", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-10", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-11", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-11", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-12", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-12", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-DIST-13", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-dist-13", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-02", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-02", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-04", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-04", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-TEST-05", .kind = .required, .obligations = .{ .{ .id = "obligation-requirement-tj-test-05", .revision = 1 }, }, }, .{ .oracle = "INV-REQ-TJ-PERF-06", .kind = .required, .obligations = .{ .{ .id = "obligation-perf-profiling-evidence", .revision = 1 }, }, }, .{ .oracle = "INV-ADAPT-TUPLE-CHANGE-MANAGER-VERSION", .kind = .required, .obligations = .{ .{ .id = "obligation-adapt-tuple-change-manager-version", .revision = 1 }, }, }, .{ .oracle = "INV-ADAPT-TUPLE-CHANGE-RUNTIME-VERSION", .kind = .required, .obligations = .{ .{ .id = "obligation-adapt-tuple-change-runtime-version", .revision = 1 }, }, }, .{ .oracle = "INV-ADAPT-TUPLE-CHANGE-CONFIGURATION", .kind = .required, .obligations = .{ .{ .id = "obligation-adapt-tuple-change-configuration", .revision = 1 }, }, }, .{ .oracle = "NO-ADAPT-TUPLE-CHANGE-SUPPORTED", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-adapt-tuple-change-no-supported", .revision = 1 }, }, }, .{ .oracle = "NO-EXEC-EXPECTED-EFFECT-MISMATCH", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-exec-expected-prior-effects-no-mismatch", .revision = 1 }, }, }, .{ .oracle = "NO-REQ-MANIFEST-UNBOUND-M", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-requirement-manifest-no-unbound-pass-m", .revision = 1 }, }, }, }, .production_boundary = .state_transition, }, .{ .id = "test-exec-mutation-a", .revision = 1, .suite = .a, .fixture = .{ .id = "fixture-test-exec-mutation-a", .revision = 4, .path = "spec/fixtures/exec/mutation_a.md", .sha256 = "5474c83f65485238b7e74cc109fff1d8e9454bd13bc2b1922bba2232768ee184", }, .claims = .{ .{ .oracle = "INV-EXEC-MUTATION-A", .kind = .required, .obligations = .{ .{ .id = "obligation-test-exec-mutation-a-holds", .revision = 1 }, }, }, .{ .oracle = "INV-EXEC-ANCESTOR-A", .kind = .required, .obligations = .{ .{ .id = "obligation-test-exec-mutation-a-ancestors", .revision = 1 }, }, }, .{ .oracle = "INV-EXEC-DIRECTORY-A", .kind = .required, .obligations = .{ .{ .id = "obligation-test-exec-mutation-a-directory", .revision = 1 }, }, }, .{ .oracle = "NO-EXEC-DIRECTORY-A", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-test-exec-mutation-a-directory-forbids", .revision = 1 }, }, }, .{ .oracle = "NO-EXEC-MUTATION-A", .kind = .forbidden, .obligations = .{ .{ .id = "obligation-test-exec-mutation-a-forbids", .revision = 1 }, }, }, }, .production_boundary = .process, }, }