cove v0.1.2 — Step-indexed Kripke evidence

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+

cove v0.1.1 — clarify source-level contract docs

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, and requirement- and rule-gated value carriers Checked and Guarded.
v0.1.1 is a documentation-only patch on top of v0.1.0; the public API and runtime behavior are unchanged, but the exported Go-surface comments now state the existing contracts more explicitly.

Usage

type Runtime struct {
    Budget int
}

_, sv := cove.StepExprWith(Runtime{Budget: 8}, computation)
for sv.Suspension != nil {
    result := dispatch(sv.Ask(), sv.Op())
    _, sv = sv.ResumeWith(result, func(r Runtime) Runtime {
        r.Budget--
        return r
    })
}

// Completion clears the suspension; the carried context is preserved.
_ = sv.Ask()

Highlights

This release turns three source-level contracts from implied knowledge into explicit exported documentation. The stepping APIs now state their inherited nil-completion rule directly, the command surface states its identity/composition law, and the Req bridge docs now make the lossy quotation/evaluation direction explicit.

What's Changed

Documentation

• Document the inherited nil-completion convention directly on Step, StepExpr, StepWith, StepExprWith, Resume, and ResumeWith in step.go.
• Document Cmd as the contextual command / coKleisli surface in cmd.go, including the identity and composition laws already enforced by the implementation.
• Document ReifyReq / ReflectReq in bridge.go as lossy quotation/evaluation helpers rather than structural inverses, including the ReifyReq(nil) invalid-input hazard.

Behavioural Contracts

• SuspensionView remains affine: each suspension is consumed exactly once via Resume, ResumeWith, or Discard.
• Completion still preserves carried context: when stepping reaches the terminal boundary, sv.Suspension becomes nil while sv.Ask() still returns the ambient context.
• Step, StepExpr, StepWith, StepExprWith, Resume, and ResumeWith still inherit kont's nil-completion convention: a nil completed payload denotes completion with the zero value of A.
• Cmd composition still follows Compose(g, f)(v) == g(Extend(v, f)), with ExtractCmd as the identity command on View.
• ReifyReq still quotes a closure predicate into an Expr atom without preserving original Expr structure on the round trip back through ReflectReq.

Compatibility

• Go: 1.26+

cove v0.1.0 - Contextual stepping for kont suspensions

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 of cove package: View as the ambient carrier, SuspensionView as the contextual observation boundary over kont.Suspension, Cmd for contextual commands, Req / ReqExpr for context predicates in closure and data form, Rule / RuleExpr plus Report for named diagnostics, and requirement-gated value carriers Checked and Guarded.

Usage

type Runtime struct {
    Budget int
}

_, sv := cove.StepExprWith(Runtime{Budget: 8}, computation)
for sv.Suspension != nil {
    result := dispatch(sv.Ask(), sv.Op())
    _, sv = sv.ResumeWith(result, func(r Runtime) Runtime {
        r.Budget--
        return r
    })
}

// Completion clears the suspension; the carried context is preserved.
_ = sv.Ask()

Highlights

cove ships an explicit context algebra for kont suspensions without becoming a runtime. The surface covers contextual stepping, contextual commands, composable requirements (closure and data forms), named rule diagnostics with reports, requirement- and rule-gated value carriers, and bridge helpers between the closure and expression worlds.

Features

Public Surface

