Skip to content

Guarantees

The value of WhippleScript is not its syntax. The value is the set of invariants that the compiler and the runtime promise and check. This page collects the invariants in one location. This page states each invariant as a promise. This page also gives the formal model or the mechanism that carries each promise. When a guarantee has an executable model, CI runs the model with the scripts/check-formal-models.sh script. Thus a guarantee is not prose.

Each model also carries its own negative test. The test shows the property fail when you remove the mechanism. A model that cannot fail proves nothing.

If you must approve WhippleScript for your organization, read For IT and data owners first. That page states each promise below as an answer to a question that you must ask, in a table. If you want the design that produces these promises, read How WhippleScript works.

Execution

Each instance has one writer. Each rule firing commits atomically. Each instance is an isolated durable store. A rule firing commits its facts, its consumed facts, its effects, and its terminal in one transaction. An instance never observes half of a firing. Two firings never interleave their writes. Carried by: the transactional commit_rule operation of the store and the single-threaded rule pass for each instance. The kernel semantics are in models/maude/kernel.maude.

The events have a causal sequence. The event log permits append only. Each event carries a causation identifier and a correlation identifier. Thus a query gives the cause of each event. You do not reconstruct the cause. A replay follows the same sequence. Carried by: the append-only event store and the trace --check conformance checker of the kernel. The file models/tla/ControlPlaneLifecycle.tla pins the lifecycle invariants of the checker.

Each effect occurs exactly one time. Each effect derives a stable idempotency key from the identity of its firing. The identity has the program version, the revision epoch, the rule, the path of the binding, and the identity of the trigger. A re-evaluation, a recovery after a crash, and a replay each deduplicate against the key. Thus the system requests an effect one time. This is true for each quantity of lowering operations on its rule. A branched timeline and a restored timeline get different keys. Thus a counterfactual run never deduplicates against a true run. Carried by: models/maude/effect-key.maude, models/maude/branch-effect-key.maude, and models/maude/prefix-replay.maude.

A firing that commits completes (pinned progressions). After a rule firing commits, the firing owns its trigger bindings as immutable values. Its continuations run from the recorded context of the firing. Thus a trigger cannot strand the progression. An adjacent rule can consume the trigger. A projection can also retract the trigger, as when a finish operation closes the ready issue that admitted the rule. In each condition, the progression completes. The match operation controls the admission only. A query stays a live read. Carried by: models/maude/pinned-progressions.maude. The model proves the fate at the commit: no step commits after the break of its condition in the sequence of the log, and no final state strands an open region. The reactive module reproduces the stall before the pin operation as the negative test.

There is no silent stall (automatic failure). An effect gets to a terminal failure, and no after block observes the effect. This condition cannot leave the instance in the running and idle state for an unlimited time. The kernel fails the instance with a generic reason. A cancellation is an exception, because a cancellation is deliberate. An @service workflow records a durable diagnostic and does not fail. Carried by: models/maude/rule-autofail.maude. At compile time, the prominent warning of the unhandled-failure check gives this condition.

Termination

Each workflow has a path to an end. This is a reachability check, not a proof of general termination. The compiler does not claim the second one. A minimum of one rule must be able to get to complete or to fail. Each matched class must have a producer: a table, a different rule, or an input of the workflow. The compiler applies both checks before the run. A workflow that runs continuously by design carries the @service tag. A rule whose facts come from outside the workflow carries the @external tag. Each tag is explicit in the source. Thus a program that does not stop is a declaration, not an accident. Carried by: the static liveness checks of the compiler. Refer to liveness checks.

A cycle of rules that runs effects without waiting on the world is refused. The compiler classifies the strongly connected components of the rule dependency graph. A component of two rules or more in which a rule runs an effect is a check error when each record of it lands in the same commit as the fact that the rule matched: each turn of such a cycle requests fresh external effects at the speed of the store, under a new idempotency key each time, so the exactly-once guarantee is no brake on it. A component with no effect is monotonic recursion and is allowed. A recurrence through an external event or a clock never enters this graph, because such a trigger matches no recorded class.

