HAMR Rust Thread Component Development - Implementation

When HAMR generates code for a thread component (which must live inside of a process component corresponding to an seL4 partition), the following types of infrastructure code are generated:

• infrastructure kernel configuration (e.g., Microkit) information for the partition,
• infrastructure code for interacting interacting with seL4/Microkit partition features including moving information in and out of the partition and hooking up to the system scheduling infrastructure,
• infrastructure code for bridging the seL4/Microkit-level abstractions to AADL-based application code level APIs for moving information in and out of ports and for invoking application methods that serve as “entry points” for the infrastructure to interact with application code.

All the above is hidden behind the scenes. While the seL4 kernel configuration information is a system-level artifact, all of the infrastructure above is organized into a single Rust crate for the thread/process. The developer should generally be aware of how the code above works and how the crate is organized, but day-to-day workflows will not interact with the above code directly.

The developer’s focus will be on implementing, testing, and verifying application code for a thread. The root of the application code (organized into standard entrypoints) is localized into a single file within the crate

• the src/component/(crate_name)_app.rs file.

The entry point implementations in this file may call to other application code files that the developer adds, but this follows the path of conventional Rust development and so it is not necessary to explain it here.

To complete the application logic for a thread component, the developer fills in the bodies of the AADL-standard “entry point” methods, while utilizing get and put methods from the auto-generated infrastructure APIs to receive and send values over ports.

HAMR also generates a variety of support files for testing in the src/test folder within the crate. Working with these testing files is the other main focus on the developer’s component implementation workflows – this is addressed in a separate chapter.

Optionally, the developer can use Verus verification tool to check that the application code satisfy Rust/Verus behavior contracts automatically generated from model-level GUMBO contracts.

This chapter focuses on concepts of the src/component/(crate_name)_app.rs application code file and on the primary developer activities involved in implementing the entry point methods to achieve the application logic of the thread component. The chapter covers:

• the structure of the crate generated for the thread,
• the initial application code skeleton produced by HAMR,
• the Verus annotations that appear in the skeleton,
• the auto-generated port API in the crate’s bridge module, and how the developer fills in the bodies of the initialize and timeTriggered entry points.

Once you have implemented the bodies, the HAMR Rust Thread Component Development - Manual Unit Testing chapter explains how to test what you’ve written. A separate chapter on GUMBO contracts will explain the precise meaning of each contract construct shown here; this chapter introduces what the constructs are for.

Example Files

This documentation uses the Simple Isolette system with periodic threads and data ports as a running example – the same example used in the testing documentation. If you want to browse the code, you can download/clone the HAMR tutorials repository and work with the system in the HAMR-SysMLv2-Rust-seL4-P-DP-Example folder.

Two snapshots of the generated code are kept in the tutorial repository:

• microkit-initial/ – the freshly generated project infrastructure and application code skeletons, before the developer has filled in any application code.
• microkit/ – the completed version with developer-supplied application code.

