### Check UCLID5 Installation

Source: https://uclid-org.github.io/introduction/installation.html

Verify that UCLID5 is installed correctly by running the --help command.

```bash
> uclid --help
```

--------------------------------

### Install and Configure UCLID5

Source: https://uclid-org.github.io/print.html

Commands to extract the UCLID5 archive, update the system PATH, and verify the installation.

```bash
> unzip uclid-0.9.5.zip
```

```bash
> export PATH=$PATH:$PWD/uclid-0.9.5/bin/
```

```bash
> uclid --help
```

--------------------------------

### K-Induction Verification Example

Source: https://uclid-org.github.io/verification/induction.html

Illustrates a module where 1-induction fails, requiring k-induction for verification.

```uclid
module main {
  var x : integer;
  var y : integer;
  var b : boolean;

  init {
    b = true;
    x = 0;
    assume (y > 0);
  }

  next {
    b' = !b;
    if (b) {
        x' = x + 3;
    } else {
        x' = x - 2;
    }
    y' = y + x;
  }

  invariant x_ge_0: x >= 0;
  invariant y_gt_0: y > 0;

  control {
    v = induction(1);
    check;
    print_results;
  }
}
```

--------------------------------

### Example Synthesis Function Declaration

Source: https://uclid-org.github.io/synthesis/basics.html

This example declares a synthesis function `inst2op` that maps a `word_t` to an `op_t`, modeling instruction-to-opcode mapping.

```plaintext
synthesis function inst2op(i : word_t) : op_t;
```

--------------------------------

### Define an ALU module

Source: https://uclid-org.github.io/language/variables.html

Example illustrating the combination of type definitions, input/output declarations, and internal variable declarations within a module.

```uclid5
module main {

  // typedef cmd_t which is an enum
  type cmd_t = enum { add, sub, mov_imm };
  // typedef result_t which is a record
  type result_t = record { valid : boolean, value : bv8 };

  input  valid  : boolean;
  input  cmd    : cmd_t;
  // the ALU takes two 3-bit input values from another module
  input  r1, r2 : bv3;
  input  immed  : bv8;
  output result : result_t;
  var    regs   : [bv3]bv8;
  var    cnt    : bv8; 
  
  // ... remaining module content
}
```

--------------------------------

### Refinement Checking Example in Uclid

Source: https://uclid-org.github.io/verification/refinement.html

This example demonstrates how to use Uclid for refinement checking, where a 'spec' module simulates a system described by an 'impl' module. This is typically used to verify that one system refines another.

```Uclid
module spec {
  // Specification of the system
}

module impl {
  // Implementation of the system
}

// Refinement check between spec and impl
check refinement spec impl

```

--------------------------------

### Module Concatenation Example

Source: https://uclid-org.github.io/print.html

Demonstrates how two separate module files can be concatenated by the UCLID5 compiler.

```uclid
// Filename: A_x.ucl
module A {
    var x: integer;
    procedure foo()
        modifies x;
    {
        x = x + 1;
    }
}
```

```uclid
// Filename: A_y.ucl
module A {
    var y: integer;
    procedure bar()
        modifies y;
    {
        y = y + 1;
    }
}
```

```uclid
module A {
    var x: integer;
    var y: integer;

    procedure foo()
        modifies x;
    {
        x = x + 1;
    }

    procedure bar()
        modifies y;
    {
        y = y + 1;
    }
}
```

--------------------------------

### Example Uclid Procedure Call

Source: https://uclid-org.github.io/language/procedures.html

Demonstrates calling the 'exec_cmd' procedure and storing its return value in a primed variable.

```uclid
    call (result') = exec_cmd();
```

--------------------------------

### UCLID5 Module Definition Example

Source: https://uclid-org.github.io/tooling.html

Example structure of UCLID5 modules, demonstrating property declarations and control blocks for verification.

```uclid
module A {
    ... 
    property p_a : ...;
    control {
        v = bmc(5);
        check;
        print_results;
    }
}
module B {
    ... 
    property p_b : ...;
    control {
        v = verify(...);
        check;
        print_results;
    }
}
module main {
    instance a : A();
    instance b : B();
    ... 
    property p_main : ...;
    control {
        v = induction;
        check;
        print_results;
    }
}
```

--------------------------------

### Uclid Verification Output

Source: https://uclid-org.github.io/print.html

Example output from running the Uclid verification command, indicating successful instantiation of modules and passing of assertions.

```text
Successfully instantiated 2 module(s).
2 assertions passed.
0 assertions failed.
0 assertions indeterminate.
  PASSED -> v: induction_base [Step #0] property determinism @ a_determinism.ucl, line 9
  PASSED -> v: induction_step [Step #1] property determinism @ a_determinism.ucl, line 9
Finished execution for module: main.

```

--------------------------------

### UCLID5 SyGuS Integration Example

Source: https://uclid-org.github.io/synthesis/basics.html

This UCLID5 module demonstrates SyGuS integration by using a synthesis function `h` to strengthen an invariant `hole`. The `control` block specifies the proof script for induction and checking.

