GUMBO System-Level Property Verification Conditions

This chapter provides a a detailed look at the verification conditions (VCs) HAMR generates for Verus to discharge when it proves a composition system-level property. We use the SysPropStructSplit example (examples/HAMR-SysMLv2-Rust-seL4-P-DP-SysPropStructSplit-Example) as the running case.

This is the companion document to gumbo-system-properties.md (which covers how to author the composition/property syntax). Here we look at the generated sys_proof_XXX crate and explain what each kind of VC is for, how the system assertions and component contracts are compiled into VCs, what the overall soundness argument is, and how independence and commutativity make the parallel schedule sound.

Unless labeled otherwise, generated code is quoted verbatim from this repository’s crate hamr/microkit/crates/sys_proof_nominal/. A few examples are quoted (also verbatim) from the Isolette and TempControl system-verification examples in loonwerks/INSPECTA-models @ 4da74d7, which exercise VC forms this example does not (event data ports, requirement-case contracts at scale) and which were generated by a newer toolchain (see the note in §3.2).

1. The proof model: induction over a schedule schema

The system proof is an induction over major frames (hyperperiods) of a schedule schema. The schedule schema potentially represents multiple possible linear static schedules. Assuming that the linear static schedule specified for the seL4 system conforms to the schedule schema, verification of a property stated in terms of the schedule schema also holds for the linear schedule (the property holds for any linear schedule that conforms to the schedule schema).

Typically, one has in mind a property that relates inputs occurring earlier in the schedule cycle (e.g., inputs from sensors) to outputs occurring later in the schedule (e.g., outputs to actuators). This property is stated as a system assertion attached to the schedule schema anywhere after the input and output values have materialized. The act of “proving” such a property requires placing auxiliary system assertions that reference the system state at other points in the schedule schema. These assertions capture facts about system state at various points in the schedule; together they form a Hoare-style proof outline of the property.

HAMR transforms the schedule schema and system assertions into verification conditions: small, independent logical obligations whose conjunction implies that every assertion holds at its place, in every frame, forever. Concretely, each VC is emitted as a Verus proof fn with an empty body:

pub proof fn vc_...(st: SystemState)
  requires  /* the VC's premises */
  ensures   /* the VC's conclusion */
{}

Verus discharges requires ⟹ ensures as an SMT query. If a VC does not discharge, the property (or the placement of its auxiliary assertions) is at fault far more often than the components are — §5 and the authoring tips in gumbo-system-properties.md show how to read a failure. Proof hints can be added to the body as a last resort, but the intended mode of use is that every VC discharges automatically.

The induction has the classic shape, distributed across VC categories (§3):

• Base case — the initial system state (after all initialize entry points) establishes the assertion at the schema’s START place (Init-State VC).
• Inductive step within a frame — each schedule transition pushes the assertions forward: the assertion before a component implies the component’s preconditions (Pre-Assert VC), and, given the component’s contract and write frame, the assertion after it holds (Next-Assert VCs).
• Closing the loop — the assertion at END re-establishes the assertion at START, so the whole argument repeats for every subsequent hyperperiod (Post-Pre VC).
• Justifying the schema’s parallelism — for branches the schema declares independent (split), reasoning about one linearization is shown to stand in for every conforming order (Non-Blocking, Preservation, Commutativity VCs).
• Justifying the contract handshakes — every connection’s producer guarantee is shown to imply the consumer’s integration assume, once, statically (Integration VCs).

What the system proof does not do is re-verify the components: each component’s own conformance to its GUMBO contract is discharged separately by that component crate’s Verus run, and the system proof consumes the contracts as axioms. §6 makes this trust boundary precise.

Where the VCs live

When a composition <name> block is present, codegen emits the proof crate hamr/microkit/crates/sys_proof_<name>/ (here: sys_proof_nominal). Shared, property-independent modules sit at the top of src/; each concrete property gets its own module directory (abstract properties get none):

crates/sys_proof_nominal/src/
  system_state.rs        # SystemState: channels + GUMBO state variables        (§2.1)
  contracts.rs           # component contracts as spec fns — the axioms         (§2.2)
  assertions.rs          # the composition's `functions` as shared spec fns     (§2.5)
  write_frames.rs        # per-component local/global write frames              (§2.4)
  actions.rs             # uninterpreted action abstractions (commutativity)    (§2.6)
  vc_integration.rs      # Integration VCs — shared, one per connection         (§3.6)
  vc_commutativity.rs    # Commutativity VCs — shared, one per MHIP pair        (§3.8)
  <property>/            # one directory per concrete property
    assertions.rs        #   place-assertion spec fns (unbound places = true)   (§2.3)
    vc_init.rs           #   Init-State VC                                      (§3.1)
    vc_sequential.rs     #   Pre-Assert + Next-Assert VCs, one pair/transition  (§3.2–3.4)
    vc_post_pre.rs       #   Post-Pre VC                                        (§3.5)
    vc_independence.rs   #   Non-Blocking + Preservation VCs                    (§3.8)

make -C crates/sys_proof_nominal verifies everything; each concrete property also gets its own Makefile target (make -C crates/sys_proof_nominal consume_range_loop_invariant), implemented with Verus --verify-module flags, for a fast loop on one property.

For SysPropStructSplit’s four concrete properties the counts are: 3 shared VCs (1 Integration + 2 Commutativity) plus 27 VCs per property (1 Init-State + 17 Sequential + 1 Post-Pre + 8 Independence), for 111 VCs total — all discharging with 0 errors.

2. What the VCs are stated over

Five shared modules set up the vocabulary the VCs are written in.

2.1 SystemState — the flat system state (system_state.rs)

HAMR system verification reasons about the evolution of key points of the system state (e.g., values of component ports and GUMBO-declared state variables) as execution proceeds through the system schedule. The generated SystemState structure is essentially an abstraction of the system state that is referenced by generated VCs. Phrasing the abstract state as a Rust struct enables the Rust-based specification to reasoning abstractly about state changes (e.g., relating the possible values of the system state before a component executes to the possible values of the system state after the component executes). Thus, we commonly see constraints on pre/before and post/after versions of the system state.

The whole composition’s state is one flat record with one field per connection channel (owned by the source out-port), plus unconnected ports and every GUMBO state variable:

pub struct SystemState {
  // -- StructSplit_System_Instance.gen.gen --
  pub gen_out: SysPropStructSplit_Data_Model::StructXY, // channel

