GUMBO Quick Reference

This chapter provides a quick reference (“cheat sheet”-like) illustration of GUMBO component contracts for HAMR SysMLv2. For the rationale and architecture of the GUMBO framework, see the GUMBO Overview; for an example-based walkthrough of contract structure using the Simple Isolette, see GUMBO Component Contracts.

Additional example resources:

• The three-part HAMR tutorial “Adding GUMBO Thread Component Contracts to an Existing System” for the Simple Isolette example provide a good illustration of how different types of GUMBO contracts are written and how they are translated down to code-level Rust executable contracts for testing and code-level Verus contracts for Verus verification (These tutorials are link off of the recommended reading order page). These tutorials only address periodic components with data ports (which model shared data communication and are never empty).

• The solution to the HAMR tutorial series “Building a HAMR System From Scratch” illustrates how to specify properties for event data ports (which model queued communication and use the ‘HasEvent’ construct to reason about presence or absence of messages on a port).

• The Isolette example from the INSPECTA models repo includes at least six thread components with extensive use of GUMBO specifications for periodic components with data ports. In particular, here are the GUMBO contracts for the Manage Heat Source component. Looking at these contracts from all thread components and associated HAMR-generated Verus contracts and executable contracts is one of the best example-based resources for understanding how GUMBO works.

• The contracts for the firewall components of the INSPECTA Open Platform example provide a good illustration of more complex properties for periodic components with event data ports.

GUMBO Specification Blocks

GUMBO contracts are embedded in Thread or Data part defs using:

language "GUMBO" /*{
  // GUMBO specification here
}*/

The content is inside a block comment /* ... */ so standard SysMLv2 parsers ignore it, but HAMR parses and processes it.

Overall Structure (Thread)

part def MyThread :> Thread {
  // ... ports, properties ...

  language "GUMBO" /*{
    state
      // state variable declarations

    functions
      // helper function definitions

    integration
      // port-level assume/guarantee constraints

    initialize
      // modifies clause (optional)
      // guarantee clauses for initialization

    compute
      // modifies clause (optional)
      // assume clauses
      // guarantee clauses
      // compute_cases
      // handle clauses (sporadic threads)
  }*/
}

Data Invariants

Note: Data invariants are not currently supported in HAMR Rust code generation.

part def Temperature :> Data {
  part degrees : Base_Types::Float_32;

  language "GUMBO" /*{
    invariants
      inv AbsZero:
        degrees >= GUMBO_Periodic_Definitions::GUMBO__Library::absoluteZero();
  }*/
}

part def TempWstatus_i :> Data {
  part degrees : Base_Types::Integer_32;
  attribute status : ValueStatus;

  language "GUMBO" /*{
    invariants
      inv MaxMinEarthTemperatures "Temps should fall within the max/min temperatures
                                  |recorded on planet Earth" :
        -128 [s32] <= degrees and degrees <= 134 [s32];
  }*/
}

part def SetPoint :> Data {
  part low : Temperature;
  part high : Temperature;

  language "GUMBO" /*{
    invariants
      inv SetPoint_Data_Invariant:
        (low.degrees >= 50.0 [f32]) &
        (high.degrees <= 110.0 [f32]) &
        (low.degrees <= high.degrees);
  }*/
}

---

11. GUMBO Library Functions

GUMBO library functions are defined in a dedicated package and can be called from any GUMBO block.

Defining Library Functions

package GUMBO_Periodic_Definitions {
  language "GUMBO" /*{
    library
      functions
        def absoluteZero(): Base_Types::Float_32 := -459.67 [f32];
  }*/
}

package GumboLib {
  language "GUMBO" /*{
    library
      functions
        def normalLibraryFunction(a: MyArrayInt32): Base_Types::Boolean :=
          (0 .. size(a) - 2) -> forAll {i; a#(i) <= a#(i + 1)};

        // Spec function (abstract, no body -- implemented externally)
        @spec def librarySpecFunction_Assume(a: MyArrayInt32): Base_Types::Boolean;
        @spec def librarySpecFunction_Guarantee(a: MyArrayInt32): Base_Types::Boolean;
  }*/
}

Complex Library Example (Isolette)

