cove v0.1.2 — Step-indexed Kripke evidence

[hayabusa-cloud]

Introduction

cove is the context layer of the nonblocking I/O stack. Around a kont computation that is advanced one suspension at a time, cove keeps ambient state — dispatch budget, ring capabilities, protocol phase, buffer-group validity, and similar runtime facts — as typed, composable data instead of hidden globals or ad-hoc side maps.

The package is policy-free by design: it carries context, checks requirements, and exposes the current suspension boundary, but it never schedules, retries, classifies outcomes, or talks to the kernel. Those responsibilities stay with takt, iox, and uring.

The public surface covers a comonadic View, a SuspensionView boundary over kont.Suspension, contextual Cmd composition, closure and defunctionalized requirement algebras Req / ReqExpr, named diagnostics Rule / RuleExpr with Report, requirement- and rule-gated value carriers Checked and Guarded, and now a generic step-indexed Kripke evidence layer for contextual worlds.

v0.1.2 builds on the v0.1.0 contextual stepping release and the v0.1.1 source-contract documentation patch by adding the Kripke/world vocabulary needed to express finite contextual observations directly in cove while preserving the existing runtime boundary: cove checks evidence, but it does not become a scheduler or event loop.

Usage

type RuntimeWorld struct {
	Epoch uint64
}

leq := func(w, next RuntimeWorld) bool {
	return w.Epoch <= next.Epoch
}

canObserve := cove.Force(leq, func(w RuntimeWorld) bool {
	return w.Epoch > 0
})
_ = canObserve.MonotoneAt(RuntimeWorld{Epoch: 1}, RuntimeWorld{Epoch: 2})

rel := cove.Relate(leq, func(w RuntimeWorld, n cove.StepIndex, value int) bool {
	return uint64(n) <= w.Epoch && value >= 0
})
later := cove.Later(rel)
_ = later.Holds(RuntimeWorld{Epoch: 8}, 3, 4)

_, sv := cove.StepExprWithIndex(RuntimeWorld{Epoch: 2}, 2, expr)
var val int
for sv.Extract() != nil {
	result := dispatch(sv.Ask(), sv.Op())
	next := sv.Ask()
	next.Epoch++
	val, sv = sv.ResumeTo(leq, result, next)
}
_ = cove.CheckCompletedRelation(sv, val, rel)

Highlights

This release makes cove the generic Kripke evidence layer for contextual observations. Callers can now name worlds, preorder extension, monotone forcing, step-indexed relations, guarded delay, indexed contextual observations, monotone indexed resume, and completed finite-trace relation checks without moving scheduler policy or runtime state ownership into cove.

The public release lineage remains additive: v0.0.0 introduced the coalgebraic context layer, v0.1.0 stabilized contextual stepping for kont suspensions, v0.1.1 clarified source-level contracts, and v0.1.2 extends that surface with Kripke evidence rather than changing existing behavior.

What's Changed

Features

• Add World as the Kripke reading of an ambient context type.
• Add StepIndex as the finite approximation level used by indexed contextual observations.
• Add Preorder, Extends, DiscreteWorlds, and TotalWorlds for world-extension evidence and local preorder checks.
• Add Transition, CheckTransition, CheckForcingTransition, and CheckInvariantTransition for concrete world-edge checks.
• Add Forcing and ForcingExpr with monotonicity checks over Req and ReqExpr.
• Add Relation, Indexed, Relate, Later, CheckRelation, and indexed weakening helpers for step-indexed Kripke relations.
• Add IndexedView, IndexedSuspensionView, StepWithIndex, StepExprWithIndex, ResumeTo, and CheckCompletedRelation for finite contextual suspension observations.

Compatibility

• Go: 1.26+

---

This discussion was created from the release cove v0.1.2 — Step-indexed Kripke evidence.