The SysMLv2 declaration of the thermostat thread that HAMR processes to generate the example code is given below. Don’t worry about the contents of the language "GUMBO" block – the GUMBO chapter explains the contract syntax in depth. For now it is enough to see the ports, state variable (lastCmd), and the rough shape of the contracts on the initialize and compute entry points.

  //===============================================================================
  // 
  //  T h e r m o s t a t   Thread  
  // 
  //===============================================================================
  part def Thermostat :> Periodic_Rust_Thread {
    //-- I n t e r f a c e  --
    port current_temp : DataPort { in :>> type : Isolette_Data_Model::Temp; }
    port desired_temp : DataPort { in :>> type : Isolette_Data_Model::Set_Points; }
    port heat_control : DataPort { out :>> type : Isolette_Data_Model::On_Off; }
    
    //-- B e h a v i o r    C o n s t r a i n t s --
    language "GUMBO" /*{
      state
        lastCmd: Isolette_Data_Model::On_Off;
            
      functions
         //  -- desired bounds on temperature values in the thermostat
         def Temp_Lower_Bound(): Base_Types::Integer_32 := 95 [i32];
         def Temp_Upper_Bound(): Base_Types::Integer_32 := 104 [s32];
          
	  //-- == I n t e g r a t i o n     C o n s t r a i n t s	
    integration
      assume ASSM_CT_Range: 
      //-- Literals used in spec below
      Temp_Lower_Bound() <= current_temp.degrees & current_temp.degrees <= Temp_Upper_Bound();


    //--  == I n i t i a l i z e    E n t r y    P o i n t    Behavior Constraints  ==
    initialize
      guarantee  //-- note: anonymous guarantee clause
         initlastCmd: lastCmd == Isolette_Data_Model::On_Off.Off;
      guarantee REQ_THERM_1 "The Heat Control command shall be Off initially.":
         heat_control == Isolette_Data_Model::On_Off.Off;
		
    //--  ====== C o m p u t e    E n t r y    P o i n t   Behavior Constraints =====      
    compute
      // -- we assume that Operator Interface enforces the contraint below on incoming 
      //    set points (desired temperature range)
      assume ASSM_LDT_LE_UDT: desired_temp.lower.degrees <= desired_temp.upper.degrees;
			
      //-- the lastCmd state variable is always equal to the value of the heat_control output port
      guarantee lastCmd "Set lastCmd to value of output Cmd port":
         lastCmd == heat_control;
			
      compute_cases
        case REQ_THERM_2 "If Current Temperature is less than
                        |the Lower Desired Temperature, the Heat Control shall be set to On.":
			
          assume (current_temp.degrees < desired_temp.lower.degrees);
			    guarantee heat_control == Isolette_Data_Model::On_Off.Onn;
			
        case REQ_THERM_3 "If the Current Temperature is greater than
                         |the Upper Desired Temperature, the Heat Control shall be set to Off.":
          assume (current_temp.degrees > desired_temp.upper.degrees);
          guarantee heat_control == Isolette_Data_Model::On_Off.Off;
			
        case REQ_THERM_4 "If the Current Temperature is greater than or equal 
                         |to the Lower Desired Temperature
                         |and less than or equal to the Upper Desired Temperature, the value of
                         |the Heat Control shall not be changed.":
         assume (current_temp.degrees >= desired_temp.lower.degrees
              & current_temp.degrees <= desired_temp.upper.degrees); 
         guarantee heat_control == In(lastCmd);
   }*/
}

Thread Crate Structure

HAMR generates a standalone Rust crate for each AADL thread component. The crate includes both the infrastructure code needed to support thread execution and communication, and the skeletons where the developer inserts application-specific behavior. For the thermostat thread, the initial generated version of the crate (archived for documentation purposes) can be found at hamr/microkit-initial/crates/thermostat_thermostat/. The completed application code lives at hamr/microkit/crates/thermostat_thermostat/.

Note: in normal development, there is a single version/location for the crate e.g., hamr/microkit/crates/thermostat_thermostat/ that is generated initially by HAMR and is then evolved over time, leading to the completed version of the crate. We have only made a archive copy of the initial state of the crate at hamr/microkit-initial/crates/thermostat_thermostat/ for the purpose of supporting this documentation.

Each thread crate is organized into three modules:

• a component module (src/component/), which contains the thread’s initialization and compute method skeletons where the developer provides the component’s behavior; and
• a bridge module (src/bridge/), which exposes developer-facing APIs for reading from and writing to ports, embeds integration contracts, and provides executable forms of the GUMBO contracts for testing and run-time monitoring.
• a test module (src/bridge/), which contains HAMR-generated infrastructure for testing the component, along with the developer’s written tests.

The general layout of files inside the crate is as follows:

crates/thermostat_thermostat/
  Cargo.toml                              # [auto-gen] Crate manifest
  Makefile                                # [auto-gen] Crate-level build/test/verus targets
  src/
    lib.rs                                # [auto-gen] Crate root, extern "C" entry points
    component/
      mod.rs                              # [auto-gen]
      thermostat_thermostat_app.rs        # [EDITABLE] Application logic (entry-point bodies)
    bridge/
      mod.rs                              # [auto-gen]
      thermostat_thermostat_api.rs        # [auto-gen] Port API (Put/Get/Full traits, ghost state)
      extern_c_api.rs                     # [auto-gen] FFI to C/Microkit shared-memory layer
      thermostat_thermostat_GUMBOX.rs     # [auto-gen] Executable GUMBO contracts (used by tests)
    test/                                 # (covered by the Testing documentation)
      ...

In addition to the thread crate, HAMR generates a shared data crate that defines the Rust representations of AADL data types used across the system. Each thread crate depends on this crate to ensure consistent typing.

This chapter focuses on the two implementation-side files: component/thermostat_thermostat_app.rs (which the developer edits) and bridge/thermostat_thermostat_api.rs (auto-generated, but important to understand).

Extra crud

Each GUMBO initialize guarantee clause becomes a Verus ensures line on initialize; each GUMBO compute assume clause becomes a Verus requires line on timeTriggered; and each GUMBO compute guarantee and compute_cases clause becomes a Verus ensures line (or implication) on timeTriggered.