```uclid
module main {
  // Part 1: System Description .
  var a , b : integer;

  init {
    a , b = 0 , 1;
  }
  next {
    a ' , b ' = b , a + b ;
  }

  // Part 2: System Specification .
  invariant a_le_b : a <= b;

  // Part 3: Synthesis Integration
  synthesis function h (x : integer , y : integer ) : boolean ;
  invariant hole : h(a , b ) ;

  // Part 4: Proof Script .
  control {
    induction ;
    check ;
    print_results ;
  }
}
```

--------------------------------

### UCLID5 Common Module Example

Source: https://uclid-org.github.io/print.html

An example of a UCLID5 module named 'common' that defines several type aliases for addresses, words, memory, and operations. This module can be imported into other modules.

```uclid
module common {
  // addresses 8-bit vectors
  type addr_t = bv8;
  type word_t = bv8;
  // 
  type mem_t = [addr_t]word_t;
  // CPU operation.
  type op_t   = enum { op_mov, op_add, op_sub, op_load, op_store };
}

```

--------------------------------

### Instantiate modules in main

Source: https://uclid-org.github.io/language/modules.html

Shows how to create instances of the cpu module and invoke them within the main module.

```UCLID5
module main {
  // ...  
  // Create two instances of the CPU module.
  instance cpu_i_1 : cpu(imem : (imem));
  instance cpu_i_2 : cpu(imem : (imem));

  init {
  	// ...
  }

  next {
  	// ...
  	// Invoke CPU 1 and CPU 2.
  	next (cpu_i_1);
  	next (cpu_i_2);
  }
  // ...
}
```

--------------------------------

### Calling Procedures Across Modules

Source: https://uclid-org.github.io/language/procedures.html

Demonstrates instantiating a module and invoking its procedures using the instance name prefix.

```uclid
module A {
    // ... other stuff
    procedure foo() {
        // ... other stuff
    }
}

module main {
    instance a: A();
    
    procedure bar() {
        call a.foo();
    }
}
```

--------------------------------

### Perform k-induction verification

Source: https://uclid-org.github.io/print.html

Demonstrates 1-induction and 2-induction for verifying state transitions.

```UCLID5
module main {
  var x : integer;
  var y : integer;
  var b : boolean;

  init {
    b = true;
    x = 0;
    assume (y > 0);
  }

  next {
    b' = !b;
    if (b) {
        x' = x + 3;
    } else {
        x' = x - 2;
    }
    y' = y + x;
  }

  invariant x_ge_0: x >= 0;
  invariant y_gt_0: y > 0;

  control {
    v = induction(1);
    check;
    print_results;
  }
}
```

```UCLID5
module main {  
  // ... same as above

  control {
      v = induction(2);
      check;
      print_results;
  }  
}
```

--------------------------------

### UCLID5 Command-Line Options

Source: https://uclid-org.github.io/tooling.html

Lists available command-line options for UCLID5, covering module selection, solver invocation, SyGuS format, and verbosity.

```bash
-m, --main <Module>                 Name of the main module.
-s, --solver <Cmd>                  Command line to invoke external SMT solver binary.
-y, --synthesizer <Cmd>             Command line to invoke SyGuS synthesizer.
-g, --smt-file-generation <value>   File prefix to generate smt files for each assertion.
-X, --exception-stack-trace         Print exception stack trace.
-f, --sygus-format                  (deprecated, enabled by default)
                                    Generate the standard SyGuS format.
-l, --llama-format                  Generates synthesis format for llama.
-e, --enum-to-numeric               Enable conversion from EnumType to NumericType
-M, --mod-set-analysis              Infers modifies set automatically.
-u, --uf-to-array                   Enable conversion from Uninterpreted Functions to Arrays.
-w, --verbosity <value>             Set verbosity level (0-4)
```

--------------------------------

### Verify Procedural Hyperproperties

Source: https://uclid-org.github.io/verification/hyperproperties.html

Demonstrates the verification of a deterministic procedural function using hyperproperty syntax.

```UCLID5
module main {
    procedure isGreaterThanOrEqual(p: integer, q:integer) returns (res: boolean)
    ensures ((res == true) ==> ( p >= q));
    ensures ((res == false) ==> ( p < q));
    ensures ((p.1 == p.2 && q.1 == q.2)  ==> (res.1 == res.2)); //determinism
    {
        res = true;
        if( p < q)
        {
            res = false;
        }
    }

    control {
        v = verify(isGreaterThanOrEqual);
        check;
        print_results;
    }
}
```

--------------------------------

### UCLID5 Command-Line Options

Source: https://uclid-org.github.io/introduction/installation.html

This output lists the available command-line options for the uclid executable, including options for specifying the main module, SMT solver, synthesizer, and output file generation.

