mbind operator Wiki

Overview

mbind is an operator used for sequence-test specifications in HOL-TestGen. It is introduced for iterations of input/output stepping functions: given a list of inputs ιs = [i1, ..., in], it feeds the inputs subsequently into the system under test (SUT) and stops when an error occurs. This gives a compact representation of valid test sequences for programs under test.

σ |= os ← mbind ιs SUT; return (P os)

In this form, mbind produces the observed output sequence os, which is then checked by a post-condition P via return.

Monad context

HOL-TestGen uses monads to express sequence test specifications because HOL is described as a purely functional specification formalism without built-in concepts for states and state transitions. The relevant monad is the state-exception monad, modeling partial state-transition functions:

type_synonym (o, σ) MONSE = σ ⇀ (o × σ)

In this setting, programs under test can be viewed as input/output stepping functions of type:

ι ⇒ (o, σ) MONSE

Such a stepping function may fail for a given state and input, or produce an output together with a successor state.

Role in sequence test specifications

mbind is described as HOL-TestGen's standard way to represent sequence test specifications. Instead of writing an explicit chain of monadic steps such as:

σ |= o₁ ← SUT i₁; ...; on ← SUT iₙ; return (P o₁ ... oₙ)

one can write the corresponding iteration over an input list as:

σ |= os ← mbind ιs SUT; return (P os)

This formulation is useful when tests describe sequences of state transitions performed by a processor while executing program instructions.

Use with state-dependent post-conditions

When the post-condition depends explicitly on the underlying state, the cited case study uses assertSE instead of return. assertSE is defined as:

definition assertSE :: (σ ⇒ bool) ⇒ (o, σ) MONSE
where assertSE P = (λσ. if P σ then Some(True, σ) else None)

A representative full-state conformance pattern is:

test_spec pre ιs::instr list ⇒
  (σ0 |= (_ ← mbind ιs execVAMP;
          assertSE (λσ. σ =k SUT σ0 ιs)))

The same source also gives a narrower variant that compares a selected general-purpose register after appending a final load action.

VAMP examples

In the VAMP microprocessor case study, execVAMP is defined as a lifting of exec_instr into the state-exception monad:

definition execVAMP where
  execVAMP ≡ (λ i σ. Some ((), exec_instr σ i))

The load/store test scenario uses mbind over instruction sequences and checks the final state against the SUT model:

σ0 |= (s ← mbind [Isw 0 1 8, Ilbu 1 0 -3, Ilbu 3 2 8] execVAMP;
       assertSE (λσ. σ =k SUT σ0 [Isw 0 1 8, Ilbu 1 0 -3, Ilbu 3 2 8]))

The corresponding assembly sequence shown in the source is:

ISW   0 1  8
LLBU  1 0 -3
LLBU  3 2  8

The arithmetic sequence scenario is analogous, using an instruction list with arithmetic operations:

σ0 |= (s ← mbind [Isub 2 1 0, Iadd 1 5 2, Iadd 1 0 4] execVAMP;
       assertSE (λσ. σ =k SUT σ0 [Isub 2 1 0, Iadd 1 5 2, Iadd 1 0 4]))

Testing significance

The case study uses mbind in generated sequence tests where execution order matters. For load/store sequences, the authors note that such test programs can reveal errors related to read/write sequencing, including byte-alignment errors or information loss due to pipelining, even when each individual operation is implemented correctly.

mbind operator