  // -- StructSplit_System_Instance.splitter.splitter --
  pub x0: i32, // channel
  pub y0: i32, // channel

  // -- StructSplit_System_Instance.incx.incx --
  pub x1: i32, // channel

  // -- StructSplit_System_Instance.clampx.clampx --
  pub x2: i32, // channel

  // -- StructSplit_System_Instance.decy.decy --
  pub y1: i32, // channel

  // -- StructSplit_System_Instance.merger.merger --
  pub merged: SysPropStructSplit_Data_Model::StructXY, // channel

  // -- StructSplit_System_Instance.consume.consume --
  pub consume_last_x: i32, // state variable
}

A connection is modeled as a single shared variable: a component “reads” the fields wired to its in-ports and “writes” the fields owned by its out-ports and its own state variables. The field names are the composition’s port and state aliases, so assertions and VCs read the way the model was written.

Data ports appear as plain values. Event data ports appear as Option<T> (a message may or may not be present in a given frame). From the TempControl example (INSPECTA-models, temp-control/.../sys_proof_nominal/src/system_state.rs):

pub struct SystemState {
  // -- TempControlSystem_Instance.tsp.tst --
  pub sensedTemp: Option<TempControl_SysVerif::Temperature>, // channel

  // -- TempControlSystem_Instance.tcp.tct --
  pub setPoint: Option<TempControl_SysVerif::SetPoint>, // channel
  pub fanCmd: Option<TempControl_SysVerif::FanCmd>, // channel
  pub sv_currentSetPoint: TempControl_SysVerif::SetPoint, // state variable
  ...
}

2.2 Component GUMBO contracts — the axioms (contracts.rs)

Every component’s GUMBO contract is re-emitted as open spec fns, grouped in one module per component. These are the axioms of the system proof: it assumes each component satisfies its own contract, and those obligations are discharged separately by each component crate’s own Verus run (make -C crates/<comp> verus) — see §3.7 and §6. Both copies are generated from the same GUMBO source, so they are identical by construction.

Six contract flavors appear:

pub mod gen {
  // 1. initialize guarantee — what the initialize entry point establishes
  pub open spec fn initialize_init_outstruct(api_outstruct: …StructXY) -> bool
  { (api_outstruct.x == 0i32) && (api_outstruct.y == 0i32) }

  // 2. integration guarantee (I-Guar) on an OUTGOING port
  pub open spec fn integration_spec_outstruct_range_guarantee(api_outstruct: …StructXY) -> bool
  { … x and y in [-100, 100] … }
}
pub mod split_stage {
  // 3. integration assume (I-Assm) on an INCOMING port
  pub open spec fn integration_spec_instruct_range_assume(api_instruct: …StructXY) -> bool
  { … x and y in [-100, 100] … }

  // 4. compute guarantee — functional post-condition of the compute entry point
  pub open spec fn compute_spec_split_x_guarantee(api_instruct: …StructXY, api_xfield: i32) -> bool
  { api_xfield == api_instruct.x }
}
pub mod consume {
  // 5. compute assume — the component's own precondition on its inputs/state
  pub open spec fn compute_spec_instruct_range_assume(api_instruct: …StructXY) -> bool
  { … x and y in [-200, 200] … }

  // compute guarantee relating a state variable to an input
  pub open spec fn compute_spec_track_x_guarantee(last_x: i32, api_instruct: …StructXY) -> bool
  { last_x == api_instruct.x }
}

The sixth flavor, compute cases (GUMBO compute_cases), comes from ClampX’s saturating-clamp contract: each case becomes its own spec fn — the case’s assume as antecedent, its guarantee as consequent — over exactly the pre-state inputs and post-state outputs it mentions:

pub mod clampx {
  /** compute case In_Range
    *   values already in [-100, 100] pass through unchanged
    */
  pub open spec fn compute_case_In_Range(api_inxfield: i32, api_outxfield: i32) -> bool
  {
    ((-100i32 <= api_inxfield) &&
      (api_inxfield <= 100i32))
    ==> (api_outxfield == api_inxfield)
  }

  /** compute case Above
    *   values above 100 saturate to 100
    */
  pub open spec fn compute_case_Above(api_inxfield: i32, api_outxfield: i32) -> bool
  {
    (api_inxfield > 100i32)
    ==> (api_outxfield == 100i32)
  }
  // … compute_case_Below analogously
}

All the cases of a component are supplied together as premises of its Next-Assert VCs (§3.3), so the prover can dispatch on whichever case the carried facts select.

IncX and DecY contribute further instances of flavors 4 and 5: functional compute guarantees (outxfield == inxfield + 1, outyfield == inyfield - 1) and their [-1000, 1000] overflow/underflow-guard compute assumes. Note the distribution across the pipeline: GenStruct and SplitStruct are the only components carrying integration constraints — everything downstream of the splitter is specified purely with compute contracts (a deliberate reusable-component design; see gumbo-system-properties.md §1.2).

The distinction between integration contracts (I-Assm/I-Guar, attached to a port, part of the cross-component handshake) and compute contracts (attached to the entry point) determines where each clause shows up in the VCs — §3.2, §3.3, §3.6.

2.3 How a place assertion becomes a spec function (<prop>/assertions.rs)

Each place assertion in a property is compiled into one open spec fn over SystemState, named sys_assert_<property>_<place>. The transformation:

For example after incx: (-99 [i32] <= x1) & (x1 <= 101 [i32]) becomes:

pub open spec fn sys_assert_merged_in_consume_range_after_incx(st: SystemState) -> bool
{ (-99i32 <= st.x1) && (st.x1 <= 101i32) }

Inheritance is compiled to conjunction. A property’s effective assertion at a place is the conjunction of every binding of that place along its inheritance chain(s). End_To_End_Functional :> Pipeline_Functional :> Pipeline_Ranges binds after split_stage twice up the chain; the generated assertion conjoins them:

pub open spec fn sys_assert_end_to_end_functional_after_split_stage(st: SystemState) -> bool
{
  (inRange100(st.x0) && inRange100(st.y0)) &&        // from Pipeline_Ranges
    ((st.x0 == st.gen_out.x) &&
      (st.y0 == st.gen_out.y))                       // from Pipeline_Functional
}

