UCLID5

https://uclid-org.github.io/
Admin
UCLID5 is a software toolkit for formal modeling, specification, verification, and synthesis of...
Tokens:20,996
Snippets:282
Trust Score:9.7
Update:3 months ago
Show doc for...
Tokens:
Raw
### UCLID5 Module for K-Induction Example

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

This snippet demonstrates the setup for k-induction, specifically using `induction(1)` for the initial check. It includes variables and transitions relevant to understanding k-induction's behavior.

```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;
  }
}
```

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

### Check UCLID5 Installation

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

Verify the UCLID5 installation by running the uclid --help command.

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

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

### 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
```

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

### Example Procedure Call

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

Shows a concrete example of calling the 'exec_cmd' procedure and storing its return value in 'result''.

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

```

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

### 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;
```

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

### Module Concatenation Example

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

Demonstrates how module concatenation combines definitions from multiple files with the same module name into a single module.

```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;
    }
}
```

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

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

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

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

### UCLID5 Model Structure Example

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

Illustrates a typical UCLID5 model file structure with multiple modules and control blocks.

```plaintext
__
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;
    }
}


```

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

### UCLID5 Module with 2-Induction for Proof Success

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

This snippet shows the updated control block for the k-induction example, changing `induction(1)` to `induction(2)`. This modification is necessary to make the proof pass, illustrating the effect of increasing the induction depth.

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

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

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

### 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
}
```

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

### 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();
```

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

### Sequential Assignment Example

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

Illustrates how sequential assignments behave like typical imperative assignments. Variable values are updated one after another.

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

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

### Parallel Assignment Example

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

Demonstrates parallel assignments where expressions are evaluated based on the values at the beginning of the step, and updates occur simultaneously.

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

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

### Fibonacci Example with Bounded Model Checking

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

Demonstrates bounded model checking for LTL properties using the 'bmc' command. The 'bmc' command unrolls the system for a specified number of steps and checks for property violations.

```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;
    }
}
```

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

### UCLID5 Verification Output

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

Example output from the UCLID5 verification process, indicating successful instantiation and assertion passing.

```text
% 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.


```

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

### 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;
    }
}
```

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

### Example Synthesis Function Declaration

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

An example of a synthesis function declaration in UCLID5, modeling the mapping of an instruction to an opcode.

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

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

### 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 Case Statement Example

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

Illustrates the use of case statements in UCLID5, similar to C++ switch statements. Expressions are evaluated in order, and the first true expression's block is executed. A 'default' keyword can act 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 Module with Synthesis Function for Invariant Strengthening

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

This example demonstrates integrating a synthesis function 'h' into a UCLID5 module to strengthen an invariant 'hole'. The system describes Fibonacci sequence generation, and the synthesis function aims to find a boolean condition based on 'a' and 'b' that holds true.

```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 ;
  }
}
```

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

### 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();
    }
}
```

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

### ALU Model Excerpt with Input/Output and Variable Declarations

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

This excerpt demonstrates 'input' and 'output' declarations alongside internal 'var' declarations within a Uclid5 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
}
```

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

### UCLID5 Command-Line Options Summary

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

Lists the available command-line flags for UCLID5, such as module selection, solver configuration, and output formatting.

```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)


```

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

### UCLID5 Usage Help Output

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

This is the expected output when running `uclid --help`, detailing available command-line options.

```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.


```

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

### 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 Determinism using Module Instantiation

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

Creates a main module to verify the determinism of module 'A'. It instantiates two copies of 'A', specifies a hyperproperty for determinism, and uses 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;
    }
}

```

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

### UCLID5 Module for Fibonacci Sequence with 1-Induction

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

This snippet demonstrates the basic usage of the induction command for verifying the Fibonacci sequence. It checks if the invariants hold for the initial state and if they are preserved by the transition.

```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;
  }
}
```

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

### 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 Typedef Examples: message_t and regfile_t

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

Demonstrates the definition of a record type 'message_t' and an array type 'regfile_t' using named typedefs. 'message_t' has a boolean 'valid' flag and a 32-bit 'payload'. 'regfile_t' is an array indexed by 4-bit values storing 32-bit elements.

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

type regfile_t = bv32[bv4];
```

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

### 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
```

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

### 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/
```

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

### Define a Transition System Module

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

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

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

    init {
        x = 0;
    }

    next {
        x' = x + a;
    }
}

```

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

### 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
}
```

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