Code Generation with Embedded Contracts

In the component module, HAMR generates a Rust struct representing the thread instance, plus skeleton entry-point methods carrying Verus contracts translated directly from the GUMBO model contracts.

The full initial skeleton for the thermostat thread is shown below. This is exactly what HAMR generates the first time code generation runs (see the unmodified version in the tutorial at microkit-initial/.../thermostat_thermostat_app.rs).

// This file will not be overwritten if codegen is rerun

use data::*;
use crate::bridge::thermostat_thermostat_api::*;
use vstd::prelude::*;

verus! {

  pub struct thermostat_thermostat {
    // BEGIN MARKER STATE VARS
    pub lastCmd: Isolette_Data_Model::On_Off,
    // END MARKER STATE VARS
  }

  impl thermostat_thermostat {
    pub fn new() -> Self
    {
      Self {
        // BEGIN MARKER STATE VAR INIT
        lastCmd: Isolette_Data_Model::On_Off::default(),
        // END MARKER STATE VAR INIT
      }
    }

    pub fn initialize<API: thermostat_thermostat_Put_Api> (
      &mut self,
      api: &mut thermostat_thermostat_Application_Api<API>)
      ensures
        // BEGIN MARKER INITIALIZATION ENSURES
        // guarantee initlastCmd
        self.lastCmd == Isolette_Data_Model::On_Off::Off,
        // guarantee REQ_THERM_1
        //   The Heat Control command shall be Off initially.
        api.heat_control == Isolette_Data_Model::On_Off::Off,
        // END MARKER INITIALIZATION ENSURES
    {
      log_info("initialize entrypoint invoked");
    }

    pub fn timeTriggered<API: thermostat_thermostat_Full_Api> (
      &mut self,
      api: &mut thermostat_thermostat_Application_Api<API>)
      requires
        // BEGIN MARKER TIME TRIGGERED REQUIRES
        // assume ASSM_LDT_LE_UDT
        old(api).desired_temp.lower.degrees <= old(api).desired_temp.upper.degrees,
        // END MARKER TIME TRIGGERED REQUIRES
      ensures
        // BEGIN MARKER TIME TRIGGERED ENSURES
        // guarantee lastCmd
        //   Set lastCmd to value of output Cmd port
        self.lastCmd == api.heat_control,
        // case REQ_THERM_2
        //   If Current Temperature is less than
        //   the Lower Desired Temperature, the Heat Control shall be set to On.
        (old(api).current_temp.degrees < old(api).desired_temp.lower.degrees) ==>
          (api.heat_control == Isolette_Data_Model::On_Off::Onn),
        // case REQ_THERM_3
        //   If the Current Temperature is greater than
        //   the Upper Desired Temperature, the Heat Control shall be set to Off.
        (old(api).current_temp.degrees > old(api).desired_temp.upper.degrees) ==>
          (api.heat_control == Isolette_Data_Model::On_Off::Off),
        // case REQ_THERM_4
        //   If the Current Temperature is greater than or equal 
        //   to the Lower Desired Temperature
        //   and less than or equal to the Upper Desired Temperature, the value of
        //   the Heat Control shall not be changed.
        ((old(api).current_temp.degrees >= old(api).desired_temp.lower.degrees) &&
          (old(api).current_temp.degrees <= old(api).desired_temp.upper.degrees)) ==>
          (api.heat_control == old(self).lastCmd),
        // END MARKER TIME TRIGGERED ENSURES
    {
      log_info("compute entrypoint invoked");
    }

    pub fn notify(
      &mut self,
      channel: microkit_channel)
    {
      // this method is called when the monitor does not handle the passed in channel
      match channel {
        _ => {
          log_warn_channel(channel)
        }
      }
    }
  }

  #[verifier::external_body]
  pub fn log_info(msg: &str)
  {
    log::info!("{0}", msg);
  }

  #[verifier::external_body]
  pub fn log_warn_channel(channel: u32)
  {
    log::warn!("Unexpected channel: {0}", channel);
  }

  // BEGIN MARKER GUMBO METHODS
  pub open spec fn Temp_Lower_Bound() -> i32
  {
    95i32
  }

  pub open spec fn Temp_Upper_Bound() -> i32
  {
    104i32
  }
  // END MARKER GUMBO METHODS

}

We walk through this file top to bottom.

File-level structure and the verus! macro