```text
uclid 0.9.5
Usage: uclid [options] <file> ...

  -m, --main <Module>      Name of the main module.
  -s, --solver <Cmd>       External SMT solver binary.
  -y, --synthesizer <Cmd>  Command line to invoke SyGuS synthesizer.
  -g, --smt-file-generation <value>
                           File prefix to generate smt files for each assertion.
  -X, --exception-stack-trace
                           Print exception stack trace.
  -f, --sygus-format       Generate the standard SyGuS format.
  -e, --enum-to-numeric    Enable conversion from EnumType to NumericType.
  -u, --uf-to-array        Enable conversion from Uninterpreted Functions to Arrays.
  -t, --test-fixedpoint    Test fixed point
  --help                   prints this usage text
  <file> ...               List of files to analyze.


```

--------------------------------

### Uclid Procedure Call Syntax

Source: https://uclid-org.github.io/language/procedures.html

Illustrates the general syntax for calling a procedure in Uclid, showing how to capture return values.

```uclid
    call (variable to store return value(s)) = <procedure_name> (argument list);
```

--------------------------------

### UCLID5 Command-Line Help Output

Source: https://uclid-org.github.io/print.html

The expected output when running the uclid binary with the --help flag.

```text
uclid 0.9.5
Usage: uclid [options] <file> ...

  -m, --main <Module>      Name of the main module.
  -s, --solver <Cmd>       External SMT solver binary.
  -y, --synthesizer <Cmd>  Command line to invoke SyGuS synthesizer.
  -g, --smt-file-generation <value>
                           File prefix to generate smt files for each assertion.
  -X, --exception-stack-trace
                           Print exception stack trace.
  -f, --sygus-format       Generate the standard SyGuS format.
  -e, --enum-to-numeric    Enable conversion from EnumType to NumericType.
  -u, --uf-to-array        Enable conversion from Uninterpreted Functions to Arrays.
  -t, --test-fixedpoint    Test fixed point
  --help                   prints this usage text
  <file> ...               List of files to analyze.
```

--------------------------------

### Verify Determinism of System A

Source: https://uclid-org.github.io/print.html

Creates a main module to verify the determinism hyperproperty of system 'A'. It instantiates two traces of 'A' and asserts that their 'x' values remain equal if their inputs 'a' are equal. Requires running `uclid a.ucl a_determinism.ucl`.

```ucl
// Filename: a_determinism.ucl
module main {
    var a: integer;

    // Two instances of A
    instance pi1: A(a: (a));
    instance pi2: A(a: (a));

    // Hyperproperty
    invariant determinism: pi1.x == pi2.x;

    // Step both instances by executing them synchronously and havoc the input a
    next {
        havoc a;
        next(pi1); next(pi2);
    }

    // Use inductive model checking to prove the hyperproperty over infinite traces
    control {
        v = induction;
        check;
        print_results;
    }
}

```

--------------------------------

### Invoke UCLID5 from command line

Source: https://uclid-org.github.io/language/modules.html

Commands for specifying the top-level module and handling file dependencies.

```bash
uclid -m <name of top-level module> <files>
```

```bash
uclid common.ucl cpu.ucl main.ucl
```

--------------------------------

### Define Transition System A

Source: https://uclid-org.github.io/print.html

Defines a simple transition system named 'A' with an input 'a' and a state variable 'x'. This serves as the base module for hyperproperty verification.

```ucl
// Filename: a.ucl
module A {
    input a: integer;
    var x: integer;

    init {
        x = 0;
    }

    next {
        x' = x + a;
    }
}

```

--------------------------------

### Execute a UCLID5 Model

Source: https://uclid-org.github.io/print.html

Command to run a specific model file and the expected verification output.

```bash
  >  uclid examples/tutorial/ex1.1-fib-model.ucl
```

```text
Successfully parsed 1 and instantiated 1 module(s).
4 assertions passed.
0 assertions failed.
0 assertions indeterminate.
Finished execution for module: main.
```

--------------------------------

### Add UCLID5 to PATH

Source: https://uclid-org.github.io/introduction/installation.html

Append the UCLID5 binary directory to your system's PATH environment variable.

```bash
> export PATH=$PATH:$PWD/uclid-0.9.5/bin/
```

--------------------------------

### Run UCLID5 on a Model

Source: https://uclid-org.github.io/introduction/installation.html

Execute a UCLID5 model file using the uclid binary. Specify the model file as a command-line argument.

```bash
>  uclid examples/tutorial/ex1.1-fib-model.ucl
```

--------------------------------

### Import types into a module

Source: https://uclid-org.github.io/language/modules.html

Demonstrates importing type definitions from the common module into a cpu module.

```UCLID5
module cpu {
  type addr_t = common.addr_t;
  type mem_t  = common.mem_t;
  type word_t = common.word_t;
  type op_t   = common.op_t;

  // remainder of the cpu module
}
```

--------------------------------

### Initialize Module Variables

Source: https://uclid-org.github.io/language/blocks.html

The `init` block is used to declare and initialize variables for a UCLID5 module. Assignments are sequential.

```uclid
init {
    x = 1; y = 1;
}
```

--------------------------------

### Invoke Alternative SMT Solver with -s Flag

Source: https://uclid-org.github.io/tooling.html

Shows how to use the `-s` option to specify an alternative SMT solver, such as CVC4, instead of the default Z3.

```bash
uclid <file.ucl> -s cvc4
```

--------------------------------

