Introduction
1.
Build System
1.1.
Project Structure
1.2.
Manifest File Format
1.3.
Module System
1.4.
Dependency Resolution Strategy
2.
Syntax and Semantics
2.1.
Comments
2.1.1.
Line
2.1.2.
Block
2.2.
Identifiers
2.3.
Paths
2.4.
Flow Control Structures
2.4.1.
Block
2.5.
Types
2.5.1.
Primitive
2.5.1.1.
nothing
2.5.1.2.
bool
2.5.1.3.
u8
2.5.1.4.
u16
2.5.1.5.
u32
2.5.1.6.
u64
2.5.1.7.
usize
2.5.1.8.
i8
2.5.1.9.
i16
2.5.1.10.
i32
2.5.1.11.
i64
2.5.1.12.
isize
2.6.
Expressions
2.6.1.
Literal
2.6.1.1.
Boolean
2.6.1.2.
Integer
2.6.2.
Item
2.6.3.
Call
2.6.4.
Syscall
2.6.5.
Block
2.7.
Specifications
2.7.1.
Propositions
2.7.2.
Assumes
2.7.3.
Requires
2.7.4.
Ensures
2.8.
Statements
2.8.1.
Import
2.8.2.
Export
2.8.3.
Function Definition
2.8.4.
Expression
2.8.5.
Block
2.9.
Complete Grammar
2.10.
Name Resolution
2.11.
Type Checking
2.12.
Type Inference
Light (default)
Rust
Coal
Navy
Ayu
The Protocol Verification Language Reference
Ensures
Syntax
<ensures> ::= "ensures" <propositions>
Semantics
They tell the compiler to verify that after the function is called, every
<proposition>
in
<propositions>
is
true
.