The header comment // This file will not be overwritten if codegen is rerun tells the developer that this is one of the editable HAMR project files: regenerating code will not clobber developer-supplied application logic. When code generation is re-run (e.g., as GUMBO contracts are updated), HAMR re-weaves only the auto-generated regions derived from the GUMBO information, which are clearly delimited by BEGIN MARKER ... / END MARKER ... comments (more on those below).

The three use lines bring in (1) the model data types from the shared data crate, (2) the auto-generated port API from the sibling bridge module, and (3) the Verus standard library prelude.

Everything else in the file sits inside a verus! { } block (the documentation for the Verus program verifier can be found here. The standard away of write code for Verus to verify is to use a Rust macro verus! { } that holds your Rust code, plus several constructs the macro recognizes:

• requires and ensures – pre-conditions and post-conditions on a method.
• ==> – logical implication, used inside contracts.
• old(x) – the value of x at method entry (used inside ensures to refer to pre-state).
• forall { ... } and exists { ... } – quantified expressions.
• assert(...) – in-body assertions used as proof hints.
• #[verifier::external_body] – attribute that marks a function whose body Verus should not try to verify.
• open spec fn and closed spec fn – specification-only functions used inside contracts.

This chapter explains what each of these is for as it appears. The detailed semantics of how GUMBO contracts translate to Verus – including the reasoning behind every clause shown above – belongs to the Verus verification chapter (TBD).

Component state struct

pub struct thermostat_thermostat {
  // BEGIN MARKER STATE VARS
  pub lastCmd: Isolette_Data_Model::On_Off,
  // END MARKER STATE VARS
}

The struct has one field per GUMBO state declaration in the model. For the thermostat, that is just lastCmd. These fields are persistent across dispatches: their values are preserved between calls to timeTriggered.

The BEGIN MARKER STATE VARS / END MARKER STATE VARS delimiters mark a region whose contents HAMR will rewrite each time code generation runs. If the developer changes the GUMBO state block in the model, HAMR re-generates this region in place by parsing the file to locate the markers, so that the code-level state struct stays in sync with the model without disturbing developer code outside the region.

If the developer wants to add local state that is not part of the GUMBO contract (e.g., counters, caches, or temporary buffers), those fields should go outside the marker region. That state will be ignored by GUMBO and will not appear in any generated contracts.

The new() constructor follows the same pattern:

pub fn new() -> Self
{
  Self {
    // BEGIN MARKER STATE VAR INIT
    lastCmd: Isolette_Data_Model::On_Off::default(),
    // END MARKER STATE VAR INIT
  }
}

Inside the marker region, HAMR provides default initializers for each GUMBO state variable. Developer-added state must be initialized outside the markers.

The initialize entry-point skeleton

pub fn initialize<API: thermostat_thermostat_Put_Api> (
  &mut self,
  api: &mut thermostat_thermostat_Application_Api<API>)
  ensures
    // BEGIN MARKER INITIALIZATION ENSURES
    // guarantee initlastCmd
    self.lastCmd == Isolette_Data_Model::On_Off::Off,
    // guarantee REQ_THERM_1
    //   The Heat Control command shall be Off initially.
    api.heat_control == Isolette_Data_Model::On_Off::Off,
    // END MARKER INITIALIZATION ENSURES
{
  log_info("initialize entrypoint invoked");
}

The signature is generic over an API type that must implement the thermostat_thermostat_Put_Api trait – the “put-only” trait that exposes only output-port methods. The Rust type system thereby enforces AADL’s rule that the initialize entry point may not read input ports. The api parameter is an Application_Api wrapper around that put-only API; Application_Api is defined in the bridge module and is described in the Thread API: Port Access section below.

The ensures clause holds the post-conditions that the body must establish. HAMR places each post-condition in the BEGIN MARKER INITIALIZATION ENSURES region, with a comment naming the originating GUMBO clause. Here:

• // guarantee initlastCmd traces to the GUMBO guarantee initlastCmd: lastCmd == Isolette_Data_Model::On_Off.Off.
• // guarantee REQ_THERM_1 traces to the GUMBO guarantee REQ_THERM_1, with the requirement’s natural-language description copied into the code.

The body skeleton contains only a log_info(...) call. The developer’s job is to add the assignments and api.put_*() calls that establish the post-conditions. For Thermostat we write self.lastCmd = On_Off::Off; and api.put_heat_control(On_Off::Off); – one developer-supplied line per ensures line. We work through this in the Coding Application Logic section below.

One important convention carried over from the testing manual: DataPort outputs must be initialized in the initialize entry point. The heat_control output of the Thermostat is a DataPort and must therefore be set; failing to do so produces a runtime exception when downstream readers fire. EventDataPort outputs do not need initialization (an event simply has not occurred yet).

The timeTriggered entry-point skeleton

pub fn timeTriggered<API: thermostat_thermostat_Full_Api> (
  &mut self,
  api: &mut thermostat_thermostat_Application_Api<API>)
  requires
    // BEGIN MARKER TIME TRIGGERED REQUIRES
    // assume ASSM_LDT_LE_UDT
    old(api).desired_temp.lower.degrees <= old(api).desired_temp.upper.degrees,
    // END MARKER TIME TRIGGERED REQUIRES
  ensures
    // BEGIN MARKER TIME TRIGGERED ENSURES
    // guarantee lastCmd
    //   Set lastCmd to value of output Cmd port
    self.lastCmd == api.heat_control,
    // case REQ_THERM_2 ...
    (old(api).current_temp.degrees < old(api).desired_temp.lower.degrees) ==>
      (api.heat_control == Isolette_Data_Model::On_Off::Onn),
    // case REQ_THERM_3 ...
    (old(api).current_temp.degrees > old(api).desired_temp.upper.degrees) ==>
      (api.heat_control == Isolette_Data_Model::On_Off::Off),
    // case REQ_THERM_4 ...
    ((old(api).current_temp.degrees >= old(api).desired_temp.lower.degrees) &&
      (old(api).current_temp.degrees <= old(api).desired_temp.upper.degrees)) ==>
      (api.heat_control == old(self).lastCmd),
    // END MARKER TIME TRIGGERED ENSURES
{
  log_info("compute entrypoint invoked");
}

The signature is generic over Full_Api, which combines Put_Api and Get_Api – so the body of timeTriggered may both read inputs and write outputs.

The contract has two regions:

Requires region. Pre-conditions are translated from GUMBO compute assume clauses. For the Thermostat, the model has one assume:

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

which appears here as old(api).desired_temp.lower.degrees <= old(api).desired_temp.upper.degrees. Pre-conditions on input ports also flow in from upstream integration constraints; the GUMBO chapter explains this in detail.

Ensures region. Post-conditions come from GUMBO compute guarantee clauses (top-level, applying to every dispatch) and from each compute_cases arm. Each compute_cases arm becomes a Verus implication in the ensures block:

• The assume of the case becomes the antecedent (left side of ==>).
• The guarantee of the case becomes the consequent (right side).

Three compute_cases clauses (REQ_THERM_2, REQ_THERM_3, REQ_THERM_4) yield three implications. The general guarantee lastCmd == heat_control appears as a single non-conditional ensures line. As in the initialize region, the GUMBO clause name is placed in a comment on the line above each post-condition for traceability.

A note on old(api) and old(self). Inside an ensures clause, old(x) denotes the value of x at method entry, while x itself denotes the value at method exit. This distinction is essential: a clause like api.heat_control == old(self).lastCmd says “the value of the heat_control output port at method exit equals the value of lastCmd at method entry” – exactly the meaning of GUMBO’s In(lastCmd) operator in the model. The “freeze inputs at dispatch” semantics that motivates this construction is described in the HAMR Modeling Elements and Semantics Concepts chapter.

A note on sporadic threads. The Thermostat is periodic and so has a single timeTriggered method. For a sporadic thread, HAMR generates one event-handler method per dispatching event/event-data port instead, each carrying its own requires/ensures block translated from the corresponding GUMBO handle clause. The structural lessons in this chapter – markers, generic API parameter, the Put_Api/Full_Api distinction – carry over directly.

The notify method

pub fn notify(
  &mut self,
  channel: microkit_channel)
{
  match channel {
    _ => {
      log_warn_channel(channel)
    }
  }
}

notify is invoked when the Microkit monitor receives a channel notification that does not correspond to one of the thread’s known input ports. The default body simply logs a warning. Most components do not need to change this method; if you have advanced needs (e.g., an interrupt-driven device), you can extend the match to handle additional channels.

Logging helpers and #[verifier::external_body]

#[verifier::external_body]
pub fn log_info(msg: &str)
{
  log::info!("{0}", msg);
}

#[verifier::external_body]
pub fn log_warn_channel(channel: u32)
{
  log::warn!("Unexpected channel: {0}", channel);
}

The #[verifier::external_body] attribute tells Verus to skip verification of the function’s body and to trust only its signature and contracts. These logging helpers need it because the log:: macros perform string formatting that Verus cannot reason about. In general, use this attribute sparingly and only at the boundary with code that Verus cannot or should not look inside (logging, low-level FFI, hardware access). Anything you mark external_body is taken on trust by the verifier.

The GUMBO methods region

// BEGIN MARKER GUMBO METHODS
pub open spec fn Temp_Lower_Bound() -> i32
{
  95i32
}

pub open spec fn Temp_Upper_Bound() -> i32
{
  104i32
}
// END MARKER GUMBO METHODS

This region is generated from the GUMBO functions block in the model. Each GUMBO function becomes a Verus open spec fn: a specification function that exists only at verification time, has no runtime representation, and whose body is visible to the verifier (open means “definition is exposed to callers’ proofs”, in contrast to closed). These functions are referenced from elsewhere in the auto-generated contracts – for instance, the bridge module embeds an integration constraint that calls Temp_Lower_Bound() and Temp_Upper_Bound().

As with the state-vars and contract regions, do not edit inside the BEGIN MARKER GUMBO METHODS / END MARKER GUMBO METHODS delimiters. HAMR will rewrite this block on regeneration.

Traceability between model and code contracts

Note that throughout the skeleton, every generated requires/ensures line carries a comment naming its source GUMBO clause – // guarantee initlastCmd, // guarantee REQ_THERM_1, // case REQ_THERM_2, and so on. When a contract is updated in the model, HAMR rewrites these lines (and updates the comments) in place. When the developer is reading the code-level contract, the comments make it easy to point back at the model and at the natural-language requirement that motivated each line.

Coding Application Logic

Given the auto-generated skeleton, the developer codes the application logic. In practice, the body of initialize is short (a few state and output-port assignments) and the body of timeTriggered carries the bulk of the thread’s behavior. The completed file for the Thermostat is at microkit/.../thermostat_thermostat_app.rs.

The completed file adds one developer-supplied use line at the top of the file (outside the marker regions, so it is preserved across regeneration):

use data::Isolette_Data_Model::*; // Add for easier reference of data types

This lets the body refer to On_Off, Set_Points, Temp, etc., without the Isolette_Data_Model:: qualifier.

Filling in initialize

The completed body for initialize is:

{
  log_info("initialize entrypoint invoked");

  self.lastCmd = On_Off::Off;
  // REQ_THERM_1: The Heat Control shall be initially Off
  let currentCmd = On_Off::Off;
  api.put_heat_control(currentCmd) 
}

Two assignments do the work:

• self.lastCmd = On_Off::Off; discharges the // guarantee initlastCmd post-condition.
• api.put_heat_control(currentCmd); discharges the // guarantee REQ_THERM_1 post-condition.

There is a one-to-one correspondence between ensures lines in the contract region and assignments in the body. This is the typical pattern for initialize: read the ensures lines, write the matching assignments, and the verifier discharges the contract.

The currentCmd local variable is just for clarity – you could equivalently write api.put_heat_control(On_Off::Off) directly.

Comment-tagging the requirement being satisfied (// REQ_THERM_1: ...) is a useful convention for traceability between requirements, model contracts, and code.

Filling in timeTriggered

The completed body for timeTriggered is:

{
  log_info("compute entrypoint invoked");

   // -------------- Get values of input ports ------------------
  let desired_temp: Set_Points = api.get_desired_temp(); 
  let currentTemp: Temp = api.get_current_temp();

  //================ compute / control logic ===========================

  // current command defaults to value of last command (REQ-THERM-4)
  let mut currentCmd: On_Off = self.lastCmd;

  if (currentTemp.degrees > desired_temp.upper.degrees) {
     // REQ-THERM-3
     currentCmd = On_Off::Off;
  } else if (currentTemp.degrees < desired_temp.lower.degrees) {
     assert(api.current_temp.degrees < api.desired_temp.lower.degrees);
     // REQ-THERM-2
     //currentCmd = On_Off::Off; // seeded bug/error
     currentCmd = On_Off::Onn;
  }

  // -------------- Set values of output ports ------------------
  api.put_heat_control(currentCmd);
  self.lastCmd = currentCmd        
}

The body follows the AADL read-compute-write structure described in the HAMR Modeling Elements and Semantics Concepts chapter:

1. Read inputs. api.get_desired_temp() and api.get_current_temp() return the current frozen values of the two input DataPorts.
2. Compute. Initialize currentCmd to self.lastCmd so that the REQ-THERM-4 case (current temperature inside the desired range, no change to the command) is satisfied by default. Then update currentCmd in the two boundary cases: above the upper bound (REQ-THERM-3) or below the lower bound (REQ-THERM-2).
3. Write outputs. api.put_heat_control(currentCmd) writes the command, and self.lastCmd = currentCmd updates the persistent state variable so the // guarantee lastCmd post-condition (self.lastCmd == api.heat_control) holds.

There is one Verus-specific line in the body:

assert(api.current_temp.degrees < api.desired_temp.lower.degrees);

This is a Verus assert inside the else if branch. It is not a runtime check in the usual Rust sense – it is a hint to the verifier (Z3 under the hood) that the indicated property holds at this program point. When the verifier needs help discharging the REQ_THERM_2 post-condition, asserting an intermediate fact gives Z3 a stepping stone. Verus assertions are the developer’s main lever when proofs do not go through automatically. Most lines in this body do not need any such hint; only this one branch did.

The line //currentCmd = On_Off::Off; // seeded bug/error is a deliberately commented-out incorrect assignment kept in the source as a teaching aid: uncommenting it (and removing the line below it) introduces a bug that violates REQ_THERM_2, and the verifier will reject the code. The companion testing chapter and a future GUMBO chapter use this seeded bug to demonstrate how Verus and the GUMBOX test harness catch the violation.

Thread API: Port Access

To enable access to a thread’s input and output ports, HAMR generates a developer-facing API in the crate’s bridge module. This API:

• Provides high-level Rust methods for reading from input ports (get_*) and writing to output ports (put_*).
• Acts as a bridge between the developer’s application code and the underlying infrastructure code, which is implemented in C.
• Introduces Verus-specific verification artifacts (ghost state and framing contracts) that allow the body of an entry point to discharge its post-conditions.

The api parameter passed into initialize() and timeTriggered() is an instance of the Application_Api struct defined in this file. The full file is at bridge/thermostat_thermostat_api.rs; the header is the standard // Do not edit this file as it will be overwritten if codegen is rerun.

Trait hierarchy

HAMR generates a small trait hierarchy that distinguishes “can write outputs”, “can read inputs”, and “can do both”:

pub trait thermostat_thermostat_Api {}

pub trait thermostat_thermostat_Put_Api: thermostat_thermostat_Api {
  #[verifier::external_body]
  fn unverified_put_heat_control(
    &mut self,
    value: Isolette_Data_Model::On_Off)
  {
    extern_api::unsafe_put_heat_control(&value);
  }
}

pub trait thermostat_thermostat_Get_Api: thermostat_thermostat_Api {
  #[verifier::external_body]
  fn unverified_get_current_temp(
    &mut self,
    value: &Ghost<Isolette_Data_Model::Temp>) -> (res : Isolette_Data_Model::Temp)
    ensures
      res == value@,
      // assume ASSM_CT_Range
      (crate::component::thermostat_thermostat_app::Temp_Lower_Bound() <= res.degrees) &&
        (res.degrees <= crate::component::thermostat_thermostat_app::Temp_Upper_Bound()),
  {
    return extern_api::unsafe_get_current_temp();
  }

  // ... unverified_get_desired_temp similar ...
}

pub trait thermostat_thermostat_Full_Api:
    thermostat_thermostat_Put_Api + thermostat_thermostat_Get_Api {}

The base trait thermostat_thermostat_Api is just a marker. The Put_Api adds methods for writing each output port; the Get_Api adds methods for reading each input port; and the Full_Api combines both. As we saw in the previous section, initialize is generic over Put_Api (so it cannot read inputs) while timeTriggered is generic over Full_Api (so it can do both). This is how the type system enforces AADL’s rule that the initialize entry point may not read input ports.

The unverified_* methods are marked #[verifier::external_body] and delegate to extern_api::unsafe_* functions defined in extern_c_api.rs – the FFI shim that calls into the C/Microkit shared-memory layer. Verus does not look inside these methods; it trusts their ensures clauses. A developer normally does not call these unverified_* methods directly; instead, the body calls the higher-level get_* / put_* methods on the Application_Api wrapper described next.

Note the interesting ensures clause on unverified_get_current_temp:

// assume ASSM_CT_Range
(crate::component::thermostat_thermostat_app::Temp_Lower_Bound() <= res.degrees) &&
  (res.degrees <= crate::component::thermostat_thermostat_app::Temp_Upper_Bound()),

This is the GUMBO integration assume ASSM_CT_Range clause from the model, compiled into the API. Every time the entry-point body reads current_temp, the verifier learns that the returned value is in the range [Temp_Lower_Bound(), Temp_Upper_Bound()]. This is how integration constraints on input ports are enforced at the code level. The GUMBO chapter covers integration constraints in detail.

Application_Api wrapper and ghost state

The wrapper struct that the entry points actually receive is:

pub struct thermostat_thermostat_Application_Api<API: thermostat_thermostat_Api> {
  pub api: API,

  pub ghost current_temp: Isolette_Data_Model::Temp,
  pub ghost desired_temp: Isolette_Data_Model::Set_Points,
  pub ghost heat_control: Isolette_Data_Model::On_Off
}

The api: API field is the concrete put/get/full API. The other three fields, marked pub ghost, are ghost state: they exist only at verification time and are erased before runtime. They abstract the logical state of each port, so that contracts can refer to “the value of the heat_control output port at this point in the method” by writing api.heat_control – even though at runtime there is no such value sitting in memory. This is what makes a contract clause like

api.heat_control == Isolette_Data_Model::On_Off::Off

meaningful in the ensures of initialize. At verification time, Verus tracks api.heat_control symbolically as it changes through the body.

The Application_Api provides the typed put_* / get_* methods that the developer’s body calls. Here is put_heat_control:

impl<API: thermostat_thermostat_Put_Api> thermostat_thermostat_Application_Api<API> {
  pub fn put_heat_control(
    &mut self,
    value: Isolette_Data_Model::On_Off)
    ensures
      old(self).current_temp == self.current_temp,
      old(self).desired_temp == self.desired_temp,
      self.heat_control == value,
  {
    self.api.unverified_put_heat_control(value);
    self.heat_control = value;
  }
}

The ensures clause says two things:

1. The heat_control ghost field is set to the new value.
2. Every other ghost field is unchanged (old(self).current_temp == self.current_temp, etc.).

The second part is called a framing condition. It tells Verus that calling put_heat_control(X) does not silently mutate any other piece of port state. Without framing, Verus would have to assume the worst – that any call could change any field – and contracts would not go through. With framing, calling api.put_heat_control(On_Off::Off) from inside the initialize body discharges the api.heat_control == On_Off::Off post-condition directly: Verus matches the post-condition of put_heat_control against the post-condition of initialize and concludes the goal.

The get_* methods follow the same pattern. Here is get_current_temp:

impl<API: thermostat_thermostat_Get_Api> thermostat_thermostat_Application_Api<API> {
  pub fn get_current_temp(&mut self) -> (res : Isolette_Data_Model::Temp)
    ensures
      old(self).current_temp == self.current_temp,
      res == self.current_temp,
      old(self).desired_temp == self.desired_temp,
      old(self).heat_control == self.heat_control,
      // assume ASSM_CT_Range
      (crate::component::thermostat_thermostat_app::Temp_Lower_Bound() <= res.degrees) &&
        (res.degrees <= crate::component::thermostat_thermostat_app::Temp_Upper_Bound()),
  {
    self.api.unverified_get_current_temp(&Ghost(self.current_temp))
  }
  // ... get_desired_temp similar ...
}

The ensures says: the returned value res equals the current current_temp ghost field; every ghost field is unchanged across the call; and the integration constraint ASSM_CT_Range continues to hold on the returned value. When the developer’s timeTriggered body writes

let currentTemp: Temp = api.get_current_temp();

Verus binds currentTemp to the returned value and learns that currentTemp.degrees lies between the lower and upper bounds, all in one step.

init_api() and compute_api()

The bridge module also provides constructors that build concrete Application_Api instances for use by the auto-generated extern “C” entry points in lib.rs:

pub const fn init_api() -> thermostat_thermostat_Application_Api<thermostat_thermostat_Initialization_Api> { ... }
pub const fn compute_api() -> thermostat_thermostat_Application_Api<thermostat_thermostat_Compute_Api> { ... }

init_api() returns an Application_Api parameterized over a concrete Initialization_Api type (which implements Put_Api only); compute_api() returns one parameterized over a Compute_Api (which implements Full_Api). These are wired up by lib.rs at start-up and at each dispatch. A developer writing application logic does not normally interact with these constructors.

Why ghost state and framing matter

By maintaining a one-to-one correspondence between ports and ghost variables, and by enforcing clear framing in every put_* / get_* accessor, the API module enables modular and compositional reasoning about thread behavior. Each entry-point body can be verified in isolation: Verus uses only the requires/ensures of the API methods and the requires/ensures of the entry point itself. And when GUMBO integration constraints are present (as ASSM_CT_Range is for the current_temp input port of the Thermostat), they are compiled into the API once and propagated to every reader of the port automatically.

That ends the implementation walk-through. With the entry-point bodies in place, the next step is to test them; that is the subject of the HAMR Rust Thread Component Development - Manual Unit Testing chapter. A separate chapter on GUMBO contracts will explain in depth the precise meaning and translation of every contract construct introduced here.