diff --git a/labs/22-yield/distribution/release-notes/2026-08-01-remove-stray-analysis-traces.md b/labs/22-yield/distribution/release-notes/2026-08-01-remove-stray-analysis-traces.md new file mode 100644 index 00000000..6f58c396 --- /dev/null +++ b/labs/22-yield/distribution/release-notes/2026-08-01-remove-stray-analysis-traces.md @@ -0,0 +1,6 @@ +### Remove stray analysis traces + +Deletes `runs/*.jsonl` — scratch traces from the formal-analysis tooling +that were accidentally committed alongside the multi-language release — +and excludes `runs/` and `target/` from the published surface so scratch +state can never ship again. No code changes. diff --git a/labs/22-yield/publish.config.json b/labs/22-yield/publish.config.json index a8030b3b..d338d5fb 100644 --- a/labs/22-yield/publish.config.json +++ b/labs/22-yield/publish.config.json @@ -29,7 +29,9 @@ "node_modules", "__pycache__", "dist", - "build" + "build", + "runs", + "target" ] }, { diff --git a/labs/22-yield/yield/.gitignore b/labs/22-yield/yield/.gitignore index 1114cf50..8942527a 100644 --- a/labs/22-yield/yield/.gitignore +++ b/labs/22-yield/yield/.gitignore @@ -1,2 +1,3 @@ .yield/ target/ +runs/ diff --git a/labs/22-yield/yield/runs/run-1785553716242371000.jsonl b/labs/22-yield/yield/runs/run-1785553716242371000.jsonl deleted file mode 100644 index 00147ee4..00000000 --- a/labs/22-yield/yield/runs/run-1785553716242371000.jsonl +++ /dev/null @@ -1 +0,0 @@ -{"run_id":"run-1785553716242371000","seq":0,"kind":"obligations","operator_id":"verification.trace-refinement","operator_version":"0.1.0","model_id":"yield-sdk-execution-contract-v1","input_sha256":"8e00a49824e8dbe1ad5a423dbfb04f35d9724e122e5c89b76dd5a607f66171da","evidence_consumed":[{"path":"labs/22-yield/yield/sdk/yield/yield.go","note":"Go SDK: step() replay/compare/emit, Main() terminal emission — the behavior TS/Python SDKs must refine"},{"path":"labs/22-yield/yield/internal/engine/engine.go","note":"supervisor: execute() consumes exactly one ProgramOutput per subprocess execution"}],"gate_verdict":{"operator_id":"verification.trace-refinement","operator_version":"0.1.0","model_id":"yield-sdk-execution-contract-v1","decision":"applicable","satisfied":[{"id":"candidate-states","check":"has-facet:states","description":"A discrete-event facet with declared states — the candidate under analysis.","satisfied":true},{"id":"candidate-events","check":"has-facet:events","description":"A declared event alphabet, shared by candidate and reference.","satisfied":true},{"id":"candidate-transitions","check":"has-facet:transitions","description":"Candidate transitions over the declared states and events.","satisfied":true},{"id":"reference-present","check":"has-facet:reference","description":"A reference automaton — the behavior the candidate is compared against must be declared, not assumed.","satisfied":true},{"id":"shared-alphabet","check":"reference-shares-alphabet","description":"Every reference transition draws its event from the main alphabet; a refinement question is only well-posed over a shared alphabet.","satisfied":true},{"id":"observation-window","check":"all-events-marked-observability","description":"Every event marked observable or unobservable — the projection both systems are compared under is declared, never assumed.","satisfied":true,"obtainable":true},{"id":"transition-lineage","check":"evidence-present:transitions","description":"Candidate transitions carry evidence references into the real system.","satisfied":true,"obtainable":true}]},"output_sha256":"87cad68bc6fce9901855fcb7a0d466e8ff4dfb23dc1e02c0ff90db592b1f9948","verify_report":{"schema_ok":true,"invariants":[{"invariant":"witness-is-a-valid-candidate-path","passed":true},{"invariant":"witness-projection-refused-by-reference","passed":true},{"invariant":"refines-iff-no-witness","passed":true}],"accepted":true}} diff --git a/labs/22-yield/yield/runs/run-1785553716271239000.jsonl b/labs/22-yield/yield/runs/run-1785553716271239000.jsonl deleted file mode 100644 index 2499e25d..00000000 --- a/labs/22-yield/yield/runs/run-1785553716271239000.jsonl +++ /dev/null @@ -1 +0,0 @@ -{"run_id":"run-1785553716271239000","seq":0,"kind":"obligations","operator_id":"control.nonblockingness","operator_version":"0.1.0","model_id":"yield-sdk-execution-contract-v1","input_sha256":"8e00a49824e8dbe1ad5a423dbfb04f35d9724e122e5c89b76dd5a607f66171da","evidence_consumed":[{"path":"labs/22-yield/yield/sdk/yield/yield.go","note":"Go SDK: step() replay/compare/emit, Main() terminal emission — the behavior TS/Python SDKs must refine"},{"path":"labs/22-yield/yield/internal/engine/engine.go","note":"supervisor: execute() consumes exactly one ProgramOutput per subprocess execution"}],"gate_verdict":{"operator_id":"control.nonblockingness","operator_version":"0.1.0","model_id":"yield-sdk-execution-contract-v1","decision":"applicable","satisfied":[{"id":"automaton-states","check":"has-facet:states","description":"A discrete-event facet with declared states.","satisfied":true},{"id":"automaton-events","check":"has-facet:events","description":"A declared event alphabet.","satisfied":true},{"id":"automaton-transitions","check":"has-facet:transitions","description":"Plant transitions over the declared states and events.","satisfied":true},{"id":"target-set","check":"has-target-states","description":"A declared target set that resolves to at least one state — completion must be named, not assumed.","satisfied":true,"obtainable":true},{"id":"transition-lineage","check":"evidence-present:transitions","description":"Transitions carry evidence references into the real system.","satisfied":true,"obtainable":true}]},"output_sha256":"1c69803c36f8acfc4f17b66b0d16d3812fab3095fce46409ca884712af197850","verify_report":{"schema_ok":true,"invariants":[{"invariant":"blocking-states-have-no-marked-path","passed":true},{"invariant":"nonblocking-states-have-marked-path","passed":true}],"accepted":true}} diff --git a/labs/22-yield/yield/runs/run-1785553716296303000.jsonl b/labs/22-yield/yield/runs/run-1785553716296303000.jsonl deleted file mode 100644 index e9b82d54..00000000 --- a/labs/22-yield/yield/runs/run-1785553716296303000.jsonl +++ /dev/null @@ -1 +0,0 @@ -{"run_id":"run-1785553716296303000","seq":0,"kind":"obligations","operator_id":"control.supervisory-rw","operator_version":"0.1.0","model_id":"yield-run-lifecycle-protocol-v1","input_sha256":"82c3490000357d66bc1f35623176a9b0279800340684047d46696d2eb43677d2","evidence_consumed":[{"path":"private/yield-landing/index.html","note":"design artifact: run-log states, five primitives, stale/duplicate rejection, evidence-bound completion, replay-diverges-loudly"}],"gate_verdict":{"operator_id":"control.supervisory-rw","operator_version":"0.1.0","model_id":"yield-run-lifecycle-protocol-v1","decision":"applicable","satisfied":[{"id":"automaton-states","check":"has-facet:states","description":"A discrete-event facet with declared states.","satisfied":true},{"id":"automaton-events","check":"has-facet:events","description":"A declared event alphabet.","satisfied":true},{"id":"automaton-transitions","check":"has-facet:transitions","description":"Plant transitions over the declared states and events.","satisfied":true},{"id":"controllability-partition","check":"all-events-marked-controllability","description":"Every event marked controllable or uncontrollable (the Sigma_c / Sigma_u partition).","satisfied":true,"obtainable":true},{"id":"spec-present","check":"has-spec-forbidden","description":"A specification naming forbidden states or forbidden (state, event) transitions.","satisfied":true,"obtainable":true},{"id":"transition-lineage","check":"evidence-present:transitions","description":"Transitions carry evidence references into the real system.","satisfied":true,"obtainable":true}]},"output_sha256":"31c828008c9d3a7daf3f21695916e7ecfafe80b87218fa06c2cfd3f8b12ee173","verify_report":{"schema_ok":true,"invariants":[{"invariant":"violations-empty-iff-controllable","passed":true},{"invariant":"violating-events-are-uncontrollable","passed":true},{"invariant":"violating-states-are-reachable","passed":true}],"accepted":true}} diff --git a/labs/22-yield/yield/runs/run-1785553723942017000.jsonl b/labs/22-yield/yield/runs/run-1785553723942017000.jsonl deleted file mode 100644 index 448f360b..00000000 --- a/labs/22-yield/yield/runs/run-1785553723942017000.jsonl +++ /dev/null @@ -1 +0,0 @@ -{"run_id":"run-1785553723942017000","seq":0,"kind":"obligations","operator_id":"verification.trace-refinement","operator_version":"0.1.0","model_id":"yield-sdk-execution-contract-v1","input_sha256":"8e00a49824e8dbe1ad5a423dbfb04f35d9724e122e5c89b76dd5a607f66171da","evidence_consumed":[{"path":"labs/22-yield/yield/sdk/yield/yield.go","note":"Go SDK: step() replay/compare/emit, Main() terminal emission — the behavior TS/Python SDKs must refine"},{"path":"labs/22-yield/yield/internal/engine/engine.go","note":"supervisor: execute() consumes exactly one ProgramOutput per subprocess execution"}],"gate_verdict":{"operator_id":"verification.trace-refinement","operator_version":"0.1.0","model_id":"yield-sdk-execution-contract-v1","decision":"applicable","satisfied":[{"id":"candidate-states","check":"has-facet:states","description":"A discrete-event facet with declared states — the candidate under analysis.","satisfied":true},{"id":"candidate-events","check":"has-facet:events","description":"A declared event alphabet, shared by candidate and reference.","satisfied":true},{"id":"candidate-transitions","check":"has-facet:transitions","description":"Candidate transitions over the declared states and events.","satisfied":true},{"id":"reference-present","check":"has-facet:reference","description":"A reference automaton — the behavior the candidate is compared against must be declared, not assumed.","satisfied":true},{"id":"shared-alphabet","check":"reference-shares-alphabet","description":"Every reference transition draws its event from the main alphabet; a refinement question is only well-posed over a shared alphabet.","satisfied":true},{"id":"observation-window","check":"all-events-marked-observability","description":"Every event marked observable or unobservable — the projection both systems are compared under is declared, never assumed.","satisfied":true,"obtainable":true},{"id":"transition-lineage","check":"evidence-present:transitions","description":"Candidate transitions carry evidence references into the real system.","satisfied":true,"obtainable":true}]},"output_sha256":"87cad68bc6fce9901855fcb7a0d466e8ff4dfb23dc1e02c0ff90db592b1f9948","verify_report":{"schema_ok":true,"invariants":[{"invariant":"witness-is-a-valid-candidate-path","passed":true},{"invariant":"witness-projection-refused-by-reference","passed":true},{"invariant":"refines-iff-no-witness","passed":true}],"accepted":true}} diff --git a/labs/22-yield/yield/runs/run-1785553734059599000.jsonl b/labs/22-yield/yield/runs/run-1785553734059599000.jsonl deleted file mode 100644 index e766f00d..00000000 --- a/labs/22-yield/yield/runs/run-1785553734059599000.jsonl +++ /dev/null @@ -1 +0,0 @@ -{"run_id":"run-1785553734059599000","seq":0,"kind":"obligations","operator_id":"verification.trace-refinement","operator_version":"0.1.0","model_id":"yield-sdk-execution-contract-v1","input_sha256":"8e00a49824e8dbe1ad5a423dbfb04f35d9724e122e5c89b76dd5a607f66171da","evidence_consumed":[{"path":"labs/22-yield/yield/sdk/yield/yield.go","note":"Go SDK: step() replay/compare/emit, Main() terminal emission — the behavior TS/Python SDKs must refine"},{"path":"labs/22-yield/yield/internal/engine/engine.go","note":"supervisor: execute() consumes exactly one ProgramOutput per subprocess execution"}],"gate_verdict":{"operator_id":"verification.trace-refinement","operator_version":"0.1.0","model_id":"yield-sdk-execution-contract-v1","decision":"applicable","satisfied":[{"id":"candidate-states","check":"has-facet:states","description":"A discrete-event facet with declared states — the candidate under analysis.","satisfied":true},{"id":"candidate-events","check":"has-facet:events","description":"A declared event alphabet, shared by candidate and reference.","satisfied":true},{"id":"candidate-transitions","check":"has-facet:transitions","description":"Candidate transitions over the declared states and events.","satisfied":true},{"id":"reference-present","check":"has-facet:reference","description":"A reference automaton — the behavior the candidate is compared against must be declared, not assumed.","satisfied":true},{"id":"shared-alphabet","check":"reference-shares-alphabet","description":"Every reference transition draws its event from the main alphabet; a refinement question is only well-posed over a shared alphabet.","satisfied":true},{"id":"observation-window","check":"all-events-marked-observability","description":"Every event marked observable or unobservable — the projection both systems are compared under is declared, never assumed.","satisfied":true,"obtainable":true},{"id":"transition-lineage","check":"evidence-present:transitions","description":"Candidate transitions carry evidence references into the real system.","satisfied":true,"obtainable":true}]},"output_sha256":"87cad68bc6fce9901855fcb7a0d466e8ff4dfb23dc1e02c0ff90db592b1f9948","verify_report":{"schema_ok":true,"invariants":[{"invariant":"witness-is-a-valid-candidate-path","passed":true},{"invariant":"witness-projection-refused-by-reference","passed":true},{"invariant":"refines-iff-no-witness","passed":true}],"accepted":true}} diff --git a/labs/22-yield/yield/runs/run-1785553734097586000.jsonl b/labs/22-yield/yield/runs/run-1785553734097586000.jsonl deleted file mode 100644 index 6dc20548..00000000 --- a/labs/22-yield/yield/runs/run-1785553734097586000.jsonl +++ /dev/null @@ -1 +0,0 @@ -{"run_id":"run-1785553734097586000","seq":0,"kind":"obligations","operator_id":"control.nonblockingness","operator_version":"0.1.0","model_id":"yield-sdk-execution-contract-v1","input_sha256":"8e00a49824e8dbe1ad5a423dbfb04f35d9724e122e5c89b76dd5a607f66171da","evidence_consumed":[{"path":"labs/22-yield/yield/sdk/yield/yield.go","note":"Go SDK: step() replay/compare/emit, Main() terminal emission — the behavior TS/Python SDKs must refine"},{"path":"labs/22-yield/yield/internal/engine/engine.go","note":"supervisor: execute() consumes exactly one ProgramOutput per subprocess execution"}],"gate_verdict":{"operator_id":"control.nonblockingness","operator_version":"0.1.0","model_id":"yield-sdk-execution-contract-v1","decision":"applicable","satisfied":[{"id":"automaton-states","check":"has-facet:states","description":"A discrete-event facet with declared states.","satisfied":true},{"id":"automaton-events","check":"has-facet:events","description":"A declared event alphabet.","satisfied":true},{"id":"automaton-transitions","check":"has-facet:transitions","description":"Plant transitions over the declared states and events.","satisfied":true},{"id":"target-set","check":"has-target-states","description":"A declared target set that resolves to at least one state — completion must be named, not assumed.","satisfied":true,"obtainable":true},{"id":"transition-lineage","check":"evidence-present:transitions","description":"Transitions carry evidence references into the real system.","satisfied":true,"obtainable":true}]},"output_sha256":"1c69803c36f8acfc4f17b66b0d16d3812fab3095fce46409ca884712af197850","verify_report":{"schema_ok":true,"invariants":[{"invariant":"blocking-states-have-no-marked-path","passed":true},{"invariant":"nonblocking-states-have-marked-path","passed":true}],"accepted":true}} diff --git a/labs/22-yield/yield/runs/run-1785553734123623000.jsonl b/labs/22-yield/yield/runs/run-1785553734123623000.jsonl deleted file mode 100644 index 9919ea80..00000000 --- a/labs/22-yield/yield/runs/run-1785553734123623000.jsonl +++ /dev/null @@ -1 +0,0 @@ -{"run_id":"run-1785553734123623000","seq":0,"kind":"obligations","operator_id":"control.supervisory-rw","operator_version":"0.1.0","model_id":"yield-run-lifecycle-protocol-v1","input_sha256":"82c3490000357d66bc1f35623176a9b0279800340684047d46696d2eb43677d2","evidence_consumed":[{"path":"private/yield-landing/index.html","note":"design artifact: run-log states, five primitives, stale/duplicate rejection, evidence-bound completion, replay-diverges-loudly"}],"gate_verdict":{"operator_id":"control.supervisory-rw","operator_version":"0.1.0","model_id":"yield-run-lifecycle-protocol-v1","decision":"applicable","satisfied":[{"id":"automaton-states","check":"has-facet:states","description":"A discrete-event facet with declared states.","satisfied":true},{"id":"automaton-events","check":"has-facet:events","description":"A declared event alphabet.","satisfied":true},{"id":"automaton-transitions","check":"has-facet:transitions","description":"Plant transitions over the declared states and events.","satisfied":true},{"id":"controllability-partition","check":"all-events-marked-controllability","description":"Every event marked controllable or uncontrollable (the Sigma_c / Sigma_u partition).","satisfied":true,"obtainable":true},{"id":"spec-present","check":"has-spec-forbidden","description":"A specification naming forbidden states or forbidden (state, event) transitions.","satisfied":true,"obtainable":true},{"id":"transition-lineage","check":"evidence-present:transitions","description":"Transitions carry evidence references into the real system.","satisfied":true,"obtainable":true}]},"output_sha256":"31c828008c9d3a7daf3f21695916e7ecfafe80b87218fa06c2cfd3f8b12ee173","verify_report":{"schema_ok":true,"invariants":[{"invariant":"violations-empty-iff-controllable","passed":true},{"invariant":"violating-events-are-uncontrollable","passed":true},{"invariant":"violating-states-are-reachable","passed":true}],"accepted":true}} diff --git a/labs/22-yield/yield/runs/run-1785553740031355000.jsonl b/labs/22-yield/yield/runs/run-1785553740031355000.jsonl deleted file mode 100644 index b1d51a22..00000000 --- a/labs/22-yield/yield/runs/run-1785553740031355000.jsonl +++ /dev/null @@ -1 +0,0 @@ -{"run_id":"run-1785553740031355000","seq":0,"kind":"obligations","operator_id":"verification.trace-refinement","operator_version":"0.1.0","model_id":"yield-sdk-execution-contract-v1","input_sha256":"8e00a49824e8dbe1ad5a423dbfb04f35d9724e122e5c89b76dd5a607f66171da","evidence_consumed":[{"path":"labs/22-yield/yield/sdk/yield/yield.go","note":"Go SDK: step() replay/compare/emit, Main() terminal emission — the behavior TS/Python SDKs must refine"},{"path":"labs/22-yield/yield/internal/engine/engine.go","note":"supervisor: execute() consumes exactly one ProgramOutput per subprocess execution"}],"gate_verdict":{"operator_id":"verification.trace-refinement","operator_version":"0.1.0","model_id":"yield-sdk-execution-contract-v1","decision":"applicable","satisfied":[{"id":"candidate-states","check":"has-facet:states","description":"A discrete-event facet with declared states — the candidate under analysis.","satisfied":true},{"id":"candidate-events","check":"has-facet:events","description":"A declared event alphabet, shared by candidate and reference.","satisfied":true},{"id":"candidate-transitions","check":"has-facet:transitions","description":"Candidate transitions over the declared states and events.","satisfied":true},{"id":"reference-present","check":"has-facet:reference","description":"A reference automaton — the behavior the candidate is compared against must be declared, not assumed.","satisfied":true},{"id":"shared-alphabet","check":"reference-shares-alphabet","description":"Every reference transition draws its event from the main alphabet; a refinement question is only well-posed over a shared alphabet.","satisfied":true},{"id":"observation-window","check":"all-events-marked-observability","description":"Every event marked observable or unobservable — the projection both systems are compared under is declared, never assumed.","satisfied":true,"obtainable":true},{"id":"transition-lineage","check":"evidence-present:transitions","description":"Candidate transitions carry evidence references into the real system.","satisfied":true,"obtainable":true}]},"output_sha256":"87cad68bc6fce9901855fcb7a0d466e8ff4dfb23dc1e02c0ff90db592b1f9948","verify_report":{"schema_ok":true,"invariants":[{"invariant":"witness-is-a-valid-candidate-path","passed":true},{"invariant":"witness-projection-refused-by-reference","passed":true},{"invariant":"refines-iff-no-witness","passed":true}],"accepted":true}} diff --git a/labs/22-yield/yield/runs/run-1785553763925295000.jsonl b/labs/22-yield/yield/runs/run-1785553763925295000.jsonl deleted file mode 100644 index 0489f697..00000000 --- a/labs/22-yield/yield/runs/run-1785553763925295000.jsonl +++ /dev/null @@ -1 +0,0 @@ -{"run_id":"run-1785553763925295000","seq":0,"kind":"obligations","operator_id":"control.nonblockingness","operator_version":"0.1.0","model_id":"yield-sdk-execution-contract-v1","input_sha256":"8e00a49824e8dbe1ad5a423dbfb04f35d9724e122e5c89b76dd5a607f66171da","evidence_consumed":[{"path":"labs/22-yield/yield/sdk/yield/yield.go","note":"Go SDK: step() replay/compare/emit, Main() terminal emission — the behavior TS/Python SDKs must refine"},{"path":"labs/22-yield/yield/internal/engine/engine.go","note":"supervisor: execute() consumes exactly one ProgramOutput per subprocess execution"}],"gate_verdict":{"operator_id":"control.nonblockingness","operator_version":"0.1.0","model_id":"yield-sdk-execution-contract-v1","decision":"applicable","satisfied":[{"id":"automaton-states","check":"has-facet:states","description":"A discrete-event facet with declared states.","satisfied":true},{"id":"automaton-events","check":"has-facet:events","description":"A declared event alphabet.","satisfied":true},{"id":"automaton-transitions","check":"has-facet:transitions","description":"Plant transitions over the declared states and events.","satisfied":true},{"id":"target-set","check":"has-target-states","description":"A declared target set that resolves to at least one state — completion must be named, not assumed.","satisfied":true,"obtainable":true},{"id":"transition-lineage","check":"evidence-present:transitions","description":"Transitions carry evidence references into the real system.","satisfied":true,"obtainable":true}]},"output_sha256":"1c69803c36f8acfc4f17b66b0d16d3812fab3095fce46409ca884712af197850","verify_report":{"schema_ok":true,"invariants":[{"invariant":"blocking-states-have-no-marked-path","passed":true},{"invariant":"nonblocking-states-have-marked-path","passed":true}],"accepted":true}} diff --git a/labs/22-yield/yield/runs/run-1785553763947600000.jsonl b/labs/22-yield/yield/runs/run-1785553763947600000.jsonl deleted file mode 100644 index 96bfce34..00000000 --- a/labs/22-yield/yield/runs/run-1785553763947600000.jsonl +++ /dev/null @@ -1 +0,0 @@ -{"run_id":"run-1785553763947600000","seq":0,"kind":"obligations","operator_id":"control.supervisory-rw","operator_version":"0.1.0","model_id":"yield-run-lifecycle-protocol-v1","input_sha256":"82c3490000357d66bc1f35623176a9b0279800340684047d46696d2eb43677d2","evidence_consumed":[{"path":"private/yield-landing/index.html","note":"design artifact: run-log states, five primitives, stale/duplicate rejection, evidence-bound completion, replay-diverges-loudly"}],"gate_verdict":{"operator_id":"control.supervisory-rw","operator_version":"0.1.0","model_id":"yield-run-lifecycle-protocol-v1","decision":"applicable","satisfied":[{"id":"automaton-states","check":"has-facet:states","description":"A discrete-event facet with declared states.","satisfied":true},{"id":"automaton-events","check":"has-facet:events","description":"A declared event alphabet.","satisfied":true},{"id":"automaton-transitions","check":"has-facet:transitions","description":"Plant transitions over the declared states and events.","satisfied":true},{"id":"controllability-partition","check":"all-events-marked-controllability","description":"Every event marked controllable or uncontrollable (the Sigma_c / Sigma_u partition).","satisfied":true,"obtainable":true},{"id":"spec-present","check":"has-spec-forbidden","description":"A specification naming forbidden states or forbidden (state, event) transitions.","satisfied":true,"obtainable":true},{"id":"transition-lineage","check":"evidence-present:transitions","description":"Transitions carry evidence references into the real system.","satisfied":true,"obtainable":true}]},"output_sha256":"31c828008c9d3a7daf3f21695916e7ecfafe80b87218fa06c2cfd3f8b12ee173","verify_report":{"schema_ok":true,"invariants":[{"invariant":"violations-empty-iff-controllable","passed":true},{"invariant":"violating-events-are-uncontrollable","passed":true},{"invariant":"violating-states-are-reachable","passed":true}],"accepted":true}} diff --git a/labs/22-yield/yield/runs/run-1785553763965938000.jsonl b/labs/22-yield/yield/runs/run-1785553763965938000.jsonl deleted file mode 100644 index 13bce023..00000000 --- a/labs/22-yield/yield/runs/run-1785553763965938000.jsonl +++ /dev/null @@ -1 +0,0 @@ -{"run_id":"run-1785553763965938000","seq":0,"kind":"obligations","operator_id":"control.nonblockingness","operator_version":"0.1.0","model_id":"yield-run-lifecycle-protocol-v1","input_sha256":"82c3490000357d66bc1f35623176a9b0279800340684047d46696d2eb43677d2","evidence_consumed":[{"path":"private/yield-landing/index.html","note":"design artifact: run-log states, five primitives, stale/duplicate rejection, evidence-bound completion, replay-diverges-loudly"}],"gate_verdict":{"operator_id":"control.nonblockingness","operator_version":"0.1.0","model_id":"yield-run-lifecycle-protocol-v1","decision":"applicable","satisfied":[{"id":"automaton-states","check":"has-facet:states","description":"A discrete-event facet with declared states.","satisfied":true},{"id":"automaton-events","check":"has-facet:events","description":"A declared event alphabet.","satisfied":true},{"id":"automaton-transitions","check":"has-facet:transitions","description":"Plant transitions over the declared states and events.","satisfied":true},{"id":"target-set","check":"has-target-states","description":"A declared target set that resolves to at least one state — completion must be named, not assumed.","satisfied":true,"obtainable":true},{"id":"transition-lineage","check":"evidence-present:transitions","description":"Transitions carry evidence references into the real system.","satisfied":true,"obtainable":true}]},"output_sha256":"d1f27298d8c86646e1d6cfe15bf400591da6ea679985c65dcb50b46922c4b556","verify_report":{"schema_ok":true,"invariants":[{"invariant":"blocking-states-have-no-marked-path","passed":true},{"invariant":"nonblocking-states-have-marked-path","passed":true}],"accepted":true}} diff --git a/labs/22-yield/yield/runs/run-1785553763983488000.jsonl b/labs/22-yield/yield/runs/run-1785553763983488000.jsonl deleted file mode 100644 index e81cfc24..00000000 --- a/labs/22-yield/yield/runs/run-1785553763983488000.jsonl +++ /dev/null @@ -1 +0,0 @@ -{"run_id":"run-1785553763983488000","seq":0,"kind":"obligations","operator_id":"control.diagnosability","operator_version":"0.1.0","model_id":"yield-offprotocol-portable-v1","input_sha256":"71f2880721196f42c82cc152c49dff6d0fd4ac71a84586c468f66442bc305051","evidence_consumed":[{"path":"private/yield-landing/index.html","note":"design artifact: run-log states, five primitives, stale/duplicate rejection, evidence-bound completion, replay-diverges-loudly"}],"gate_verdict":{"operator_id":"control.diagnosability","operator_version":"0.1.0","model_id":"yield-offprotocol-portable-v1","decision":"applicable","satisfied":[{"id":"automaton-states","check":"has-facet:states","description":"A discrete-event facet with declared states.","satisfied":true},{"id":"automaton-events","check":"has-facet:events","description":"A declared event alphabet.","satisfied":true},{"id":"automaton-transitions","check":"has-facet:transitions","description":"Plant transitions over the declared states and events.","satisfied":true},{"id":"observability-partition","check":"all-events-marked-observability","description":"Every event marked observable or unobservable (the observation mask).","satisfied":true,"obtainable":true},{"id":"spec-present","check":"has-spec-forbidden","description":"A specification naming the fault: forbidden states or forbidden (state, event) transitions.","satisfied":true,"obtainable":true},{"id":"transition-lineage","check":"evidence-present:transitions","description":"Transitions carry evidence references into the real system.","satisfied":true,"obtainable":true}]},"output_sha256":"fe6352801ce59ae07cb0678642fdd58531228f7011303e454f52323a05045ede","verify_report":{"schema_ok":true,"invariants":[{"invariant":"pairs-empty-iff-diagnosable","passed":true}],"accepted":true}} diff --git a/labs/22-yield/yield/runs/run-1785553968444780000.jsonl b/labs/22-yield/yield/runs/run-1785553968444780000.jsonl deleted file mode 100644 index d9bbb90e..00000000 --- a/labs/22-yield/yield/runs/run-1785553968444780000.jsonl +++ /dev/null @@ -1 +0,0 @@ -{"run_id":"run-1785553968444780000","seq":0,"kind":"obligations","operator_id":"control.supervisory-rw","operator_version":"0.1.0","model_id":"yield-run-lifecycle-protocol-v1","input_sha256":"82c3490000357d66bc1f35623176a9b0279800340684047d46696d2eb43677d2","evidence_consumed":[{"path":"private/yield-landing/index.html","note":"design artifact: run-log states, five primitives, stale/duplicate rejection, evidence-bound completion, replay-diverges-loudly"}],"gate_verdict":{"operator_id":"control.supervisory-rw","operator_version":"0.1.0","model_id":"yield-run-lifecycle-protocol-v1","decision":"applicable","satisfied":[{"id":"automaton-states","check":"has-facet:states","description":"A discrete-event facet with declared states.","satisfied":true},{"id":"automaton-events","check":"has-facet:events","description":"A declared event alphabet.","satisfied":true},{"id":"automaton-transitions","check":"has-facet:transitions","description":"Plant transitions over the declared states and events.","satisfied":true},{"id":"controllability-partition","check":"all-events-marked-controllability","description":"Every event marked controllable or uncontrollable (the Sigma_c / Sigma_u partition).","satisfied":true,"obtainable":true},{"id":"spec-present","check":"has-spec-forbidden","description":"A specification naming forbidden states or forbidden (state, event) transitions.","satisfied":true,"obtainable":true},{"id":"transition-lineage","check":"evidence-present:transitions","description":"Transitions carry evidence references into the real system.","satisfied":true,"obtainable":true}]},"output_sha256":"31c828008c9d3a7daf3f21695916e7ecfafe80b87218fa06c2cfd3f8b12ee173","verify_report":{"schema_ok":true,"invariants":[{"invariant":"violations-empty-iff-controllable","passed":true},{"invariant":"violating-events-are-uncontrollable","passed":true},{"invariant":"violating-states-are-reachable","passed":true}],"accepted":true}}