• Ambient carrier. View[C, A] with Observe, Extract, Ask, Map, MapContext, Replace, WithContext, Duplicate, and Extend.
• Contextual commands. Cmd[C, A, B] with Run, ExtractCmd, LiftCmd, and Compose for command composition through Extend.
• Contextual stepping. SuspensionView[C, A], ObserveSuspension, StepWith, StepExprWith, Step, StepExpr, Op, Resume, ResumeWith, and Discard for stepping kont computations under ambient context; MapContextSuspension and WithContextSuspension for explicit context transport on already-observed suspensions.
• Requirements. Req[C] with Need, Pullback, All, Any, Not, True, False; ReqExpr[C] with NeedExpr, ExprAtom, ExprPullback, ExprAll, ExprAny, ExprNot, ExprTrue, ExprFalse as a defunctionalized Boolean algebra over predicates.
• Diagnostics. Rule[C], RuleExpr[C], Report, RuleError, Require, RequireExpr, PullbackRule, CheckRule, CheckRules, CheckRuleExpr, and CheckRulesExpr for named, ordered diagnostic checks.
• Gated values. Checked[C, A], CheckedExpr[C, A], Guarded[C, A], and GuardedExpr[C, A] as requirement-gated and rule-gated value carriers, with Guard, GuardExpr, GuardRule, GuardRuleExpr, IntoView, MustView, MapChecked, MapGuarded, PullbackChecked, and PullbackGuarded.
• Bridges. Reify, Reflect, ReifyReq, and ReflectReq between the closure and expression worlds.
• Gated suspensions. CheckSuspension and CheckSuspensionExpr gate contextualization of a raw kont.Suspension on a requirement.

Behavioural contracts

• SuspensionView is affine: each suspension is consumed exactly once via Resume, ResumeWith, or Discard.
• Completion preserves carried context: when stepping reaches the terminal boundary, sv.Suspension becomes nil while sv.Ask() still returns the ambient context.
• cove performs no scheduling, retry, or outcome classification; semantic outcome branching belongs to iox, kernel mechanics belong to uring, and proactor advancement belongs to takt.

Laws

• Duplicate(v).Extract() == v
• Extend(v, func(w View[C, A]) A { return w.Extract() }) == v
• Compose(g, f)(v) == g(Extend(v, f))
• Compose(ExtractCmd, f) == f and Compose(g, ExtractCmd) == g

Compatibility

• Go: 1.26+

cove v0.0.0 - Coalgebraic context layer for kont suspensions in Go

Introduction

• cove carries ambient context across kont suspension boundaries as explicit, typed data. It is designed for runtimes that step one suspension at a time while still needing budget, capability, phase, or buffer-state information at each boundary. Instead of side maps or hidden globals, cove keeps that context attached to values and suspensions through View and SuspensionView.
• cove also introduces two forms of context requirements: closure-based Req for direct use and data-based ReqExpr for composable boolean structure. On top of those requirements, the package provides named rules, diagnostics, and guarded values that can be checked before a step proceeds. The stepping helpers remain policy-free: they preserve and evolve context, but they do not schedule, retry, or dispatch. That keeps ownership clean across the wider stack while making contextual stepping easy to reason about and test.

Usage

type Runtime struct {
    Budget int
}

_, sv := cove.StepExprWith(Runtime{Budget: 8}, computation)
for sv.Suspension != nil {
    result := dispatch(sv.Ask(), sv.Op())
    _, sv = sv.ResumeWith(result, func(r Runtime) Runtime {
        r.Budget--
        return r
    })
}

Highlights

cove launches with a contextual stepping surface for kont, including typed carriers for ambient context, guarded values, and suspension-aware resume helpers. The release also ships both closure and expression forms of the requirement algebra so callers can choose between direct predicates and data-first composition.

Features

• View[C, A] and SuspensionView[C, A] to pair values and suspensions with ambient context.
• Req[C] and ReqExpr[C] with All, Any, Not, True, False, and pullback helpers for context predicates.
• Rule[C], RuleExpr[C], Report, and rule-checking helpers for named diagnostics.
• Checked, Guarded, CheckedExpr, and GuardedExpr for requirement-gated values.
• StepWith, StepExprWith, CheckSuspension, CheckSuspensionExpr, and resume helpers for contextual stepping.
• Reify, Reflect, ReifyReq, and ReflectReq bridges between closure and expression worlds.

Compatibility

• Go: 1.26+