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
Assumes
Syntax
<assumes> ::= "assumes" <propositions>
Semantics
They hint the compiler to take every
<proposition>
in
<propositions>
as
true
.
They will be used primarily when creating a
C
API.