How GUMBO Contracts are Translated to Rust Boolean Functions to Provide GUMBOX Executable Contracts

This chapter is a developer-oriented, example-based walkthrough of how HAMR translates GUMBO thread component contracts into GUMBOX — executable Rust boolean functions that evaluate the contracts on concrete values. It continues with the same running examples as the GUMBO Component Contracts chapter: the Simple Isolette from the HAMR tutorials repository, first the data-port variant (P-DP) and then the event-data-port variant (P-EDP), both centered on the Thermostat thread.

We assume you have read the GUMBO Component Contracts chapter — every contract translated below is introduced and motivated there. Familiarity with the Rust component development chapters (implementation, manual unit testing) is helpful but not required.

This chapter addresses the translation itself: what functions HAMR generates, where they live, how each GUMBO contract form maps to Rust, and how you (or a tool) can call the functions directly to probe what a contract means. Using the generated functions through the test harnesses is covered in the Manual GUMBOX Testing and Property-Based Testing chapters. The parallel translation of the same contracts into Verus logical contracts for formal verification is covered in the Verus translation chapter.

Why Executable Contracts?

A GUMBO contract is written once, at the model level, and HAMR derives multiple code-level artifacts from it. GUMBOX is the executable derivation: every contract clause becomes an ordinary, pure Rust boolean function — a function you can call with concrete port values and state variable values and that answers true (the values satisfy the clause) or false (they violate it). We call these functions contract oracles, because their primary role is to judge observed behavior against the specification.

Executable contracts earn their keep in several distinct ways:

Test oracles. A test that runs a component entry point needs a way to decide whether the outputs are correct. With GUMBOX, correctness checking is automatic: the harness evaluates the generated postcondition oracle on the observed outputs, so the test author supplies only inputs — never hand-coded expected-result assertions. This is what powers both manual GUMBOX unit testing (you pick the inputs — see the Manual GUMBOX Testing chapter) and automated property-based testing (PropTest generates the inputs — see the Property-Based Testing chapter).
Run-time monitoring. Because the oracles are plain Rust functions over port and state values, they can also be evaluated against a deployed component’s observed behavior, forming the basis of HAMR’s run-time monitoring support — checking, in operation, that each dispatch satisfies the same contracts that were tested and verified during development.
Companions to Verus proofs. HAMR also translates the same GUMBO clauses into Verus requires/ensures contracts for formal verification of the component’s Rust implementation (see the Verus translation chapter). The two artifacts are complementary: Verus establishes that all executions satisfy a clause, while GUMBOX evaluates the clause on one concrete execution. When a Verus proof fails, the corresponding GUMBOX clause function turns the abstract failure into an explanation — you call the very clause that would not verify with concrete values and watch it return false, producing a runnable test case that demonstrates exactly which requirement is violated and on what data (an example appears below). Because both artifacts are generated from the same GUMBO source, they agree by construction — a GUMBOX counterexample is a counterexample to the Verus contract, and vice versa.
Machine-readable specifications. A contract you can call is a contract that tools — and LLM-based agents — can interrogate without any implementation in the loop. By constructing input/output pairs and asking the postcondition oracle whether the specification accepts them, an agent can probe the spec for gaps (scenarios it should reject but accepts), vacuity, boundary ambiguity, and contradictions. The audit-gumbo-contracts skill in HAMR’s agent-context materials automates exactly this: it audits a component’s GUMBO compute contract against a catalog of specification anti-patterns and emits demonstration tests that call the GUMBOX functions directly (see Interrogating a Contract below).

Throughout, keep the trust story in mind: GUMBOX functions are generated, marked do-not-edit, and re-generated whenever the model changes — the executable form cannot silently drift from the model-level specification.

Where HAMR Generates GUMBOX Code

For each thread component, HAMR code generation places the GUMBOX functions in a single file inside the component crate’s bridge module:

hamr/microkit/crates/<component>/
  src/
    bridge/
      <component>_GUMBOX.rs      <- the GUMBOX contract oracles (this chapter)
      <component>_api.rs         <- port APIs with woven Verus contracts
      extern_c_api.rs
    component/
      <component>_app.rs         <- application code (developer-edited)
    test/
      util/
        cb_apis.rs               <- harness entry points that call the oracles
        test_apis.rs
        generators.rs
      tests.rs                   <- developer-edited tests

