@@ -144,7 +144,7 @@ func (suite KernelConformance) stalePrescriptionPrecedesEffects(t *testing.T) {
144144 fixture .Scenario .ChangeObservation ()
145145 _ , err := runtime .Apply (context .Background (), kernel.ApplyRequest {ResolveRequest : request , Prescription : prescription })
146146 after := fixture .Scenario .Snapshot ()
147- if ! kernel .IsStale (err ) || effectCount (after , transition ) != effectCount (before , transition ) || after .CommitCount != before .CommitCount {
147+ if ! kernel .IsStale (err ) || effectCount (after , transition ) != effectCount (before , transition ) || after .CommitCount != before .CommitCount || len ( after . Receipts ) != len ( before . Receipts ) {
148148 t .Fatalf ("control-law prescription-freshness: error=%v before=%#v after=%#v" , err , before , after )
149149 }
150150}
@@ -161,7 +161,7 @@ func (suite KernelConformance) authorityDenialFailsClosed(t *testing.T) {
161161 request .Authority = kernel.Authority {}
162162 _ , err = runtime .Apply (context .Background (), kernel.ApplyRequest {ResolveRequest : request , Prescription : prescription })
163163 after := fixture .Scenario .Snapshot ()
164- if ! kernel .IsStale (err ) || effectCount (after , transition ) != effectCount (before , transition ) || after .CommitCount != before .CommitCount {
164+ if ! kernel .IsStale (err ) || effectCount (after , transition ) != effectCount (before , transition ) || after .CommitCount != before .CommitCount || len ( after . Receipts ) != len ( before . Receipts ) {
165165 t .Fatalf ("control-law authority-denial: apply error=%v before=%#v after=%#v" , err , before , after )
166166 }
167167}
@@ -175,7 +175,7 @@ func (suite KernelConformance) futureAuthorityFailsClosed(t *testing.T) {
175175 before := fixture .Scenario .Snapshot ()
176176 resolution , err := runtime .Resolve (context .Background (), kernel.ResolveRequest {InstanceID : fixture .Scenario .InstanceID , Objective : & fixture .Scenario .Objective , Authority : authority , Requested : transition })
177177 after := fixture .Scenario .Snapshot ()
178- if err != nil || resolution .Decision .Kind != kernel .Refused || effectCount (after , transition ) != effectCount (before , transition ) || after .CommitCount != before .CommitCount {
178+ if err != nil || resolution .Decision .Kind != kernel .Refused || effectCount (after , transition ) != effectCount (before , transition ) || after .CommitCount != before .CommitCount || len ( after . Receipts ) != len ( before . Receipts ) {
179179 t .Fatalf ("control-law authority-time-validity: decision=%#v error=%v" , resolution .Decision , err )
180180 }
181181}
@@ -191,7 +191,7 @@ func (suite KernelConformance) capabilityClassifierCannotBeWeakened(t *testing.T
191191 before := fixture .Scenario .Snapshot ()
192192 resolution , err := runtime .Resolve (context .Background (), kernel.ResolveRequest {InstanceID : fixture .Scenario .InstanceID , Objective : & fixture .Scenario .Objective , Authority : fixture .Scenario .Authority , Requested : transition })
193193 after := fixture .Scenario .Snapshot ()
194- if err != nil || resolution .Decision .Kind != kernel .Frontier || effectCount (after , transition ) != effectCount (before , transition ) {
194+ if err != nil || resolution .Decision .Kind != kernel .Frontier || effectCount (after , transition ) != effectCount (before , transition ) || after . CommitCount != before . CommitCount || len ( after . Receipts ) != len ( before . Receipts ) {
195195 t .Fatalf ("control-law capability-non-weakening: decision=%#v error=%v" , resolution .Decision , err )
196196 }
197197}
@@ -218,9 +218,10 @@ func (suite KernelConformance) interruptedOperatorRequiresExplicitRecovery(t *te
218218 transition := fixture .Scenario .AdvanceTransitions [0 ]
219219 fixture .Scenario .InterruptNextOperator ()
220220 request , prescription := resolve (t , runtime , fixture .Scenario , transition , & fixture .Scenario .Objective , fixture .Scenario .Authority )
221+ before := fixture .Scenario .Snapshot ()
221222 _ , err := runtime .Apply (context .Background (), kernel.ApplyRequest {ResolveRequest : request , Prescription : prescription })
222223 interrupted := fixture .Scenario .Snapshot ()
223- if ! kernel .IsRecoveryRequired (err ) || interrupted .State .Recovery == nil || interrupted .State .Recovery .TransitionID != transition || effectCount (interrupted , transition ) != 1 {
224+ if ! kernel .IsRecoveryRequired (err ) || interrupted .State .Recovery == nil || interrupted .State .Recovery .TransitionID != transition || effectCount (interrupted , transition ) != effectCount ( before , transition ) + 1 || interrupted . CommitCount != before . CommitCount || len ( interrupted . Receipts ) != len ( before . Receipts ) {
224225 t .Fatalf ("control-law explicit-recovery: state=%#v error=%v" , interrupted , err )
225226 }
226227 recovery := resolveAndApply (t , runtime , fixture .Program , fixture .Scenario , fixture .Scenario .RecoveryTransition , & fixture .Scenario .Objective )
@@ -235,17 +236,18 @@ func (suite KernelConformance) processPanicRequiresExplicitRecovery(t *testing.T
235236 transition := fixture .Scenario .AdvanceTransitions [0 ]
236237 fixture .Scenario .PanicNextOperator ()
237238 request , prescription := resolve (t , runtime , fixture .Scenario , transition , & fixture .Scenario .Objective , fixture .Scenario .Authority )
239+ before := fixture .Scenario .Snapshot ()
238240 var recovered any
239241 func () {
240242 defer func () { recovered = recover () }()
241243 _ , _ = runtime .Apply (context .Background (), kernel.ApplyRequest {ResolveRequest : request , Prescription : prescription })
242244 }()
243245 after := fixture .Scenario .Snapshot ()
244- if recovered == nil || after .State .Recovery == nil || after .State .Recovery .TransitionID != transition || effectCount (after , transition ) != 1 {
246+ if recovered == nil || after .State .Recovery == nil || after .State .Recovery .TransitionID != transition || effectCount (after , transition ) != effectCount ( before , transition ) + 1 || after . CommitCount != before . CommitCount || len ( after . Receipts ) != len ( before . Receipts ) {
245247 t .Fatalf ("control-law panic-recovery: panic=%v snapshot=%#v" , recovered , after )
246248 }
247249 resolution , err := runtime .Resolve (context .Background (), kernel.ResolveRequest {InstanceID : fixture .Scenario .InstanceID , Objective : & fixture .Scenario .Objective , Authority : fixture .Scenario .Authority })
248- if err != nil || resolution .Decision .Kind != kernel .Prescribed || resolution .Decision .Transition != fixture .Scenario .RecoveryTransition || effectCount (fixture .Scenario .Snapshot (), transition ) != 1 {
250+ if err != nil || resolution .Decision .Kind != kernel .Prescribed || resolution .Decision .Transition != fixture .Scenario .RecoveryTransition || effectCount (fixture .Scenario .Snapshot (), transition ) != effectCount ( before , transition ) + 1 {
249251 t .Fatalf ("control-law panic-no-replay: decision=%#v error=%v" , resolution .Decision , err )
250252 }
251253}
@@ -255,13 +257,14 @@ func (suite KernelConformance) atomicCommitFailureRequiresRecovery(t *testing.T)
255257 transition := fixture .Scenario .AdvanceTransitions [0 ]
256258 fixture .Scenario .FailNextCommit ()
257259 request , prescription := resolve (t , runtime , fixture .Scenario , transition , & fixture .Scenario .Objective , fixture .Scenario .Authority )
260+ before := fixture .Scenario .Snapshot ()
258261 _ , err := runtime .Apply (context .Background (), kernel.ApplyRequest {ResolveRequest : request , Prescription : prescription })
259262 after := fixture .Scenario .Snapshot ()
260- if ! kernel .IsRecoveryRequired (err ) || after .State .Recovery == nil || after .CommitCount != 0 || len (after .Receipts ) != 0 || effectCount (after , transition ) != 1 {
263+ if ! kernel .IsRecoveryRequired (err ) || after .State .Recovery == nil || after .CommitCount != before . CommitCount || len (after .Receipts ) != len ( before . Receipts ) || effectCount (after , transition ) != effectCount ( before , transition ) + 1 {
261264 t .Fatalf ("control-law atomic-commit-recovery: snapshot=%#v error=%v" , after , err )
262265 }
263266 resolution , resolveErr := runtime .Resolve (context .Background (), kernel.ResolveRequest {InstanceID : fixture .Scenario .InstanceID , Objective : & fixture .Scenario .Objective , Authority : fixture .Scenario .Authority })
264- if resolveErr != nil || resolution .Decision .Kind != kernel .Prescribed || resolution .Decision .Transition != fixture .Scenario .RecoveryTransition || effectCount (fixture .Scenario .Snapshot (), transition ) != 1 {
267+ if resolveErr != nil || resolution .Decision .Kind != kernel .Prescribed || resolution .Decision .Transition != fixture .Scenario .RecoveryTransition || effectCount (fixture .Scenario .Snapshot (), transition ) != effectCount ( before , transition ) + 1 {
265268 t .Fatalf ("control-law no-duplicate-effect: decision=%#v error=%v" , resolution .Decision , resolveErr )
266269 }
267270}
@@ -271,22 +274,23 @@ func (suite KernelConformance) failedRecoveryPreservesOriginalObligation(t *test
271274 transition := fixture .Scenario .AdvanceTransitions [0 ]
272275 fixture .Scenario .InterruptNextOperator ()
273276 request , prescription := resolve (t , runtime , fixture .Scenario , transition , & fixture .Scenario .Objective , fixture .Scenario .Authority )
277+ before := fixture .Scenario .Snapshot ()
274278 _ , err := runtime .Apply (context .Background (), kernel.ApplyRequest {ResolveRequest : request , Prescription : prescription })
275279 interrupted := fixture .Scenario .Snapshot ()
276- if ! kernel .IsRecoveryRequired (err ) || interrupted .State .Recovery == nil {
280+ if ! kernel .IsRecoveryRequired (err ) || interrupted .State .Recovery == nil || effectCount ( interrupted , transition ) != effectCount ( before , transition ) + 1 || interrupted . CommitCount != before . CommitCount || len ( interrupted . Receipts ) != len ( before . Receipts ) {
277281 t .Fatalf ("control-law recovery-retry: initial state=%#v error=%v" , interrupted .State , err )
278282 }
279283 original := * interrupted .State .Recovery
280284 recoveryRequest , recoveryPrescription := resolve (t , runtime , fixture .Scenario , fixture .Scenario .RecoveryTransition , & fixture .Scenario .Objective , fixture .Scenario .Authority )
281285 fixture .Scenario .FailNextCommit ()
282286 _ , err = runtime .Apply (context .Background (), kernel.ApplyRequest {ResolveRequest : recoveryRequest , Prescription : recoveryPrescription })
283287 failed := fixture .Scenario .Snapshot ()
284- if ! kernel .IsRecoveryRequired (err ) || failed .State .Recovery == nil || * failed .State .Recovery != original || effectCount (failed , transition ) != 1 {
288+ if ! kernel .IsRecoveryRequired (err ) || failed .State .Recovery == nil || * failed .State .Recovery != original || effectCount (failed , transition ) != effectCount ( interrupted , transition ) || failed . CommitCount != interrupted . CommitCount || len ( failed . Receipts ) != len ( interrupted . Receipts ) {
285289 t .Fatalf ("control-law recovery-obligation-preservation: state=%#v error=%v" , failed .State , err )
286290 }
287291 resolveAndApply (t , runtime , fixture .Program , fixture .Scenario , fixture .Scenario .RecoveryTransition , & fixture .Scenario .Objective )
288292 settled := fixture .Scenario .Snapshot ()
289- if settled .State .Recovery != nil || effectCount (settled , transition ) != 1 {
293+ if settled .State .Recovery != nil || effectCount (settled , transition ) != effectCount ( interrupted , transition ) {
290294 t .Fatalf ("control-law recovery-retry: state=%#v" , settled .State )
291295 }
292296}
@@ -301,7 +305,7 @@ func (suite KernelConformance) prescriptionCannotReplayAcrossInstances(t *testin
301305 request .InstanceID = other
302306 _ , err := runtime .Apply (context .Background (), kernel.ApplyRequest {ResolveRequest : request , Prescription : prescription })
303307 after := fixture .Scenario .Snapshot ()
304- if ! kernel .IsStale (err ) || effectCount (after , transition ) != effectCount (before , transition ) || after .CommitCount != before .CommitCount {
308+ if ! kernel .IsStale (err ) || effectCount (after , transition ) != effectCount (before , transition ) || after .CommitCount != before .CommitCount || len ( after . Receipts ) != len ( before . Receipts ) {
305309 t .Fatalf ("control-law prescription-instance-binding: error=%v snapshot=%#v" , err , after )
306310 }
307311}
@@ -337,7 +341,7 @@ func (suite KernelConformance) concurrentApplyCommitsOnce(t *testing.T) {
337341 }
338342 }
339343 after := fixture .Scenario .Snapshot ()
340- if successes != 1 || refusals != 1 || after .CommitCount != 1 || len (after .Receipts ) != 1 || effectCount (after , transition ) != 1 {
344+ if successes != 1 || refusals != 1 || after .CommitCount != before . CommitCount + 1 || len (after .Receipts ) != len ( before . Receipts ) + 1 || effectCount (after , transition ) != effectCount ( before , transition ) + 1 {
341345 t .Fatalf ("control-law concurrent-cas: success/refusal=%d/%d snapshot=%#v" , successes , refusals , after )
342346 }
343347 if err := committedOutcomeError (fixture .Program , before , after , winner ); err != nil {
@@ -347,6 +351,7 @@ func (suite KernelConformance) concurrentApplyCommitsOnce(t *testing.T) {
347351
348352func (suite KernelConformance ) programReachesMarkedState (t * testing.T ) {
349353 fixture , runtime := suite .fresh (t , SetupUnbound )
354+ before := fixture .Scenario .Snapshot ()
350355 receipts , err := runUntargetedToMarked (context .Background (), runtime , fixture .Program , fixture .Scenario , len (fixture .Scenario .AdvanceTransitions )+ 1 )
351356 if err != nil {
352357 t .Fatal (err )
@@ -357,7 +362,7 @@ func (suite KernelConformance) programReachesMarkedState(t *testing.T) {
357362 }
358363 }
359364 after := fixture .Scenario .Snapshot ()
360- if ! fixture .Program .Marked (after .State .Mode ) || len (after .Receipts ) != len (receipts ) {
365+ if ! fixture .Program .Marked (after .State .Mode ) || len (after .Receipts ) != len (before . Receipts ) + len ( receipts ) {
361366 t .Fatalf ("control-law marked-reachability: snapshot=%#v" , after )
362367 }
363368}
0 commit comments