From a05db7dc559eaeab7986a2e6ddcabc2455e18e42 Mon Sep 17 00:00:00 2001 From: mbaxter Date: Tue, 5 Nov 2024 15:15:34 -0500 Subject: [PATCH] cannon: Migrate MTCannon spec to 64-bit (#447) --- .../experimental/cannon-fault-proof-vm-mt.md | 245 ++++++++++-------- 1 file changed, 144 insertions(+), 101 deletions(-) diff --git a/specs/experimental/cannon-fault-proof-vm-mt.md b/specs/experimental/cannon-fault-proof-vm-mt.md index f5fb2d69c..739cf5cd1 100644 --- a/specs/experimental/cannon-fault-proof-vm-mt.md +++ b/specs/experimental/cannon-fault-proof-vm-mt.md @@ -6,10 +6,13 @@ - [Overview](#overview) - [Definitions](#definitions) + - [Concepts](#concepts) + - [Natural Alignment](#natural-alignment) - [Data types](#data-types) - [Constants](#constants) - [New Features](#new-features) - [Multithreading](#multithreading) + - [64-bit Architecture](#64-bit-architecture) - [Robustness](#robustness) - [Multithreading](#multithreading-1) - [Thread Management](#thread-management) @@ -21,6 +24,8 @@ - [Voluntary Preemption](#voluntary-preemption) - [Forced Preemption](#forced-preemption) - [Stateful Instructions](#stateful-instructions) + - [Load Linked / Store Conditional Word](#load-linked--store-conditional-word) + - [Load Linked / Store Conditional Doubleword](#load-linked--store-conditional-doubleword) - [FPVM State](#fpvm-state) - [State](#state) - [State Hash](#state-hash) @@ -52,7 +57,7 @@ When necessary to distinguish this version from the initial implementation, it can be referred to as Multithreaded Cannon (MTCannon). Similarly, the original Cannon implementation can be referred to as Singlethreaded Cannon (STCannon) where necessary for clarity. -The MTCannon FPVM emulates a minimal uniprocessor Linux-based system running on big-endian 32-bit MIPS32 architecture. +The MTCannon FPVM emulates a minimal uniprocessor Linux-based system running on big-endian 64-bit MIPS64 architecture. A lot of its behaviors are copied from Linux/MIPS with a few tweaks made for fault proofs. For the rest of this doc, we refer to the MTCannon FPVM as simply the FPVM. @@ -65,19 +70,35 @@ Thus, the trace of a program executed by the FPVM is an ordered set of VM states ### Definitions +#### Concepts + +##### Natural Alignment + +A memory address is said to be "naturally aligned" in the context of some data type +if it is a multiple of that data type's byte size. +For example, the address of a 32-bit (4-byte) value is naturally aligned if it is a multiple of 4 (e.g. `0x1000`, `0x1004`). +Similarly, the address of a 64-bit (8-byte) value is naturally aligned if it is a multiple of 8 (e.g. `0x1000`, `0x1008`). + +A non-aligned address can be naturally aligned by dropping the least significant bits of the address: +`aligned = unaligned & ^(byteSize - 1)`. +For example, to align the address `0x1002` targeting a 32-bit value: +`aligned = 0x1002 & ^(0x3) = 0x1000`. + #### Data types - `Boolean` - An 8-bit boolean value equal to 0 (false) or 1 (true). -- `Byte` - An 8-bit value. - `Hash` - A 256-bit fixed-size value produced by the Keccak-256 cryptographic hash function. +- `UInt8` - An 8-bit unsigned integer value. - `UInt64` - A 64-bit unsigned integer value. -- `Word` - A 32-bit value. +- `Word` - A 64-bit value. #### Constants -- `MaxWord` - A `Word` with all bits set to 1: `0xFFFFFFFF`. +- `EBADF` - A Linux error number indicating a bad file descriptor: `0x9`. +- `MaxWord` - A `Word` with all bits set to 1: `0xFFFFFFFFFFFFFFFF`. When interpreted as a signed value, this is equivalent to -1. -- `WordSize` - The number of bytes in a `Word` (4). +- `ProgramBreakAddress` - The fixed memory address for the program break: `Word(0x0000_4000_0000_0000)`. +- `WordSize` - The number of bytes in a `Word` (8). ### New Features @@ -91,6 +112,11 @@ As such, this implementation includes a few new Linux-specific thread-related [s Additionally, the [FPVM state](#fpvm-state) has been modified in order to track the set of active threads and thread-related global state. +#### 64-bit Architecture + +MTCannon emulates a MIPS64 machine whereas STCannon emulates a MIPS32 machine. The transition from MIPS32 to MIPS64 +means the address space goes from 32-bit to 64-bit, greatly expanding addressable memory. + #### Robustness In the initial implementation of Cannon, unrecognized syscalls were treated as @@ -205,43 +231,59 @@ the FPVM preempts the active thread. ## Stateful Instructions +### Load Linked / Store Conditional Word + The Load Linked Word (`ll`) and Store Conditional Word (`sc`) instructions provide the low-level primitives used to implement atomic read-modify-write (RMW) operations. A typical RMW sequence might play out as follows: -- `ll` place a "reservation" on a particular memory address. -- Subsequent instructions take the value at this address and perform some operation on it: - - For example, maybe a counter variable is reserved and incremented. -- `sc` is called and the modified value is stored at the reserved address only if it has not been modified since the -reservation was placed. +- `ll` places a "reservation" targeting a 32-bit value in memory and returns the current value at this location. +- Subsequent instructions take this value and perform some operation on it: + - For example, maybe a counter variable is loaded and then incremented. +- `sc` is called and the modified value overwrites the original value in memory +only if the memory reservation is still intact. -This RMW sequence ensures that if another thread or process modifies a target memory address while -an atomic update is being performed, the atomic update will fail. +This RMW sequence ensures that if another thread or process modifies a reserved value while +an atomic update is being performed, the reservation will be invalidated and the atomic update will fail. -Prior to MTCannon, we could be assured that no intervening process would modify that target memory location because +Prior to MTCannon, we could be assured that no intervening process would modify such a reserved value because STCannon is singlethreaded. With the introduction of multithreading, additional fields need to be stored in the FPVM state to track memory reservations initiated by `ll` operations. When an `ll` instruction is executed: -- `llReservationActive` is set to true. -- `llAddress` is set to the memory address specified by `ll`. +- `llReservationStatus` is set to `1`. +- `llAddress` is set to the virtual memory address specified by `ll`. - `llOwnerThread` is set to the `threadID` of the active thread. Only a single memory reservation can be active at a given time - a new reservation will clear any previous reservation. -When the VM writes any data to memory, these `ll`-related fields are checked and the memory reservation is cleared if -a memory write touches a reserved `llAddress`. +When the VM writes any data to memory, these `ll`-related fields are checked and any existing memory reservation +is cleared if a memory write touches the naturally-aligned `Word` that contains `llAddress`. When an `sc` instruction is executed, the operation will only succeed if: -- There exists an active reservation (`llReservationActive == true`). +- The `llReservationStatus` field is equal to `1`. - The active thread's `threadID` matches `llOwnerThread`. -- The requested address matches `llAddress`. +- The virtual address specified by `sc` matches `llAddress`. + +On success, `sc` stores a value to the specified address after it is naturally aligned, +clears the memory reservation by zeroing out `llReservationStatus`, `llOwnerThread`, and `llAddress` +and returns `1`. -On success, `sc` stores a value at the target memory address, clears the memory reservation and returns `1`. On failure, `sc` returns `0`. +### Load Linked / Store Conditional Doubleword + +With the transition to MIPS64, Load Linked Doubleword (`lld`), and Store Conditional Doubleword (`scd`) instructions +are also now supported. +These instructions are similar to `ll` and `sc`, but they operate on 64-bit rather than 32-bit values. + +The `lld` instruction functions similarly to `ll`, but the `llReservationStatus` is set to `2`. +The `scd` instruction functions similarly to `sc`, but the `llReservationStatus` must be equal to `2` +for the operation to succeed. In other words, an `scd` instruction must be preceded by a matching `lld` instruction +just as the `sc` instruction must be preceded by a matching `ll` instruction if the store operation is to succeed. + ## FPVM State ### State @@ -252,11 +294,16 @@ The FPVM is a state transition function that operates on a state object consisti 1. `preimageKey` - [`Hash`] The value of the last requested pre-image key. 1. `preimageOffset` - [`Word`] The value of the last requested pre-image offset. 1. `heap` - [`Word`] The base address of the most recent memory allocation via mmap. -1. `llReservationActive` - [`Boolean`] Indicates whether a memory reservation, - which is reserved via a Load Linked Word (`ll`) instruction, is active. -1. `llAddress` - [`Word`] The address of the currently active memory reservation if one exists. -1. `llOwnerThread` - [`Word`] The id of the thread that initiated the current memory reservation if one exists. -1. `exitCode` - [`Byte`] The exit code value. +1. `llReservationStatus` - [`UInt8`] The current memory reservation status where: `0` means there is no + reservation, `1` means an `ll`/`sc`-compatible reservation is active, + and `2` means an `lld`/`scd`-compatible reservation is active. + Memory is reserved via Load Linked Word (`ll`) and Load Linked Doubleword (`lld`) instructions. +1. `llAddress` - [`Word`] If a memory reservation is active, the value of + the address specified by the last `ll` or `lld` instruction. + Otherwise, set to `0`. +1. `llOwnerThread` - [`Word`] The id of the thread that initiated the current memory reservation + or `0` if there is no active reservation. +1. `exitCode` - [`UInt8`] The exit code value. 1. `exited` - [`Boolean`] Indicates whether the VM has exited. 1. `step` - [`UInt64`] A step counter. 1. `stepsSinceLastContextSwitch` - [`UInt64`] A step counter that tracks the number of steps executed on the current @@ -272,11 +319,11 @@ The FPVM is a state transition function that operates on a state object consisti For details, see the [β€œThread Stack Hashing” section.](#thread-stack-hashing) 1. `nextThreadID` - [`Word`] The value defining the id to assign to the next thread that is created. -The state is represented by packing the above fields, in order, into a 172-byte buffer. +The state is represented by packing the above fields, in order, into a 196-byte buffer. ### State Hash -The state hash is computed by hashing the 172-byte state buffer with the Keccak256 hash function +The state hash is computed by hashing the 196-byte state buffer with the Keccak256 hash function and then setting the high-order byte to the respective VM status. The VM status can be derived from the state's `exited` and `exitCode` fields. @@ -307,7 +354,7 @@ fn vm_status(exit_code: u8, exited: bool) -> u8 { The state of a single thread is tracked and represented by a thread state object consisting of the following fields: 1. `threadID` - [`Word`] A unique thread identifier. -1. `exitCode` - [`Byte`] The exit code value. +1. `exitCode` - [`UInt8`] The exit code value. 1. `exited` - [`Boolean`] Indicates whether the thread has exited. 1. `futexAddr` - [`Word`] An address set via a futex syscall indicating that this thread is waiting on a value change at this address. @@ -321,11 +368,11 @@ Set to `MaxWord` if no timeout is active. 1. `hi` - [`Word`] The MIPS HI special register. 1. `registers` - 32 general-purpose MIPS registers numbered 0 - 31. Each register contains a `Word` value. -A thread is represented by packing the above fields, in order, into a 166-byte buffer. +A thread is represented by packing the above fields, in order, into a 322-byte buffer. ### Thread Hash -A thread hash is computed by hashing the 166-byte thread state buffer with the Keccak256 hash function. +A thread hash is computed by hashing the 322-byte thread state buffer with the Keccak256 hash function. ### Thread Stack Hashing @@ -350,8 +397,8 @@ value: ## Memory Memory is represented as a binary merkle tree. -The tree has a fixed-depth of 27 levels, with leaf values of 32 bytes each. -This spans the full 32-bit address space, where each leaf contains the memory at that part of the tree. +The tree has a fixed-depth of 59 levels, with leaf values of 32 bytes each. +This spans the full 64-bit address space, where each leaf contains the memory at that part of the tree. The state `memRoot` represents the merkle root of the tree, reflecting the effects of memory writes. As a result of this memory representation, all memory operations are `WordSize`-byte aligned. Memory access doesn't require any privileges. An instruction step can access any memory @@ -364,7 +411,7 @@ Heap pages are bump allocated at the page boundary, per `mmap` syscall. mmap-ing is purely to satisfy program runtimes that need the memory-pointer result of the syscall to locate free memory. The page size is 4096. -The FPVM has a fixed program break at `0x40000000`. However, the FPVM is permitted to extend the +The FPVM has a fixed program break at `ProgramBreakAddress`. However, the FPVM is permitted to extend the heap beyond this limit via mmap syscalls. For simplicity, there are no memory protections against "heap overruns" against other memory segments. Such VM steps are still considered valid state transitions. @@ -400,23 +447,23 @@ If an unsupported syscall is encountered, the VM will raise an exception. ### Supported Syscalls -| \$v0 | system call | \$a0 | \$a1 | \$a2 | \$a3 | Effect | -|------|---------------|-----------------|------------------|--------------|------------------|-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| -| 4090 | mmap | uint32 addr | uint32 len | 🚫 | 🚫 | Allocates a page from the heap. See [heap](#heap) for details. | -| 4045 | brk | 🚫 | 🚫 | 🚫 | 🚫 | Returns a fixed address for the program break at `0x40000000` | -| 4246 | exit_group | uint8 exit_code | 🚫 | 🚫 | 🚫 | Sets the exited and exitCode state fields to `true` and `$a0` respectively. | -| 4003 | read | uint32 fd | char \*buf | uint32 count | 🚫 | Similar behavior as Linux/MIPS with support for unaligned reads. See [I/O](#io) for more details. | -| 4004 | write | uint32 fd | char \*buf | uint32 count | 🚫 | Similar behavior as Linux/MIPS with support for unaligned writes. See [I/O](#io) for more details. | -| 4055 | fcntl | uint32 fd | int32 cmd | 🚫 | 🚫 | Similar behavior as Linux/MIPS. Only the `F_GETFD`(1) and `F_GETFL` (3) cmds are supported. Sets errno to `0x16` for all other commands. | -| 4120 | clone | uint32 flags | uint32 stack_ptr | 🚫 | 🚫 | Creates a new thread based on the currently active thread's state. Supports a `flags` argument equal to `0x00050f00`, other values cause the VM to exit with exit_code `VmStatus.PANIC`. | -| 4001 | exit | uint8 exit_code | 🚫 | 🚫 | 🚫 | Sets the active thread's exited and exitCode state fields to `true` and `$a0` respectively. | -| 4162 | sched_yield | 🚫 | 🚫 | 🚫 | 🚫 | Preempts the active thread and returns 0. | -| 4222 | gettid | 🚫 | 🚫 | 🚫 | 🚫 | Returns the active thread's threadID field. | -| 4238 | futex | uint32 addr | uint32 futex_op | uint32 val | uint32 \*timeout | Supports `futex_op`'s `FUTEX_WAIT_PRIVATE` (128) and `FUTEX_WAKE_PRIVATE` (129). Other operations set errno to `0x16`. | -| 4005 | open | 🚫 | 🚫 | 🚫 | 🚫 | Sets errno to `0x9`. | -| 4166 | nanosleep | 🚫 | 🚫 | 🚫 | 🚫 | Preempts the active thread and returns 0. | -| 4263 | clock_gettime | uint32 clock_id | uint32 addr | 🚫 | 🚫 | Supports `clock_id`'s `REALTIME`(0) and `MONOTONIC`(1). For other `clock_id`'s, sets errno to `0x16`. Calculates a deterministic time value based on the state's `step` field and a constant `HZ` (10,000,000) where `HZ` represents the approximate clock rate (steps / second) of the FPVM:

`seconds = step/HZ`
`nsecs = (step % HZ) * 10^9/HZ`

Seconds are set at memory address `addr` and nsecs are set at `addr + WordSize`. | -| 4020 | getpid | 🚫 | 🚫 | 🚫 | 🚫 | Returns 0. | +| \$v0 | system call | \$a0 | \$a1 | \$a2 | \$a3 | Effect | +|------|---------------|-----------------|------------------|--------------|------------------|----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| +| 5009 | mmap | uint64 addr | uint64 len | 🚫 | 🚫 | Allocates a page from the heap. See [heap](#heap) for details. | +| 5012 | brk | 🚫 | 🚫 | 🚫 | 🚫 | Returns a fixed address for the program break at `ProgramBreakAddress` | +| 5205 | exit_group | uint8 exit_code | 🚫 | 🚫 | 🚫 | Sets the exited and exitCode state fields to `true` and `$a0` respectively. | +| 5000 | read | uint64 fd | char \*buf | uint64 count | 🚫 | Similar behavior as Linux/MIPS with support for unaligned reads. See [I/O](#io) for more details. | +| 5001 | write | uint64 fd | char \*buf | uint64 count | 🚫 | Similar behavior as Linux/MIPS with support for unaligned writes. See [I/O](#io) for more details. | +| 5070 | fcntl | uint64 fd | int64 cmd | 🚫 | 🚫 | Similar behavior as Linux/MIPS. Only the `F_GETFD`(1) and `F_GETFL` (3) cmds are supported. Sets errno to `0x16` for all other commands. | +| 5055 | clone | uint64 flags | uint64 stack_ptr | 🚫 | 🚫 | Creates a new thread based on the currently active thread's state. Supports a `flags` argument equal to `0x00050f00`, other values cause the VM to exit with exit_code `VmStatus.PANIC`. | +| 5058 | exit | uint8 exit_code | 🚫 | 🚫 | 🚫 | Sets the active thread's exited and exitCode state fields to `true` and `$a0` respectively. | +| 5023 | sched_yield | 🚫 | 🚫 | 🚫 | 🚫 | Preempts the active thread and returns 0. | +| 5178 | gettid | 🚫 | 🚫 | 🚫 | 🚫 | Returns the active thread's threadID field. | +| 5194 | futex | uint64 addr | uint64 futex_op | uint64 val | uint64 \*timeout | Supports `futex_op`'s `FUTEX_WAIT_PRIVATE` (128) and `FUTEX_WAKE_PRIVATE` (129). Other operations set errno to `0x16`. | +| 5002 | open | 🚫 | 🚫 | 🚫 | 🚫 | Sets errno to `EBADF`. | +| 5034 | nanosleep | 🚫 | 🚫 | 🚫 | 🚫 | Preempts the active thread and returns 0. | +| 5222 | clock_gettime | uint64 clock_id | uint64 addr | 🚫 | 🚫 | Supports `clock_id`'s `REALTIME`(0) and `MONOTONIC`(1). For other `clock_id`'s, sets errno to `0x16`. Calculates a deterministic time value based on the state's `step` field and a constant `HZ` (10,000,000) where `HZ` represents the approximate clock rate (steps / second) of the FPVM:

`seconds = step/HZ`
`nsecs = (step % HZ) * 10^9/HZ`

Seconds are set at memory address `addr` and nsecs are set at `addr + WordSize`. | +| 5038 | getpid | 🚫 | 🚫 | 🚫 | 🚫 | Returns 0. | ### Noop Syscalls @@ -425,40 +472,37 @@ and errno (`$a3`) registers. | \$v0 | system call | |------|--------------------| -| 4091 | munmap | -| 4240 | sched_get_affinity | -| 4218 | madvise | -| 4195 | rt_sigprocmask | -| 4206 | sigaltstack | -| 4194 | rt_sigaction | -| 4338 | prlimit64 | -| 4006 | close | -| 4200 | pread64 | -| 4106 | stat | -| 4108 | fstat | -| 4215 | fstat64 | -| 4288 | openat | -| 4085 | readlink | -| 4298 | readlinkat | -| 4054 | ioctl | -| 4326 | epoll_create1 | -| 4328 | pipe2 | -| 4249 | epoll_ctl | -| 4313 | epoll_pwait | -| 4353 | getrandom | -| 4122 | uname | -| 4213 | stat64 | -| 4024 | getuid | -| 4047 | getgid | -| 4140 | llseek | -| 4217 | mincore | -| 4266 | tgkill | -| 4076 | getrlimit | -| 4019 | lseek | -| 4104 | setitimer | -| 4257 | timer_create | -| 4258 | timer_settime | -| 4261 | timer_delete | +| 5011 | munmap | +| 5196 | sched_get_affinity | +| 5027 | madvise | +| 5014 | rt_sigprocmask | +| 5129 | sigaltstack | +| 5013 | rt_sigaction | +| 5297 | prlimit64 | +| 5003 | close | +| 5016 | pread64 | +| 5004 | stat | +| 5005 | fstat | +| 5247 | openat | +| 5087 | readlink | +| 5257 | readlinkat | +| 5015 | ioctl | +| 5285 | epoll_create1 | +| 5287 | pipe2 | +| 5208 | epoll_ctl | +| 5272 | epoll_pwait | +| 5313 | getrandom | +| 5061 | uname | +| 5100 | getuid | +| 5102 | getgid | +| 5026 | mincore | +| 5225 | tgkill | +| 5095 | getrlimit | +| 5008 | lseek | +| 5036 | setitimer | +| 5216 | timer_create | +| 5217 | timer_settime | +| 5220 | timer_delete | ## I/O @@ -531,8 +575,7 @@ transition. Nominally, the FPVM must raise an exception in at least the followin - Unsupported syscall. - Pre-image read at an offset larger than the size of the pre-image. - Delay slot contains branch/jump instruction types. -- Invalid thread state: - - The active thread stack is empty. +- Invalid thread state: the active thread stack is empty. VM implementations may raise an exception in other cases that is specific to the implementation. For example, an on-chain FPVM that relies on pre-supplied merkle proofs for memory access may @@ -542,39 +585,39 @@ raise an exception if the supplied merkle proof does not match the pre-state `me ### Compiler Correctness -Cannon is designed to prove the correctness of a particular state transition that emulates a MIPS32 machine. -Cannon does not guarantee that the MIPS32 instructions correctly implement the program that the user intends to prove. -As a result, Cannon's use as a Fault Proof system inherently depends to some extent on the correctness of the compiler -used to generate the MIPS32 instructions over which Cannon operates. +MTCannon is designed to prove the correctness of a particular state transition that emulates a MIPS64 machine. +MTCannon does not guarantee that the MIPS64 instructions correctly implement the program that the user intends to prove. +As a result, MTCannon's use as a Fault Proof system inherently depends to some extent on the correctness of the compiler +used to generate the MIPS64 instructions over which MTCannon operates. To illustrate this concept, suppose that a user intends to prove simple program `input + 1 = output`. Suppose then that the user's compiler for this program contains a bug and errantly generates the MIPS instructions for a -slightly different program `input + 2 = output`. Although Cannon would correctly prove the operation of this compiled program, -the result proven would differ from the user's intent. Cannon proves the MIPS state transition but makes no assertion about +slightly different program `input + 2 = output`. Although MTCannon would correctly prove the operation of this compiled program, +the result proven would differ from the user's intent. MTCannon proves the MIPS state transition but makes no assertion about the correctness of the translation between the user's high-level code and the resulting MIPS program. -As a consequence of the above, it is the responsibility of a program developer to develop tests that demonstrate that Cannon +As a consequence of the above, it is the responsibility of a program developer to develop tests that demonstrate that MTCannon is capable of proving their intended program correctly over a large number of possible inputs. Such tests defend against -bugs in the user's compiler as well as ways in which the compiler may inadvertently break one of Cannon's +bugs in the user's compiler as well as ways in which the compiler may inadvertently break one of MTCannon's [Compiler Assumptions](#compiler-assumptions). Users of Fault Proof systems are strongly encouraged to utilize multiple proof systems and/or compilers to mitigate the impact of errant behavior in any one toolchain. ### Compiler Assumptions -Cannon makes the simplifying assumption that users are utilizing compilers that do not rely on MIPS exception states for -standard program behavior. In other words, Cannon generally assumes that the user's compiler generates spec-compliant +MTCannon makes the simplifying assumption that users are utilizing compilers that do not rely on MIPS exception states for +standard program behavior. In other words, MTCannon generally assumes that the user's compiler generates spec-compliant instructions that would not trigger an exception. Refer to [Exceptions](#exceptions) for a list of conditions that are explicitly handled. -Certain cases that would typically be asserted by a strict implementation of the MIPS32 specification are not handled by -Cannon as follows: +Certain cases that would typically be asserted by a strict implementation of the MIPS64 specification are not handled by +MTCannon as follows: - `add`, `addi`, and `sub` do not trigger an exception on signed integer overflow. - Instruction encoding validation does not trigger an exception for fields that should be zero. - Memory instructions do not trigger an exception when addresses are not naturally aligned. Many compilers, including the Golang compiler, will not generate code that would trigger these conditions under bug-free -operation. Given the inherent reliance on [Compiler Correctness](#compiler-correctness) in applications using Cannon, the -tests and defense mechanisms that must necessarily be employed by Cannon users to protect their particular programs -against compiler bugs should also suffice to surface bugs that would break these compiler assumptions. Stated simply, Cannon +operation. Given the inherent reliance on [Compiler Correctness](#compiler-correctness) in applications using MTCannon, the +tests and defense mechanisms that must necessarily be employed by MTCannon users to protect their particular programs +against compiler bugs should also suffice to surface bugs that would break these compiler assumptions. Stated simply, MTCannon can rely on specific compiler behaviors because users inherently must employ safety nets to guard against compiler bugs.