GUMBO System-Level Properties – Overview

This chapter provides an overview of how to specify and verify system-level properties in HAMR. HAMR system properties are cross-component properties of a whole composed system, written in an extension of the GUMBO contract language. For verification, HAMR generates verification conditions (VCs) (in special Rust crates) represented and Verus specifications and contracts. System properties are proved when Verus verifies HAMR generated VCs.

The current state of a the tool is a “usable prototype”. The approach currently has a number of manual features (like adding support system assertions to enable system properties to be proved) that we will automate in the future. Moreover, other then syntax highlighting and checking, there is no high-level model IDE support that, for example, reports failure of VCs to verify in terms of problem markers in model-level specifications. All of these features will be added later.

In our initial experiments, we have found that HAMR’s agentic framework (using Claude code and Codex) can write and verify system specifications in a highly automated fashion.

The worked example throughout this document is the Struct Split example, whose composition block and four properties are reproduced verbatim below and verify end-to-end. Two larger examples — the Isolette and TempControl system-verification models in loonwerks/INSPECTA-models — are excerpted where they demonstrate things Struct Split cannot (§10).

1. What a system-level property is (and why)

Component-level GUMBO contracts (integration assume/guarantee, compute contracts) specify the behavior of each component in isolation. However, we often want to specify and verify behavior properties that address the combined behavior of components as they are executed according to some schedule. A common example is the formalization of “system properties” that specify some desired “end-to-end” behavior relating inputs occurring earlier in the schedule cycle (e.g., inputs from sensors or external data sources) to outputs occurring later in the schedule (e.g., outputs to actuators or external data sources).

GUMBO system specifications layer on top of GUMBO component contracts to specify such properties. In this approach, verification of system specifications does not “see” or utilize component implementations (e.g., Rust application code implementing a component). Instead, system verification uses only information represented in component contracts; each component GUMBO contract provides a “summary” of the component behavior that is used as the basis of proving the desired system properties.

Like GUMBO component contracts, GUMBO system specifications support both formal verification, testing, and run-time monitoring. This chapter focuses on using system specifications for formal verification.

This documentation uses a contrived example called Struct Split as an example. The example implements a simple pipeline of components that manipulate a struct of two int32 fields named x and y (see full SysMLv2 model).

  • A GenStruct component generates a struct with arbitrary x and y values between -100 and 100 inclusive (the component has no inputs). The range constraints on the x and y are expressed as GUMBO integration constraints on the output port
  • A SplitStruct component receives a struct and splits out the x and y fields on two separate output ports so that the values can be processed in parallel.
  • The processing of the x value proceeds as follows…
    • An IncX component takes in x, increments it, and places the new value of x on the output port.
    • Then a ClampX component moves the value of x back to within the range [-100,100] if it happens to lie outside of it.
  • The processing of the y value proceeds as follows…
    • An DecY component takes in y, decrements it, and places the new value of y on the output port.
  • A MergeStruct component takes the individual x and y values and re-assembles them into a struct.
  • A ConsumeStruct component receives the final struct and logs it.

One can imagine several system properties for this example:

  • Range properties: Struct values initially lie within a small range of -100 and 100. The operations on values are single increments and decrements as the values flow through the system. Even though the contracts of the components generally don’t mention ranges of the values (except for a few cases), we should be able to prove that values entering ConsumeStruct are still within the tight expected ranges since all intermediate components either copy the values through or just do a single increment or decrement.
  • Functional “end-to-end” properties: We should be able to verify, e.g., that the final value of x flowing into ConsumeStruct is either (a) one greater than its initial value if the initial value is less than 100 or (b) equal to its initial value if the initial value was 100.

The example is explicitly constructed to illustrate several concepts:

  • the role that component independence and scheduling play in system specifications
  • the interplay between component level contracts (which should generally be constructed to be independent of the system contracts) and system specifications (which specify important facts about the system execution and utilize component contracts to verify desired system properties).

1.1 Scheduling and Independence

First, the component computations have natural data dependences on other components leading to execution order dependences. For example, the data dependences in the system sketch above imply that a system schedule should have…

  • GenStruct executed first
  • SplitStruct executed next
  • then components that process of x and y should be scheduled before MergeStruct
  • ConsumeStruct is scheduled last.

Second, there is natural independence of the x and y processing, leading us to not care about the possible schedule order of the x and y steps. The only thing to enforce is that IncX happens before ClampX.

Thus, we can have the following cyclic schedules that satisfy the constraints above.

Schedule 1: (x processing goes before y processing):

  • GenStruct
  • SplitStruct
  • IncX
  • ClampX
  • DecY
  • MergeStruct
  • ConsumeStruct

Schedule 2: (y processing goes before x processing):

  • GenStruct
  • SplitStruct
  • DecY
  • IncX
  • ClampX
  • MergeStruct
  • ConsumeStruct

Schedule 3: (x processing is interleaved with y processing):

  • GenStruct
  • SplitStruct
  • IncX
  • DecY
  • ClampX
  • MergeStruct
  • ConsumeStruct

Due to the above reasoning, we say that IncX “may happen in parallel” with DecY because the two are independent. Similarly, ClampX “may happen in parallel” with DecY because the two are independent. Even though we don’t have true parallelism in our HAMR executions (except for multi-core, which we don’t address here), we use the phrase “X may happen in parallel with Y” (MHIP(X,Y)) because it is a classic phrase/concept from concurrency theory indicating that two tasks are independent and thus may be scheduled in any order wrt each other (or even executed simultaneously). MHIP(IncX,DecY) is reflected in schedules 1 and 3 in which the precedence of IncX and DecY is reversed. MHIP(ClampX,DecY) is reflected in schedules 2 and 3 in which the precedence of ClampX and DecY is reversed.

Note that MHIP(X,Y) is symmetric, i.e., if MHIP(X,Y) holds, then we also have MHIP(Y,X).

Because HAMR components do not have shared state, we can tell if two components are independent within a system by analyzing the data flow implied by the system connection topology. Our verification framework for system properties checks components for the MHIP parallel property.

When we verify system properties, we want to avoid the burden of having to verify them for every possible schedule that appropriately addresses dependence notions. Therefore, the HAMR system verification framework allows developers to specify a “schedule schema” that abstractly represents a family of possible schedules (e.g., the three schedules above) that conform to dependence and indendence notions that we have outlined above.

For example, after introducing a few more ideas, we will end up writing a GUMBO schedule schema for our running example that looks like this (also full definition in SysMLv2 models).

schema {
  gen; // GenStruct
  split_stage; // SplitStruct
  split {
    sequence { 
      incx; // IncX
      clampx // ClampX
      },
    sequence { 
      decy // DecY
    }
  };
  label branches_joined;
  merge_stage; // MergeStruct
  consume // ConsumeStruct
}

In the above, we see abbreviations like gen used for GenStruct. We will see how to define these and use them as short-hand to reference component execution steps in schedule schema and in property specifications. Names like branches_joined can be introduced to label specific control points of interest.