### 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 overall model.

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

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

### 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
```

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

### Command to Run Verification

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

Command to execute the UCLID5 verification process for the defined modules.

```bash
uclid a.ucl a_determinism.ucl

```

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

### Declare Input and Output Variables in Uclid5

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

Variables can be marked as 'input' or 'output' to indicate external connectivity. The 'var' keyword is not used for these declarations.

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

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

### Procedure Call Syntax

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

Demonstrates the syntax for calling a procedure in Uclid. The return values are assigned to specified variables.

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

```

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

### 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; }
    }
```

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

### Verifying Determinism of isGreaterThanOrEqual Procedure

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

This snippet demonstrates how to verify the determinism of a procedural function using UCLID5's verification constructs. It includes the procedure definition and the control block for verification.

```uclid
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;
    }
}
```

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

### 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 Dependencies

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

List module files in the order of their dependencies when invoking the UCLID5 tool. This ensures correct compilation.

```Shell
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
```

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

### 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>;
```

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

### Command to Verify Module with Hyperinvariant

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

Command to run bounded model checking for a module containing a hyperinvariant, specifying the module to execute.

```bash
uclid -m A a_hyperinvariant.ucl

```

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

### Basic Procedure Definition

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

Illustrates a basic procedure definition with a modifies clause. Procedures take arguments and return named values.

```uclid
module main {
    // global variables such as valid
    // ... other stuff

    procedure exec_cmd() returns (r : result_t)
        modifies regs;
    {
        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; }
    }

    // ... other stuff 
}

```

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

### 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"
```

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

### Instance Procedure Call

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

Call a procedure from an instance of another module. This executes the procedure as if its variables were defined within the calling module.

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

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

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

### Sequential Assignment Syntax

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

Defines the basic syntax for sequential assignments in UCLID5. These are executed in order.

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

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

### Run UCLID5 on a Model File

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

Invoke UCLID5 on a model file, such as `ex1.1-fib-model.ucl`, to execute its control blocks.

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

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

### 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; }
```

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

### Fixed-Range For Loop

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

Illustrates the syntax for a for loop in UCLID5, which requires numeric literals for its range. The loop iterates inclusively between the specified bounds.

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

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

### UCLID5 Control Block for Verification Actions

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

Illustrates the 'control' block in UCLID5, used in the top-level 'main' module for verification scripts. It contains actions like unrolling the transition system, checking properties, and printing results.

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

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

### 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;
        }
    }
```

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

### Parallel Assignment Syntax

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

Introduces the syntax for parallel assignments using a prime symbol. These assignments are evaluated and updated simultaneously.

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

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

### UCLID5 Synthesis Function Declaration Syntax

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

This shows the basic syntax for declaring a synthesis function in UCLID5, which is used for Syntax-Guided Synthesis.

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

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

### 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];
```

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

### UCLID5 Model Execution Output

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

This is the expected output after successfully running UCLID5 on a model file, indicating parsing, assertion status, and execution completion.

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


```

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

### Determinism Hyperproperty Syntax

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

This snippet highlights the specific syntax used to express the determinism hyperproperty for a procedure in UCLID5. It shows how to reference variables from different traces using the '.i' operator.

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

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

### 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;
    }
}
```

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

### Procedure with Requires and Ensures

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

Extends a procedure definition with requires and ensures clauses for pre- and post-conditions. These are optional but aid in 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; }
    }

```

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

### UCLID5 Module with Additional Invariant for Fibonacci

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

This snippet shows how to add an invariant (`a_ge_0`) to the Fibonacci module to ensure the induction check passes. This is a common pattern to strengthen the invariants for successful verification.

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

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

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

### Constant Declaration in Uclid5

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

Illustrates the declaration of a constant in Uclid5. Constants hold symbolic values that do not change during computation and can be controlled using assumptions.

```Uclid5
const flag : boolean;
```

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

### 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;
```

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

### 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>;
```

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

### 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;
}
```

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

### Declare a Variable in Uclid5

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

Variables are declared using the 'var' keyword followed by the variable name and its type.

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

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

### Embedded Assumptions in Uclid5

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

Demonstrates the use of embedded assumptions within a procedure. These assumptions are evaluated 'instantaneously' at their location, unlike module-level assumptions which hold for the entire execution.

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

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

### Importing Type Definitions

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

Import type definitions from a 'common' module into another module. This allows leveraging shared type declarations.

```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
}
```
Tokens:
Raw