### Fibonacci Sequence Induction Verification

Source: https://uclid-org.github.io/verification/induction.html

Demonstrates the use of the induction command to verify the invariant a <= b in a Fibonacci sequence model.

```uclid
module main {
  var a, b : integer;

  init {
    a = 0; b = 1;
  }
  next {
    a', b' = b, a + b;
  }

  // First inductive invariant
  invariant a_le_b: a <= b;

  control {
    // The induction command.
    induction;
    check;
    print_results;
  }
}
```

--------------------------------

### Verify hyperproperty via module instantiation

Source: https://uclid-org.github.io/verification/hyperproperties.html

Instantiates two traces of module A to prove a determinism hyperproperty using inductive model checking.

```uclid
// Filename: a_determinism.ucl
module main {
    var a: integer;

    // Two instances of A
    instance pi1: A(a: (a));
    instance pi2: A(a: (a));

    // Hyperproperty
    invariant determinism: pi1.x == pi2.x;

    // Step both instances by executing them synchronously and havoc the input a
    next {
        havoc a;
        next(pi1); next(pi2);
    }

    // Use inductive model checking to prove the hyperproperty over infinite traces
    control {
        v = induction;
        check;
        print_results;
    }
}
```

--------------------------------

### Define a transition system module

Source: https://uclid-org.github.io/verification/hyperproperties.html

Defines a basic transition system module A with an input and a state variable.

```uclid
// Filename: a.ucl
module A {
    input a: integer;
    var x: integer;

    init {
        x = 0;
    }

    next {
        x' = x + a;
    }
}
```

--------------------------------

### Sequential vs. Parallel Assignment Behavior

Source: https://uclid-org.github.io/language/statements.html

Illustrates the difference in execution between sequential and parallel assignments, especially when multiple assignments target the same variable.

```UCLID5
x = 1;
x = x + 2;
x = x + 3;
```

```UCLID5
// Error, will not compile.
x' = 1;
x' = x + 2;
x' = x + 3;
```

--------------------------------

### Declare module inputs and outputs

Source: https://uclid-org.github.io/language/variables.html

Mark variables as input or output to allow connection to external modules without using the var keyword.

```uclid5
input my_input_1 : int
output my_output_2 : bv8
```

--------------------------------

### Uclid Procedure with Requires and Ensures

Source: https://uclid-org.github.io/language/procedures.html

Extends the 'exec_cmd' procedure with 'requires' and 'ensures' clauses to specify pre-conditions and post-conditions for verification.

```uclid
    procedure exec_cmd() returns (r : result_t)
        modifies regs;
        requires valid;
        ensures cmd == add => regs = old(regs)[r1 -> old(regs)[r1] + old(regs)[r1]];
        ensures cmd == sub ==> regs == old(regs)[r1 -> old(regs)[r1] - old(regs)[r2]];
        ensures cmd == mov_imm ==> regs == old(regs)[r1 -> immed];
    {
        var r1val, r2val : bv8;
        if (valid) {
          r1val, r2val = regs[r1], regs[r2];
          case
            (cmd == add)     : { regs[r1] = r1val + r2val; }
            (cmd == sub)     : { regs[r1] = r1val - r2val; }
            (cmd == mov_imm) : { regs[r1] = immed; }
          esac
          r.valid, r.value = true, regs[r1];
        } else { r.valid = false; }
    }
```

--------------------------------

### Specify Top-Level Module with -m Flag

Source: https://uclid-org.github.io/tooling.html

Demonstrates how to use the `-m` flag to specify a module other than 'main' as the top-level module for analysis.

```bash
uclid model.ucl -m A
```

--------------------------------

### Fibonacci Sequence Module in UCLID5

Source: https://uclid-org.github.io/introduction/firstlook.html

A basic module demonstrating state variable declaration, initialization, transition relations, invariant specification, and control flow for verification.

```uclid5
module main {
    // Part 1: System description.
    var a, b : integer;
    
    init {
        a = 0;
        b = 1;
    }

    next {
        a’, b’ = b, a + b;
    }

    // Part 2: System specification.
    invariant a_le_b: a <= b;

    // Part 3: Proof script.
    control {
        unroll (3);
        check;
        print_results;
    }
}
```

--------------------------------

### UCLID5 Model Execution Output

Source: https://uclid-org.github.io/introduction/installation.html

This is a sample output indicating successful parsing and execution of a UCLID5 model, showing the number of assertions passed and failed.

```text
Successfully parsed 1 and instantiated 1 module(s).
4 assertions passed.
0 assertions failed.
0 assertions indeterminate.
Finished execution for module: main.


```

--------------------------------

### Specifying Module File Order

Source: https://uclid-org.github.io/print.html

List module files in the order of their dependencies when invoking the UCLID5 tool. This ensures that modules are processed correctly.

```bash
uclid common.ucl cpu.ucl main.ucl
```

--------------------------------

### Implement Case Statements in UCLID5

Source: https://uclid-org.github.io/language/statements.html

Use case statements to execute blocks based on the first matching boolean expression. The 'default' keyword acts as a catch-all.

