Skip to content

Commit dfb8525

Browse files
authored
Settle candidates only through verified atomic binding-plus-receipt commits (#242)
* Settle candidates only through verified atomic binding-plus-receipt commits An immutable candidate becomes accepted state only when verification succeeds and the exact objective binding plus its receipt commit atomically. Receipts move to schema 4 with explicit prior/requested/result objective lineage so the exact accepted delta is provable from the receipt alone. A second domain-neutral revisioned-register fixture executes reusable settlement laws — positive admission, verification rejection, freshness drift, substitution, commit failure, concurrency, replay, restart reconstruction, and fail-closed reading — and white-box counterexamples prove those laws reject dishonest store and reader implementations. * Seal converged self-review attestation
1 parent 8acf654 commit dfb8525

13 files changed

Lines changed: 1639 additions & 29 deletions
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
{
2+
"reviewed_tree": "a76b668137a154fe54cbf0d3cf5398ebda7387ff",
3+
"program_fingerprint": "3ca3397ff275d89bdb6d5c934b86b51d3cbdfab0ee628c47fe94d1d4f5767155"
4+
}

boatstack/kernel/conformance/conformance.go

Lines changed: 20 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -114,7 +114,10 @@ func (suite KernelConformance) objectiveBinding(t *testing.T) {
114114
if after.State.ObjectiveBinding == nil || !after.State.ObjectiveBinding.Matches(fixture.Scenario.Objective) {
115115
t.Fatal("control-law objective-binding: apply did not bind the exact objective")
116116
}
117-
if after.CommitCount != before.CommitCount+1 || len(after.Receipts) != len(before.Receipts)+1 || receipt.ObjectiveBinding == nil {
117+
if after.CommitCount != before.CommitCount+1 || len(after.Receipts) != len(before.Receipts)+1 ||
118+
receipt.PriorObjectiveBinding != nil ||
119+
receipt.RequestedObjectiveBinding == nil || !receipt.RequestedObjectiveBinding.Matches(fixture.Scenario.Objective) ||
120+
receipt.ResultObjectiveBinding == nil || !receipt.ResultObjectiveBinding.Matches(fixture.Scenario.Objective) {
118121
t.Fatalf("control-law objective-binding: commit/receipt evidence is incomplete: %#v", after)
119122
}
120123
}
@@ -127,6 +130,10 @@ func (suite KernelConformance) objectiveAbsence(t *testing.T) {
127130
if before.State.ObjectiveBinding != nil || after.State.ObjectiveBinding != nil {
128131
t.Fatal("control-law objective-absence: maintenance synthesized an objective binding")
129132
}
133+
receipt := after.Receipts[len(after.Receipts)-1]
134+
if receipt.PriorObjectiveBinding != nil || receipt.RequestedObjectiveBinding != nil || receipt.ResultObjectiveBinding != nil {
135+
t.Fatalf("control-law objective-absence: maintenance receipt synthesized objective lineage: %#v", receipt)
136+
}
130137
}
131138

132139
func (suite KernelConformance) maintenancePreservesExactBinding(t *testing.T) {
@@ -137,6 +144,12 @@ func (suite KernelConformance) maintenancePreservesExactBinding(t *testing.T) {
137144
if before.State.ObjectiveBinding == nil || after.State.ObjectiveBinding == nil || *after.State.ObjectiveBinding != *before.State.ObjectiveBinding {
138145
t.Fatal("control-law objective-preservation: maintenance changed the exact binding")
139146
}
147+
receipt := after.Receipts[len(after.Receipts)-1]
148+
if !reflect.DeepEqual(receipt.PriorObjectiveBinding, before.State.ObjectiveBinding) ||
149+
receipt.RequestedObjectiveBinding != nil ||
150+
!reflect.DeepEqual(receipt.ResultObjectiveBinding, after.State.ObjectiveBinding) {
151+
t.Fatalf("control-law objective-preservation: receipt lineage differs from preserved binding: %#v", receipt)
152+
}
140153
}
141154

142155
func (suite KernelConformance) objectiveRevisionInvalidatesPrescription(t *testing.T) {
@@ -811,7 +824,12 @@ func committedOutcomeError(program kernel.Program, scenario Scenario, before, af
811824
if !ok {
812825
return fmt.Errorf("returned receipt transition is absent from program")
813826
}
814-
if after.State.InstanceID != returned.InstanceID || after.State.Program != returned.Program || after.State.Revision != returned.ResultStateRevision || after.State.Mode != transition.TargetMode || after.State.Recovery != nil || !reflect.DeepEqual(after.State.ObjectiveBinding, returned.ObjectiveBinding) {
827+
if !reflect.DeepEqual(returned.PriorObjectiveBinding, before.State.ObjectiveBinding) ||
828+
!reflect.DeepEqual(returned.RequestedObjectiveBinding, prescription.RequestedObjectiveBinding) ||
829+
!reflect.DeepEqual(returned.ResultObjectiveBinding, after.State.ObjectiveBinding) {
830+
return fmt.Errorf("receipt objective lineage differs from prior, requested, or resulting state")
831+
}
832+
if after.State.InstanceID != returned.InstanceID || after.State.Program != returned.Program || after.State.Revision != returned.ResultStateRevision || after.State.Mode != transition.TargetMode || after.State.Recovery != nil {
815833
return fmt.Errorf("durable state differs from winning receipt outcome")
816834
}
817835
if err := exactEffectDelta(before.Effects, after.Effects, returned.TransitionID, 1); err != nil {

boatstack/kernel/conformance/conformance_test.go

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -229,6 +229,49 @@ func TestCommittedOutcomeRejectsFalsePriorObservation(t *testing.T) {
229229
}
230230
}
231231

232+
func TestCommittedOutcomeRejectsObjectiveLineageSubstitution(t *testing.T) {
233+
for name, mutate := range map[string]func(*kernel.Receipt, *kernel.ObjectiveBinding){
234+
"prior": func(receipt *kernel.Receipt, other *kernel.ObjectiveBinding) {
235+
receipt.PriorObjectiveBinding = other
236+
},
237+
"requested": func(receipt *kernel.Receipt, other *kernel.ObjectiveBinding) {
238+
receipt.RequestedObjectiveBinding = other
239+
},
240+
"result": func(receipt *kernel.Receipt, other *kernel.ObjectiveBinding) {
241+
receipt.ResultObjectiveBinding = other
242+
},
243+
} {
244+
t.Run(name, func(t *testing.T) {
245+
fixture := newIntegerFixture(SetupUnbound)
246+
runtime := mustRuntime(t, fixture)
247+
request, prescription := resolve(t, runtime, fixture.Scenario, fixture.Scenario.BindTransition, &fixture.Scenario.Objective, fixture.Scenario.Authority)
248+
before := fixture.Scenario.Snapshot()
249+
returned, err := runtime.Apply(context.Background(), kernel.ApplyRequest{ResolveRequest: request, Prescription: prescription})
250+
if err != nil {
251+
t.Fatal(err)
252+
}
253+
other, err := kernel.BindObjective(fixture.Scenario.ConflictingObjective)
254+
if err != nil {
255+
t.Fatal(err)
256+
}
257+
mutate(&returned, &other)
258+
returned.ID = ""
259+
digest, err := kernel.Fingerprint(returned)
260+
if err != nil {
261+
t.Fatal(err)
262+
}
263+
returned.ID = "rcp-" + digest
264+
receipts := fixture.Store.(*MemoryStateStore).receipts
265+
receipts.mu.Lock()
266+
receipts.values[len(receipts.values)-1] = returned
267+
receipts.mu.Unlock()
268+
if err := committedOutcomeError(fixture.Program, fixture.Scenario, before, fixture.Scenario.Snapshot(), prescription, returned); err == nil {
269+
t.Fatalf("content-rehashed %s objective lineage substitution was accepted", name)
270+
}
271+
})
272+
}
273+
}
274+
232275
func TestCommittedOutcomeRejectsNoOpAcceptedByDomainVerifier(t *testing.T) {
233276
fixture := newIntegerFixture(SetupBound)
234277
domain := fixture.Domain.(*IntegerDomain)

0 commit comments

Comments
 (0)