The same flattening handles multiple inheritance: Consume_Range_Loop_Invariant :> Pipeline_Ranges, Consume_State_Base simply takes the union of both bases’ bindings (they bind disjoint places here; shared places would be conjoined). Abstract properties themselves generate no spec fns and no VCs.

2.4 Write frames (write_frames.rs)

For each component, a global write frame pins every SystemState field outside the component’s write set (its out-port channels plus its own state variables) to be unchanged across its firing; the local write frame is true (the component may do anything within its own scope). IncX writes only x1:

/** INCX writes: x1.
  * Everything else must be unchanged.
  */
pub open spec fn incx_global_write_frame(pre: SystemState, post: SystemState) -> bool
{
  pre.gen_out == post.gen_out
  && pre.x0 == post.x0
  && pre.y0 == post.y0
  && pre.x2 == post.x2
  && pre.y1 == post.y1
  && pre.merged == post.merged
  && pre.consume_last_x == post.consume_last_x
}

Write frames are derived automatically from the model (connection topology + GUMBO state sections). They are how facts “survive” a step that doesn’t touch them (frame reasoning), and they are the crux of why the independence VCs discharge (§3.8).

2.5 Shared GUMBO functions (assertions.rs)

The composition-level functions become shared spec fns used by the place assertions:

pub open spec fn inRange100(v: i32) -> bool { (-100i32 <= v) && (v <= 100i32) }
pub open spec fn inConsumeRange(s: …StructXY) -> bool
{ (((-200i32 <= s.x) && (s.x <= 200i32)) && (-200i32 <= s.y)) && (s.y <= 200i32) }
pub open spec fn inRange200(v: i32) -> bool { (-200i32 <= v) && (v <= 200i32) }

2.6 Action abstractions (actions.rs) — only for commutativity

Each component gets an uninterpreted action function per written field plus a <comp>_fire predicate: the written fields are an (unknown) function of the component’s read scope, and everything else is framed.

pub uninterp spec fn incx_action_outxfield(inxfield: i32, outxfield: i32) -> i32;

/** "INCX fires": every written field is determined by the read scope;
  * everything else is framed.
  */
pub open spec fn incx_fire(pre: SystemState, post: SystemState) -> bool
{
  post.x1 == incx_action_outxfield(pre.x0, pre.x1)
  && incx_global_write_frame(pre, post)
}

Note the read scope is encoded as the arguments of the action function (incx reads x0 and its own prior x1). Verus proves the commutativity VCs for all interpretations of these functions; the real component behavior is one such interpretation, so a discharged commutativity VC holds for it too. Why this encoding is needed — rather than write frames alone — is explained in §3.8.

3. VC taxonomy

Every obligation the proof depends on falls into one of the categories below. For each category we give: Informal (its role in the argument), Inputs (what feeds it), Generated form (the logical schema of the emitted VC — premises ⊢ conclusion), and generated example(s).

Overview, with this example’s counts (4 concrete properties):

Trivial instances (a true premise or conclusion, from an unbound place or a projected contract) are emitted anyway — uniformity keeps the VC set in one-to-one correspondence with the obligations of the soundness argument, and Verus discharges them instantly.

3.1 Init-State VC

Informal. The base case of the frame induction: the initial state — reached after every component’s initialize entry point has run — must satisfy the assertion at the schema’s START place. Since the initialize entry points are also required to establish the integration guarantees on their output ports, those are available as premises too.

Inputs.

• All component initialize guarantees
• All component integration guarantees (out-port constraints), over the initial channel values
• The property’s START assertion

Generated form.

∧ (all component initialize guarantees)
∧ (all component integration guarantees)
⊢ START assertion

Note this VC substitutes the initialize contracts for the real initial state; it is sound only because each component’s initialize entry point is separately verified to satisfy those guarantees (assumption T2 in §6).

Example — consume_range_loop_invariant/vc_init.rs. The property binds at START: inRange200(consume_last_x), and ConsumeStruct’s initialize guarantee last_x == 0 establishes it:

/** VC[0]: Init-State -- all initialize + integration guarantees |- START */
pub proof fn vc_init_state(st: SystemState)
  requires
    gen::initialize_init_outstruct(st.gen_out),
    gen::integration_spec_outstruct_range_guarantee(st.gen_out),
    split_stage::integration_spec_xfield_range_guarantee(st.x0),
    split_stage::integration_spec_yfield_range_guarantee(st.y0),
    consume::initialize_init_last_x(st.consume_last_x),
  ensures
    sys_assert_consume_range_loop_invariant_START(st),
{}

(Only GenStruct and SplitStruct carry integration guarantees in this example, so only their I-Guars appear alongside the initialize guarantees.) For a property with no at START binding (the other three here), the conclusion is true /* START has no assertion */ and the VC is trivial.

3.2 Pre-Assert VC (one per component transition)

Informal. At every point in the schedule where a component fires, the assertion carried into its before place must imply the component’s precondition — the component is only ever invoked in a state its contract covers. This is the VC that fails when a property “reaches” a component but the proof outline does not carry the needed fact to its before place.

Inputs.

• The assertion at the transition’s in-place(s)
• The component’s compute assume clauses

Generated form.