package GUMBO_Library {
  language "GUMBO" /*{
    library
      functions
        def LowerAlarmTemp_lower(): Base_Types::Integer_32 := 96[s32];
        def LowerAlarmTemp_upper(): Base_Types::Integer_32 := 101[s32];

        def Allowed_LowerAlarmTemp(lower: Base_Types::Integer_32): Base_Types::Boolean :=
          LowerAlarmTemp_lower() <= lower & lower <= LowerAlarmTemp_upper();

        def Allowed_LowerAlarmTempWStatus(
              lower: Isolette_Data_Model::TempWstatus_i): Base_Types::Boolean :=
          (isValidTempWstatus(lower) implies
                Allowed_LowerAlarmTemp(lower.degrees));

        def isValidTempWstatus(
              value: Isolette_Data_Model::TempWstatus_i): Base_Types::Boolean :=
          value.status == Isolette_Data_Model::ValueStatus.Valid;
  }*/
}

Calling Library Functions

// Fully qualified: PackageName::GUMBO__Library::functionName(args)
GUMBO_Library::GUMBO__Library::Allowed_LowerAlarmTemp(lower_alarm_temp.degrees)
GUMBO_Periodic_Definitions::GUMBO__Library::absoluteZero()
TempControlPeriodic::GUMBO__Library::inRange(currentTemp)

Note: The GUMBO__Library (double underscore) is the auto-generated container name for library functions.

Inline Library (within a component package)

package TempControlPeriodic {
  private import HAMR::*;

  language "GUMBO" /*{
    library
      functions
        def inRange(temp: Temperature): Base_Types::Boolean :=
          temp.degrees >= -40.0 [f32] and temp.degrees <= 122.0 [f32];
  }*/

  // ... component definitions follow ...
}

---

12. GUMBO State Declarations

State variables represent persistent internal component state that influences behavior across dispatches.

language "GUMBO" /*{
  state
    lastRegulatorMode: Isolette_Data_Model::Regulator_Mode;
}*/

state
  lastCmd: Isolette_Data_Model::On_Off;

state
  currentSetPoint: SetPoint;
  currentFanState: FanCmd;
  latestTemp: Temperature;

state
  myArrayInt32_StateVar: MyArrayInt32;
  myArrayStruct_StateVar: MyArrayStruct;
  myStructArray_StateVar: MyStructArray_i;

---

13. GUMBO Subclause Functions

Functions defined within a thread’s GUMBO block (not in a library).

Regular Functions

functions
  def ROUND(num: Base_Types::Integer_32): Base_Types::Integer_32 := num;

  def timeout_condition_satisfied(): Base_Types::Boolean := T;

  def defaultTempDegrees(): Base_Types::Float_32 := 72 [f32];

Functions Operating on Arrays

