P12.c DiffT Before 5211acfe95a0c6d82a60e2524b5e46b47fe67a3e After bb35b941115a0a9f818e8512eebe67c29ee68355 Threshold: ZERO semantic mismatches to declared oracle; ZERO reducer mismatches; all mandatory head assertions PASS. Compare each stream and service/upstream channel independently; ignore only cross-channel arrival interleaving. --- P12.c 5211acfe95a0c6d82a60e2524b5e46b47fe67a3e +++ P12.c bb35b941115a0a9f818e8512eebe67c29ee68355 @@ -23,36 +23,40 @@ "hasWorkingTreeChanges": false, "isDefaultRef": false, "isRepo": true, - "refName": "A", + "refName": "B", "workingTree": { "deletions": 0, "files": [], "insertions": 0 } }, - "remote": { - "aheadCount": 0, - "aheadOfDefaultCount": 1, - "behindCount": 0, - "hasUpstream": true, - "pr": { - "baseRef": "main", - "headRef": "A", - "number": 613, - "state": "open", - "title": "Fixture A", - "url": "https://github.com/proof-audit/status-fixture/pull/613" - } - } + "remote": null }, "expectedPredicate": true, - "observedPredicate": false, - "outcome": "FAIL", + "observedPredicate": true, + "outcome": "PASS", "test": "held-A-discarded-B-null", "virtualTimeMs": 10000 } ], - "branchProbeChannel": [], + "branchProbeChannel": [ + { + "branch": "A", + "virtualTimeMs": 0 + }, + { + "branch": "A", + "virtualTimeMs": 0 + }, + { + "branch": "A", + "virtualTimeMs": 10000 + }, + { + "branch": "B", + "virtualTimeMs": 10000 + } + ], "checkpoints": [ { "localReads": 1, @@ -86,9 +90,34 @@ "virtualTimeMs": 10000 }, { - "events": [], + "events": [ + { + "_tag": "remoteUpdated", + "remote": null + }, + { + "_tag": "localUpdated", + "local": { + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "refName": "B", + "workingTree": { + "deletions": 0, + "files": [], + "insertions": 0 + } + } + } + ], "kind": "tick-outcome", - "localReadsOwned": 0, + "localReadsOwned": 1, "remoteReadsOwned": 1, "snapshot": { "_tag": "snapshot", @@ -102,27 +131,14 @@ "hasWorkingTreeChanges": false, "isDefaultRef": false, "isRepo": true, - "refName": "A", + "refName": "B", "workingTree": { "deletions": 0, "files": [], "insertions": 0 } }, - "remote": { - "aheadCount": 0, - "aheadOfDefaultCount": 1, - "behindCount": 0, - "hasUpstream": true, - "pr": { - "baseRef": "main", - "headRef": "A", - "number": 613, - "state": "open", - "title": "Fixture A", - "url": "https://github.com/proof-audit/status-fixture/pull/613" - } - } + "remote": null }, "variant": "held-switch", "virtualTimeMs": 10000 @@ -131,6 +147,12 @@ "invalidationChannel": [ { "kind": "invalidate-remote" + }, + { + "kind": "invalidate-remote" + }, + { + "kind": "invalidate-local" } ], "localReadChannel": [ @@ -154,6 +176,27 @@ }, "n": 1, "virtualTimeMs": 0 + }, + { + "local": { + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "refName": "B", + "workingTree": { + "deletions": 0, + "files": [], + "insertions": 0 + } + }, + "n": 2, + "virtualTimeMs": 10000 } ], "mutations": [ @@ -214,51 +257,31 @@ "hasWorkingTreeChanges": false, "isDefaultRef": false, "isRepo": true, - "refName": "A", + "refName": "B", "workingTree": { "deletions": 0, "files": [], "insertions": 0 } }, - "remote": { - "aheadCount": 0, - "aheadOfDefaultCount": 1, - "behindCount": 0, - "hasUpstream": true, - "pr": { - "baseRef": "main", - "headRef": "A", - "number": 613, - "state": "open", - "title": "Fixture A", - "url": "https://github.com/proof-audit/status-fixture/pull/613" - } - } + "remote": null }, "merged": { "aheadCount": 0, - "aheadOfDefaultCount": 1, - "behindCount": 0, - "branchChanges": { - "baseRef": "origin/main", - "deletions": 0, - "insertions": 1 - }, - "hasPrimaryRemote": true, - "hasUpstream": true, - "hasWorkingTreeChanges": false, - "isDefaultRef": false, - "isRepo": true, - "pr": { - "baseRef": "main", - "headRef": "A", - "number": 613, - "state": "open", - "title": "Fixture A", - "url": "https://github.com/proof-audit/status-fixture/pull/613" - }, - "refName": "A", + "aheadOfDefaultCount": 0, + "behindCount": 0, + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasUpstream": false, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "pr": null, + "refName": "B", "workingTree": { "deletions": 0, "files": [], @@ -452,6 +475,80 @@ } }, "virtualTimeMs": 0 + }, + { + "event": { + "_tag": "remoteUpdated", + "remote": null + }, + "merged": { + "aheadCount": 0, + "aheadOfDefaultCount": 0, + "behindCount": 0, + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasUpstream": false, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "pr": null, + "refName": "A", + "workingTree": { + "deletions": 0, + "files": [], + "insertions": 0 + } + }, + "virtualTimeMs": 10000 + }, + { + "event": { + "_tag": "localUpdated", + "local": { + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "refName": "B", + "workingTree": { + "deletions": 0, + "files": [], + "insertions": 0 + } + } + }, + "merged": { + "aheadCount": 0, + "aheadOfDefaultCount": 0, + "behindCount": 0, + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasUpstream": false, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "pr": null, + "refName": "B", + "workingTree": { + "deletions": 0, + "files": [], + "insertions": 0 + } + }, + "virtualTimeMs": 10000 } ], "P12-held-switch/P12-held-switch/passive-1": [ @@ -520,6 +617,80 @@ } }, "virtualTimeMs": 0 + }, + { + "event": { + "_tag": "remoteUpdated", + "remote": null + }, + "merged": { + "aheadCount": 0, + "aheadOfDefaultCount": 0, + "behindCount": 0, + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasUpstream": false, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "pr": null, + "refName": "A", + "workingTree": { + "deletions": 0, + "files": [], + "insertions": 0 + } + }, + "virtualTimeMs": 10000 + }, + { + "event": { + "_tag": "localUpdated", + "local": { + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "refName": "B", + "workingTree": { + "deletions": 0, + "files": [], + "insertions": 0 + } + } + }, + "merged": { + "aheadCount": 0, + "aheadOfDefaultCount": 0, + "behindCount": 0, + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasUpstream": false, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "pr": null, + "refName": "B", + "workingTree": { + "deletions": 0, + "files": [], + "insertions": 0 + } + }, + "virtualTimeMs": 10000 } ] }