```UCLID5
__
    case
      (cmd == add)     : { regs[r1] = r1val + r2val; }
      (cmd == sub)     : { regs[r1] = r1val - r2val; }
      (cmd == mov_imm) : { regs[r1] = immed; }
    esac
```

--------------------------------

### Specifying Top-Level Module

Source: https://uclid-org.github.io/print.html

Use the `-m` or `--main` command-line option to specify the top-level module for the UCLID5 tool. This is required if the top-level module is not named `main`.

```bash
uclid -m <name of top-level module> <files>
```

--------------------------------

### Declare a variable

Source: https://uclid-org.github.io/language/variables.html

Use the var keyword to instantiate a variable with a specific type.

```uclid5
    var <variable_name> : <type>;
```

--------------------------------

### Updating to 2-Induction

Source: https://uclid-org.github.io/verification/induction.html

Updates the control block to use 2-induction to successfully verify the module.

```uclid
module main {  
  // ... same as above

  control {
      v = induction(2);
      check;
      print_results;
  }  
}
```

--------------------------------

### Run Uclid Verification Command

Source: https://uclid-org.github.io/print.html

Command to execute the Uclid5 verification process for the defined modules. This command initiates the model checking and assertion verification.

```bash
% uclid a.ucl a_determinism.ucl

```

--------------------------------

### Generate SMT Files with -g Flag

Source: https://uclid-org.github.io/tooling.html

Illustrates the use of the `-g` flag to generate SMT files for each assertion, with a specified filename prefix.

```bash
uclid <file.ucl> -g "debug"
```

--------------------------------

### Execute UCLID5 verification

Source: https://uclid-org.github.io/verification/hyperproperties.html

Command-line execution for verifying the specified UCLID5 modules.

```bash
% uclid a.ucl a_determinism.ucl
Successfully instantiated 2 module(s).
2 assertions passed.
0 assertions failed.
0 assertions indeterminate.
  PASSED -> v: induction_base [Step #0] property determinism @ a_determinism.ucl, line 9
  PASSED -> v: induction_step [Step #1] property determinism @ a_determinism.ucl, line 9
Finished execution for module: main.
```

--------------------------------

### For Loop with Macro Definitions

Source: https://uclid-org.github.io/language/statements.html

Uses macro definitions for loop bounds, allowing for more dynamic or parameterized ranges.

```UCLID5
define begin() : bv3 = 0bv3;
define end() : bv3 = 7bv3;
```

```UCLID5
for (i : bv3) in (begin(), end()) { regs[i] = 1bv8; }
```

--------------------------------

### Traffic Light State and Transition Logic

Source: https://uclid-org.github.io/verification/bmc.html

Core logic defining the traffic light states, timers, and the state transition procedure.

```uclid5
    type light_t = enum { red, yellow, green };
    var step1, step2 : integer;
    var light1, light2 : light_t;

    init {
        light1, step1 = red,   2;
        light2, step2 = green, 1;
    }

    next {
        call (light1', step1') = next_light(light1, step1);
        call (light2', step2') = next_light(light2, step2);
    }

    procedure next_light(light : light_t, step : integer)
        returns (lightP : light_t, stepP: integer)
    {
        if (step == 0) {
            case
            (light == green) : {
                lightP = yellow;
                stepP = step;
            }
            (light == yellow) : {
                lightP = red;
                stepP = 2;
            }
            (light == red) : {
                lightP = green;
                stepP = 1;
            }
            esac
        } else {
            lightP = light;
            stepP = step - 1;
        }
    }
```

--------------------------------

### Define Macro Expression Syntax

Source: https://uclid-org.github.io/language/statements.html

Defines C-like macro expressions with arguments and return types, useful for reusable and readable code.

```UCLID5
define <name> (arg list) : <return types> = <expression>
```

--------------------------------

### Unzip UCLID5 Archive

Source: https://uclid-org.github.io/introduction/installation.html

Use this command to extract the UCLID5 release archive.

```bash
> unzip uclid-0.9.5.zip
```

--------------------------------

### Define modules for concatenation

Source: https://uclid-org.github.io/language/modules.html

Separate files defining the same module name for syntactic concatenation.

```UCLID5
// Filename: A_x.ucl
module A {
    var x: integer;
    procedure foo()
        modifies x;
    {
        x = x + 1;
    }
}
```

```UCLID5
// Filename: A_y.ucl
module A {
    var y: integer;
    procedure bar()
        modifies y;
    {
        y = y + 1;
    }
}
```

--------------------------------

### Perform Bounded Model Checking with bmc

Source: https://uclid-org.github.io/verification/bmc.html

Uses the bmc command to check invariants over a specified number of steps.

```UCLID5
module main {
    var a, b : integer;
    
    init {
        a = 0; b = 1;
    }

    next {
        a’, b’ = b, a + b;
    }

    // This time the invariant will be checked by BMC 
    // 	instead of an inductiveness check.
    invariant a_le_b: a <= b;

    control {
    	// The bmc command
        bmc (3);
        check;
        print_results;
    }
}
```

--------------------------------

