Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions .github/reviews/trusted-settlement.receipt.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
{
"reviewed_tree": "a76b668137a154fe54cbf0d3cf5398ebda7387ff",
"program_fingerprint": "3ca3397ff275d89bdb6d5c934b86b51d3cbdfab0ee628c47fe94d1d4f5767155"
}
22 changes: 20 additions & 2 deletions boatstack/kernel/conformance/conformance.go
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,10 @@ func (suite KernelConformance) objectiveBinding(t *testing.T) {
if after.State.ObjectiveBinding == nil || !after.State.ObjectiveBinding.Matches(fixture.Scenario.Objective) {
t.Fatal("control-law objective-binding: apply did not bind the exact objective")
}
if after.CommitCount != before.CommitCount+1 || len(after.Receipts) != len(before.Receipts)+1 || receipt.ObjectiveBinding == nil {
if after.CommitCount != before.CommitCount+1 || len(after.Receipts) != len(before.Receipts)+1 ||
receipt.PriorObjectiveBinding != nil ||
receipt.RequestedObjectiveBinding == nil || !receipt.RequestedObjectiveBinding.Matches(fixture.Scenario.Objective) ||
receipt.ResultObjectiveBinding == nil || !receipt.ResultObjectiveBinding.Matches(fixture.Scenario.Objective) {
t.Fatalf("control-law objective-binding: commit/receipt evidence is incomplete: %#v", after)
}
}
Expand All @@ -127,6 +130,10 @@ func (suite KernelConformance) objectiveAbsence(t *testing.T) {
if before.State.ObjectiveBinding != nil || after.State.ObjectiveBinding != nil {
t.Fatal("control-law objective-absence: maintenance synthesized an objective binding")
}
receipt := after.Receipts[len(after.Receipts)-1]
if receipt.PriorObjectiveBinding != nil || receipt.RequestedObjectiveBinding != nil || receipt.ResultObjectiveBinding != nil {
t.Fatalf("control-law objective-absence: maintenance receipt synthesized objective lineage: %#v", receipt)
}
}

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

func (suite KernelConformance) objectiveRevisionInvalidatesPrescription(t *testing.T) {
Expand Down Expand Up @@ -811,7 +824,12 @@ func committedOutcomeError(program kernel.Program, scenario Scenario, before, af
if !ok {
return fmt.Errorf("returned receipt transition is absent from program")
}
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) {
if !reflect.DeepEqual(returned.PriorObjectiveBinding, before.State.ObjectiveBinding) ||
!reflect.DeepEqual(returned.RequestedObjectiveBinding, prescription.RequestedObjectiveBinding) ||
!reflect.DeepEqual(returned.ResultObjectiveBinding, after.State.ObjectiveBinding) {
return fmt.Errorf("receipt objective lineage differs from prior, requested, or resulting state")
}
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 {
return fmt.Errorf("durable state differs from winning receipt outcome")
}
if err := exactEffectDelta(before.Effects, after.Effects, returned.TransitionID, 1); err != nil {
Expand Down
43 changes: 43 additions & 0 deletions boatstack/kernel/conformance/conformance_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -229,6 +229,49 @@ func TestCommittedOutcomeRejectsFalsePriorObservation(t *testing.T) {
}
}

func TestCommittedOutcomeRejectsObjectiveLineageSubstitution(t *testing.T) {
for name, mutate := range map[string]func(*kernel.Receipt, *kernel.ObjectiveBinding){
"prior": func(receipt *kernel.Receipt, other *kernel.ObjectiveBinding) {
receipt.PriorObjectiveBinding = other
},
"requested": func(receipt *kernel.Receipt, other *kernel.ObjectiveBinding) {
receipt.RequestedObjectiveBinding = other
},
"result": func(receipt *kernel.Receipt, other *kernel.ObjectiveBinding) {
receipt.ResultObjectiveBinding = other
},
} {
t.Run(name, func(t *testing.T) {
fixture := newIntegerFixture(SetupUnbound)
runtime := mustRuntime(t, fixture)
request, prescription := resolve(t, runtime, fixture.Scenario, fixture.Scenario.BindTransition, &fixture.Scenario.Objective, fixture.Scenario.Authority)
before := fixture.Scenario.Snapshot()
returned, err := runtime.Apply(context.Background(), kernel.ApplyRequest{ResolveRequest: request, Prescription: prescription})
if err != nil {
t.Fatal(err)
}
other, err := kernel.BindObjective(fixture.Scenario.ConflictingObjective)
if err != nil {
t.Fatal(err)
}
mutate(&returned, &other)
returned.ID = ""
digest, err := kernel.Fingerprint(returned)
if err != nil {
t.Fatal(err)
}
returned.ID = "rcp-" + digest
receipts := fixture.Store.(*MemoryStateStore).receipts
receipts.mu.Lock()
receipts.values[len(receipts.values)-1] = returned
receipts.mu.Unlock()
if err := committedOutcomeError(fixture.Program, fixture.Scenario, before, fixture.Scenario.Snapshot(), prescription, returned); err == nil {
t.Fatalf("content-rehashed %s objective lineage substitution was accepted", name)
}
})
}
}

func TestCommittedOutcomeRejectsNoOpAcceptedByDomainVerifier(t *testing.T) {
fixture := newIntegerFixture(SetupBound)
domain := fixture.Domain.(*IntegerDomain)
Expand Down
Loading
Loading