For the DP thermostat the file is crates/thermostat_thermostat/src/bridge/thermostat_thermostat_GUMBOX.rs, and for the EDP variant the file of the same name in the P-EDP example. The file is fully auto-generated (// Do not edit this file as it will be overwritten if HAMR codegen is rerun) and is regenerated in place whenever code generation reruns, keeping the oracles in sync with the model.

From tests and other code in the crate, the functions are reached through the module path crate::bridge::<component>_GUMBOX; the generated test harness aliases it:

use crate::bridge::thermostat_thermostat_GUMBOX as GUMBOX;

(Reference: Microkit Folder Structure for the full crate layout.)

The Translation at a Glance

The generated file contains one boolean function per contract clause, plus composite functions that conjoin the clauses into the entry-point-level oracles the harnesses call. The naming scheme is uniform across components:

GUMBO construct	GUMBOX function	Role
helper `def f(...)` in `functions`	`f(...)` (same name)	callable from the oracles and from your tests
integration `assume` on input port `p`	`I_Assm_p`	payload constraint on `p`
integration `assume` on input event data port `p`	`I_Assm_Guard_p` (wraps `I_Assm_p`)	applies `I_Assm_p` only when a message is present
integration `guarantee` on output port `p`	`I_Guar_p` (and `I_Guar_Guard_p` for event data ports)	payload promise on `p`
initialize `guarantee N`	`initialize_N`	one function per clause
(composite)	`initialize_IEP_Guar`	conjunction of all initialize guarantees
(top level)	`initialize_IEP_Post`	initialize oracle — the post-check entry point
compute `assume N`	`compute_spec_N_assume`	one function per clause
(composite)	`compute_CEP_T_Assm`	conjunction of all compute assumes
(top level)	`compute_CEP_Pre`	compute precondition oracle — integration assumes ∧ compute assumes
compute `guarantee N`	`compute_spec_N_guarantee`	one function per general guarantee
(composite)	`compute_CEP_T_Guar`	conjunction of all general guarantees
compute `case N`	`compute_case_N`	the case as an implication (assume ⟹ guarantee)
(composite)	`compute_CEP_T_Case`	conjunction of all cases
(top level)	`compute_CEP_Post`	compute postcondition oracle — `CEP_T_Guar` ∧ `CEP_T_Case`

The abbreviations follow the entry point structure: IEP = Initialize Entry Point, CEP = Compute Entry Point, I-Assm/I-Guar = integration assume/guarantee, and T marks the top-level composite for a clause category. The three bold rows are the entry points into the contract: initialize_IEP_Post and compute_CEP_Post judge outputs, and compute_CEP_Pre judges inputs.

Each function’s parameters follow equally uniform conventions:

Contract reference	GUMBOX parameter	Rust type
state variable `x` in the pre-state — `In(x)`	`In_x`	the variable’s data type
state variable `x` in the post-state	`x` (bare name)	the variable’s data type
data port `p` (input or output)	`api_p`	the port’s payload type
event data port `p` (input or output)	`api_p`	`Option<payload type>`

So a function’s signature is a statement of which parts of the component state and interface the clause depends on — the generated doc comments spell each parameter’s role out (pre-state state variable, incoming data port, …), and the clause name and requirement prose from the model are carried into the doc comment, preserving requirement traceability at the code level.

One last preliminary: the top of every GUMBOX file defines two macros used in the clause bodies,

macro_rules! implies {
  ($lhs: expr, $rhs: expr) => {
    !$lhs || $rhs
  };
}

macro_rules! impliesL {
  ($lhs: expr, $rhs: expr) => {
    !$lhs | $rhs
  };
}

mirroring GUMBO’s two families of logical operators: GUMBO’s short-circuit implies becomes implies! (Rust || does not evaluate the right side when the left is false — important when the right side accesses an event data port payload), and the logical, both-sides-evaluated forms map to impliesL and Rust’s non-short-circuit &/| on booleans.

The DP Thermostat, Translated

We now walk the DP thermostat’s GUMBO block — exactly the contract developed section-by-section in the prerequisite chapter — through its translation. Each subsection shows a brief reminder of the GUMBO source, then the generated Rust, verbatim.

Helper Functions

functions
  def Temp_Lower_Bound(): Base_Types::Integer_32 := 95 [i32];
  def Temp_Upper_Bound(): Base_Types::Integer_32 := 104 [s32];

becomes

pub fn Temp_Lower_Bound() -> i32
{
  95i32
}

pub fn Temp_Upper_Bound() -> i32
{
  104i32
}

GUMBO helper functions translate to same-named Rust functions, so the single-sourcing benefit described in the prerequisite chapter carries directly to the code level: the requirement-level bounds have one definition, and every oracle that mentions them calls it.

Integration Constraints

integration
  assume ASSM_CT_Range:
    Temp_Lower_Bound() <= current_temp.degrees & current_temp.degrees <= Temp_Upper_Bound();

becomes

/** I-Assm: Integration constraint on thermostat's incoming data port current_temp
  *
  * assume ASSM_CT_Range
  */
pub fn I_Assm_current_temp(current_temp: Isolette_Data_Model::Temp) -> bool
{
  (Temp_Lower_Bound() <= current_temp.degrees) &
    (current_temp.degrees <= Temp_Upper_Bound())
}

An integration constraint is a property of a single port’s value, so its oracle takes exactly one parameter: the payload. Note the translation of GUMBO’s logical & to Rust’s non-short-circuit & on booleans. Integration assumes are folded into the compute precondition oracle compute_CEP_Pre below; a component with integration guarantees on output ports would additionally get I_Guar_<port> functions folded into its postcondition oracle (the EDP OperatorInterface provides an example).

Initialize Contracts and the Initialize Oracle

initialize
  guarantee
    initlastCmd: lastCmd == Isolette_Data_Model::On_Off.Off;
  guarantee REQ_THERM_1 "The Heat Control command shall be Off initially.":
    heat_control == Isolette_Data_Model::On_Off.Off;

Each guarantee becomes its own function, over only the values it mentions:

/** Initialize EntryPointContract
  *
  * guarantee initlastCmd
  * @param lastCmd post-state state variable
  */
pub fn initialize_initlastCmd(lastCmd: Isolette_Data_Model::On_Off) -> bool
{
  lastCmd == Isolette_Data_Model::On_Off::Off
}

/** Initialize EntryPointContract
  *
  * guarantee REQ_THERM_1
  *   The Heat Control command shall be Off initially.
  * @param api_heat_control outgoing data port
  */
pub fn initialize_REQ_THERM_1(api_heat_control: Isolette_Data_Model::On_Off) -> bool
{
  api_heat_control == Isolette_Data_Model::On_Off::Off
}

(Notice the notational shift for enum values: GUMBO’s On_Off.Off is Rust’s On_Off::Off.) The composite conjoins the clauses, and the top-level oracle wraps the composite:

/** IEP-Guar: Initialize Entrypoint for thermostat
  *
  * @param lastCmd post-state state variable
  * @param api_heat_control outgoing data port
  */
pub fn initialize_IEP_Guar(
  lastCmd: Isolette_Data_Model::On_Off,
  api_heat_control: Isolette_Data_Model::On_Off) -> bool
{
  initialize_initlastCmd(lastCmd) &&
  initialize_REQ_THERM_1(api_heat_control)
}

/** IEP-Post: Initialize Entrypoint Post-Condition
  *
  * @param lastCmd post-state state variable
  * @param api_heat_control outgoing data port
  */
pub fn initialize_IEP_Post(
  lastCmd: Isolette_Data_Model::On_Off,
  api_heat_control: Isolette_Data_Model::On_Off) -> bool
{
  initialize_IEP_Guar(lastCmd, api_heat_control)
}

initialize_IEP_Post is the function a test harness (or monitor) calls after the initialize entry point runs, passing the observed post-state and output port values. There is no IEP_Pre: as the prerequisite chapter explains, initialization has no inputs, so there is nothing to check beforehand.

Compute Assumptions and the Precondition Oracle

compute
  assume ASSM_LDT_LE_UDT: desired_temp.lower.degrees <= desired_temp.upper.degrees;

becomes a per-clause function and its composite:

/** Compute Entrypoint Contract
  *
  * assumes ASSM_LDT_LE_UDT
  * @param api_desired_temp incoming data port
  */
pub fn compute_spec_ASSM_LDT_LE_UDT_assume(api_desired_temp: Isolette_Data_Model::Set_Points) -> bool
{
  api_desired_temp.lower.degrees <= api_desired_temp.upper.degrees
}

/** CEP-T-Assm: Top-level assume contracts for thermostat's compute entrypoint
  *
  * @param api_desired_temp incoming data port
  */
pub fn compute_CEP_T_Assm(api_desired_temp: Isolette_Data_Model::Set_Points) -> bool
{
  let r0: bool = compute_spec_ASSM_LDT_LE_UDT_assume(api_desired_temp);

  return r0;
}

The precondition oracle then assembles everything the component relies on at dispatch — the integration assumes on its input ports and its compute assumes:

/** CEP-Pre: Compute Entrypoint Pre-Condition for thermostat
  *
  * @param In_lastCmd pre-state state variable
  * @param api_current_temp incoming data port
  * @param api_desired_temp incoming data port
  */
pub fn compute_CEP_Pre(
  In_lastCmd: Isolette_Data_Model::On_Off,
  api_current_temp: Isolette_Data_Model::Temp,
  api_desired_temp: Isolette_Data_Model::Set_Points) -> bool
{
  // I-Assm-Guard: Integration constraints for thermostat's incoming ports
  let r0: bool = I_Assm_current_temp(api_current_temp);

  // CEP-Assm: assume clauses of thermostat's compute entrypoint
  let r1: bool = compute_CEP_T_Assm(api_desired_temp);

  return r0 && r1;
}

This is the function the test harnesses use to filter inputs: a test vector for which compute_CEP_Pre returns false is outside the component’s specified envelope, and running the component on it would prove nothing. Note the discipline of the composites: each conjunct is bound to a named intermediate (r0, r1, …) and the constituent functions are all pub — so when a composite returns false, you can call the pieces individually to localize exactly which clause failed.

General Guarantees

  guarantee lastCmd "Set lastCmd to value of output Cmd port":
    lastCmd == heat_control;

becomes

/** Compute Entrypoint Contract
  *
  * guarantee lastCmd
  *   Set lastCmd to value of output Cmd port
  * @param lastCmd post-state state variable
  * @param api_heat_control outgoing data port
  */
pub fn compute_spec_lastCmd_guarantee(
  lastCmd: Isolette_Data_Model::On_Off,
  api_heat_control: Isolette_Data_Model::On_Off) -> bool
{
  lastCmd == api_heat_control
}

with the composite compute_CEP_T_Guar conjoining all general guarantees (here there is just this one).

Compute Cases

Each compute_cases case translates to a single implication: the case’s assume becomes the antecedent, its guarantee the consequent.

    case REQ_THERM_2 "If Current Temperature is less than
                      |the Lower Desired Temperature, the Heat Control shall be set to On.":
      assume (current_temp.degrees < desired_temp.lower.degrees);
      guarantee heat_control == Isolette_Data_Model::On_Off.Onn;

becomes

/** guarantee REQ_THERM_2
  *   If Current Temperature is less than
  *   the Lower Desired Temperature, the Heat Control shall be set to On.
  * @param api_current_temp incoming data port
  * @param api_desired_temp incoming data port
  * @param api_heat_control outgoing data port
  */
pub fn compute_case_REQ_THERM_2(
  api_current_temp: Isolette_Data_Model::Temp,
  api_desired_temp: Isolette_Data_Model::Set_Points,
  api_heat_control: Isolette_Data_Model::On_Off) -> bool
{
  implies!(
    api_current_temp.degrees < api_desired_temp.lower.degrees,
    api_heat_control == Isolette_Data_Model::On_Off::Onn)
}

REQ_THERM_4 shows the translation of the In() operator — the pre-state reference In(lastCmd) simply becomes the In_lastCmd parameter:

/** guarantee REQ_THERM_4
  *   If the Current Temperature is greater than or equal
  *   to the Lower Desired Temperature
  *   and less than or equal to the Upper Desired Temperature, the value of
  *   the Heat Control shall not be changed.
  * @param In_lastCmd pre-state state variable
  * @param api_current_temp incoming data port
  * @param api_desired_temp incoming data port
  * @param api_heat_control outgoing data port
  */
pub fn compute_case_REQ_THERM_4(
  In_lastCmd: Isolette_Data_Model::On_Off,
  api_current_temp: Isolette_Data_Model::Temp,
  api_desired_temp: Isolette_Data_Model::Set_Points,
  api_heat_control: Isolette_Data_Model::On_Off) -> bool
{
  implies!(
    (api_current_temp.degrees >= api_desired_temp.lower.degrees) &
      (api_current_temp.degrees <= api_desired_temp.upper.degrees),
    api_heat_control == In_lastCmd)
}

At the model level, In() needs an operator because a state variable name is a single identifier that must be read two ways; at the code level, the ambiguity disappears — pre- and post-state are just two parameters. The composite conjoins the three cases:

pub fn compute_CEP_T_Case(
  In_lastCmd: Isolette_Data_Model::On_Off,
  api_current_temp: Isolette_Data_Model::Temp,
  api_desired_temp: Isolette_Data_Model::Set_Points,
  api_heat_control: Isolette_Data_Model::On_Off) -> bool
{
  let r0: bool = compute_case_REQ_THERM_2(api_current_temp, api_desired_temp, api_heat_control);
  let r1: bool = compute_case_REQ_THERM_3(api_current_temp, api_desired_temp, api_heat_control);
  let r2: bool = compute_case_REQ_THERM_4(In_lastCmd, api_current_temp, api_desired_temp, api_heat_control);

  return r0 && r1 && r2;
}

Because each case is an implication, conjoining them reproduces the model-level case semantics exactly: on any given dispatch, the cases whose assumptions do not hold are vacuously true, and the cases whose assumptions do hold impose their guarantees.

The Postcondition Oracle

Finally, the top-level compute oracle conjoins the general guarantees and the cases:

/** CEP-Post: Compute Entrypoint Post-Condition for thermostat
  *
  * @param In_lastCmd pre-state state variable
  * @param lastCmd post-state state variable
  * @param api_current_temp incoming data port
  * @param api_desired_temp incoming data port
  * @param api_heat_control outgoing data port
  */
pub fn compute_CEP_Post(
  In_lastCmd: Isolette_Data_Model::On_Off,
  lastCmd: Isolette_Data_Model::On_Off,
  api_current_temp: Isolette_Data_Model::Temp,
  api_desired_temp: Isolette_Data_Model::Set_Points,
  api_heat_control: Isolette_Data_Model::On_Off) -> bool
{
  // CEP-Guar: guarantee clauses of thermostat's compute entrypoint
  let r0: bool = compute_CEP_T_Guar(lastCmd, api_heat_control);

  // CEP-T-Case: case clauses of thermostat's compute entrypoint
  let r1: bool = compute_CEP_T_Case(In_lastCmd, api_current_temp, api_desired_temp, api_heat_control);

  return r0 && r1;
}

Read its signature as a summary of the compute contract’s whole vocabulary: pre-state (In_lastCmd), post-state (lastCmd), frozen inputs (api_current_temp, api_desired_temp), and outputs (api_heat_control). Given one dispatch’s worth of those values — whether they came from a unit test, a PropTest run, a deployed monitor, or were simply made up to ask a question — compute_CEP_Post answers whether that dispatch satisfied the contract.

The EDP Variant: Message Presence Becomes Option

The event-data-port variant of the Simple Isolette introduced the GUMBO constructs for message-oriented communication: HasEvent, MustSend, NoSend, and the latching state pattern. Their translations all rest on one encoding decision: an event data port’s value is an Option<T> — None when no message is present at the dispatch, Some(payload) when one is. Everything else follows mechanically:

GUMBO (model level)	GUMBOX (Rust)
event data port `p` of payload type `T`	parameter `api_p: Option<T>`
`HasEvent(p)`	`api_p.is_some()`
payload access `p.field` (under a presence guard)	`api_p.unwrap().field`
`MustSend(p, v)`	`api_p.is_some() && (api_p.unwrap() == v)`
`NoSend(p)`	`api_p.is_none()`

Integration Guards

An integration constraint on an event data port constrains the payload whenever a message is present — the presence guard is implicit at the model level, so the translation makes it explicit. The EDP thermostat’s integration assume

integration
  assume ASSM_LDT_LE_UDT "Incoming set point messages must be well-formed
                         |(lower desired temp at most upper desired temp).":
    desired_temp.lower.degrees <= desired_temp.upper.degrees;

generates two functions — the payload constraint, and a guard that applies it only under presence:

pub fn I_Assm_desired_temp(desired_temp: Isolette_Data_Model::Set_Points) -> bool
{
  desired_temp.lower.degrees <= desired_temp.upper.degrees
}

pub fn I_Assm_Guard_desired_temp(desired_temp: Option<Isolette_Data_Model::Set_Points>) -> bool
{
  implies!(
    desired_temp.is_some(),
    I_Assm_desired_temp(desired_temp.unwrap())
  )
}

It is the guard form that participates in the precondition oracle: a dispatch with no set point message trivially satisfies the constraint. Integration guarantees on output event data ports follow the same pattern (I_Guar_<port> wrapped by I_Guar_Guard_<port>), folded into the sender’s postcondition oracle.

HasEvent: the Latch Pair, Translated

The latch pair from the prerequisite chapter,

  guarantee latchSetPointsOnEvent "A newly received set point message is latched.":
    HasEvent(desired_temp) implies
      (currentSetPoints.lower.degrees == desired_temp.lower.degrees and
       currentSetPoints.upper.degrees == desired_temp.upper.degrees);
  guarantee latchSetPointsNoEvent "Otherwise the latched set points are unchanged.":
    (not HasEvent(desired_temp)) implies currentSetPoints == In(currentSetPoints);

becomes

pub fn compute_spec_latchSetPointsOnEvent_guarantee(
  currentSetPoints: Isolette_Data_Model::Set_Points,
  api_desired_temp: Option<Isolette_Data_Model::Set_Points>) -> bool
{
  implies!(
    api_desired_temp.is_some(),
    (currentSetPoints.lower.degrees == api_desired_temp.unwrap().lower.degrees) &&
      (currentSetPoints.upper.degrees == api_desired_temp.unwrap().upper.degrees))
}

pub fn compute_spec_latchSetPointsNoEvent_guarantee(
  In_currentSetPoints: Isolette_Data_Model::Set_Points,
  currentSetPoints: Isolette_Data_Model::Set_Points,
  api_desired_temp: Option<Isolette_Data_Model::Set_Points>) -> bool
{
  implies!(
    !(api_desired_temp.is_some()),
    (currentSetPoints == In_currentSetPoints))
}

Here the reason GUMBO insists on the short-circuit operators around payload access becomes concrete: implies! expands to !lhs || rhs, and Rust’s || does not evaluate the right side when the left is false — so api_desired_temp.unwrap() is only reached when a message is actually present, and the unwrap() cannot panic.

MustSend and NoSend

The send-on-change policy,

  guarantee mustSendOnChange "A command message is sent exactly when the commanded
                             |state changes, and it carries the new state.":
    (lastCmd != In(lastCmd)) implies MustSend(heat_control, lastCmd);
  guarantee noSendNoChange "No message is sent when the commanded state is unchanged.":
    (lastCmd == In(lastCmd)) implies NoSend(heat_control);

becomes

pub fn compute_spec_mustSendOnChange_guarantee(
  In_lastCmd: Isolette_Data_Model::On_Off,
  lastCmd: Isolette_Data_Model::On_Off,
  api_heat_control: Option<Isolette_Data_Model::On_Off>) -> bool
{
  implies!(
    (lastCmd != In_lastCmd),
    api_heat_control.is_some() &&
      (api_heat_control.unwrap() == lastCmd))
}

pub fn compute_spec_noSendNoChange_guarantee(
  In_lastCmd: Isolette_Data_Model::On_Off,
  lastCmd: Isolette_Data_Model::On_Off,
  api_heat_control: Option<Isolette_Data_Model::On_Off>) -> bool
{
  implies!(
    (lastCmd == In_lastCmd),
    api_heat_control.is_none())
}

MustSend(heat_control, lastCmd) unfolds to presence plus payload equality; NoSend(heat_control) is simply absence. An output event data port’s Option value thus captures the communication decision — whether a message was emitted at all — as first-class data the oracle can judge, something a plain payload parameter could not express.

The Full-Width Oracles

The EDP thermostat’s top-level oracles have wider signatures than the DP variant’s, mixing data ports, event data ports, and two state variables — but the composition pattern is identical:

pub fn compute_CEP_Pre(
  In_currentSetPoints: Isolette_Data_Model::Set_Points,
  In_lastCmd: Isolette_Data_Model::On_Off,
  api_desired_temp: Option<Isolette_Data_Model::Set_Points>,
  api_temp_changed: Option<Isolette_Data_Model::Temp>,
  api_current_temp: Isolette_Data_Model::Temp) -> bool
{
  // I-Assm-Guard: Integration constraints for thermostat's incoming ports
  let r0: bool = I_Assm_current_temp(api_current_temp);
  let r1: bool = I_Assm_Guard_desired_temp(api_desired_temp);

  // CEP-Assm: assume clauses of thermostat's compute entrypoint
  let r2: bool = compute_CEP_T_Assm(In_currentSetPoints);

  return r0 && r1 && r2;
}

and compute_CEP_Post conjoins all nine of the variant’s guarantees (the latch pair, the invariant maintenance, the trigger frame condition, REQ_THERM_2/3/4, and the two send-policy clauses) through compute_CEP_T_Guar. One detail worth noticing: the EDP initialize_IEP_Post takes an api_heat_control: Option<...> parameter but no clause constrains it — output event data ports need no initialization, so the initialize contract says nothing about the port, and the oracle’s signature simply records that the port exists in the initialize phase’s output vocabulary.

Interrogating a Contract by Calling GUMBOX Directly

The oracles are pure functions: they read no component state, invoke no entry point, and need no seL4 libraries. You can call them from any Rust test — with values observed from a real execution, or with values you simply make up — which turns the specification itself into something you can query. This section shows the technique on the thermostat; the same moves work for any component.

(Because these probes never touch the component’s static state, they are unaffected by the test-serialization concerns that apply to tests that run the component — a topic for the manual testing chapter.)

Asking What the Contract Requires

Suppose you want to check your reading of the DP contract: below the desired range, is the thermostat required to command heat on? Two probe calls answer it — one presenting the behavior you believe is required, one presenting its opposite:

use crate::bridge::thermostat_thermostat_GUMBOX as GUMBOX;
use data::*;

fn temp(degrees: i32) -> Isolette_Data_Model::Temp {
  Isolette_Data_Model::Temp { degrees }
}

fn set_points(lower: i32, upper: i32) -> Isolette_Data_Model::Set_Points {
  Isolette_Data_Model::Set_Points { lower: temp(lower), upper: temp(upper) }
}

#[test]
fn probe_below_range_requires_heat_on() {
  use Isolette_Data_Model::On_Off;
  // 96 degrees, desired range [98, 101]: below range.
  // The spec ACCEPTS commanding Onn (and latching it) ...
  assert!(GUMBOX::compute_CEP_Post(
    On_Off::Off,            // In_lastCmd  (pre-state)
    On_Off::Onn,            // lastCmd     (post-state)
    temp(96), set_points(98, 101),
    On_Off::Onn));          // api_heat_control
  // ... and REJECTS commanding Off.
  assert!(!GUMBOX::compute_CEP_Post(
    On_Off::Off, On_Off::Off,
    temp(96), set_points(98, 101),
    On_Off::Off));
}

No thermostat code ran — the second call returns false purely because compute_case_REQ_THERM_2’s antecedent holds (96 < 98) and its consequent does not (Off != Onn). The pair of calls is the semantics of the requirement, demonstrated on concrete numbers.

The same technique settles boundary questions without squinting at inequalities. At exactly the lower bound, does the contract require heating or holding?

#[test]
fn probe_at_lower_bound_hold_not_heat() {
  use Isolette_Data_Model::On_Off;
  // Exactly 98 degrees with range [98, 101]: REQ_THERM_2 uses strict <,
  // so the "hold" case REQ_THERM_4 governs.  Holding the previous command
  // (Off) is accepted ...
  assert!(GUMBOX::compute_CEP_Post(
    On_Off::Off, On_Off::Off,
    temp(98), set_points(98, 101),
    On_Off::Off));
  // ... and switching heat on at the boundary is rejected (violates REQ_THERM_4).
  assert!(!GUMBOX::compute_CEP_Post(
    On_Off::Off, On_Off::Onn,
    temp(98), set_points(98, 101),
    On_Off::Onn));
}

The precondition oracle can be interrogated the same way — for instance, confirming that inverted set points are outside the component’s specified envelope: GUMBOX::compute_CEP_Pre(On_Off::Off, temp(100), set_points(101, 98)) returns false because compute_spec_ASSM_LDT_LE_UDT_assume fails.

Explaining a Failing Verus Proof

The Rust implementation chapter keeps a seeded bug in the thermostat’s application code: an assignment that commands Off where the control law requires Onn, which the Verus verifier duly rejects. A Verus failure report tells you which clause could not be proved, but it speaks in the language of the proof. The corresponding GUMBOX clause function restates the failure as a concrete, runnable demonstration:

#[test]
fn explain_verus_failure_REQ_THERM_2() {
  use Isolette_Data_Model::On_Off;
  // The seeded bug emits Off when the temperature is below range.
  // Evaluating the failing clause on that scenario shows the violation:
  assert!(!GUMBOX::compute_case_REQ_THERM_2(
    temp(96), set_points(98, 101),
    On_Off::Off));   // what the buggy implementation emits
}

Because the individual clause functions are public, you evaluate exactly the clause the prover named — not the whole postcondition — on values drawn from the scenario you suspect. A probe like this makes a proof failure reviewable by anyone who can read a unit test, and once the bug is fixed it can be inverted (assert the clause holds on the same inputs with the corrected output) and kept as a regression test.

Auditing the Specification Itself

The probes above interrogate a contract to confirm its meaning. The same technique, applied adversarially, audits a specification for weaknesses: construct a scenario the component’s intent should forbid, and ask the postcondition oracle whether the specification actually forbids it. If the oracle accepts the scenario, you have found a specification gap — before any implementation exists to exploit it.

For example, a frame-condition audit of the EDP thermostat asks: when no set point message arrives, does the specification actually prevent the latched set points from drifting?

#[test]
fn audit_no_event_forbids_latch_drift() {
  // No message on desired_temp, but the latched set points changed [98,101] -> [97,102].
  // latchSetPointsNoEvent must reject this.
  assert!(!GUMBOX::compute_spec_latchSetPointsNoEvent_guarantee(
    set_points(98, 101),   // In_currentSetPoints (pre-state)
    set_points(97, 102),   // currentSetPoints    (post-state)
    None));                // api_desired_temp    (no message)
}

Here the audit passes — the contract is tight. Had the contract omitted the latchSetPointsNoEvent frame condition, the probe would have exposed the gap: the oracle would accept silent drift of safety-relevant state. Typical gaps this style of probing uncovers include missing “no input, no output” guarantees (the spec accepts fabricated output on a dispatch with no message), data fields no guarantee ever mentions (the spec accepts any value for them), vacuous clauses, and overlapping cases with contradictory guarantees.

Because the probes are just function calls over plain data, they are as natural for an LLM-based agent to write as for a human — this is the basis of the audit-gumbo-contracts skill in HAMR’s agent-context materials, which walks a component’s GUMBO compute contract through an anti-pattern catalog and emits a specification_audit_tests module of exactly such probes, each documenting a finding as an executable demonstration. The essential discipline, for humans and agents alike: these tests probe the spec, not the implementation — they call the GUMBOX functions directly on constructed values and never invoke the component’s entry points.

How the Test Harnesses Enter the Contracts

The testing chapters build on generated harness functions in src/test/util/cb_apis.rs that orchestrate a complete contract-checked execution of an entry point. Here we note only where those harnesses enter the GUMBOX contracts, so the oracle roles established above connect forward.

Each harness returns a three-valued result:

pub enum HarnessResult {
  RejectedPrecondition,
  FailedPostcondition(TestCaseError),
  Passed,
}

and the entry points into the contracts are exactly the three top-level oracles:

Harness function	Checks before running	Oracle after running
`testInitializeCB()`	— (no inputs)	`initialize_IEP_Post`
`testComputeCB(inputs...)`	`compute_CEP_Pre`	`compute_CEP_Post`
`testComputeCBwGSV(In_state..., inputs...)`	`compute_CEP_Pre`	`compute_CEP_Post`

For example, the DP thermostat’s compute harness runs the pipeline pre-check → set inputs → invoke entry point → retrieve outputs → post-check:

pub fn testComputeCB(
  api_current_temp: Isolette_Data_Model::Temp,
  api_desired_temp: Isolette_Data_Model::Set_Points) -> HarnessResult
{
  // Initialize the app
  crate::thermostat_thermostat_initialize();

  // [SaveInLocal]: retrieve and save the current (input) values of GUMBO-declared local state variables
  let In_lastCmd: Isolette_Data_Model::On_Off = get_lastCmd();

  // [CheckPre]: check/filter based on pre-condition.
  if !GUMBOX::compute_CEP_Pre (In_lastCmd, api_current_temp, api_desired_temp) {
    return HarnessResult::RejectedPrecondition;
  }

  // [PutInPorts]: Set values on the input ports
  put_current_temp(api_current_temp);
  put_desired_temp(api_desired_temp);

  // [InvokeEntryPoint]: Invoke the entry point
  crate::thermostat_thermostat_timeTriggered();

  // [RetrieveOutState]: retrieve values of the output ports via get operations and GUMBO declared local state variable
  let lastCmd = get_lastCmd();
  let api_heat_control = get_heat_control();

  // [CheckPost]: invoke the oracle function
  if !GUMBOX::compute_CEP_Post(In_lastCmd, lastCmd, api_current_temp, api_desired_temp, api_heat_control) {
    return HarnessResult::FailedPostcondition(TestCaseError::Fail("Postcondition failed: incorrect output behavior".into()));
  }

  return HarnessResult::Passed
}

compute_CEP_Pre acts as the input filter (an input outside the contract’s envelope yields RejectedPrecondition — the test is inapplicable, not failed), and compute_CEP_Post acts as the correctness oracle. The wGSV variant additionally lets the caller set the pre-state values of GUMBO state variables before invocation, so contracts that mention In(...) can be exercised from chosen pre-states. The property-based testing macros (testInitializeCB_macro!, testComputeCB_macro!, testComputeCBwGSV_macro!) wrap these same harness functions in PropTest drivers — random inputs flow through the identical pre-filter and post-oracle.

How to use these harnesses — writing manual GUMBOX tests and choosing inputs — is the subject of the Manual GUMBOX Testing chapter; configuring PropTest generators and rejection budgets is the subject of the Property-Based Testing chapter.

What Comes Next

This chapter covered the translation from GUMBO to GUMBOX and the direct use of the generated functions. Building on it:

Manual GUMBOX Unit Testing — the Manual GUMBOX Testing chapter covers writing unit tests that drive the testInitializeCB/testComputeCB/testComputeCBwGSV harnesses with chosen inputs, and interpreting HarnessResult outcomes.
GUMBOX Property-Based Testing — the Property-Based Testing chapter covers using the PropTest macros with HAMR-generated value generators to explore the input space automatically against the same oracles.
GUMBO-to-Verus Translation — the Verus translation chapter shows how the same clauses become Verus requires/ensures contracts woven into the application code skeletons, and how the two artifact families cooperate (as previewed in Explaining a Failing Verus Proof above).

For hands-on practice, Part 2 of the tutorial series Adding GUMBO Thread Component Contracts to an Existing System takes the Simple Isolette through GUMBOX-based testing — see Part 2 or follow the Recommended Reading Order.