### Uclid Noinline Procedure Expansion

Source: https://uclid-org.github.io/language/procedures.html

Shows the expanded code when a procedure is marked with 'noinline', demonstrating havoc, assert, and assume statements.

```uclid
havoc regs;
assert valid;
assume cmd == add => regs = old(regs)[r1 -> old(regs)[r1] + old(regs)[r1]];
assume cmd == sub ==> regs == old(regs)[r1 -> old(regs)[r1] - old(regs)[r2]];
assume cmd == mov_imm ==> regs == old(regs)[r1 -> immed];
```

--------------------------------

### Call a procedure

Source: https://uclid-org.github.io/print.html

Procedures are invoked using the call keyword, which can store return values into variables.

```uclid
    call (variable to store return value(s)) = <procedure_name> (argument list);
```

```uclid
    call (result') = exec_cmd();
```

--------------------------------

### Data-Flow Order in Parallel Assignments

Source: https://uclid-org.github.io/language/statements.html

Demonstrates that parallel assignments are computed in data-flow order, meaning dependencies dictate execution order, not declaration order.

```UCLID5
next {
    x' = x + 1;
    y' = x' + 1;
}
```

```UCLID5
next {
    y' = x' + 1;
    x' = x + 1;
}
```

--------------------------------

### Check Embedded Specifications with unroll

Source: https://uclid-org.github.io/verification/bmc.html

Demonstrates the use of embedded assumptions and assertions within a procedure and the next block.

```UCLID5
module main {
    // System description.
    var a, b : integer;
    const flag : boolean;

    procedure set_init()
        modifies a, b;
    {
        havoc a;
        havoc b;
        // embedded assumptions.
        assume (a <= b);
        assume (a >= 0 && b >= 0);
        assume (flag);
    }

    init {
        call set_init();
    }
    next {
        a', b' = b, a + b;
        if (flag) {
            assert (a' <= b');
        } else {
            assert (false);
        }
    }

    // Proof script.
    control {
        unroll (3);
        check;
        print_results;
    }
}
```

--------------------------------

### Fibonacci Sequence Module in UCLID5

Source: https://uclid-org.github.io/print.html

A simple UCLID5 module that computes the Fibonacci sequence. It includes state variables, initialization, transition logic, an invariant, and a proof script to verify the invariant.

```uclid
module main {
    // Part 1: System description.
    var a, b : integer;
    
    init {
        a = 0;
        b = 1;
    }

    next {
        a’, b’ = b, a + b;
    }

    // Part 2: System specification.
    invariant a_le_b: a <= b;

    // Part 3: Proof script.
    control {
        unroll (3);
        check;
        print_results;
    }
}

```

--------------------------------

### Define Module Transition Relation

Source: https://uclid-org.github.io/language/blocks.html

The `next` block defines the transition relation of a UCLID5 module. It supports parallel assignments, procedure calls for complex logic, and transitions of submodules.

```uclid
next {
    // simple parallel assignments
    x' = 1; y' = 0;

    // use of procedures to handle complex assignments
    call (z') = complex_procedure (x, y);

    // transition submodules
    next (a_submodule);
}
```

--------------------------------

### If-Then-Else Statement Syntax

Source: https://uclid-org.github.io/language/statements.html

Standard conditional branching construct with 'then' and 'else' blocks.

```UCLID5
if (condition_expression) {
    // then statements
  } else { 
    // else statements
  }
```

--------------------------------

### Sequential Assignment in UCLID5

Source: https://uclid-org.github.io/language/statements.html

Used for standard imperative assignments. Ensure correct variable values before and after execution.

```UCLID5
// a sequential assignment
variable = expression;
```

```UCLID5
x = x + 1;
y = x;
```

--------------------------------

### Reference Trace Variables

Source: https://uclid-org.github.io/verification/hyperproperties.html

Syntax for referencing the i-th trace variable within a hyperproperty specification.

```UCLID5
    ensures ((p.1 == p.2 && q.1 == q.2)  ==> (res.1 == res.2)); //determinism
```

--------------------------------

### Declare a Synthesis Function in UCLID5

Source: https://uclid-org.github.io/synthesis/basics.html

Use the `synthesis function` keyword to declare functions that UCLID5 will attempt to synthesize. These functions map input types to an output type.

```plaintext
synthesis function <function_name>(<input_type_list>) : <output_type>;
```

--------------------------------

### Case Statement Syntax in UCLID5

Source: https://uclid-org.github.io/print.html

UCLID5 supports case statements similar to C++ switch statements. Expressions are evaluated in order, and the block for the first true expression is executed. A 'default' case can be used as a catch-all.

```UCLID5
case
  (cmd == add)     : { regs[r1] = r1val + r2val; }
  (cmd == sub)     : { regs[r1] = r1val - r2val; }
  (cmd == mov_imm) : { regs[r1] = immed; }
esac
```

--------------------------------

### UCLID5 Traffic Light State and Transitions

Source: https://uclid-org.github.io/print.html

Defines the state variables, initialization, and transition logic for a single traffic light. This is a reusable component for modeling traffic light behavior.