A cycle that waits on the world is allowed, and it needs no declaration. When the recurring record sits inside an after block, the fact of the next turn arrives only with the terminal of an effect, so the loop turns at the pace of the agent or the service that it talks to. That is the long-running agent loop of the language. Whether it may run forever is the question of liveness above, which the @service tag answers.

A workflow tagged @bounded gives up the paced loop as well. The tag is the opposite of @service: it declares that the workflow reaches a terminal after a number of steps that the program fixes and the data does not, so any effect-bearing cycle in it is a check error. A @tool workflow carries that promise with no tag, because an agent invokes it inside a turn and the turn must end. Carried by: the strongly-connected-component classification of the compiler over the rule dependency graph, models/maude/effect-cycle-pacing.maude. The fixtures are examples/invalid/effectful-rule-cycle.whip and examples/invalid/bounded-workflow-effect-cycle.whip.

A whole-program refusal holds for every workflow of a file. A file may declare more than one workflow, and --root names the entry point. Each check applies to each workflow, not only to that entry point. Thus a refusal is never escapable by a move of the offending code into a second workflow that an invoke statement reaches. Carried by: the per-workflow check battery of whip check.

A tree of recursive agent tools converges. An agent can invoke a curated set of @tool workflows synchronously. The whole invoke tree must converge. Thus a turn never blocks for an unlimited time. Two static checks give this property. The invoke-tool graph must be acyclic, because a cycle gives an unbounded depth of recursion. Each @tool workflow must also be locally convergent: a @tool node that reads external signals, and a @tool node with the @service tag, cannot be shown to terminate. The same property on a node that is not a tool is permitted. Non-termination is a privilege of the root only. A workflow that an invoke statement awaits must also promise to terminate. The parent of an invocation observes the typed terminal output of the child, and @service is the declaration that a workflow is not required to reach one, so the compiler refuses the invocation. The refusal rests on the missing promise, not on a claim about the run: a @service workflow with a completing rule does reach a terminal. This is the rule the agent-tool seam already applies on the tag alone. The tag stays legitimate: what is refused is the await, never the declaration, and non-termination remains a privilege of the root. Carried by: models/maude/subworkflow-convergence.maude. The model records each reason that the system is not provably convergent. A valid system never gets to that marker. The acyclicity of the grant graph and the refusal at the invoke seam are checks of the compiler; the fixtures are examples/invalid/tool-grant-cycle.whip and examples/invalid/invoke-service-workflow.whip.

A spend cap parks work. A spend cap never truncates work. A campaign that gets to its cap parks. Its state, its candidates, and its evidence stay intact. The whip improve --resume <campaign-id> command continues the campaign later with a new allowance. Thus a boundary of the budget is a pause. It is never a silently smaller evaluation. Carried by: the cap accounting of the campaign. Refer to Precedents, spend & estimators.

A step budget parks an instance. A step budget never truncates one. The same promise at the scope of one run. An instance may take a number of crossings to the world in each window of its life. On the last of them it moves to paused, and it records a diagnostic that names the count, the budget, and the two ways to continue. It reaches no terminal. Its facts, its effects, the resources that it holds, and its place in the program are what they were. The whip resume command continues it with a fresh window. Thus a run that is long is a run that pauses. It is never a run that the runtime decided was wrong. Carried by: the step budget of the instance, in the rule pass of the kernel, so a hosted run and a local run answer alike. Refer to DR-0082. The fixture is crates/whipplescript-cli/tests/step_budget.rs.

Typing

Each outcome settles. A case statement on a closed domain must be exhaustive. The domains are an enum, a literal union, and the terminal union of an effect. A branch handles each outcome of an effect, or the automatic failure catches the outcome. No outcome passes through silently. Carried by: models/maude/case-family.maude and models/lean/Whipple/Narrowing.lean, which proves that exhaustive implies total. These compose with models/maude/rule-autofail.maude.