assertion(before C)
⊢ ∧ (C's compute assume clauses)

Toolchain note — integration assumes. In the current design, a component’s integration assumes (in-port constraints) are not Pre-Assert obligations: they are assumed as premises of the component’s Next-Assert VC (§3.3), a substitution justified once per connection by the Integration VCs (§3.6). Toolchains predating this integration-constraint folding — including the one that generated this repository’s example crate — instead emit the integration assumes as additional Pre-Assert obligations (conclusions) and omit them from the Next-Assert premises. Both forms are sound; the folded form is cheaper because the handshake is proved once per connection instead of being re-derived from carried facts at every firing. Both example styles are shown below.

Example (a compute assume) — merged_in_consume_range/vc_sequential.rs. Pipeline_Ranges carries before incx: inRange100(x0), which discharges IncX’s [-1000, 1000] overflow-guard compute assume ([-100,100] ⊂ [-1000,1000], so the discharge is immediate — the carried system-context fact is much stronger than the component’s reusable-envelope precondition):

/** VC[5]: Pre-Assert -- before_incx |- INCX compute + integration assumes */
pub proof fn vc_pre_assert_incx(st: SystemState)
  requires
    sys_assert_merged_in_consume_range_before_incx(st),  // inRange100(x0)
  ensures
    incx::compute_spec_inxfield_bounded_assume(st.x0),   // -1000 <= x0 <= 1000
{}

(In the first draft of the example the before incx clause was missing and this VC failed; see gumbo-system-properties.md §5.)

The x branch’s second element, ClampX, has no assumes of any kind — its compute cases are total — so its Pre-Assert is trivial and a property may cover it without carrying anything to its dispatch:

/** VC[7]: Pre-Assert -- after_incx |- CLAMPX compute + integration assumes */
pub proof fn vc_pre_assert_clampx(st: SystemState)
  requires
    sys_assert_merged_in_consume_range_after_incx(st),  // x1 ∈ [-99,101]
  ensures
    true /* no assertions at out-places */,
{}

(The shared-place rule is still doing work here: after incx is the place before clampx — consecutive branch elements share a place — so the single after incx binding is both IncX’s post-fact and the input fact ClampX’s compute cases will dispatch on in its Next-Assert VC, §3.3.)

Example (a defensive compute assume at the sink) — consume_range_loop_invariant/vc_sequential.rs. Because this property binds after consume, ConsumeStruct is covered (§4) and its defensive compute assume becomes a real obligation, discharged by the inConsumeRange(merged) fact the property binds at before consume (canonical place name after_merge_stage in the generated code — the two are the same place):

/** VC[15]: Pre-Assert -- after_merge_stage |- CONSUME compute + integration assumes */
pub proof fn vc_pre_assert_consume(st: SystemState)
  requires
    sys_assert_consume_range_loop_invariant_after_merge_stage(st),  // inConsumeRange(merged)
  ensures
    consume::compute_spec_instruct_range_assume(st.merged),         // merged ∈ [-200,200]
{}

Example (this repository’s crate — pre-folding form, an integration assume) — merged_in_consume_range/vc_sequential.rs. SplitStruct is the one component here that still carries an in-port integration assume, and in the pre-folding toolchain that generated this crate it surfaces as a Pre-Assert obligation, discharged by the carried after gen fact:

/** VC[3]: Pre-Assert -- after_gen |- SPLIT_STAGE compute + integration assumes */
pub proof fn vc_pre_assert_split_stage(st: SystemState)
  requires
    sys_assert_merged_in_consume_range_after_gen(st),         // gen_out ∈ [-100,100]
  ensures
    split_stage::integration_spec_instruct_range_assume(st.gen_out),
{}

Example (current toolchains — folded form) — Isolette, normal_mode_heat/vc_sequential.rs (INSPECTA-models @ 4da74d7). Only MRI’s compute assume is an obligation; its integration assumes appear instead as Next-Assert premises:

/** VC[9]: Pre-Assert -- after_drf |- MRI compute assumes */
pub proof fn vc_pre_assert_mri(st: SystemState)
  requires
    sys_assert_normal_mode_heat_after_drf(st),
  ensures
    mri::compute_spec_lower_is_not_higher_than_upper_assume(
      st.lower_desired_tempWstatus, st.upper_desired_tempWstatus),
{}

3.3 Next-Assert VC — component (one per component transition)

Informal. The inductive step across a firing: if the assertion at the component’s before place holds, and the component behaves according to its contract, and everything outside its write set is unchanged, then the assertion at its after place holds. This is where a component’s guarantees are spent to advance the property.

Inputs.

• The assertion at the in-place(s), over the pre-state
• The component’s integration assumes (in-port constraints), over the pre-state — assumed, justified by the Integration VCs (§3.6; pre-folding toolchains discharge them at Pre-Assert instead and omit them here)
• Local and global write frames over (pre, post)
• The component’s post-condition: compute guarantees, compute cases, and integration guarantees on out-ports
• The assertion at the out-place(s), over the post-state

Generated form.

assertion(before C)(pre)
∧ (C's integration assumes)(pre)
∧ local_write_frame(pre, post)
∧ global_write_frame(pre, post)
∧ (C's compute guarantees/cases + integration guarantees)(pre, post)
⊢ assertion(after C)(post)

Example (this repository’s crate) — merged_in_consume_range/vc_sequential.rs:

/** VC[6]: Next-Assert (task) -- before_incx + frames + INCX postcondition |- after_incx */
pub proof fn vc_next_assert_task_incx(pre: SystemState, post: SystemState)
  requires
    sys_assert_merged_in_consume_range_before_incx(pre),        // inRange100(x0)
    incx_local_write_frame(pre, post),                          // true
    incx_global_write_frame(pre, post),                         // everything but x1 unchanged
    incx::compute_spec_incx_guarantee(pre.x0, post.x1),         // x1 == x0 + 1
  ensures
    sys_assert_merged_in_consume_range_after_incx(post),        // x1 ∈ [-99,101]
{}

IncX carries no integration guarantee, so its functional compute guarantee is the only post-fact available — the conclusion x1 ∈ [-99,101] must be derived: the carried x0 ∈ [-100,100] plus x1 == x0 + 1 yield it by arithmetic. For end_to_end_functional the same VC shape instead concludes x1 == gen_out.x + 1, discharged by the same guarantee combined with the carried x0 == gen_out.x. One transition, two properties, two different proofs — each property’s VC sees only its own assertions.

Example (compute cases) — ClampX’s contract is written as compute_cases; every case spec fn (§2.2) is supplied as a premise, and the prover selects the applicable case from the carried facts (here x1 ∈ [-99,101], and for end_to_end_functional additionally x1 == gen_out.x + 1, which decides between In_Range and Above):

/** VC[8]: Next-Assert (task) -- after_incx + frames + CLAMPX postcondition |- after_clampx */
pub proof fn vc_next_assert_task_clampx(pre: SystemState, post: SystemState)
  requires
    sys_assert_merged_in_consume_range_after_incx(pre),          // x1 ∈ [-99,101]
    clampx_local_write_frame(pre, post),
    clampx_global_write_frame(pre, post),
    clampx::compute_case_In_Range(pre.x1, post.x2),              // in range ⟹ identity
    clampx::compute_case_Above(pre.x1, post.x2),                 // above ⟹ 100
    clampx::compute_case_Below(pre.x1, post.x2),                 // below ⟹ -100
  ensures
    sys_assert_merged_in_consume_range_after_clampx(post),       // inRange100(x2)
{}

The conclusion x2 ∈ [-100,100] — formerly ClampX’s integration guarantee — is here derived from the cases alone: In_Range yields x2 == x1 ∈ [-100,100], Above yields 100, Below yields -100.

Example (state variable) — consume_range_loop_invariant/vc_sequential.rs. Consume’s compute guarantee relates its post-state variable to its pre-state input, re-establishing the loop invariant:

/** VC[16]: Next-Assert (task) -- after_merge_stage + frames + CONSUME postcondition |- after_consume */
pub proof fn vc_next_assert_task_consume(pre: SystemState, post: SystemState)
  requires
    sys_assert_consume_range_loop_invariant_after_merge_stage(pre),    // inConsumeRange(merged)
    consume_local_write_frame(pre, post),
    consume_global_write_frame(pre, post),                             // everything but consume_last_x unchanged
    consume::compute_spec_track_x_guarantee(post.consume_last_x, pre.merged),  // last_x' == merged.x
  ensures
    sys_assert_consume_range_loop_invariant_after_consume(post),       // inRange200(consume_last_x')
{}

Example (current toolchains — folded integration assumes, cases at scale) — Isolette, normal_mode_alarm/vc_sequential.rs (INSPECTA-models @ 4da74d7). MMI’s seven requirement cases are premises exactly as above, and — this is the folded form of §3.2’s toolchain note — MMI’s in-port integration assumes appear as premises over the pre-state:

/** VC[18]: Next-Assert (task) -- after_dmf + frames + MMI postcondition |- after_mmi */
pub proof fn vc_next_assert_task_mmi(pre: SystemState, post: SystemState)
  requires
    sys_assert_normal_mode_alarm_after_dmf(pre),
    mmi_local_write_frame(pre, post),
    mmi_global_write_frame(pre, post),
    mmi::compute_case_REQ_MMI_1(pre.monitor_mode, post.monitor_status),
    mmi::compute_case_REQ_MMI_2(pre.monitor_mode, post.monitor_status),
    mmi::compute_case_REQ_MMI_3(pre.monitor_mode, post.monitor_status),
    mmi::compute_case_REQ_MMI_4(pre.lower_alarm_tempWstatus, pre.upper_alarm_tempWstatus, post.mon_interface_failure),
    mmi::compute_case_REQ_MMI_5(pre.lower_alarm_tempWstatus, pre.upper_alarm_tempWstatus, post.mon_interface_failure),
    mmi::compute_case_REQ_MMI_6(pre.lower_alarm_tempWstatus, pre.upper_alarm_tempWstatus, post.mon_interface_failure, post.lower_alarm_temp, post.upper_alarm_temp),
    mmi::compute_case_REQ_MMI_7(post.mon_interface_failure),
    mmi::integration_spec_Allowed_UpperAlarmTemp_assume(pre.upper_alarm_tempWstatus),
    mmi::integration_spec_Allowed_LowerAlarmTemp_assume(pre.lower_alarm_tempWstatus),
  ensures
    sys_assert_normal_mode_alarm_after_mmi(post),
{}

3.4 Next-Assert VC — control point (one per control-point transition)

Informal. At a schedule control point (split fan-out, join, pass-through to END) no component runs and the state is unchanged; the assertions at the in-place(s) must directly imply the assertions at the out-place(s), over a single state.

Inputs.

• Assertions at the in-place(s)
• Assertions at the out-place(s)

Generated form.

∧ (assertions at in-places)
⊢ ∧ (assertions at out-places)

Sub-cases:

• Split fan-out (1 in-place → N out-places): the pre-split assertion must imply each branch-entry assertion.
• Join exit (N in-places → 1 out-place): the conjunction of all branch-end assertions must imply the post-join assertion.

Examples — merged_in_consume_range/vc_sequential.rs. The fan-out copies the pre-split facts into both branch entries:

/** VC[11]: Next-Assert (control point) -- after_split_stage |- before_incx, before_decy (state unchanged) */
pub proof fn vc_next_assert_skip_t5(st: SystemState)
  requires
    sys_assert_merged_in_consume_range_after_split_stage(st),  // inRange100(x0) & inRange100(y0)
  ensures
    sys_assert_merged_in_consume_range_before_incx(st),        // inRange100(x0)
    sys_assert_merged_in_consume_range_before_decy(st),        // inRange100(y0)
{}

The join conjoins the branches’ end post-conditions — for the x branch that is the assertion after its last element, after clampx — making both branch results simultaneously available downstream:

/** VC[12]: Next-Assert (control point) -- after_clampx, after_decy |- post_join_1 (state unchanged) */
pub proof fn vc_next_assert_skip_t6(st: SystemState)
  requires
    sys_assert_merged_in_consume_range_after_clampx(st), // inRange100(x2)
    sys_assert_merged_in_consume_range_after_decy(st),   // y1 ∈ [-101,99]
  ensures
    sys_assert_merged_in_consume_range_post_join_1(st),  // both, conjoined
{}

The soundness of treating the two branch posts as jointly available at the join is not assumed — it is exactly what the Preservation VCs discharge (§3.8).

3.5 Post-Pre VC (one per property)

Informal. Loop closure of the frame induction: the assertion at END must re-establish the assertion at START, so whatever held at the end of one hyperperiod holds at the start of the next — turning “held this frame” into “holds every frame”.

Inputs. The property’s END and START assertions.

Generated form.

END assertion
⊢ START assertion

Example — consume_range_loop_invariant/vc_post_pre.rs. Both places carry inRange200(consume_last_x), so the invariant survives the frame boundary:

/** VC[18]: Post-Pre -- END |- START (hyperperiod loop invariant) */
pub proof fn vc_post_pre(st: SystemState)
  requires
    sys_assert_consume_range_loop_invariant_END(st),
  ensures
    sys_assert_consume_range_loop_invariant_START(st),
{}

For properties with no at START/at END bindings this VC is true ⊢ true. A more consequential instance is the Isolette’s Regulator_Failsafe_Latching property (INSPECTA-models): its invariant FailedModeImpliesHeatOff(reg_last_mode, heat_control) is asserted at both boundaries, and — because MRM’s Failed mode is absorbing — the discharged Post-Pre VC yields “once the regulator fails, the heat stays off forever.”

3.6 Integration VC (shared, one per connection)

Informal. For every connection whose destination in-port carries an integration assume, the sender’s integration guarantee must imply the receiver’s integration assume, over the value the wire carries. This is the assume/guarantee handshake — the code-level twin of the model-level sireum hamr sysml logika integration check. It is property-independent and schedule-independent.

This VC is what licenses the folding described in §3.2/§3.3: since whatever a producer places on a channel already satisfies the consumer’s integration assume, the consumer’s Next-Assert VC may take that assume as a premise at every dispatch without it being re-derived from carried facts. It also closes a soundness loop for the component-level verification: each component crate verifies its compute entry point assuming its in-port constraints hold; the Integration VCs prove the upstream producers actually deliver them, so no component verifies vacuously against an unjustified assumption.

Inputs.

• The source out-port’s integration guarantee
• The destination in-port’s integration assume

Generated form.

sender's integration guarantee (wire value)
⊢ receiver's integration assume (wire value)

Example — vc_integration.rs:

/** VC[0]: Integration -- connection StructSplit_System_Instance.gen.gen.outstruct -> StructSplit_System_Instance.splitter.splitter.instruct: gen.outstruct's I-Guar `outstruct_range`
  * implies split_stage.instruct's I-Assm `instruct_range`, over
  * the value the connection carries. Discharges when the sender's
  * guarantee is at least as strong as the receiver's assume. */
pub proof fn vc_integration_gen_outstruct_to_split_stage_instruct(wire: SysPropStructSplit_Data_Model::StructXY)
  requires
    gen::integration_spec_outstruct_range_guarantee(wire),
  ensures
    split_stage::integration_spec_instruct_range_assume(wire),
{}

SysPropStructSplit has exactly one such VC: gen.outstruct → splitter.instruct, the only connection whose destination carries an integration assume. Every other connection produces no Integration VC, for one of two reasons that are both design points of the example. Downstream of the splitter, IncX and DecY state their input constraints as compute assumes (per-dispatch preconditions, discharged by Pre-Assert VCs from carried facts — §3.2) and ClampX and MergeStruct assume nothing at all — so there is no port-level handshake to check. And at the far end, merger.outstruct → consume.instruct has no producer-side guarantee: with no handshake at the merger, the merged range cannot be established by integration checking and must instead be recovered by a system property (§5.1).

3.7 Component Contract Conformance (assumed — not emitted)

Informal. Each component’s implementation must satisfy its own GUMBO contract: if the component’s assumes hold when it is dispatched, executing its actual entry-point code yields a state satisfying its guarantees. Every Next-Assert VC uses the contract as a proxy for the real behavior, so the whole system proof is sound only if this proxy is faithful.

Generated form (for the reader’s mental model — the system-level generator emits no such VC):

∧ (C's assume clauses, over the pre-state)
∧ (C's entry point executes)
⊢ ∧ (C's guarantee/case clauses, over pre- and post-state)

This obligation is discharged per component by each component crate’s own Verus run — the HAMR-generated requires/ensures on the initialize and compute entry points are precisely these clauses (see component-implementation-guide.md). In the trust accounting of §6 these are assumptions T1 (compute) and T2 (initialize): the system-level VC set depends on them but does not check them.

3.8 Independence requirements (per MHIP pair)

A split { sequence{incx; clampx}, sequence{decy} } declares that the two branches may happen in parallel (MHIP). The Sequential VCs reason about one linearization (incx, then clampx, then decy, then join). Three obligation kinds justify that this single-order reasoning stands in for every order the schema permits.

The MHIP relation ranges over all pairs of schedule transitions that can be co-enabled — both fireable at some reachable point of the schema’s control structure. This includes (component, control-point) pairs, which arise with nested splits or multi-element branches. Emission per pair:

SysPropStructSplit has two MHIP pairs — decy is co-enabled with each element of the multi-element x branch: incx/decy (transitions t2/t4) and clampx/decy (t3/t4) — hence 8 per-property independence VCs plus 2 shared commutativity VCs. Note which pair is absent: incx/clampx are consecutive elements of one sequence, never co-enabled, so no independence obligations arise between them — which is just as well, since clampx reads incx’s output (§3.8.4).

3.8.1 Non-Blocking — a firing does not disable its sibling

Informal. Executing one branch must not invalidate the assertion at the sibling’s before place (its enabledness). Bidirectional: one VC per direction.

Inputs. Both transitions’ pre-assertions; the firing component’s global write frame.

Generated form.

pre-asserts(t1) ∧ pre-asserts(t2) ∧ (t1 fires: global_write_frame(t1))
⊢ pre-asserts(t2) still hold in the post-state        (and symmetrically for t2)

Example — merged_in_consume_range/vc_independence.rs:

/** VC[19]: Non-Blocking -- INCX firing does not block DECY (MHIP pair t2/t4) */
pub proof fn vc_non_blocking_incx_decy(pre: SystemState, post: SystemState)
  requires
    sys_assert_merged_in_consume_range_before_incx(pre),   // inRange100(x0)
    sys_assert_merged_in_consume_range_before_decy(pre),   // inRange100(y0)
    incx_global_write_frame(pre, post),                    // everything but x1 unchanged
  ensures
    sys_assert_merged_in_consume_range_before_decy(post),  // inRange100(y0) still holds
{}

3.8.2 Preservation — a firing does not destroy an established post

Informal. Executing one branch must not invalidate the sibling’s already-established after assertion — this is exactly what the join VC (§3.4) relies on when it conjoins the branch posts. Bidirectional.

Inputs. The firing transition’s pre-assertions; the sibling’s post-assertions; the firing component’s global write frame.

Generated form.

pre-asserts(t1) ∧ post-asserts(t2) ∧ (t1 fires: global_write_frame(t1))
⊢ post-asserts(t2) still hold in the post-state       (and symmetrically for t2)

Example — merged_in_consume_range/vc_independence.rs:

/** VC[21]: Preservation -- INCX firing preserves DECY's post-assertions (MHIP pair t2/t4) */
pub proof fn vc_preservation_incx_decy(pre: SystemState, post: SystemState)
  requires
    sys_assert_merged_in_consume_range_before_incx(pre),
    sys_assert_merged_in_consume_range_after_decy(pre),    // y1 ∈ [-101,99]
    incx_global_write_frame(pre, post),
  ensures
    sys_assert_merged_in_consume_range_after_decy(post),   // y1 ∈ [-101,99] survives
{}

Both kinds discharge from write-frame disjointness: the before_decy/after_decy assertions are over {y0}/{y1}, which incx_global_write_frame holds fixed (incx writes only x1).

3.8.3 Commutativity — the state comes out the same in either order

Informal. Firing the pair in either order yields the same SystemState, so the one linearization the Sequential VCs analyzed represents both. This is property-independent — a structural fact about the two components’ read/write behavior — and symmetric in the pair, so exactly one VC is emitted per component-component MHIP pair.

Inputs. Both components’ fire predicates (action abstractions + global write frames, §2.6).

Generated form.

(t1 fires; then t2 fires)  ∧  (t2 fires; then t1 fires)   -- from the same start state
⊢ the two resulting states are equal

Example — vc_commutativity.rs:

/** VC[0]: Commutativity (execIndependent) -- firing INCX then DECY
  * yields the same state as DECY then INCX (MHIP pair t2/t4).
  * Discharges by congruence when the write sets are disjoint from each
  * other's write sets and read scopes. */
pub proof fn vc_commutativity_incx_decy(
  st: SystemState, mid_a: SystemState, post_a: SystemState,
  mid_b: SystemState, post_b: SystemState)
  requires
    incx_fire(st, mid_a),
    decy_fire(mid_a, post_a),
    decy_fire(st, mid_b),
    incx_fire(mid_b, post_b),
  ensures
    post_a == post_b,
{}

Why the action abstractions are needed. Write-frame disjointness alone is not a valid discharge argument for commutativity: frames only pin down the fields a component does not write — they never determine the written values, and a relational postcondition does not either, so a frames-only encoding is unprovable even for perfectly disjoint components. Commutativity actually requires Bernstein’s conditions: each component’s write set must be disjoint from the other’s write set and read scope. The uninterpreted-action encoding (§2.6) captures exactly this — each written field is an unknown function of the component’s read scope — so a genuinely independent pair discharges automatically by congruence (incx writes {x1} reading {x0, x1}; clampx writes {x2} reading {x1, x2}; decy writes {y1} reading {y0, y1}; in each MHIP pair, neither member reads or writes what the other writes), while an interfering pair fails.

3.8.4 When independence and commutativity fail

These VCs discharge here only because the branches are genuinely independent. They would fail — correctly flagging an unsound split — in scenarios like these:

• Commutativity fails — shared write (output fan-in). If both incx and decy wrote the same channel, incx;decy leaves the second writer’s value and decy;incx the other’s, so the final states differ. HAMR’s channel model (one owning out-port per channel) rules this out for well-formed connections, but it is the canonical commutativity breaker.
• Commutativity fails — read-after-write dependency. If decy read x1 (IncX’s output), then decy fired after incx sees the updated x1 but fired before incx sees the old one — different y1, different final states. Such a data dependency means the two are not parallel; they must be modeled in a sequence, not a split. The failing VC is the tool telling you so. The example contains the positive counterpart: clampx reads incx’s output x1, and the schema accordingly places them in one sequence { incx; clampx } — had they been put in separate split branches instead, vc_commutativity_incx_clampx would be emitted and would fail on exactly this dependency (clampx’s read scope overlaps incx’s write set).
• Non-Blocking fails — a firing disables its sibling. If incx’s write set included y0 (clobbering the splitter’s y channel), then after incx fires, before_decy = inRange100(y0) might no longer hold — decy is no longer enabled in a state its contract covers.
• Preservation fails — a firing invalidates an established post. If incx’s write set included y1, incx firing after decy would overwrite decy’s result; after_decy would not survive, and the join (§3.4) could not soundly conjoin the branch posts.

In every failing case the root cause is a violation of the read/write disjointness that the write frames and action abstractions encode. The remedy is either to fix the modeled read/write scopes or to serialize the components with sequence instead of split.

4. Contract projection — which contracts a property pays for

Per property, a component’s contract is projected out — instantiated as (assumes, guarantees) := (true, true) — unless the property binds one of the component’s out-places (i.e., that component’s Next-Assert conclusion is non-trivial). An uncovered component contributes only its write frames (which hold unconditionally), so its Pre-Assert VC is trivial and its Next-Assert VC is frame-only.

The generated code says so explicitly. In merged_in_consume_range (which binds before consume — the canonical place after_merge_stage — but not after consume), ConsumeStruct is projected away:

/** VC[15]: Pre-Assert -- trivial: this property does not use CONSUME's contract (no bound out-place; contract projection) */
pub proof fn vc_pre_assert_consume(st: SystemState)
  requires
    sys_assert_merged_in_consume_range_after_merge_stage(st),
  ensures
    true /* no assertions at out-places */,
{}

Consequences worth internalizing:

• A property only pays for the components its story concludes something about. Gen_Range_Sanity binds only after gen, so SplitStruct, IncX, ClampX, DecY, MergeStruct, and ConsumeStruct are all projected away — no downstream assume must be discharged, and the smoke test stays a one-step proof. The moment a property binds after incx, IncX’s contract turns on and a fact must be carried to before incx.
• Sparse properties stay sparse. In a multi-property composition each property’s VC set sees only its own assertions and only its covered components’ contracts, so adding properties scales the proof linearly without entangling the proofs of existing ones.
• Compare merged_in_consume_range (consume projected, VC[15] trivial) with consume_range_loop_invariant (consume covered, VC[15] a real obligation — §3.2): the same transition generates a different obligation per property, driven solely by which out-places each property binds.

5. Two worked proofs

5.1 Merged_In_Consume_Range — recovering a range the contracts don’t state

This property’s payoff VC is where the constraint-free merger’s output range is recovered:

/** VC[14]: Next-Assert (task) -- post_join_1 + frames + MERGE_STAGE postcondition |- after_merge_stage */
pub proof fn vc_next_assert_task_merge_stage(pre: SystemState, post: SystemState)
  requires
    sys_assert_merged_in_consume_range_post_join_1(pre),   // x2 ∈ [-100,100] & y1 ∈ [-101,99]
    merge_stage_local_write_frame(pre, post),
    merge_stage_global_write_frame(pre, post),
    merge_stage::compute_spec_merge_x_guarantee(pre.x2, post.merged),  // merged.x == x2
    merge_stage::compute_spec_merge_y_guarantee(pre.y1, post.merged),  // merged.y == y1
  ensures
    sys_assert_merged_in_consume_range_after_merge_stage(post),        // inConsumeRange(merged)
{}

MergeStruct contributes only its functional compute guarantee — it has no integration guarantee to offer. The range comes entirely from the carried post_join_1 fact: merged.x == x2 ∈ [-100,100] ⊆ [-200,200], likewise for y. This is the whole point of the system property: inConsumeRange(merged) is the same predicate ConsumeStruct assumes, proved at the exact channel feeding consume.instruct — which is why the model binds it through the place name before consume (the generated code’s canonical name for that place is after_merge_stage; they are the same place). With no producer-side integration guarantee there is no Integration VC handshake at that connection (§3.6); the system property closes that assurance gap as a first-class, machine-checked system fact.

The full sequential chain (17 VCs, from merged_in_consume_range/vc_sequential.rs):

(Verus verifies these as independent obligations; the file order — branch VCs 5–10 before the fan-out VC 11 — is layout, not proof order. VC numbers restart per file, which is why vc_integration.rs and vc_commutativity.rs also start at VC[0].)

5.2 Consume_Range_Loop_Invariant — a state-variable loop invariant

This property exercises the START/END machinery that Merged_In_Consume_Range leaves trivial. Its invariant inRange200(consume_last_x) over ConsumeStruct’s GUMBO state variable holds every cycle, by exactly the textbook loop-invariant argument:

1. Establish — the Init-State VC (§3.1): consume’s initialize guarantee last_x == 0 implies the START assertion.
2. Maintain across the frame — consume_last_x is in no other component’s write set, so every other firing’s global write frame carries the invariant for free; the property need not restate it at intermediate places.
3. Re-establish at the firing that writes it — the Pre-Assert VC discharges consume’s [-200,200] compute assume from the carried inConsumeRange(merged) (§3.2), and the Next-Assert VC derives after consume from track_x: last_x == instruct.x plus that same carried range fact (§3.3).
4. Close the loop — after consume flows to END (control-point VC), and the Post-Pre VC END ⊢ START (§3.5) extends the invariant to every subsequent hyperperiod.

The upstream range plumbing (Pipeline_Ranges) and the state plumbing (Consume_State_Base) enter by multiple inheritance — the flattened assertion set is their union, place by place (§2.3).

6. Soundness and the trusted base

6.1 What discharging all VCs establishes

If every generated VC discharges, then: every place assertion of every concrete property holds whenever execution reaches that place, in every major frame, under any linear static schedule that conforms to the schedule schema. The argument is the induction of §1: the Init-State VC gives the base case, the Sequential VCs push assertions across each frame, the Post-Pre VC closes the frame-to-frame loop, and the Independence/Commutativity VCs reduce every schema-conforming order of the split branches to the one linearization the Sequential VCs analyzed. The Integration VCs certify the cross-component handshakes those steps (and the per-component verifications) rely on.

6.2 The modular architecture

Verification is split into two layers connected by a shared contract interface:

• Component level. Verus verifies each component’s entry-point code against its local GUMBO contracts (the generated requires/ensures on initialize and the compute entry point) — this is §3.7’s Contract Conformance.
• System level. The VCs in this document reason about the schedule structure and the place assertions. They never see component code; they work with copies of the component contracts (contracts.rs).

The separation is not just conceptual: component crates are compiled as staticlib (a Microkit platform requirement), so the proof crate cannot depend on them. The system proof is thereby forced to reason only about contract interfaces, never implementations — the assume-guarantee boundary is enforced by the build system.

6.3 The trusted assumptions (TCB)

“Every generated VC discharges” does not by itself mean “the system satisfies the properties.” It means the properties hold relative to the following assumptions, which are discharged outside the system-level VC set or currently trusted. They are the trusted computing base (TCB) of the system proof, listed so the trust boundary is explicit and auditable:

Why each is load-bearing:

• T1/T2. Every Next-Assert VC takes a component’s guarantees as a premise, and the Init-State VC takes the initialize guarantees as premises — the contracts stand proxy for the real code (§3.7). The proxy is faithful only if the per-component verifications actually pass. Run make verus from hamr/microkit/ to discharge T1/T2 and the system proof together.
• T3. If a copied contract diverged from the one the component crate verified, T1/T2 would be discharged against a different specification than the one the system proof consumes. Identity holds because a single generator derives both from one GUMBO source.
• T4. T1/T2 are discharged as Verus proofs about Rust entry-point functions, but the VCs consume them as facts about abstract “component firing” steps over SystemState. That identification assumes the generated infrastructure delivers the read-compute-write execution model the VCs encode: inputs frozen at dispatch, one owning writer per channel, outputs released on completion, and no writes outside the modeled write set. This correspondence is not itself machine-checked; it is the deliberate, standard cost of assume-guarantee modularity.

A practical corollary: because the VCs are proved, a runtime violation of a system assertion (e.g., observed by the optional runtime monitor) cannot be a logic error in the property chain — it localizes to a TCB breach: a component not conforming to its contract, an execution-model deviation (T4), or hardware/environment faults.

7. How the pieces fit — a synthesis

The component contracts (contracts.rs) are axioms discharged by the per-component Verus runs (T1/T2); the Integration VCs certify their boundary handshakes so those axioms are non-vacuous and so in-port assumes may be assumed at dispatch. Each property compiles its place assertions into SystemState predicates, with inheritance flattened to conjunction. The Init-State VC establishes the entry assertion; the Sequential VCs thread the assertions through the schedule — Pre-Assert VCs guard each covered component’s preconditions, Next-Assert (component) VCs spend the component’s guarantees to advance the assertion, Next-Assert (control point) VCs fan out and rejoin the parallel branches — and the Post-Pre VC closes the frame loop. The Non-Blocking, Preservation, and Commutativity VCs certify that the one linearization the Sequential chain reasoned about stands in for every legal interleaving of the split. Discharging all of them proves the system-level properties of the composed system — given only each component’s local contract, and relative to the explicit trusted base of §6.

Related

• gumbo-system-properties.md — authoring the composition/property syntax; the verified StructSplit example in full.
• gumbo-bnf.md, sysmlv2-gumbo-quick-reference.md — the GUMBO expression language used in assertions.
• build-and-verification-commands.md — the component-level Verus targets that discharge T1/T2.
• technical-approach.md — the read-compute-write execution semantics underlying T4.
• Further generated-proof examples (INSPECTA-models @ 4da74d7): Isolette (11 components, 15 properties, compute cases, latched fail-safe invariant) and TempControl (event data ports, state-variable loop invariant).