```uclid
    type light_t = enum { red, yellow, green };
    var step1, step2 : integer;
    var light1, light2 : light_t;

    init {
        light1, step1 = red,   2;
        light2, step2 = green, 1;
    }

    next {
        call (light1', step1') = next_light(light1, step1);
        call (light2', step2') = next_light(light2, step2);
    }

    procedure next_light(light : light_t, step : integer)
        returns (lightP : light_t, stepP: integer)
    {
        if (step == 0) {
            case
            (light == green) : {
                lightP = yellow;
                stepP = step;
            }
            (light == yellow) : {
                lightP = red;
                stepP = 2;
            }
            (light == red) : {
                lightP = green;
                stepP = 1;
            }
            esac
        } else {
            lightP = light;
            stepP = step - 1;
        }
    }

```

--------------------------------

### Control Block for Verification Scripting

Source: https://uclid-org.github.io/language/blocks.html

The `control` block contains verification actions for the top-level module. It includes commands like `unroll`, `check`, and `print_results`.

```uclid
control {
    unroll (3);
    check;
    print_results;
}
```

--------------------------------

### Sequential Assignment in UCLID5

Source: https://uclid-org.github.io/print.html

Perform sequential assignments using the `=` operator. These assignments behave like typical imperative assignments.

```uclid
// a sequential assignment
variable = expression;
```

```uclid
  x = x + 1;
  y = x;
```

--------------------------------

### Uclid Embedded Assumptions

Source: https://uclid-org.github.io/print.html

Shows embedded assumptions within the set_init procedure. These assumptions are evaluated 'instantaneously' at their location, constraining the possible values of variables 'a' and 'b' and the 'flag'.

```euclid
assume (a <= b);
        assume (a >= 0 && b >= 0);
        assume (flag);
```

--------------------------------

### BMC Command Invocation

Source: https://uclid-org.github.io/verification/bmc.html

Command to perform bounded model checking for a specified number of steps.

```uclid5
        v = bmc(10);
```

--------------------------------

### Specify Hyperaxiom and Hyperinvariant

Source: https://uclid-org.github.io/print.html

Defines a 'same_inputs' hyperaxiom and a 'determinism' hyperinvariant within the 'A' module. Hyperaxioms act as assumptions over multiple traces. Supported for BMC only. Requires running `uclid -m A a_hyperaxiom.ucl`.

```ucl
// Filename: a_hyperaxiom.ucl
module A {
    input a: integer;
    var x: integer;

    init {
        x = 0;
    }

    next {
        x' = x + a;
    }

    hyperaxiom[2]     same_inputs: (a.1 == a.2);
    hyperinvariant[2] determinism: (x.1 == x.2);

    control {
        v = bmc(10);
        check;
        print_results;
    }
}

```

--------------------------------

### UCLID5 Type Definition Syntax

Source: https://uclid-org.github.io/print.html

Demonstrates the syntax for defining named types (typedefs) in UCLID5. These can be used for complex types like records and arrays.

```uclid
type <typename> = <typedefinition>;
```

```uclid
type message_t = record { valid : boolean, payload : bv32 };

type regfile_t = bv32[bv4];
```

--------------------------------

### Parallel Assignment in UCLID5

Source: https://uclid-org.github.io/language/statements.html

