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
u64
Type
Syntax
<u64-type> ::= "u64"
Semantics
It is
8
bytes in size.
It can contain the numbers between
0
and
2
64
-1 (18446744073709551615)
.