The schema indicates both required sequencing (such as in gen; split_stage (i.e., SplitStruct must immediately follow GenStruct) as well as independence of the components mentioned in the split construct. The split structure aligns with the MHIP concept: each item on one branch of the split may happen in parallel with each item on the other branch of the split. GUMBO schedule schemas have an underlying Petri Net formalization that reflects these notions.

There is a notion of schedule conformance to a schema: Schedule 1, 2, and 3 above all conform to the given schema because each of the orderings in the given schedules obeys the sequencing and independence properties expressed in the schema. The verification framework includes a step to check that HAMR schedule supplied for seL4 scheduling in the deployed system conforms to the given schema.

Note that one can specify schema that is overly conservative wrt to independence notions. For example, we could have…

schema {
  gen; // GenStruct
  split_stage; // SplitStruct
  incx; // IncX
  split {
    sequence { 
      clampx // ClampX
      },
    sequence { 
      decy // DecY
    }
  };
  label branches_joined;
  merge_stage; // MergeStruct
  consume // ConsumeStruct
}

…which forces IncX to come before DecY. In this case, Schedules 1 and 3 would conform to the schema, but not Schedule 2.

We can even specify a complete linearization of tasks in a schedule…

schema {
  gen; // GenStruct
  split_stage; // SplitStruct
  incx; // IncX
  clampx; // ClampX
  decy; // DecY
  merge_stage; // MergeStruct
  consume // ConsumeStruct
}

In this case, only Schedule 1 would be conformant.

The point here is that these last two scheduling schemas are overly conservative with respect to required ordering. We could possibly use them for verification, but the verification would apply to fewer possible schedules.

1.2 Illustration of Component Contracts as a Foundation, not a Complete Specification of Behavior

In component-oriented development where the emphasis is on reusable components, one aims to design components to be re-useable, i.e., to be independent of a specific system context so that they can be reused in multiple systems. With respect to component contracts, that means that we want our GUMBO component contracts to focus on the required behavior of the component itself, not on how the component deals with properties relevant to a larger system context.

The component contracts in this example have been chosen to illustrate how component contracts can focus on their local behavior, but then how facts about the broader system context can be reasoned about in a layering on top of the component contracts.

Let’s look at each component’s GUMBO component contracts (also see actual models)

GenStruct

part def GenStruct :> Periodic_Rust_Thread {
    //-- I n t e r f a c e  --
    port outstruct : DataPort { out :>> type : SysPropStructSplit_Data_Model::StructXY; }

    //-- B e h a v i o r    C o n s t r a i n t s --
    language "GUMBO" /*{
      integration
        guarantee outstruct_range "Both fields of the generated struct lie in [-100, 100].":
          (-100 [i32] <= outstruct.x) & (outstruct.x <= 100 [i32]) &
          (-100 [i32] <= outstruct.y) & (outstruct.y <= 100 [i32]);

      initialize
        guarantee init_outstruct "The output data port must be initialized.":
          (outstruct.x == 0 [i32]) & (outstruct.y == 0 [i32]);
    }*/
  }

Here we use integration constraints to reflect the fact that field values of the generated structure are limited to the range of -100 to 100. Note that we could also specify these range constraints as compute guarantees, but then we would lose the benefit if being able to utilize those contraints at the time of model assembly.

Impact on model assembly integration constraint checking: Phrasing the range constraints as integration constraints makes the constraints available for verification before system verification at model assembly time, i.e., by the HAMR SysML Logika Check action. For any component’s input port that connects to the outstruct port, the integration constraint checking will know the range of values guaranteed to be flowing from the outstruct port and will be able to use the fact in the process of trying to discharge any assume integration constraints on the connected input port. For example, we’ll see in the SplitStruct component whose instruct input is connected to outstruct that assumption made on the instruct port can be discharged using the fact represented by the outstruct guarantee above.

Impact on system verification: The information about the range of values on the outstruct port will also be available for us as we perform system verification. Specifically, after GenStruct is executed in the system schedule (and also after the system initialize phase completes), we will know that value on the outstruct port satisfies the range constraint. We will be able to use that knowledge to make deductions about outstruct values as they flow into the inputs of other components. For example, we may be able to use that knowledge to discharge any compute assume obligations on connected components.

Impact on component implementation verification (e.g., by Verus): When we implement our component application logic for GenStruct, e.g., in Rust and use Verus to verify the code against HAMR-generated Verus constracts derived from the GUMBO contracts above, we will be required to prove (via Verus) that any time we call the put_outstruct API method to put a value on the outstruct port, the argument to the put_ method satisfies the constraints. These steps in verifying via Verus that the Rust component application logic conforms to the contract allow us to trust that the constraints in the GUMBO contract are satisfied when we use them in integration constraint checking and system reasoning.

SplitStruct

  part def SplitStruct :> Periodic_Rust_Thread {
    //-- I n t e r f a c e  --
    port instruct : DataPort { in :>> type : SysPropStructSplit_Data_Model::StructXY; }
    port xfield   : DataPort { out :>> type : Base_Types::Integer_32; }
    port yfield   : DataPort { out :>> type : Base_Types::Integer_32; }

    //-- B e h a v i o r    C o n s t r a i n t s --
    language "GUMBO" /*{
      integration
        assume instruct_range "Incoming struct fields lie in [-100, 100].":
          (-100 [i32] <= instruct.x) & (instruct.x <= 100 [i32]) &
          (-100 [i32] <= instruct.y) & (instruct.y <= 100 [i32]);
        guarantee xfield_range "xfield lies in [-100, 100].":
          (-100 [i32] <= xfield) & (xfield <= 100 [i32]);
        guarantee yfield_range "yfield lies in [-100, 100].":
          (-100 [i32] <= yfield) & (yfield <= 100 [i32]);

      compute
        guarantee split_x "xfield equals the x field of the incoming struct.":
          xfield == instruct.x;
        guarantee split_y "yfield equals the y field of the incoming struct.":
          yfield == instruct.y;
    }*/
  }

The compute contracts represent the local behavior of the component: the component copies the x and y values from the input struct onto separate output ports.

The integration constraints in this case are overkill: too much of the system behavior constraints have been pushed down to the component. Specifically, the act of struct splitting can be expected to work fine regardless of the specific values of the fields. There is no need to limit the values to the ranges specified by the integration constraints.

The best contract design for this component would be to eliminate the integration constraints. However, we keep them in this contrived example to illustrate other aspects of how integration constraints are handled in VC generation and verification.

Impact on model assembly integration constraint checking: When performing HAMR model-level integration constraint checking at model assembly time, the checking will be able to verify that the assume constraint is satisfied because the instruct input is connected to the outstruct output port of the GenStruct component, which guarantees that its output value lies within the same range.

Impact on system verification: The integration assume on instruct is justified once, per connection, by the handshake with GenStruct’s output guarantee (the same implication the assembly-time check verifies, re-established as an Integration VC in the generated system proof). After SplitStruct fires in the schedule, the system proof has both its compute guarantees (xfield == instruct.x, yfield == instruct.y) and its integration guarantees (each output in [-100, 100]) available as premises — so a property can establish range facts at the after split_stage place either directly from the output guarantees or by combining the field equalities with the range already known for instruct. In this example, both routes reach the same conclusion. In contrast, in downstream components (which will omit integration constraints), we will reason about the outputs of components in terms of facts the system specs establish for inputs and the component contract.

Impact on component implementation verification (e.g., by Verus): The integration assume becomes an ensures clause on the generated get_instruct API method — the component body may rely on the incoming fields lying in [-100, 100] without checking them. Dually, the integration guarantees become requires clauses on put_xfield and put_yfield, so Verus demands proof that every value the implementation sends is in range. Because the implementation forwards fields of the input struct (whose range the get_ ensures supplies), the obligations discharge directly.

IncX

  part def IncX :> Periodic_Rust_Thread {
    //-- I n t e r f a c e  --
    port inxfield  : DataPort { in :>> type : Base_Types::Integer_32; }
    port outxfield : DataPort { out :>> type : Base_Types::Integer_32; }

    //-- B e h a v i o r    C o n s t r a i n t s --
    language "GUMBO" /*{
      compute
        assume inxfield_bounded "Overflow guard only: the input lies in a
          |conservative [-1000, 1000] envelope so the increment cannot overflow.":
          (-1000 [i32] <= inxfield) & (inxfield <= 1000 [i32]);
        guarantee incx "Output is the input incremented by one.":
          outxfield == inxfield + 1 [i32];
    }*/
  }

Again, the compute guarantee represents the local behavior of the component: the value of x is incremented as it flows through the component.

This component is written to be reusable. One possible approach would be to use integration constraints tying its input to [-100, 100] and its output to [-99, 101] — the ranges of this particular system. That design would push too much of the system context down into the component: a general-purpose increment stage should accept arbitrary values of x. The only thing it genuinely must guard against is overflow of the increment. Ideally the contract would assume just “inxfield is below the i32 maximum,” but GUMBO currently has no way to reference machine-integer bounds, so we adopt a conservative envelope of [-1000, 1000] — deliberately distinct from the [-100, 100] range of the system context, so the two are easy to tell apart in what follows. We also state the constraint as a compute assume rather than an integration assume, to illustrate how the two kinds of assumptions are handled differently by the verification machinery.

Impact on model assembly integration constraint checking: IncX no longer participates in assembly-time integration checking at all — there is no assume on its input port for the checker to discharge, and it offers no output guarantee for downstream checks to consume; the connection splitter.xfield → incx.inxfield needs no handshake. Note what is given up relative to the alternate design: assembly-time checking can no longer conclude anything about the range of values on outxfield. Recovering such derived facts is exactly what the system-level property layer is for. Moreover, the current design is more reusable because the input ranges are more permissive.

Impact on system verification: A compute assume is a genuine per-dispatch precondition. Whenever a system property covers IncX (binds one of its after places — see §5 on contract projection), the proof must show that the facts carried into the before incx place imply inxfield ∈ [-1000, 1000] (the Pre-Assert VC of gumbo-system-property-vcs.md). Intuitively we expect this to be provable from the contracts of the components that precede IncX in the schedule schema: GenStruct guarantees the generated x lies in [-100, 100], and SplitStruct’s compute guarantee forwards it unchanged — so the value reaching IncX lies in [-100, 100], comfortably inside [-1000, 1000]. §5–§6 show how this intuition is written down as a chain of “place assertions”, and the VCs document shows the mechanics of the formal proof. A second consequence: since IncX no longer publishes an output-range guarantee, any fact about outxfield’s range must now be derived — from the compute guarantee outxfield == inxfield + 1 combined with whatever input range the property carries into the dispatch.

Impact on component implementation verification (e.g., by Verus): The compute assume is woven into the requires clause of the timeTriggered entry point, so the body may rely on inxfield ∈ [-1000, 1000] — which is exactly what Verus needs to prove that v + 1 cannot overflow. The port APIs are now unconstrained: get_inxfield no longer ensures a range, and put_outxfield no longer requires one.

ClampX

  part def ClampX :> Periodic_Rust_Thread {
    //-- I n t e r f a c e  --
    port inxfield  : DataPort { in :>> type : Base_Types::Integer_32; }
    port outxfield : DataPort { out :>> type : Base_Types::Integer_32; }

    //-- B e h a v i o r    C o n s t r a i n t s --
    language "GUMBO" /*{
      compute
        compute_cases
          case In_Range "values already in [-100, 100] pass through unchanged":
            assume (-100 [i32] <= inxfield) & (inxfield <= 100 [i32]);
            guarantee outxfield == inxfield;
          case Above "values above 100 saturate to 100":
            assume inxfield > 100 [i32];
            guarantee outxfield == 100 [i32];
          case Below "values below -100 saturate to -100":
            assume inxfield < -100 [i32];
            guarantee outxfield == -100 [i32];
    }*/
  }

The compute contract captures the behavior of the component as follows: The component forwards its scalar input unchanged when it lies in [-100, 100] and saturates it to the nearest bound otherwise.

ClampX carries no constraints beyond its compute cases — no integration constraints, and (unlike IncX and DecY) not even a compute assume. None are needed: the compute_cases are total — the three case assumptions cover every possible i32 input — the clamp performs no arithmetic that could overflow, and the output range is fully determined by the cases themselves. An alternate design might give integration constraint ranges, but as indicated in earlier discussions, that would be over-constraining the components behavior and would limit its reuse. Without integration constraints, the component works correctly in any context and is maximally reusable.

Impact on model assembly integration constraint checking: Nothing to check — the connection incx.outxfield → clampx.inxfield carries no assume to discharge, and downstream checking receives no guarantee from clampx.outxfield.

Impact on system verification: ClampX imposes no proof obligation at its dispatch — with no assumes of any kind, its Pre-Assert VC is trivially true, and a property may cover it without carrying anything to its before place. When it is covered, all three compute cases are available as premises after it fires, and the prover selects the applicable case from whatever input fact the property carries (e.g., knowing x1 ∈ [-99, 101] at the before clampx place). The [-100, 100] output-range fact can be derived from the cases: In_Range yields outxfield == inxfield ∈ [-100, 100], Above yields 100, Below yields -100; in every case the output lies in [-100, 100].

Impact on component implementation verification (e.g., by Verus): The three cases are woven as ensures implications on the timeTriggered entry point, and the body must satisfy all of them — straightforward, since the implementation’s if/else mirrors the case structure. The port APIs carry no range contracts in either direction.

DecY

  part def DecY :> Periodic_Rust_Thread {
    //-- I n t e r f a c e  --
    port inyfield  : DataPort { in :>> type : Base_Types::Integer_32; }
    port outyfield : DataPort { out :>> type : Base_Types::Integer_32; }

    //-- B e h a v i o r    C o n s t r a i n t s --
    language "GUMBO" /*{
      compute
        assume inyfield_bounded "Underflow guard only: the input lies in a
          |conservative [-1000, 1000] envelope so the decrement cannot underflow.":
          (-1000 [i32] <= inyfield) & (inyfield <= 1000 [i32]);
        guarantee decy "Output is the input decremented by one.":
          outyfield == inyfield - 1 [i32];
    }*/
  }

DecY mirrors IncX: a reusable decrement stage whose only assumption is the guard against underflow of the decrement (the symmetric hazard — here it is the i32 minimum that GUMBO cannot reference, so the same conservative [-1000, 1000] envelope stands in).

The impacts track IncX’s exactly.

Model assembly: no handshake on splitter.yfield → decy.inyfield, and no published output range.

System verification: whenever a property covers DecY, its [-1000, 1000] compute assume must be discharged from the assertion carried to the before decy place — provable by the same intuition as for IncX, since GenStruct’s guarantee and SplitStruct’s forwarding deliver a y value in [-100, 100]; and the output range [-101, 99] must be derived from the compute guarantee outyfield == inyfield - 1 plus the carried input range.

Component Verus verification: the assume is woven as a requires on timeTriggered — sufficient to prove v - 1 cannot underflow — and the port APIs are unconstrained.

MergeStruct

  //===============================================================================
  //
  //  M e r g e S t r u c t   Thread
  //
  //  Re-assembles a StructXY from its two scalar inputs.
  //
  //  NOTE: this component intentionally carries NO integration
  //  constraints -- it makes no assumption about the ranges of its
  //  inputs and offers no range guarantee on its output.  Its only
  //  contract is the functional compute guarantee below.  Recovering
  //  the output range is the motivating use case for the system-level
  //  property feature (see the composition block in SysPropStructSplit.sysml).
  //===============================================================================
  part def MergeStruct :> Periodic_Rust_Thread {
    //-- I n t e r f a c e  --
    port inxfield : DataPort { in :>> type : Base_Types::Integer_32; }
    port inyfield : DataPort { in :>> type : Base_Types::Integer_32; }
    port outstruct : DataPort { out :>> type : SysPropStructSplit_Data_Model::StructXY; }

    //-- B e h a v i o r    C o n s t r a i n t s --
    language "GUMBO" /*{
      compute
        guarantee merge_x "Output struct's x field equals the inxfield input.":
          outstruct.x == inxfield;
        guarantee merge_y "Output struct's y field equals the inyfield input.":
          outstruct.y == inyfield;
    }*/
  }

MergeStruct’s only contract is functional: two compute guarantees stating that the output struct’s fields equal the respective scalar inputs. It makes no assumption about its inputs and offers no range guarantee on its output — as the NOTE in the model banner says, this is the deliberate design (not a specification flaw) that motivates the system-property feature: the range of the reassembled struct is a system fact, not a property of the merge operation itself.

Impact on model assembly integration constraint checking: The connections clampx.outxfield → merger.inxfield and decy.outyfield → merger.inyfield carry no assumes to discharge. More consequentially, the connection merger.outstruct → consume.instruct offers no producer-side guarantee — so nothing available at assembly time establishes the range of struct values flowing to ConsumeStruct. Whatever the consumer needs must be proved at the system level.

Impact on system verification: When a property covers MergeStruct, its contribution is exactly the two equalities merged.x == inxfield and merged.y == inyfield — nothing more. Any range (or value) fact about merged must be recovered by combining those equalities with facts the property has carried from the two branches to the join. That recovery is precisely Property 1 (Merged_In_Consume_Range) in §6.

Impact on component implementation verification (e.g., by Verus): The woven ensures clauses force the implementation to copy its two inputs into the output struct’s fields; put_outstruct carries no precondition, so no range reasoning is needed in the body.

ConsumeStruct

  //===============================================================================
  //
  //  C o n s u m e S t r u c t   Thread
  //
  //  Sink component.  Receives a StructXY and logs it; has no output ports.
  //  Carries a GUMBO state variable `last_x` that records the x field of the
  //  most recently consumed struct -- persistent component state that the
  //  system-level loop-invariant property (see the composition block in
  //  SysPropStructSplit.sysml) reasons about across hyperperiod boundaries.
  //===============================================================================
  part def ConsumeStruct :> Periodic_Rust_Thread {
    //-- I n t e r f a c e  --
    port instruct : DataPort { in :>> type : SysPropStructSplit_Data_Model::StructXY; }

    //-- B e h a v i o r    C o n s t r a i n t s --
    language "GUMBO" /*{
      state
        last_x: Base_Types::Integer_32;

      initialize
        guarantee init_last_x "The state variable starts at zero.":
          last_x == 0 [i32];

      compute
        assume instruct_range "Incoming struct fields lie in [-200, 200].":
          (-200 [i32] <= instruct.x) & (instruct.x <= 200 [i32]) &
          (-200 [i32] <= instruct.y) & (instruct.y <= 200 [i32]);
        guarantee track_x "last_x records the x field of the most recently consumed struct.":
          last_x == instruct.x;
    }*/
  }

ConsumeStruct is the pipeline’s sink. Its compute assume is a contrived defensive precondition: the component is specified (and its implementation verified) only for structs whose fields lie in [-200, 200] — a deliberately loose envelope around anything the pipeline could produce. And this specification is chosen to motivate how we can use system reasoning to satisfy the assumption even though contract of the preceding component is not directly strongly enough to satisfy it.

Another contrived feature of this component is the last_x state variable, which we introduce to illustrate facts that we want to reason about across schedule boundaries (i.e., from the end of the schedule back to the beginning of the schedule as it cycles/loops). The guarantee track_x latches the input’s x field into the GUMBO state variable last_x on every dispatch, and the initialize guarantee pins the latch’s starting value; together they are the raw material for the loop-invariant (i.e., schedule cycle) property (Property 3 in §6).

Impact on model assembly integration constraint checking: The [-200, 200] constraint is a compute assume, not an integration assume, so assembly-time integration checking does not attempt to discharge it — and could not if it tried: the upstream producer, MergeStruct, publishes no integration guarantee for the checker to use.

Impact on system verification: Whenever a property covers ConsumeStruct (binds after consume), the [-200, 200] compute assume becomes a Pre-Assert obligation at the before consume place. The intuition for why it is provable from the upstream contracts along the schedule schema: GenStruct produces x, y ∈ [-100, 100]; the x branch increments (to [-99, 101]) and then clamps back into [-100, 100]; the y branch decrements to [-101, 99]; and MergeStruct reassembles exactly those values — so both fields of the arriving struct lie within [-101, 100], comfortably inside [-200, 200]. §6 writes this chain down as place assertions, and gumbo-system-property-vcs.md shows each link discharged as a VC.

Impact on component implementation verification (e.g., by Verus): The compute assume is woven as a requires on the timeTriggered entry point (the body may rely on it), track_x becomes an ensures relating the post-state variable to the input, and the initialize guarantee obliges initialize() to set last_x to zero.

2. Where the specification lives

Now that we have discussed the intuition behind system specifications and their relationship to component specifications, we’ll start with discuss how the above concepts are actually achieved (also see full example).

A system-level specification is a language "GUMBO" block placed inside the top-level System part def, after the allocation declarations. (The delimiters are /*{ … }*/, exactly as for component GUMBO blocks; the type checker parses the contents.)

part def StructSplit_System :> System {
  part gen : Gen_Process;         // … process instances …
  connection c1 : PortConnection connect gen.outstruct to splitter.instruct;   // … connections …
  allocation pb0 : Deployment_Properties::Actual_Processor_Binding allocate gen to struct_split_processor;

  language "GUMBO" /*{
    functions           // optional: reusable spec functions
      …
    composition nominal {
      components …
      ports …
      state …           // optional: aliases for component GUMBO state variables
      schema { … }
      property … { … }
    }
  }*/
}

Inside the block, functions (optional) is a sibling of composition <name> { … }. Just as in GUMBO component contract specifications, we can use these functions to defined named properties or helper predicates that we want to use in the system specification.

The composition name (nominal here) names this system-level specification; codegen derives a sys_proof_<name> crate from it (sys_proof_nominal). Multiple composition blocks are allowed. HAMR will generate a distinct sys_proof_<name> crate for each one.

3. The composition block

3.1 functions — reusable spec patterns

This section contains ordinary GUMBO function definitions, identical in form to component-level or library GUMBO functions. Use them to specify predicates that recur across properties. Some examples are given below.

functions
  def inRange100(v: Base_Types::Integer_32): Base_Types::Boolean :=
    (-100 [i32] <= v) & (v <= 100 [i32]);
  def inConsumeRange(s: SysPropStructSplit_Data_Model::StructXY): Base_Types::Boolean :=
    (-200 [i32] <= s.x) & (s.x <= 200 [i32]) &
    (-200 [i32] <= s.y) & (s.y <= 200 [i32]);
  def inRange200(v: Base_Types::Integer_32): Base_Types::Boolean :=
    (-200 [i32] <= v) & (v <= 200 [i32]);
  def mergedReflectsGen(m: SysPropStructSplit_Data_Model::StructXY,
                        g: SysPropStructSplit_Data_Model::StructXY): Base_Types::Boolean :=
    ((g.x < 100 [i32]) implies (m.x == g.x + 1 [i32])) &
    ((g.x == 100 [i32]) implies (m.x == 100 [i32])) &
    (m.y == g.y - 1 [i32]);

Bundle recurring conjunct groups into one function. Because related properties often restate the same group of facts at several places (§5), a group of facts that always “travels” through schedule schema togther should be a single function — the restatements collapse to one call, the definition stays single-sourced, and a change to the group cannot silently diverge between properties. (The Isolette does this with sysProp_REQ_MRI_7, sysProp_REQ_MMI_5, etc.)

Name the property itself as a function when you can. inConsumeRange is Property 1’s claim and mergedReflectsGen is Property 2’s — each stated once, given a meaningful name, and bound at a single place in the concrete property (§6). The function name then serves as the property’s citable statement in reviews and assurance arguments.

3.2 components — short aliases for thread instances

Each entry aliases a fully-qualified thread instance path (<process-instance>.<thread-instance>) to a short name used everywhere else in the composition and in the schema. This reduces effort in writing specifications.

components
  gen         = gen.gen;             // process `gen`, thread `gen`
  split_stage = splitter.splitter;
  incx        = incx.incx;
  clampx      = clampx.clampx;
  decy        = decy.decy;
  merge_stage = merger.merger;
  consume     = consume.consume;

3.3 ports — named handles for the values properties reason about

Each entry aliases <component-alias>.<port>. In assertions the alias denotes the port’s value (for a struct port, use .field access, e.g. merged.x).

ports
  gen_out = gen.outstruct;      // StructXY
  x0      = split_stage.xfield; // Integer_32
  x1      = incx.outxfield;
  x2      = clampx.outxfield;
  merged  = merge_stage.outstruct;

3.4 state — aliases for component GUMBO state variables (optional)

When properties refer to a component’s persistent GUMBO state variable, alias it here as <alias> = <component-alias>.<stateVar>. Struct Split aliases ConsumeStruct’s latch:

state
  consume_last_x = consume.last_x;

The Isolette does the same for the mode/command state its properties track:

state
  ma_lastCmd    = ma.lastCmd;
  mmi_lastCmd   = mmi.lastCmd;
  reg_last_mode = mrm.lastRegulatorMode;

3.5 schema — the abstract schedule

The schema describes the order in which the components fire within one major frame — the abstract control structure the proof reasons over. It is built from:

Construct Meaning
comp fire component comp (a bare component alias)
sequence { a; b; … } fire a, then b, … in order
split { seqA, seqB, … } independent (parallel) branches that rejoin afterwards
label NAME; name a control point (typically a branch join) so properties can assert at NAME
(implicit) START / END the frame’s entry/exit control points, for loop invariants

Note the punctuation: ; separates the elements of a sequence (order is claimed), while , separates the branches of a split (order is deliberately not claimed).

schema {
  gen;
  split_stage;
  split {
    sequence { incx; clampx },   // a multi-element branch: incx, then clampx
    sequence { decy }
  };
  label branches_joined;         // the join point after the two branches
  merge_stage;
  consume
}

split models genuine independence: the branches must not interfere (codegen emits Commutativity and Independence VCs that check this), and at the join the post-conditions of all branches hold simultaneously — so no cross-branch frame condition is needed. Use a plain sequence (or bare list) when stages are strictly ordered.

Schemas scale to realistic systems. The Isolette’s schema has eleven components, two splits with multi-element branches, and a label naming the point between the first join and the second split (a point no before/after name can reach):

schema {
  split {
    sequence { oi },
    sequence { ts }
  };
  label ts_oi_done;
  split {
    sequence { drf; mri; mrm; mhs },
    sequence { dmf; mmi; mmm; ma }
  };
  hs
}

Places and their names

Assertions are bound to places — the points between component execution in a schedule schema — via the position names of §4.1. The rules:

  • Consecutive elements share a place: after incx and before clampx are two names for the same place (likewise Isolette’s after mrm ≡ before mhs). All names of a place are synonyms, and a property may bind a given place through only one of its names (binding both is an error). Struct Split’s Pipeline_Ranges exploits this: its single after incx binding is both IncX’s post-fact and the fact ClampX’s compute cases dispatch on. Pick the synonym that names the role the assertion plays — Struct Split binds before consume (not after merge_stage) for the fact that discharges the consumer’s precondition. Note that generated code uses one canonical identifier per place regardless of which synonym bound it: a before consume binding appears in sys_proof_<name> under the place name after_merge_stage.
  • Labels are optional and purely naming — never structural. Every point exists in the schema whether or not it is labeled; an unlabeled point simply cannot be bound (it carries true). A label is needed exactly when a property wants to bind a point with no unambiguous derived name (like ts_oi_done above). When a point has both a label and a derived name, binding the label is the edit-stable choice: it names the point by structural role, so inserting a component later does not silently re-point the binding the way before <next-component> would.
  • at <component> is illegal — it does not say which side of the dispatch is meant; use before/after.

4. Properties

A property binds place assertions (aka system assertions) to points in the schedule. (ToDo: property may not be the best name for this concept, as it is actually a collection of assertions. It’s more like a proof outline - a collection of assertions positioned in the schedule schema as needed to established the particular property that you have in mind.) A concrete property becomes a proof obligation; an abstract property does not (it exists only to be inherited).

4.1 Place-assertion (System assertion) clauses

<position> <target> ["optional description"] : <boolean-expr> ;
Position + target Assertion holds …
after <comp> immediately after comp fires (its guarantees are available)
before <comp> immediately before comp fires (its compute assume must follow from here)
at <label> at a named control point (e.g. a branch join)
at START / at END at frame entry / exit — used for loop invariants

The optional description may span lines using | continuation (as in component GUMBO). Expressions use the full GUMBO expression language (see gumbo-bnf.md): &/|/not (non-short-circuit), and/or/implies (short-circuit), ==/!=/</<=, arithmetic, typed literals [i32]/[s32]/[f32], .field access, port and state aliases, and the function-call implication '->:'(antecedent, consequent) used by the Isolette model.

4.2 Concrete vs. abstract, and inheritance

abstract property Pipeline_Ranges " … " { … }              // reusable, no proof target
property Merged_In_Consume_Range :> Pipeline_Ranges { … }  // concrete, inherits the carries
abstract property Pipeline_Functional :> Pipeline_Ranges { … }   // an abstract extending an abstract
property Consume_Range_Loop_Invariant :> Pipeline_Ranges, Consume_State_Base { … }  // multiple inheritance

The semantics is flattening with conjunction:

  • A property’s effective binding set is its parent’s effective set (transitively) extended with its own; multiple inheritance takes the union across all parents.
  • When two contributions bind the same place, the assertions are conjoined there. This is what lets Pipeline_Functional add value-equality carries onto the same places where Pipeline_Ranges already carries range facts. (Unbound places are true, and conjunction with true is identity, so sparse bases and children flatten cleanly.)
  • Inheritance therefore only strengthens: a child implies its parent at every place. There is deliberately no override/weaken form (SysMLv2’s :>> redefinition is not supported here) — replacing a parent’s binding could silently drop a safety assertion.
  • A concrete property generates exactly the VC set it would have had if its effective bindings were written inline. An abstract property is a base only: no VCs and no runtime-monitor checks are generated for it. Parents must be sibling properties of the same composition, and the inheritance graph must be acyclic.

4.3 Property name → verification target

Each concrete property name maps to a lowercased proof target: Merged_In_Consume_Range → merged_in_consume_range, Consume_Range_Loop_Invariant → consume_range_loop_invariant. Abstract properties produce no target.

4.4 Loop invariants: at START / at END

Properties over state variables can assert facts that hold at the frame boundaries. Codegen closes the loop with two obligations: the initial system state (after all initialize entry points) must establish the START assertion, and the END assertion must re-establish START (the Post-Pre VC) — so an invariant asserted at both boundaries holds in every cycle, forever. The pattern, from Consume_Range_Loop_Invariant (§6):

  1. at START: inRange200(consume_last_x) — established initially by ConsumeStruct’s initialize guarantee last_x == 0.
  2. Between START and consume’s firing, nothing needs restating: consume_last_x is in no other component’s write set, so the generated write frames preserve it for free.
  3. after consume: inRange200(consume_last_x) — re-established by consume’s compute guarantee last_x == instruct.x together with the carried inConsumeRange(merged) fact at consume’s dispatch place.
  4. at END: inRange200(consume_last_x) — closes the loop (END ⊢ START).

The same pattern carries much stronger safety arguments. The Isolette’s Regulator_Failsafe_Latching asserts FailedModeImpliesHeatOff(reg_last_mode, heat_control) at START, across the regulator chain, and at END; combined with MRM’s absorbing Failed mode, the discharged Post-Pre VC yields “once the regulator fails, the heat stays off forever.” TempControl’s Control_Invariant_Base uses the frame boundaries to carry the control component’s own compute assumes as a system-level invariant.

4.5 Event data ports, and current limitations

System assertions may range over event data port channels; the channel value is an option (a message may or may not be present in a frame), and HasEvent(...) guards access, exactly as in component compute contracts. From TempControl’s TC_Req_01:

after control "post-control: the fan state reflects the just-sensed temperature":
  '->:'(HasEvent(sensedTemp) and (not sv_fanError & sensedTemp.degrees < sv_currentSetPoint.low.degrees),
        sv_currentFanState == FanCmd.Off);

Current limitation: In(...) (pre-state reference) is not yet supported in system-property assertions — a pre/post relationship across one firing (e.g. “the fan state is unchanged when the temperature is in range”) cannot yet be stated directly at the system level. The workaround is a component state variable that latches the prior value, reasoned about with the loop-invariant pattern of §4.4.

5. The modular proof model (essential mental model)

The system proof is modular and Hoare-style. For each place in the schedule a property binds an assertion (unbound places carry true), and codegen emits, per schedule transition:

  • a Pre-Assert VC: assertion(before C) ⟹ C's compute assume (you may run C only if its precondition holds here), and
  • a Next-Assert VC: assertion(before C) ∧ C's integration assumes ∧ frame(C) ∧ C's guarantees ⟹ assertion(after C).

A component’s integration assumes (in-port constraints) are handled by a separate, per-connection Integration VC (sender's guarantee ⟹ receiver's assume), which is why the Next-Assert may simply assume them at each dispatch. (Toolchains predating this folding — including the one that generated this repository’s example crate — discharge the integration assumes at the Pre-Assert instead; both forms are sound, and the authoring guidance below is the same either way. See gumbo-system-property-vcs.md §3.2.)

Three consequences drive how you write properties:

  1. Contract projection. Per property, a component’s contract is used only if the property binds one of that component’s after places — otherwise the contract is projected to true and only the component’s write frame participates. The smoke-test property Gen_Range_Sanity binds only after gen, so IncX/ClampX/DecY/Merge/Consume generate no assume obligations at all. The moment a property binds after incx, IncX’s assumes must be discharged — which needs a fact at the before incx place. Compare Merged_In_Consume_Range (consume’s [-200,200] assume projected away) with Consume_Range_Loop_Invariant (binds after consume, so that assume becomes a real obligation — discharged by the same inConsumeRange(merged) fact the property carries).

  2. Facts do not flow implicitly between places. Each VC sees only the assertion at its own place. To make a fact available where it is needed you must assert it there:

    • to discharge a component’s assume, put the needed fact at its before place (the “branch entry” pattern);
    • to make a branch’s result available to the merge, assert it at the join label;
    • to carry a value across a step that doesn’t touch it, rely on the generated write frame (each component leaves everything outside its write set unchanged) and restate the fact at the next place.

    This is why the abstract bases restate the range/equality at after gen, after split_stage, before incx, after incx, at branches_joined, and so on — the chain of carries is the proof. Factoring that chain into an abstract property is the recommended way to avoid repeating it across related properties.

  3. Properties are proved independently. Each property’s VCs see only its own (flattened) assertions — never another property’s. A fact another property establishes must be restated (or inherited) to be used. The failure mode is benign: an omission fails loudly as an unprovable VC naming the missing premise.

at START / at END close a hyperperiod loop invariant: codegen emits a Post-Pre VC requiring END ⟹ START, so an invariant asserted at both boundaries is proved to hold every cycle (§4.4).

6. Worked example (verified verbatim)

6.1 How system-property verification fits the developer workflow

System-property work starts from properties the developer already has in mind — claims they believe hold of the system’s execution and want machine-checked. Two archetypes recur. First, “every component is dispatched within its contract”: each component’s compute assume should hold at every dispatch, established by what the rest of the system does upstream. ConsumeStruct is our running example — its defensive [-200, 200] assume is a per-dispatch precondition that nothing at the component level justifies, because its producer (MergeStruct) publishes no guarantee. Second, end-to-end functional results: outputs late in the schedule should relate to inputs generated early (here, the consumed struct should be a deterministic function of the generated one).

The method, step by step:

  1. Write the property as a GUMBO function. inConsumeRange(s) specifies our first “in mind” claim as a GUMBO function; mergedReflectsGen(m, g) specifies the second. A named function gives the claim a single-sourced, citable statement (§3.1) that assertions can bind at a place.
  2. Choose the place where the property should hold. Both of our claims are about what reaches the consumer, so their natural home is before consume — the place where ConsumeStruct is dispatched.
  3. Sketch the proof backwards through the schema. Ask, for the chosen place: which component establishes this fact, and what must be true before that component fires? Repeat until you reach facts that component contracts supply directly (GenStruct’s integration guarantee, initialize guarantees). The answers become supporting assertions at intermediate places: facts that discharge each covered component’s compute assume at its before place, branch results made available at the join label, and restatements that carry a fact across steps that do not touch it (§5).
  4. Factor shared base facts into abstract property bases. Related properties tend to need the same supporting chains. Stating them once as an abstract property and inheriting via :> (§4.2) keeps each concrete property down to its actual conclusion.

With that method in mind, here are the three properties we verify, stated informally:

  1. Merged_In_Consume_Range — the struct handed to ConsumeStruct always lies within [-200, 200] on both fields; i.e., ConsumeStruct’s defensive compute assume is satisfied on every dispatch, in every frame.
  2. End_To_End_Functional — the struct arriving at the consumer is exactly (gen.x + 1 saturated at 100, gen.y - 1): the generated values, transformed by the two branches, reassembled without loss.
  3. Consume_Range_Loop_Invariant — in every hyperperiod, the value latched in ConsumeStruct’s last_x state variable lies in [-200, 200].

(A fourth concrete property, Gen_Range_Sanity, is a one-step toolchain smoke test.) After the model text below, §6.3 explains how the properties are verified by reading their assertion chains as proofs.

6.2 The composition block

The full composition block from SysPropStructSplit.sysml — this verifies with 0 errors:

language "GUMBO" /*{

  functions

    // Repeated range predicates, factored as GUMBO functions (spec-pattern reuse).
    def inRange100(v: Base_Types::Integer_32): Base_Types::Boolean :=
      (-100 [i32] <= v) & (v <= 100 [i32]);

    def inConsumeRange(s: SysPropStructSplit_Data_Model::StructXY): Base_Types::Boolean :=
      (-200 [i32] <= s.x) & (s.x <= 200 [i32]) &
      (-200 [i32] <= s.y) & (s.y <= 200 [i32]);

    def inRange200(v: Base_Types::Integer_32): Base_Types::Boolean :=
      (-200 [i32] <= v) & (v <= 200 [i32]);

    // The end-to-end functional result, named as a spec function: the struct
    // arriving at the consumer equals (g.x + 1 saturated at 100, g.y - 1).
    // ClampX's saturation only bites at g.x == 100, so the x field is stated
    // as a case split on g.x.
    def mergedReflectsGen(m: SysPropStructSplit_Data_Model::StructXY,
                          g: SysPropStructSplit_Data_Model::StructXY): Base_Types::Boolean :=
      ((g.x < 100 [i32]) implies (m.x == g.x + 1 [i32])) &
      ((g.x == 100 [i32]) implies (m.x == 100 [i32])) &
      (m.y == g.y - 1 [i32]);

  composition nominal {

    // Short alias  =  <process-instance>.<thread-instance>
    components
      gen         = gen.gen;
      split_stage = splitter.splitter;
      incx        = incx.incx;
      clampx      = clampx.clampx;
      decy        = decy.decy;
      merge_stage = merger.merger;
      consume     = consume.consume;

    // Named handles for the port values the properties refer to.
    ports
      gen_out = gen.outstruct;
      x0      = split_stage.xfield;
      y0      = split_stage.yfield;
      x1      = incx.outxfield;
      x2      = clampx.outxfield;
      y1      = decy.outyfield;
      merged  = merge_stage.outstruct;

    // Named handles for the component GUMBO state variables the properties refer to.
    state
      consume_last_x = consume.last_x;

    // Abstract schedule: after the splitter, the x branch (incx then clampx --
    // a multi-element branch) and the decy branch run independently and rejoin
    // (branches_joined) before the merger.
    schema {
      gen;
      split_stage;
      split {
        sequence { incx; clampx },
        sequence { decy }
      };
      label branches_joined;
      merge_stage;
      consume
    }

    // Smoke test: a minimal single-step property discharged directly by
    // GenStruct's integration guarantee -- exercises the whole toolchain path.
    property Gen_Range_Sanity
      "toolchain smoke test: the generator output lies in [-100, 100]" {
      after gen "GenStruct integration guarantee":
        inRange100(gen_out.x) & inRange100(gen_out.y);
    }

    //-----------------------------------------------------------------------------
    //  Property 1 -- recover the merger's output range from upstream contracts and
    //  show it satisfies ConsumeStruct's defensive [-200, 200] assume.
    //-----------------------------------------------------------------------------

    abstract property Pipeline_Ranges
      "shared range plumbing: carry [-100,100] from gen through split into each
      |branch (discharging IncX's and DecY's [-1000,1000] compute assumes), then
      |carry the transformed ranges across the branch join to the merger" {
      after gen "GenStruct guarantees both fields in [-100, 100]":
        inRange100(gen_out.x) & inRange100(gen_out.y);
      after split_stage "SplitStruct forwards each field, preserving [-100, 100]":
        inRange100(x0) & inRange100(y0);
      before incx "branch entry: x still in [-100, 100] -- discharges IncX's
        |[-1000, 1000] overflow-guard compute assume":
        inRange100(x0);
      after incx "IncX's compute guarantee (x1 == x0 + 1) plus the carried
        |[-100, 100] range yield x1 in [-99, 101]; this place IS `before clampx`
        |(consecutive branch elements share a place), and ClampX -- whose
        |compute_cases are total -- needs no assume discharged here":
        (-99 [i32] <= x1) & (x1 <= 101 [i32]);
      after clampx "ClampX saturates back into [-100, 100]":
        inRange100(x2);
      before decy "branch entry: y still in [-100, 100] -- discharges DecY's
        |[-1000, 1000] underflow-guard compute assume":
        inRange100(y0);
      after decy "DecY's compute guarantee (y1 == y0 - 1) plus the carried
        |[-100, 100] range yield y1 in [-101, 99]":
        (-101 [i32] <= y1) & (y1 <= 99 [i32]);
      at branches_joined "join: both transformed ranges are available to the merger":
        inRange100(x2) &
        (-101 [i32] <= y1) & (y1 <= 99 [i32]);
    }

    property Merged_In_Consume_Range :> Pipeline_Ranges
      "the merger carries no integration constraint; its output range is recovered
      |here from the upstream guarantees and shown to satisfy ConsumeStruct's
      |defensive [-200, 200] assume" {
      before consume "ConsumeStruct's precondition, established at its dispatch
        |from MergeStruct's guarantees merged.x == x2 and merged.y == y1
        |(this place IS `after merge_stage` -- consecutive schema elements
        |share a place)":
        inConsumeRange(merged);
    }

    //-----------------------------------------------------------------------------
    //  Property 2 -- end-to-end functional result: the consumer ultimately sees
    //  (gen.x + 1 saturated at 100, gen.y - 1); ClampX's saturation only bites
    //  at gen.x == 100, so the x result is stated as a case split on gen.x.
    //  Pipeline_Functional EXTENDS Pipeline_Ranges: the range plumbing is still
    //  needed to discharge each component's input assume (and to select ClampX's
    //  compute case), and the value-equality carries are conjoined onto the same
    //  schema places.
    //-----------------------------------------------------------------------------

    abstract property Pipeline_Functional :> Pipeline_Ranges
      "adds value-equality carries on top of the inherited range plumbing" {
      after split_stage "SplitStruct forwards the struct fields unchanged":
        (x0 == gen_out.x) & (y0 == gen_out.y);
      before incx "branch entry: x still equals the generated x":
        x0 == gen_out.x;
      after incx "IncX adds one":
        x1 == gen_out.x + 1 [i32];
      after clampx "ClampX's compute cases yield the saturated value: the clamp
        |only bites when gen.x == 100 (i.e., x1 == 101)":
        ((gen_out.x < 100 [i32]) implies (x2 == gen_out.x + 1 [i32])) &
        ((gen_out.x == 100 [i32]) implies (x2 == 100 [i32]));
      before decy "branch entry: y still equals the generated y":
        y0 == gen_out.y;
      after decy "DecY subtracts one":
        y1 == gen_out.y - 1 [i32];
      at branches_joined "join: the transformed values are available to the merger":
        ((gen_out.x < 100 [i32]) implies (x2 == gen_out.x + 1 [i32])) &
        ((gen_out.x == 100 [i32]) implies (x2 == 100 [i32])) &
        (y1 == gen_out.y - 1 [i32]);
    }

    property End_To_End_Functional :> Pipeline_Functional
      "end-to-end: the merged struct equals (gen.x + 1 saturated at 100, gen.y - 1)" {
      before consume "MergeStruct reassembles the transformed fields; the named
        |spec function states the end-to-end result at the end of the chain --
        |the struct arriving at the consumer reflects the generated struct":
        mergedReflectsGen(merged, gen_out);
    }

    //-----------------------------------------------------------------------------
    //  Property 3 -- a loop invariant over ConsumeStruct's `last_x` state variable:
    //  in every hyperperiod, the value it latched lies in [-200, 200].
    //
    //  The concrete property uses MULTIPLE inheritance: Pipeline_Ranges supplies
    //  the range chain that establishes inConsumeRange(merged) at consume's
    //  dispatch, and Consume_State_Base supplies the state-variable plumbing.
    //-----------------------------------------------------------------------------

    abstract property Consume_State_Base
      "loop-invariant plumbing for ConsumeStruct's last_x state variable: hold
      |the invariant at frame entry, carry the merged range to consume's dispatch,
      |and re-establish the invariant when consume fires" {
      at START "frame entry: established initially by consume's initialize guarantee":
        inRange200(consume_last_x);
      before consume "the merged range fact at consume's dispatch; discharges
        |consume's [-200, 200] compute assume":
        inConsumeRange(merged);
      after consume "consume's guarantee last_x == instruct.x re-establishes the invariant":
        inRange200(consume_last_x);
    }

    property Consume_Range_Loop_Invariant :> Pipeline_Ranges, Consume_State_Base
      "every cycle, ConsumeStruct's latched last_x lies in [-200, 200]; the
      |Post-Pre VC (END |- START) makes the invariant hold across hyperperiod
      |boundaries" {
      at END "loop closure: carried from `after consume` to the frame boundary":
        inRange200(consume_last_x);
    }
  }
}*/

6.3 Reading the properties as proofs

Reading Merged_In_Consume_Range as a proof:

  • after gen gives gen_out ∈ [-100,100] (from GenStruct’s integration guarantee; the handshake with SplitStruct’s integration assume is certified separately, per connection);
  • after split_stage gives x0,y0 ∈ [-100,100] (SplitStruct forwards the fields);
  • before incx/before decy carry each field into its branch — these are the facts that discharge IncX’s and DecY’s [-1000,1000] compute assumes ([-100,100] ⊂ [-1000,1000], so the discharge is easy by design);
  • after incx gives x1 ∈ [-99,101] — derived from IncX’s compute guarantee x1 == x0 + 1 plus the carried range, since IncX no longer publishes an output-range guarantee — and, being the same place as before clampx, it is also the fact ClampX’s compute cases will dispatch on;
  • after clampx gives x2 ∈ [-100,100] (from the cases: In_Range passes the value through, Above/Below saturate to a bound);
  • after decy gives y1 ∈ [-101,99] (from y1 == y0 − 1); at branches_joined makes both branch results available to the merger;
  • then, using MergeStruct’s functional guarantees (merged.x == x2, merged.y == y1), before consume concludes merged ∈ [-200,200] — ConsumeStruct’s precondition, proved by composition at exactly the place where the consumer is dispatched.

Reading End_To_End_Functional as a proof: the same chain, with value equalities conjoined onto the range facts at each place (Pipeline_Functional :> Pipeline_Ranges — the ranges are still needed to discharge the compute assumes and to select ClampX’s compute case). The conclusion is the single call mergedReflectsGen(merged, gen_out) at before consume: the case split on gen_out.x carried through the x branch, and y1 == gen_out.y − 1 through the y branch, land in the merger’s reassembly.

Reading Consume_Range_Loop_Invariant as a proof: see §4.4 — establish at START from the initialize guarantee, preserve across the frame by write frames, re-establish at consume’s firing from track_x plus the carried merged range, close with END ⟹ START.

7. What codegen generates

When a composition <name> block is present, sireum hamr sysml codegen (Microkit target) emits a dedicated proof crate hamr/microkit/crates/sys_proof_<name>/ in addition to the per-component crates. No extra codegen flag is required. Structure:

crates/sys_proof_nominal/
  Cargo.toml  Makefile  rust-toolchain.toml
  src/
    lib.rs                # wires the shared modules + one module group per concrete property
    system_state.rs       # `SystemState`: one field per connection channel / unconnected port / GUMBO state var
    contracts.rs          # copies of the component GUMBO contracts (same GUMBO source; identical by construction)
    assertions.rs         # the composition's `functions` (e.g. inRange100, inRange200) as spec fns
    write_frames.rs       # per-component write frames (out-port channels + own state vars; everything else unchanged)
    actions.rs            # uninterpreted action abstractions (used only by Commutativity VCs)
    vc_commutativity.rs   # Commutativity VCs — one per independent component pair; property-independent
    vc_integration.rs     # Integration-constraint VCs (sender guarantee ⟹ receiver assume); property-independent
    <property>/           # one directory per CONCRETE property (abstract properties get none)
      assertions.rs       #   place-assertion spec fns (one per bound place; unbound = true; inheritance flattened)
      vc_init.rs          #   Init-State VC: initialize + integration guarantees ⟹ START
      vc_sequential.rs    #   Pre-Assert + Next-Assert VCs for every schema transition (the Hoare chain)
      vc_independence.rs  #   Non-Blocking / Preservation VCs for each independent transition pair
      vc_post_pre.rs      #   Post-Pre VC: END ⟹ START (hyperperiod loop invariant)
      mod.rs

All generated proof files are auto-generated (Do not edit …); the proof fns have empty bodies and Verus discharges requires ⟹ ensures by SMT. The system proof assumes each component satisfies its own contract (discharged separately by the per-component Verus runs) and proves the system properties from those contracts. gumbo-system-property-vcs.md walks every VC category in detail, including the soundness argument and its trusted assumptions.

8. Running the verification

Requires Rust + Verus (cargo-verus on PATH); it does not require MICROKIT_SDK/MICROKIT_BOARD. From hamr/microkit/:

# whole system proof (all properties + the shared Commutativity/Integration VCs)
make -C crates/sys_proof_nominal            # or: make -C crates/sys_proof_nominal all

# a single property in isolation (target = lowercased property name)
make -C crates/sys_proof_nominal merged_in_consume_range
make -C crates/sys_proof_nominal end_to_end_functional
make -C crates/sys_proof_nominal consume_range_loop_invariant

# everything: each component crate AND the system proof
make verus

In the Struct Split example each of the four concrete properties discharges 27 VCs (1 Init-State + 17 Sequential + 1 Post-Pre + 8 Independence); with the 3 shared VCs (1 Integration — only the gen → splitter connection still has an assume/guarantee handshake — plus 2 Commutativity, one per independent component pair) the whole sys_proof_nominal crate is 111 VCs; all seven component crates plus the system proof verify with 0 errors.

9. Authoring workflow and tips

  1. Type-check first. sireum hamr sysml tipe --sourcepath ../aadl-lib:. <Model>.sysml validates the composition/property syntax before codegen. Run it from the model directory.
  2. Regenerate from the model directory (not via the MCP tool) so the relative --output-dir resolves correctly and editable files are preserved — see mcp-tools.md. Codegen adds crates/sys_proof_<name>/; confirm it appeared and that no stray tree landed outside the project. Codegen may also (re)write a hamr/microkit/attestation/ tree — this example does not commit those artifacts, so delete it after regenerating.
  3. Start with a one-step smoke property (like Gen_Range_Sanity) to confirm the whole path — codegen → sys_proof_<name> → Verus — works before writing the real carries.
  4. Factor the carry chain into an abstract property. The shared plumbing that discharges each component’s assume and threads facts to the join is identical across related properties; write it once and inherit it (multiple bases compose, §4.2).
  5. Reach for GUMBO functions for range/relationship predicates used at several places (inRange100, inConsumeRange), and bundle conjunct groups that always travel together into a single function (§3.1).
  6. When a VC fails, read crates/sys_proof_<name>/src/<property>/vc_sequential.rs: each failing vc_pre_assert_* means a component’s assume is not established at its before place; each failing vc_next_assert_task_* means the after/join assertion is not derivable from the prior place plus the component’s contract. Add the missing carry.
  7. Remember contract projection when a property seems too easy or too hard. If a component’s guarantee “isn’t being used,” check whether the property binds one of that component’s after places (§5.1); if an assume obligation “appeared from nowhere,” a newly bound after place has just made that component covered.
  8. Alias collisions. Component/port/state aliases must not collide with SysMLv2 keywords or with the schema keywords sequence/split/label; the type checker flags these (see modeling-tips.md). Rename if tipe objects.
  9. New state variables need code. Adding a GUMBO state variable re-weaves the component’s *_app.rs marker regions with the variable and its contracts, but the entry-point bodies are yours: set the variable in initialize() (to satisfy the initialize guarantee) and in the compute entry point (to satisfy the compute guarantee), then re-run the component’s make verus.
  10. Adding a component to the schema needs deployment follow-up. Codegen re-weaves microkit.system; if it reports a conflict it writes microkit.system_fixme instead — reconcile it with the live file (see modeling-tips.md) and delete the _fixme. microkit.schedule.xml is never regenerated: hand-add the new component’s <domain …> slot (and rebalance the padding) so the static schedule matches the domain assignments.

10. Further examples

Two larger system-property compositions (with committed, verifying sys_proof_nominal crates) live in loonwerks/INSPECTA-models @ 4da74d7:

  • Isolette (isolette/sysml/Isolette.sysml, composition at the top-level system) — eleven components across regulator and monitor subsystems; two splits with multi-element branches and a label between them; state aliases; fifteen concrete properties built on two abstract bases (Regulator_Base, Monitor_Base); requirement-linked assertions via sysProp_* functions and '->:'; and the latched fail-safe loop invariant Regulator_Failsafe_Latching (“once the regulator fails, the heat stays off forever”).
  • TempControl (micro-examples/microkit/system-verification/temp-control/sysml/TempControl_SysVerif.sysml) — a three-component event data port system: HasEvent in system assertions, Option<T> channels in the generated SystemState, and a loop invariant (Control_Invariant_Base) that carries the control component’s compute assumes across the frame so every property covering it can discharge its Pre-Assert.
  • gumbo-system-property-vcs.md — a detailed walkthrough of the verification conditions generated for these properties (the full VC taxonomy with generated examples, contract projection, independence/commutativity, and the soundness argument with its trusted assumptions).
  • sysmlv2-gumbo-quick-reference.md — GUMBO expression/operator syntax used inside assertions.
  • gumbo-bnf.md — grammar and built-in predicates (In, HasEvent, NoSend, MustSend, '->:').
  • mcp-tools.md — running tipe / codegen (and the model-directory codegen procedure).
  • build-and-verification-commands.md — component-level Verus targets.
  • component-implementation-guide.md — implementing entry points against the woven contracts.