A conditional field is unreadable where it may not exist. A field declared when <discriminant> is "<literal>" is required at admission exactly when its discriminant holds that literal. A read of it is accepted only where the discriminant is pinned to that literal, which is the matching arm of a case on it. A _ arm pins nothing and grants no read. This holds in each read position of a rule body, including an effect operand and a from projection that copies the field implicitly, so the value cannot leave the instance under a state in which it may be absent. Carried by: models/maude/discriminant-schema.maude.

Typed effect failures are additive by construction. Each effect failure carries the same base. The base has reason, summary, effect_id, run_id, and kind. Each kind adds its own extras. The exit_code field of an exec effect and the error_class field of a coercion are examples. Such a field is reachable only under the applicable static narrowing of the effect kind. Thus a new variant can never change a read of the base that exists. Carried by: models/maude/effect-error.maude and models/lean/Whipple/EffectError.lean, which proves that the base is a subset of each variant and proves the additivity.

Authority

There is no ambient authority. Authority only becomes more narrow. Capability enters a program explicitly. A use statement imports a package that carries authority. An operator grant gives the machine. Capability then only becomes more narrow. The access grants of a turn, the authority at the invoke seam of a child workflow, and the fields that a redaction keeps are each a subset of the authority of the granter. Nothing becomes larger downstream. Carried by: models/maude/workflow-authority-attenuation.maude, models/maude/turn-access-grant.maude, and models/maude/script-hard-off.maude. The last model shows that an exec statement fails closed without the allowlist of the operator. A file store has the same position. A store is read-only by default. A write operation fails closed unless the store declares allow write.

Information flow is a set of denials. Under a governance envelope, the checker applies universal deny properties. Each property has exactly one permitted crossing, and the source marks that crossing:

  • The checker denies a value to each audience outside its set of readers. The crossing is a declassified coerce statement. The output schema limits the crossing.
  • The checker denies the context of a turn to each provider that has no clearance for the data that the turn read.
  • The checker denies untrusted data influence over a sink with more trust. The crossing is an endorsed coerce statement.
  • The checker denies data that an attacker can control the ability to steer its own release. This property is NMIF.
  • The checker denies a field that a redact … keep statement dropped to each sink. The runtime physically removes the field. A proof shows the non-interference.
  • The checker denies an agent each read above the clearance of its user.
  • A consumed fact gives its consumers its computed producer reach. Thus the checker gates labeled content on its exit as on its entry. Untrusted content cannot pass through an intermediate fact with no label.
  • The checker denies an output of an effect influence over a sink with a from label above the vouched clearance of the executor. The output can be the result of a turn, the output of a coercion, or the result of an exec statement. Thus a model writes only where governance vouched for the model.

Carried by: the models/maude/infoflow-*.maude suite and the proofs in models/lean/Whipple/. The proofs are ReaderSets.lean, NMIF.lean, and Redaction.lean.

Data

A fact is immutable, and the content keys the fact. A recorded fact never changes. Identical content becomes one fact. These are set semantics. To express a change, record a new fact or consume an old fact. Thus the match operation is deterministic and the history is honest. Carried by: the fact identity of the store, which the content keys, and the idempotent insert operation.

A replay is honest. The whip checkpoint command and the whip restore command rewind to a coherent cut. A suffix that executes again never deduplicates against the abandoned timeline, because the generation of the restore is part of the identity of an effect. The whip trace --check command verifies the stream of events of a run against the model of the lifecycle. Carried by: models/maude/restore-replay.maude and the trace --check conformance checker of the kernel (models/tla/ControlPlaneLifecycle.tla).

If you observe a violation of a promise on this page, the system has a bug. Report the bug with the whip log output of the instance. A guarantee has a value only when you can falsify it.