Assignments marked with a prime (') execute simultaneously. Only one parallel assignment per variable is allowed per block.

```UCLID5
variable' = expression;
```

```UCLID5
x' = x + 1;
y' = x;
```

--------------------------------

### Specify hyperaxiom and hyperinvariant

Source: https://uclid-org.github.io/verification/hyperproperties.html

Uses hyperaxioms to define assumptions over multiple traces alongside hyperinvariants for bounded model checking.

```uclid
// Filename: a_hyperaxiom.ucl
module A {
    input a: integer;
    var x: integer;

    init {
        x = 0;
    }

    next {
        x' = x + a;
    }

    hyperaxiom[2]     same_inputs: (a.1 == a.2);
    hyperinvariant[2] determinism: (x.1 == x.2);

    control {
        v = bmc(10);
        check;
        print_results;
    }
}
```

--------------------------------

### Define UCLID5 modules

Source: https://uclid-org.github.io/print.html

Structure of a UCLID5 file containing multiple modules and control blocks.

```uclid
module A {
    ...
    property p_a : ...;
    control {
        v = bmc(5);
        check;
        print_results;
    }
}
module B {
    ...
    property p_b : ...;
    control {
        v = verify(...);
        check;
        print_results;
    }
}
module main {
    instance a : A();
    instance b : B();
    ...
    property p_main : ...;
    control {
        v = induction;
        check;
        print_results;
    }
}
```

--------------------------------

### Access Array and Record Elements in UCLID5

Source: https://uclid-org.github.io/print.html

Access array elements using `[]` and record fields using `.`. Arrays are 0-indexed.

```uclid
var myarr : [int]bool;
sixthval = myarr[5];

var myrec : record { valid : bool, payload : bv32 };
pyld = myrec.payload;
```

--------------------------------

### Full UCLID5 Traffic Light Model

Source: https://uclid-org.github.io/verification/bmc.html

Complete model definition including state variables, transition logic, LTL properties, and control block for BMC verification.

```uclid5
module main
{
    type light_t = enum { red, yellow, green };
    var step1, step2 : integer;
    var light1, light2 : light_t;

    init {
        light1, step1 = red,   2;
        light2, step2 = green, 1;
    }

    next {
        call (light1', step1') = next_light(light1, step1);
        call (light2', step2') = next_light(light2, step2);
    }

    procedure next_light(light : light_t, step : integer)
        returns (lightP : light_t, stepP: integer)
    {
        if (step == 0) {
            case
            (light == green) : {
                lightP = yellow;
                stepP = step;
            }
            (light == yellow) : {
                lightP = red;
                stepP = 2;
            }
            (light == red) : {
                lightP = green;
                stepP = 1;
            }
            esac
        } else {
            lightP = light;
            stepP = step - 1;
        }
    }

    property[LTL] always_one_red: G(light1 == red || light2 == red);
    // property[LTL] eventually_green:
    //     G(F(light1 == green)) && G(F(light2 == green));

    control {
        v = bmc(10);
        check;
        print_results;
        v.print_cex(light1, step1, light2, step2);
    }
}
```

--------------------------------

### Declare a symbolic constant

Source: https://uclid-org.github.io/language/variables.html

Use the const keyword to declare a constant. The value is not defined at declaration.

```uclid5
    const <const_name> : <type>;
```

--------------------------------

### Declare a Variable in UCLID5

Source: https://uclid-org.github.io/print.html

Use the `var` keyword to declare a variable with a specified type. This is for general-purpose variables within the language.

```uclid
var <variable_name> : <type>;
```

--------------------------------

### UCLID5 BMC Command

Source: https://uclid-org.github.io/print.html

Invokes the Bounded Model Checking (BMC) command with a bound of 10. This command is used to verify LTL properties.

```uclid
        v = bmc(10);

```

--------------------------------

### Result of module concatenation

Source: https://uclid-org.github.io/language/modules.html

The resulting module A after concatenating A_x.ucl and A_y.ucl.

```UCLID5
module A {
    var x: integer;
    var y: integer;

    procedure foo()
        modifies x;
    {
        x = x + 1;
    }

    procedure bar()
        modifies y;
    {
        y = y + 1;
    }
}
```

--------------------------------

### Define a common module for type definitions

Source: https://uclid-org.github.io/language/modules.html

Declares shared datatypes for use across multiple modules.

```UCLID5
// This module declares types that are used in the rest of the model.
module common {
    // addresses are uninterpreted types.
    type addr_t = bv8;
    type word_t = bv8;
    // memory
    type mem_t = [addr_t]word_t;
    // CPU operation.
    type op_t = enum { op_mov, op_add, op_sub, op_load, op_store };
}
```

--------------------------------

### Procedure with Inline Qualifier

Source: https://uclid-org.github.io/print.html

Use the `inline` qualifier to have the UCLID5 compiler replace procedure calls with the procedure's body. This is the default behavior if no qualifier is specified.

```uclid
procedure [inline] exec_cmd() returns (r : result_t)
```

--------------------------------

### For Loop with Numeric Literals

Source: https://uclid-org.github.io/language/statements.html

Iterates over a fixed range specified by numeric literals. The loop iterator must be typed.

```UCLID5
for (i : bv3) in (0bv3, 7bv3) { regs[i] = 1bv8; }
```

--------------------------------

### LTL Property Definitions

Source: https://uclid-org.github.io/verification/bmc.html

Safety and liveness properties defined using LTL operators.

```uclid5
    property[LTL] always_one_red: G(light1 == red || light2 == red);
    // property[LTL] eventually_green:
    //     G(F(light1 == green)) && G(F(light2 == green));
```

--------------------------------

### Specify hyperinvariant within a module

Source: https://uclid-org.github.io/verification/hyperproperties.html

Uses the hyperinvariant syntax for bounded model checking of properties across multiple traces.

```uclid
// Filename: a_hyperinvariant.ucl
module A {
    input a: integer;
    var x: integer;

    init {
        x = 0;
    }

    next {
        x' = x + a;
    }

    hyperinvariant[2] determinism: (a.1 == a.2) ==> (x.1 == x.2);

    control {
        v = bmc(10);
        check;
        print_results;
    }
}
```

--------------------------------

### Fibonacci Sequence with Additional Invariant

Source: https://uclid-org.github.io/verification/induction.html

Shows the addition of the a_ge_0 invariant to satisfy the inductive check requirements.

```uclid
module main {
  // ... same as above 

  invariant a_le_b: a <= b;
  invariant a_ge_0: a >= 0;
  
  // ... same as above
}
```

--------------------------------

### Declare an uninterpreted function

Source: https://uclid-org.github.io/language/variables.html

Define functions that map a tuple of typed arguments to a return type.

```uclid5
    function <function_name>(<input_type_list>) : <output_type>;
```

```uclid5
    function inst2op(i : word_t) : op_t;
```