functions
  def myArrayInt32_FunctionReturn(v: MyArrayInt32): MyArrayInt32 := v;

  def myArrayInt32_FunctionParam(v: MyArrayInt32): Base_Types::Boolean :=
    (0 .. size(v) - 1) -> exists {i; v#(i) == 0[i32] };

  def myStructArray_i_FunctionParam(v: MyStructArray_i): Base_Types::Boolean :=
    (0 .. size(v.fieldArray) - 1) -> exists {i;
      v.fieldArray#(i).fieldSInt32 == 0[i32] };

Spec Functions (Abstract – no body)

functions
  // For assume contexts
  @spec def subclauseSpecFunction_Assume(a: MyArrayInt32): Base_Types::Boolean;

  // For guarantee contexts
  def subclauseSpecFunction_Guarantee(a: MyArrayInt32): Base_Types::Boolean;

Calling a Library Function from a Subclause Function

functions
  def Allowed_UpperAlarmTempWStatus(
        upper: Isolette_Data_Model::TempWstatus_i): Base_Types::Boolean :=
    GUMBO_Library::GUMBO__Library::Allowed_UpperAlarmTempWStatus(upper);

---

14. GUMBO Integration Constraints

Integration constraints specify assumptions and guarantees on ports that hold between dispatches – they constrain the values flowing through connections. Integration constraints can also be understood as invariants on values flowing through ports.

Assume (on input ports – receiver side)

integration
  assume currentTempRange:
    (currentTemp.degrees >= -40.0 [f32]) & (currentTemp.degrees <= 122.0 [f32]);

  assume Allowed_LowerAlarmTemp:
    GUMBO_Library::GUMBO__Library::Allowed_LowerAlarmTempWStatus(
      lower_alarm_tempWstatus);

  assume Allowed_UpperAlarmTemp:
    GUMBO_Library::GUMBO__Library::Allowed_UpperAlarmTempWStatus(
      upper_alarm_tempWstatus);

Guarantee (on output ports – sender side)

integration
  guarantee Sensor_Temperature_Range:
    TempControlPeriodic::GUMBO__Library::inRange(currentTemp);

  guarantee Allowed_LowerAlarmTempWstatus
    "Table_A_12_LowerAlarmTemp: Range [96..101]" :
    (GUMBO_Library::GUMBO__Library::isValidTempWstatus(lower_alarm_tempWstatus) implies
          (96[i32] <= lower_alarm_tempWstatus.degrees
          & lower_alarm_tempWstatus.degrees <= 101[i32]));

Integration with Array Quantifiers

integration
  guarantee integrationArrayInt32_DataPort:
    p_myArrayInt32_DataPort#(0) == 1[s32] &
    GumboLib::GUMBO__Library::librarySpecFunction_Guarantee(
      p_myArrayInt32_DataPort) &
    (0 .. size(p_myArrayInt32_DataPort) - 2) -> forAll {i;
      p_myArrayInt32_DataPort#(i) <= p_myArrayInt32_DataPort#(i + 1) };

  assume integrationStructArray_EventDataPort
    "Example of optional descriptor" :
    (0 .. size(c_myStructArray_EventDataPort.fieldArray) - 2) -> forAll {i;
      c_myStructArray_EventDataPort.fieldArray#(i).fieldSInt32
        <= c_myStructArray_EventDataPort.fieldArray#(i + 1).fieldSInt32 };

---

15. GUMBO Initialize Contracts

Initialize contracts specify what must hold after the component’s initialize entrypoint executes. The only include guarantee clauses on output ports and GUMBO-declared state variables since AADL semantics disallows reading of input ports in the initialize entrypoint.

Basic Guarantee

initialize
  guarantee
    RegulatorStatusIsInitiallyInit:
      regulator_status == Isolette_Data_Model::Status.Init_Status;

Multiple Guarantees

initialize
  guarantee
    initlastCmd: lastCmd == Isolette_Data_Model::On_Off.Off;
  guarantee REQ_MHS_1 "If the Regulator Mode is INIT, the Heat Control
                       |shall be set to Off." :
    heat_control == Isolette_Data_Model::On_Off.Off;

With Modifies Clause

initialize
  modifies (latestFanCmd);
  guarantee initLatestFanCmd "Initialize state variable":
    latestFanCmd == FanCmd.Off;
  guarantee initFanCmd "Initial fan command":
    fanCmd == FanCmd.Off;

initialize
  modifies currentSetPoint, currentFanState, latestTemp;

  guarantee defaultSetPoint:
    (currentSetPoint.low.degrees == 70 [f32])
    and (currentSetPoint.high.degrees == 80 [f32]);
  guarantee defaultFanStates:
    currentFanState == FanCmd.Off;
  guarantee defaultLatestTemp:
    latestTemp.degrees == 72.0[f32];

Compound Guarantee

initialize
  guarantee REQ_MA_1 "..." :
    alarm_control == Isolette_Data_Model::On_Off.Off &
    lastCmd == Isolette_Data_Model::On_Off.Off;

Output Port Initialization

initialize
  guarantee initOutputDataPort
    "The Initialize Entry Point must initialize all component
    |local state and all output data ports." :
    output == false;

---

16. GUMBO Compute Contracts

Compute contracts specify the behavior of the compute entrypoint.

Assume Clauses

compute
  assume lower_is_not_higher_than_upper:
    lower_desired_tempWstatus.degrees <= upper_desired_tempWstatus.degrees;

  assume Figure_A_7 "This is not explicitly stated in the requirements..." :
    upper_alarm_temp.degrees - lower_alarm_temp.degrees >= 1 [s32];

Guarantee Clauses (General)

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

  guarantee orOutput:
    actuate == (channel1 | channel2);

  guarantee coincidenceOutput "description..." :
    actuate == ((channel1 & channel2) |
                (channel1 & channel3) |
                (channel1 & channel4) |
                (channel2 & channel3) |
                (channel2 & channel4) |
                (channel3 & channel4));

Modifies Clause in Compute

compute
  modifies (latestFanCmd);
  // or
  modifies currentSetPoint, currentFanState, latestTemp;

Compute Cases

Compute cases provide case-based specifications with per-case assumes and guarantees.

compute
  compute_cases

    case REQ_MRI_1 "If the Regulator Mode is INIT,
                    |the Regulator Status shall be set to Init." :
      assume regulator_mode == Isolette_Data_Model::Regulator_Mode.Init_Regulator_Mode;
      guarantee regulator_status == Isolette_Data_Model::Status.Init_Status;

    case REQ_MRI_2 "If the Regulator Mode is NORMAL,
                    |the Regulator Status shall be set to On" :
      assume regulator_mode == Isolette_Data_Model::Regulator_Mode.Normal_Regulator_Mode;
      guarantee regulator_status == Isolette_Data_Model::Status.On_Status;

    case REQ_MRI_3 "If the Regulator Mode is FAILED,
                    |the Regulator Status shall be set to Failed." :
      assume regulator_mode == Isolette_Data_Model::Regulator_Mode.Failed_Regulator_Mode;
      guarantee regulator_status == Isolette_Data_Model::Status.Failed_Status;

Mixed General + Case-Based Guarantees

compute
  assume lower_is_lower_temp:
    lower_desired_temp.degrees <= upper_desired_temp.degrees;

  // General guarantee (always holds)
  guarantee lastCmd "Set lastCmd to value of output Cmd port":
    lastCmd == heat_control;

  // Case-specific guarantees
  compute_cases
    case REQ_MHS_1 "..." :
      assume regulator_mode ==
        Isolette_Data_Model::Regulator_Mode.Init_Regulator_Mode;
      guarantee heat_control == Isolette_Data_Model::On_Off.Off;

    case REQ_MHS_4 "If ... in range, the value shall not be changed." :
      assume (regulator_mode ==
          Isolette_Data_Model::Regulator_Mode.Normal_Regulator_Mode)
        & (current_tempWstatus.degrees >= lower_desired_temp.degrees
        & current_tempWstatus.degrees <= upper_desired_temp.degrees);
      guarantee heat_control == In(lastCmd);

Guarantee with Implication

guarantee
  (not interface_failure.flag) implies
    (lower_alarm_temp.degrees == lower_alarm_tempWstatus.degrees
    &
    upper_alarm_temp.degrees == upper_alarm_tempWstatus.degrees);

Using the Implication Operator

guarantee altCurrentTempLTSetPoint "If current temperature is less than
                                   |the current low set point, then the
                                   |fan state shall be Off" :
  (currentTemp.degrees < setPoint.low.degrees implies
        (latestFanCmd == FanCmd.Off and fanCmd == FanCmd.Off));

guarantee REQ_MRI_8 "..." :
  (not interface_failure.flag implies
        ((lower_desired_temp.degrees == lower_desired_tempWstatus.degrees)
        & (upper_desired_temp.degrees == upper_desired_tempWstatus.degrees)));

Unspecified Behavior

case REQ_MRI_5 "If the Regulator Mode is not NORMAL,
                |the value of the Display Temperature is UNSPECIFIED." :
  guarantee true;

case REQ_MRI_9 "..." :
  guarantee true;

---

17. GUMBO Handler Contracts (Sporadic Threads)

For sporadic (event-driven) threads, handler contracts specify behavior per event handler.

compute
  modifies currentSetPoint, currentFanState, latestTemp;

  // General guarantees (hold for all handlers)
  guarantee TC_Req_01 "..." :
    (latestTemp.degrees < currentSetPoint.low.degrees implies
          currentFanState == FanCmd.Off);

  guarantee mustSendFanCmd "..." :
    (In(currentFanState) != currentFanState)
      implies MustSend(fanCmd, currentFanState) and
    (currentFanState == In(currentFanState))
      implies NoSend(fanCmd);

  // Per-handler contracts
  handle setPoint:
    modifies (currentSetPoint);
    guarantee setPointChanged:
      currentSetPoint == setPoint;
    guarantee latestTempNotModified:
      (latestTemp == In(latestTemp));

  handle tempChanged:
    modifies (latestTemp);
    guarantee tempChanged:
      latestTemp == currentTemp;
    guarantee setPointNotModified:
      currentSetPoint == In(currentSetPoint);

  handle fanAck:
    guarantee setPointNotModified:
      currentSetPoint == In(currentSetPoint);
    guarantee lastTempNotModified:
      latestTemp == In(latestTemp);
    guarantee currentFanState:
      currentFanState == In(currentFanState);
    guarantee noEventsSent:
      NoSend(fanCmd);

---

18. GUMBO Operators and Expressions

The In() Operator (Pre-State Values)

In(stateVar) refers to the value of a state variable at the beginning of the current dispatch (pre-state). It can only be used on state variables, not on ports.

// State variable unchanged
guarantee heat_control == In(lastCmd);

// Comparing pre and post state
guarantee
  latestFanCmd == In(latestFanCmd) & fanCmd == latestFanCmd;

// In() with array indexing
guarantee noChange:
  In(myArrayInt32_StateVar)#(0) == myArrayInt32_StateVar#(0);

// In() with struct field access on arrays
guarantee:
  In(myArrayStruct_StateVar)#(0).fieldSInt32
    == myArrayStruct_StateVar#(0).fieldSInt32;

// In() passed to functions
guarantee:
  myArrayInt32_FunctionParam(In(myArrayInt32_StateVar));

GUMBO on Event Data Ports

Event data ports can be empty (no message) or contain a message on any given cycle. GUMBO provides three operators for reasoning about event data port state:

Operator	Meaning	Slang Translation
HasEvent(port)	Port contains a message	port.nonEmpty
MustSend(port)	A message must be sent on the port	port.nonEmpty
MustSend(port, value)	A message with the given value must be sent	port == Some(value)
NoSend(port)	No message must be sent on the port	port.isEmpty

Integration Constraints on Event Data Ports

Integration constraints on event data ports apply only when a message is present:

// Producer: guarantee output payload is in range when a message is sent
part def Prod :> Thread {
    port output : EventDataPort { out :>> type : Message; }

    language "GUMBO" /*{
        integration
            guarantee Payload_Range:
                (0 [i32] <= output.payload) & (output.payload <= 90 [i32]);
    }*/
}

// Consumer: assume input payload is in range when a message is received
part def Cons :> Thread {
    port input : EventDataPort { in :>> type : Message; }

    language "GUMBO" /*{
        integration
            assume Payload_Range:
                (0 [i32] <= input.payload) & (input.payload <= 100 [i32]);
    }*/
}

The Producer’s integration guarantee on output becomes the Consumer’s integration assume on input — this is compositional reasoning across the pipeline.

State and Initialize with Event Data Ports

part def Cons :> Thread {
    port input : EventDataPort { in :>> type : Message; }

    language "GUMBO" /*{
        state
            payload_sum: Base_Types::Integer_32;

        functions
            def Init_Payload_Sum(): Base_Types::Integer_32 := 0 [i32];

        integration
            assume Payload_Range:
                (0 [i32] <= input.payload) & (input.payload <= 100 [i32]);

        initialize
            guarantee initSum: payload_sum == Init_Payload_Sum();
    }*/
}

Compute Guarantees with HasEvent / NoSend

Compute contracts use HasEvent to check if a message is present on an event data port, then NoSend or field-level guarantees to specify output behavior.

Important: Use and (conditional/short-circuit) rather than & (logical) when combining HasEvent with field access. With &, both sides are evaluated — so HasEvent(input) & input.payload > 0 would attempt to access input.payload even when there is no message, causing a verification error. With and, the field access is only evaluated when HasEvent(input) is true.

compute
    // No input → no output
    guarantee No_Input_No_Output:
        (not HasEvent(input)) implies NoSend(output);

    // Critical input → drop (no output)
    guarantee Critical_Dropped:
        (HasEvent(input) and input.security_level == SecurityLevel.Critical)
        implies NoSend(output);

    // Non-critical input → forward unchanged
    guarantee Non_Critical_Forwarded:
        (HasEvent(input) and input.security_level != SecurityLevel.Critical)
        implies (HasEvent(output) and output == input);

    // Restricted payload > 100 → clamp to 100
    guarantee Restricted_Clamped_High:
        (HasEvent(input) and input.security_level == SecurityLevel.Restricted
            and input.payload > 100)
        implies (HasEvent(output)
                 and output.security_level == input.security_level
                 and output.payload == 100);

HasEvent with Array Quantifiers

HasEvent(c_myArrayInt32_EventDataPort) implies
  (0 .. size(c_myArrayInt32_EventDataPort) - 2) -> forAll { in i;
    c_myArrayInt32_EventDataPort#(i)
      <= c_myArrayInt32_EventDataPort#(i + 1) };

Logical Operators

Operator	Meaning
&	Logical AND (evaluates both sides)
and	Conditional AND (short-circuit: skips right side if left is false)
|	Logical OR (evaluates both sides)
or	Conditional OR (short-circuit: skips right side if left is true)
not	Logical NOT
implies	Conditional implication (short-circuit: skips consequent if antecedent is false)

Note: &/| are defined in KerML’s BooleanFunctions as non-conditional (evaluate both sides). and/or/implies are defined in KerML’s ControlFunctions as conditional (second operand is an expr — short-circuit).

Comparison and Arithmetic

Operator	Meaning
==	Equality
!=	Inequality
<, <=, >, >=	Relational
+, -, *, /	Arithmetic

Type-Annotated Literals

-128 [s32]        // signed 32-bit integer literal
134 [s32]         // signed 32-bit integer literal
96 [i32]          // integer 32 literal (alternative)
72 [f32]          // float 32 literal
-459.67 [f32]     // negative float 32 literal
50.0 [f32]        // float 32 literal
1 [s32]           // signed 32 literal
0 [i32]           // integer 32 literal

Boolean Literals

true
false
T     // shorthand for true
F     // shorthand for false

Field Access

// Simple field access
current_tempWstatus.degrees
current_tempWstatus.status
interface_failure.flag

// Nested field access
setPoint.low.degrees
setPoint.high.degrees

// Array element field access
v.fieldArray#(i).fieldSInt32

---

19. GUMBO Quantified Expressions (Arrays)

Array Element Access

// Index-based access with #()
p_myArrayInt32_DataPort#(0)
myArrayInt32_StateVar#(i)
v.fieldArray#(i).fieldSInt32

Array Size

size(p_myArrayInt32_DataPort)
size(v)
size(v.fieldArray)

ForAll (Universal Quantifier)

// All adjacent elements are sorted
(0 .. size(p_myArrayInt32_DataPort) - 2) -> forAll {i;
  p_myArrayInt32_DataPort#(i) <= p_myArrayInt32_DataPort#(i + 1) };

// With `in` keyword (alternative form)
(0 .. size(myArrayInt32_StateVar) - 2) -> forAll { in i;
  myArrayInt32_StateVar#(i) <= myArrayInt32_StateVar#(i + 1) };

// Over struct array fields
(0 .. size(c_myArrayStruct_DataPort) - 2) -> forAll { in i;
  c_myArrayStruct_DataPort#(i).fieldSInt32
    <= c_myArrayStruct_DataPort#(i + 1).fieldSInt32 };

// Over nested array in struct
(0 .. size(c_myStructArray_DataPort.fieldArray) - 2) -> forAll { in i;
  c_myStructArray_DataPort.fieldArray#(i).fieldSInt32
    <= c_myStructArray_DataPort.fieldArray#(i + 1).fieldSInt32 };

Exists (Existential Quantifier)

(0 .. size(c_myArrayInt32_DataPort) - 1) -> exists { in i;
  c_myArrayInt32_DataPort#(i) == 0[i32] };

(0 .. size(v) - 1) -> exists {i; v#(i) == 0[i32] };

Combining In() with Array Quantifiers

// Compare pre-state array with post-state
guarantee isSorted_MyArrayInt32_StateVar_Guarantee:
  (0 .. size(myArrayInt32_StateVar) - 2) -> forAll { in i;
    In(myArrayInt32_StateVar)#(i)
      <= myArrayInt32_StateVar#(i + 1) };

// In() on struct containing array
guarantee:
  (0 .. size(myStructArray_StateVar.fieldArray) - 2) -> forAll { in i;
    In(myStructArray_StateVar).fieldArray#(i).fieldSInt32
      <= myStructArray_StateVar.fieldArray#(i + 1).fieldSInt32 };

// In() passed to function returning array
guarantee:
  (0 .. size(myArrayInt32_FunctionReturn(myArrayInt32_StateVar)) - 2)
    -> forAll { in i;
      myArrayInt32_FunctionReturn(In(myArrayInt32_StateVar))#(i) <=
        myArrayInt32_FunctionReturn(myArrayInt32_StateVar)#(i + 1) };

GUMBO Literal Suffixes

Suffix	Type
[s32]	Signed 32-bit integer
[i32]	Integer 32 (alias)
[f32]	Float 32
[ms]	Milliseconds (for Period, etc.)
[s]	Seconds
[byte]	Bytes (for Data_Size)