diff --git a/compiler/jasmin.opam b/compiler/jasmin.opam
index 28767d384..dcdb5109c 100644
--- a/compiler/jasmin.opam
+++ b/compiler/jasmin.opam
@@ -19,7 +19,7 @@ install: [
   [make "install" "PREFIX=%{prefix}%"]
 ]
 depends: [
-  "ocaml" { >= "4.12" & build }
+  "ocaml" { >= "4.14" & build }
   "batteries" {>= "3.5"}
   "cmdliner" {>= "1.1" & build }
   "dune" {>= "3.7"}
diff --git a/docs/source/index.md b/docs/source/index.md
index 84d726872..87c96dff8 100644
--- a/docs/source/index.md
+++ b/docs/source/index.md
@@ -9,6 +9,7 @@
 
 language/syntax/index
 language/semantics/index
+language/annotations/index
 :::
 
 :::{toctree}
diff --git a/docs/source/language/annotations/index.md b/docs/source/language/annotations/index.md
new file mode 100644
index 000000000..c65126eac
--- /dev/null
+++ b/docs/source/language/annotations/index.md
@@ -0,0 +1,292 @@
+# Annotations
+
+Annotations attach metadata to functions, parameters, return types, variables,
+and statements. They are used to control compiler behavior, declare security
+properties, and specify verification contracts.
+
+## Syntax
+
+```
+#[returnaddress = stack]
+fn f(reg u64 x) -> reg u64 { ... }
+
+#[inline] x = g(y);
+```
+
+```
+<annotations> ::= <annotation>*
+
+<annotation> ::= "#[" <annot-entry> ("," <annot-entry>)* "]"
+
+<annot-entry> ::= <label> ("=" <attribute>)?
+
+<label> ::= <ident> | <keyword> | <string>
+
+<attribute> ::= <expr>
+              | <keyword>
+              | <word-type>
+              | "{" <struct-annot> "}"
+
+<struct-annot> ::= <annot-entry> ("," <annot-entry>)*
+```
+
+Multiple annotations can be written in a single bracket pair separated by commas,
+or as separate bracket pairs:
+
+```
+#[returnaddress = stack, stacksize = 128]
+/* is equivalent to */
+#[returnaddress = stack]
+#[stacksize = 128]
+```
+
+## Function annotations
+
+These annotations appear before a function definition and control
+compilation and verification of the function.
+
+### `returnaddress`
+
+```
+#[returnaddress = stack]
+fn f(reg u64 x) -> reg u64 { ... }
+```
+
+Controls where the return address is stored for subroutine (local) functions.
+
+| Value   | Effect |
+|---------|--------|
+| `stack` | Return address is saved on the stack. |
+| `reg`   | Return address is kept in a register. |
+
+Only valid on subroutine functions (not `inline` or `export`).
+
+### `stacksize`
+
+```
+#[stacksize = 64]
+export fn f(reg u64 x) -> reg u64 { ... }
+```
+
+Declares the expected stack frame size (in bytes). The compiler verifies that
+the actual stack frame matches this value. Useful for ensuring that code changes
+do not inadvertently increase stack usage.
+
+### `stackallocsize`
+
+```
+#[stackallocsize = 128]
+export fn f(reg u64 x) -> reg u64 { ... }
+```
+
+Declares the expected total stack allocation size (frame size rounded up to
+alignment, plus extra size). The compiler verifies this after stack allocation.
+
+### `stackalign`
+
+```
+#[stackalign = u256]
+export fn f(reg u64 x) -> reg u64 { ... }
+```
+
+Controls the alignment of the stack frame. The value is a word type indicating
+the alignment boundary (e.g., `u256` for 32-byte alignment).
+
+### `calldepth`
+
+```
+#[calldepth = 3]
+export fn f(reg u64 x) -> reg u64 { ... }
+```
+
+Declares the expected maximum call depth for the function. The compiler verifies
+this after compilation.
+
+### `stackzero`
+
+```
+#[stackzero = loop]
+export fn f(reg u64 x) -> reg u64 { ... }
+```
+
+Enables stack zeroization: the stack frame is zeroed before the function returns.
+Only valid on `export` functions.
+
+| Strategy    | Description |
+|-------------|-------------|
+| `loop`      | Zero the stack using a loop. |
+| `unrolled`  | Zero the stack using unrolled stores. |
+| `loopSCT`   | Zero using a loop that preserves speculative constant-time. |
+
+### `stackzerosize`
+
+```
+#[stackzero = loop, stackzerosize = u64]
+export fn f(reg u64 x) -> reg u64 { ... }
+```
+
+Sets the word size used for stack zeroization stores. Must be used together
+with `stackzero`. The value is a word type (e.g., `u64`, `u128`).
+
+## Security annotations
+
+These annotations are used by the constant-time and speculative constant-time
+checkers to verify information-flow properties.
+
+### `public` / `secret`
+
+```
+fn f(#[public] reg u64 x, #[secret] reg u64 y) -> #[public] reg u64 { ... }
+```
+
+Placed on function parameters and return types to declare their security level.
+The constant-time checker verifies that secret values do not influence
+branch conditions or memory access indices.
+
+### `msf`
+
+```
+fn f(#[msf] reg u64 ms, #[secret] reg u64 x) -> #[msf] reg u64, reg u64 { ... }
+```
+
+Marks a register as carrying the *misspeculation flag* (MSF), used for
+Speculative Load Hardening (SLH). An MSF variable tracks whether execution
+is on the correct speculative path. It is used by the speculative
+constant-time checker.
+
+### `sct`
+
+```
+#[sct = "public * secret -> public"]
+fn f(reg u64 x, reg u64 y) -> reg u64 { ... }
+```
+
+Declares the speculative constant-time type signature of a function as a string.
+The signature uses `*` (or `×`) to separate parameter types and `->` (or `→`)
+before return types. Each type can be:
+
+- `public` -- publicly observable
+- `secret` -- confidential
+- `msf` -- misspeculation flag
+- `transient` -- public normally, secret speculatively
+- `{ normal: <level>, speculative: <level> }` -- explicit per-mode levels
+- `{ ptr: <level>, val: <level> }` -- for pointer parameters with separate
+  pointer and value levels
+
+### `ct`
+
+```
+#[ct = "public * secret -> public"]
+fn f(reg u64 x, reg u64 y) -> reg u64 { ... }
+```
+
+Declares the (sequential) constant-time type signature. Same string format as
+`sct` but without speculative components. Types are `public`, `secret`, or `_`
+(unspecified).
+
+## Safety annotations
+
+### `safety`
+
+```
+#[safety = {
+    args  = { x, y },
+    res   = { r },
+    requires = x + y <u64 0xFFFFFFFFFFFFFFFF,
+    ensures  = r == x + y
+}]
+fn add(reg u64 x, reg u64 y) -> reg u64 {
+    reg u64 r;
+    r = x + y;
+    return r;
+}
+```
+
+Declares a safety contract for a function. The annotation is a struct with
+the following fields:
+
+| Field      | Description |
+|------------|-------------|
+| `args`     | Names for the function's input values (used in `requires`/`ensures`). |
+| `res`      | Names for the function's output values (used in `ensures`). |
+| `requires` | Precondition expression. |
+| `ensures`  | Postcondition expression. |
+
+Safety contracts are used by the [safety checker](../../tools/safety_checker.md).
+
+## Variable annotations
+
+These annotations appear on variable declarations.
+
+### `mmx`
+
+```
+reg u64 #[mmx] t;
+```
+
+Forces the register allocator to place this variable in an MMX register
+(x86-64 only).
+
+### `spill_to_mmx`
+
+```
+reg u64 #[spill_to_mmx] x;
+```
+
+Allows the auto-spiller to use MMX registers for spilling this variable
+(x86-64 only).
+
+### `nospill`
+
+```
+reg u64 #[nospill] x;
+```
+
+Prevents the auto-spiller from spilling this variable.
+
+## Statement annotations
+
+These annotations appear before a statement.
+
+### `inline`
+
+```
+#[inline] x = f(y);
+```
+
+When placed on a function call statement, forces the called function to be
+inlined at this specific call site, regardless of the function's own
+calling convention.
+
+### `align`
+
+```
+#[align] while { ... } (cond) { ... }
+```
+
+When placed on a `while` loop, aligns the loop entry point in the generated
+assembly. This can improve performance for tight loops by ensuring the loop
+body starts at an aligned address.
+
+## Summary table
+
+| Annotation        | Function | Parameter | Return type | Variable | Statement |
+|-------------------|:--------:|:---------:|:-----------:|:--------:|:---------:|
+| `returnaddress`   | yes      |           |             |          |           |
+| `stacksize`       | yes      |           |             |          |           |
+| `stackallocsize`  | yes      |           |             |          |           |
+| `stackalign`      | yes      |           |             |          |           |
+| `calldepth`       | yes      |           |             |          |           |
+| `stackzero`       | yes      |           |             |          |           |
+| `stackzerosize`   | yes      |           |             |          |           |
+| `public`          |          | yes       | yes         |          |           |
+| `secret`          |          | yes       | yes         |          |           |
+| `msf`             |          | yes       | yes         |          |           |
+| `sct`             | yes      |           |             |          |           |
+| `ct`              | yes      |           |             |          |           |
+| `safety`          | yes      |           |             |          |           |
+| `mmx`             |          |           |             | yes      |           |
+| `spill_to_mmx`    |          |           |             | yes      |           |
+| `nospill`         |          |           |             | yes      |           |
+| `inline`          |          |           |             |          | yes       |
+| `align`           |          |           |             |          | yes       |
diff --git a/docs/source/language/syntax/code.md b/docs/source/language/syntax/code.md
index d62f5443c..719f8a181 100644
--- a/docs/source/language/syntax/code.md
+++ b/docs/source/language/syntax/code.md
@@ -1,241 +1,296 @@
-# Code
+# Statements
 
-Jasmin code comprises the following constructs:
+The body of a function is a sequence of statements (instructions).
+Each statement can be preceded by [annotations](../annotations/index.md).
 
 ```
-<code> ::=
-  | <empty>
-  | <instr> <code>
+<block> ::= "{" <instr>* "}"
 
-<instr> ::=
-  | <instr_assign>
-  | <instr_intrinsic>
-  | <instr_assert>
-  | <instr_conditional>
-  | <instr_while>
-  | <instr_for>
-  | <instr_call>
+<instr> ::= <annotations>? <instr-body>
+
+<instr-body> ::= <var-decl>
+               | <assignment>
+               | <intrinsic-call>
+               | <function-call>
+               | <conditional>
+               | <for-loop>
+               | <while-loop>
+               | <assertion>
+               | <array-init>
 ```
 
-## Variable declaration
+## Variable declarations
 
-Variables in Jasmin have both a type (`int`, `bool`, `u8`, `u16`, `u32`, ...)
-and a storage qualifier (`inline`, `reg`, `stack`).
-Variables qualified as `inline` are removed in compile time, for instance the
-counter of a for loop that is unrolled.
-Variables qualified as `reg` must go into architecture registers or flags,
-and those qualified as `stack` must live in the stack.
-In Jasmin there is no variable spilling: the programmer must do it explicitly.
+```
+reg u64 x;
+stack u8[32] buf;
+inline int i;
+reg u64 a b c;         /* multiple variables, same type */
+reg u32 x = 1;         /* declaration with initialization */
+reg u64 a = 2, b = a;  /* sequential initialization */
+```
 
-Syntax for variable declaration is as follows:
 ```
-<var_list> ::=
-  | <var>
-  | <var>, <var_list>
+<var-decl> ::= <storage> <type> <ident> (","? <ident>)* ";"
+             | <storage> <type> <ident> "=" <expr> ("," <ident> "=" <expr>)* ";"
+```
+
+Each variable must have a [storage qualifier and type](types.md).
+
+For plain declarations (without initialization), the separating comma between
+variable names is optional. For declarations with initialization, commas are
+mandatory and all variables must have an initial value.
+
+Initialized variables are declared and assigned in order, so later initializers
+can reference earlier variables from the same declaration:
 
-<var_decl> ::=
-  | <type> <var_list>;
 ```
-For instance,
+reg u32 base = 10, exp = x << base;
 ```
-reg u64 var;
-stack u64[N] arr;
-inline int i, j;
+
+The initial value can be any expression that evaluates to a single value.
+
+## Assignments
+
+```
+x = y + 1;
+x += y;
+x = y if b;
 ```
 
-Note that the separating comma may be omitted.
+```
+<assignment> ::= <lvalues> <assign-op> <expr> ("if" <expr>)? ";"
 
-### Declaration with initialization
+<lvalues> ::= <lvalue> ("," <lvalue>)*
+            | "(" ")"
+            | <implicits> ("," <lvalue> ("," <lvalue>)*)?
 
-Variables may be declared and initialized at once, in which case if several
-variables are declared, they must all be given an initial value, and separating
-commas are mandatory. Variables are declared and initialized in the given order,
-therefore an initialization expression can refer to a variable declared earlier
-in the same declaration list.
+<implicits> ::= "?" "{" <struct-annot> "}"
 
-Some examples are given below.
+<assign-op> ::= "="
+              | "+=" | "-=" | "*=" | "/=" | "%="
+              | "&=" | "|=" | "^="
+              | "<<=" | ">>=" | "<<r=" | ">>r="
+```
 
-~~~
-reg u32 x = 1; // Declares and initializes a variable x
-reg u64 a = 2, b = 0x10, c = 0o07; // Declares and initializes three variables: a, b, and c
-reg u32 base = 10, exp = x << base; // Declares and initilizes two variables: base, and exp.
-~~~
+The basic assignment uses `=`. Compound assignment operators (like `+=`) are
+syntactic sugar: `x += y` is equivalent to `x = x + y`.
 
-The expression representing the initial value of a declared variable is any
-Jasmin expression evaluating to a single value, for instance an immediate value,
-an arithmetic expression, a memory read, a function call, etc.
+Compound operators can carry size and sign annotations, just like the
+corresponding binary operators: `x +=32u y;`, `x >>=s 4;`.
 
+### Conditional assignments
 
-## Assignments
+Appending `if <expr>` makes the assignment conditional:
 
 ```
-<instr_assign> ::=
-  | <lval> = <expr>;
+x = y if b;       /* assigns y to x only if b is true */
+x += z if cond;
 ```
 
-The basic syntax for assignments is the usual equal sign:
+### Implicit flag capture
+
+Intrinsics and some operations produce CPU status flags. These can be captured
+using the `?{ ... }` syntax on the left-hand side:
+
 ```
-x = y + 1;
+?{of=of, cf=cf}, x = #ADD_64(x, y);
+?{}, x = #SUB_64(x, y);     /* ignore all flags */
+?{zf=zf}, x = #XOR_64(x, x);
 ```
-and prefixing the equal sign with a binary operator `x += y;` is simply
-syntactic sugar for `x = x + y;`.
 
-There is an [expression](expressions) on the right-hand side of the expression
-and a [left-value](lvalues) on the left-hand side.
+The braces contain named flag bindings: `flag_name = variable`.
+Use `?{}` to indicate that flags are produced but all are discarded.
+
+### Multiple return values
+
+Functions and intrinsics can return multiple values:
 
-Assignments can be made conditional by adding an `if` clause as a suffix
 ```
-x = y if b;
+q, r = #DIVMOD(x, y);
+a, b, c = swap_and_add(a, b, c);
 ```
-This means that the assignment is only performed if the condition `b` evaluates to `true`.
 
-## Intrinsics
+Use `_` to discard unwanted return values (see [left-values](lvalues.md)).
+
+## Intrinsic calls
 
 ```
-<instr_intrinsic> ::=
-  | <lval>, ..., <lval> = #<ident>(<expr>, ..., <expr>);
+of, cf, x = #ROL_64(y, 4);
+x = #VPAND_256(a, b);
+#VPBROADCAST_4u64(x);
 ```
 
-Intrinsics are architecture-specific instructions.
-The basic syntax is as follows
 ```
-of, cf, x = #ROL(y, 4);
+<intrinsic-call> ::= <lvalues>? "#" <ident> "(" (<expr> ("," <expr>)*)? ")" ";"
 ```
-where to the left of the equals sign is a list of variables and to the right
-the architecture-specific instruction is prefixed by a `#` and used as a
-function name.
 
-The list of available architecture-specific instructions can be seen using
-`$ jasminc -help-intrinsics`.
+Intrinsics invoke architecture-specific instructions directly. The instruction
+name is prefixed with `#`.
 
+The list of available intrinsics depends on the target architecture and can be
+viewed with:
 
-## Assertions
+```
+jasminc -help-intrinsics
+```
+
+### Flag handling
+
+Many intrinsics produce CPU flags as additional outputs. These appear as extra
+left-values before the primary result:
 
 ```
-<instr_assert> ::=
-  | assert("label", <expr_assert>);
+/* x86-64: ROL produces overflow and carry flags */
+of, cf, x = #ROL_64(y, 4);
 
-<expr_assert> ::=
-  | is_var_init(<var>)
-  | is_arr_init(<expr>, <expr>, <expr>)
-  | is_mem_init(<expr>, <expr>)
-  | <expr_assert> && <expr_assert>
-  | <expr>
+/* Capture specific flags by name */
+?{zf = zero_flag}, x = #AND_64(x, mask);
+
+/* Ignore unwanted flags with _ */
+_, _, x = #ADDC_64(x, y, cf);
 ```
 
-Assertions do nothing, provided their argument evaluates properly to `true`.
-They can be used in the [reference
-interpreter](../../tools/reference_interpreter). The compiler erases the
-assertions in an early pass (soon after type-checking): they do not contribute
-to any code in the target assembly program.
+### Architecture examples
 
-The constructions occurring in assertions have the following semantics:
+**x86-64:**
+```
+x = #VMOVDQU_256([ptr]);             /* 256-bit unaligned load */
+a = #VPSHUFB_256(a, pattern);         /* byte shuffle */
+?{cf = cf}, x = #ADD_64(x, y);       /* addition with carry flag */
+```
 
- - `a && b`: checks that both assertions `a` and `b` hold;
- - `is_var_init(x)`: checks that the variable `x` is initialized;
- - `is_arr_init(t, ofs, len)`: checks that all bytes of the array `t` between
-   `ofs` (included) and `ofs + len` (excluded) are initialized;
- - `is_mem_init(p, len)`: checks that all addresses between `p` and `p + len`
-   are initialized.
+**ARMv7-M (ARM Cortex-M4):**
+```
+x = #UXTB(y);                        /* unsigned extend byte */
+x = #REV(y);                         /* byte reverse */
+x = #MUL(x, y);                      /* multiply */
+```
 
-## Conditionals
+**RISC-V:**
+```
+x = #ADD(x, y);
+x = #SLL(x, shift);
+```
+
+## Function calls
+
+```
+z = add_then_shift(x, y, 2);
+do_something(x, y);
+a, b = swap(a, b);
+r = A::helper(x);
+```
+
+```
+<function-call> ::= <lvalues> "=" <var> "(" (<expr> ("," <expr>)*)? ")" ";"
+                  | <var> "(" (<expr> ("," <expr>)*)? ")" ";"
+```
+
+Function calls pass arguments by value and return zero or more values.
+The left-hand side is a comma-separated list of [left-values](lvalues.md)
+matching the function's result types, followed by `=`.
+
+A function with no results can be called without a left-hand side:
+
+```
+store_result(ptr, value);
+```
+
+A call can be forced to inline at a specific site using the
+[`#[inline]` annotation](../annotations/index.md#inline):
 
 ```
-<instr_conditional> ::=
-  | if <expr> { <code> }
-  | if <expr> { <code> } else { <code> }
-  | if <expr> { <code> } else <instr_conditional>  // else-if syntax.
+#[inline] x = f(y);
 ```
 
-Conditionals take an expression and two pieces of code, and execute one piece
-or the other depending on whether the expression evaluates to `true` or
-`false` (conditions cannot be complex expressions).
-The basic syntax for conditionals is as follows
+## Conditionals
+
 ```
-if (x != y) {
+if x != y {
+    x += 1;
+}
+
+if x < y {
     x += 1;
 } else {
     x += 2;
 }
-```
-where the `else` branch can be omitted.
 
-Conditionals can be chained as follows
-```
-if (x < y) {
-    x += 1
-} else if (x == y) {
-    x += 2;
+if x < y {
+    x = 1;
+} else if x == y {
+    x = 2;
 } else {
-    x += 3;
+    x = 3;
 }
 ```
-where again last `else` branch can be omitted.
-This is syntactic sugar for nested conditionals.
 
+```
+<conditional> ::= "if" <expr> <block> ("else" (<block> | <conditional>))?
+```
+
+The `else` branch is optional. Conditionals can be chained with `else if`,
+which is syntactic sugar for nested conditionals.
 
 ## For loops
 
 ```
-<instr_for> ::=
-  | for <ident> = <expr> to <expr> { <code> }
-  | for <ident> = <expr> downto <expr> { <code> }
-```
+for i = 0 to 5 {
+    a[i] = 0;
+}
 
-For loops execute a piece of code some fixed number of times.
-These iterations depend on an `inline int` counter, that takes values in a given
-range.
-The basic syntax for for loops is
-```
-for i = 0 to 13 {
-    x += x;
-    i += 2;
+for i = 4 downto 0 {
+    process(a[i]);
 }
 ```
-where the counter starts taking the value of the first expression, and increases
-until it reaches the second one.
-For example, the loop `for i = 0 to 5 { ... }` executes the code in the body of
-the loop five times, as `i` takes the values 0, 1, 2, 3, and 4 in each iteration
-respectively.
 
-The iteration can be made decreasing as well, as follows
 ```
-for i = 13 downto 0 {
-    x += x;
-    i -= 2;
-}
+<for-loop> ::= "for" <ident> "=" <expr> ("to" | "downto") <expr> <block>
 ```
 
+For loops execute the body a fixed number of times. The loop variable is
+implicitly `inline int` and does not need to be declared.
+
+With `to`, the variable starts at the first bound and increases by 1 each
+iteration, stopping *before* reaching the second bound (half-open range).
+`for i = 0 to 5` runs with `i` = 0, 1, 2, 3, 4.
+
+With `downto`, the variable starts at the first bound and decreases by 1 each
+iteration, stopping *before* reaching the second bound.
+`for i = 4 downto 0` runs with `i` = 4, 3, 2, 1.
+
+Both bounds must be compile-time constant expressions. For loops are always
+fully unrolled by the compiler.
 
 ## While loops
 
-```
-<instr_while> ::=
-  | while ( <expr> ) { <code> }  // Usual while loop.
-  | while { <code> } ( <expr> )  // do-while loop.
-  | while { <code> } ( <expr> ) { <code> }  // Both.
-```
+Jasmin supports three forms of while loops:
+
+### Pre-condition (while)
 
-While loops execute a piece of code until a condition is met.
-The basic syntax for while loops is
 ```
 while (x <= y) {
     y -= 1;
 }
 ```
-where the condition `x <= y` is evaluated before each iteration, and the body
-is executed only if it evaluated to `true`.
 
-Do-while loops first execute the body and only then evaluate the condition, and
-are written as follows
+The condition is evaluated before each iteration. The body executes only if the
+condition is true.
+
+### Post-condition (do-while)
+
 ```
 while {
     y -= 1;
 } (x <= y)
 ```
 
-In Jasmin, we can do both: execute some code before evaluating the condition,
-and also after
+The body executes first, then the condition is evaluated. The body always
+executes at least once.
+
+### Combined (do-while-do)
+
 ```
 while {
     y -= 1;
@@ -244,24 +299,60 @@ while {
 }
 ```
 
+The first block (before the condition) executes, then the condition is evaluated.
+If true, the second block executes and the loop repeats from the first block.
 
-## Function calls
+```
+<while-loop> ::= "while" <block>? "(" <expr> ")" <block>?
+```
+
+At least one block must be present. The loop entry point can be aligned using
+the [`#[align]` annotation](../annotations/index.md#align).
+
+## Assertions
 
 ```
-<instr_call> ::=
-  | <ident>(<expr>, ..., <expr>);
-  | <lval>, ..., <lval> = <ident>(<expr>, ..., <expr>);
+assert("bounds check", i < 10);
+assert("initialized", is_var_init(x));
 ```
 
-The syntax for function calls is as follows
 ```
-z = add_then_shift_left(x, y, 2);
+<assertion> ::= "assert" "(" <string> "," <assert-expr> ")" ";"
+
+<assert-expr> ::= "is_var_init" "(" <var> ")"
+                | "is_arr_init" "(" <expr> "," <expr> "," <expr> ")"
+                | "is_mem_init" "(" <expr> "," <expr> ")"
+                | <assert-expr> "&&" <assert-expr>
+                | <expr>
 ```
-where to the left of the equals sign we have a comma-separated list of
-[left-values](lvalues) corresponding to the return type of the function and the
-parentheses contain the arguments as a comma-separated list of [expression](expressions).
 
-The following is valid syntax for a function that does not return any values:
+Assertions are erased by the compiler in an early pass. They do not contribute
+to the generated assembly. They are meaningful in the
+[reference interpreter](../../tools/reference_interpreter.md) and the
+[safety checker](../../tools/safety_checker.md).
+
+The first argument is a label string identifying the assertion. The second
+argument is the assertion expression, which can use these special forms:
+
+| Form | Description |
+|------|-------------|
+| `is_var_init(x)` | Checks that variable `x` is initialized. |
+| `is_arr_init(t, ofs, len)` | Checks that bytes `ofs` to `ofs+len` of array `t` are initialized. |
+| `is_mem_init(p, len)` | Checks that addresses `p` to `p+len` are initialized. |
+
+Assertion expressions can be combined with `&&`.
+
+## Array initialization
+
+```
+stack u64[10] a;
+ArrayInit(a);
 ```
-do_side_effect_computation(x, y);
+
 ```
+<array-init> ::= "ArrayInit" "(" <var> ")" ";"
+```
+
+`ArrayInit` marks a stack array as initialized without writing specific values.
+This is used to satisfy initialization checks when the array will be fully
+written before being read.
diff --git a/docs/source/language/syntax/expressions.md b/docs/source/language/syntax/expressions.md
index 9b498a727..65ed157d5 100644
--- a/docs/source/language/syntax/expressions.md
+++ b/docs/source/language/syntax/expressions.md
@@ -1,179 +1,397 @@
 # Expressions
+
+Expressions compute values. They appear on the right-hand side of assignments,
+in conditions, loop bounds, and anywhere a value is needed.
+
+```
+<expr> ::= <literal>
+         | <var>
+         | <array-access>
+         | <memory-load>
+         | <pack-expr>
+         | <cast-expr>
+         | <unary-expr>
+         | <binary-expr>
+         | <ternary-expr>
+         | "(" <expr> ")"
+```
+
+## Literals
+
+### Boolean literals
+
+```
+reg bool b;
+b = true;
+b = false;
+```
+
+The two Boolean literals are `true` and `false`.
+
+### Integer literals
+
+```
+reg u64 x;
+x = 42;
+x = 0xFF;
+x = 0b1010;
+x = 0o77;
+x = 1_000_000;
+x = 0xDEAD_BEEF;
+```
+
+Integer literals can be written in decimal, hexadecimal (prefix `0x` or `0X`),
+binary (prefix `0b` or `0B`), or octal (prefix `0o` or `0O`).
+Underscores can be used as digit separators for readability; they are ignored by
+the compiler.
+
+```
+<integer> ::= <decimal>
+            | "0" ("x" | "X") <hex-digits>
+            | "0" ("b" | "B") <bin-digits>
+            | "0" ("o" | "O") <oct-digits>
+```
+
+Digit groups can be separated by underscores: `1_000`, `0xFF_FF`.
+
+### String literals
+
+```
+assert("bounds check", i < 10);
+```
+
+String literals are enclosed in double quotes (`"..."`) and support standard
+escape sequences. They appear in assertions and annotations.
+
+## Variables
+
+```
+x
+A::B::x
+```
+
+```
+<var> ::= <ident> ("::" <ident>)*
+```
+
+A variable is a simple identifier or a namespace-qualified name using `::`.
+See [namespaces](structure.md#namespaces) for details on qualification.
+
+## Array access
+
+For an array `stack u64[10] a;`, the following access forms are available:
+
+### Scaled element access
+
+```
+a[i]          /* i-th element of declared type (u64) */
+a[:u16 i]     /* i-th element, viewed as array of u16 */
+```
+
+The index `i` is in units of the element type. For `a[i]` with a `u64[10]`
+array, index 0 is the first 8-byte element, index 1 is the second, etc.
+
+The `:` prefix before the type is required. The form `a[u16 i]` without `:` is
+deprecated.
+
+### Unscaled (direct byte) element access
+
 ```
-<expr> ::=
-  | <int>  // Integer constant.
-  | <bool>  // Boolean constant.
-  | <string> // String constant.
-  | <var>  // Variable.
-  | [<expr>] // Memory access.
-  | [:<wsize> <expr>] // Memory access.
-  | <var>[<expr>]  // Array access.
-  | <var>[:<wsize> <expr>]  // Array access.
-  | <var>.[<expr>]  // Unscaled array access.
-  | <var>.[:<wsize> <expr>]  // Unscaled array access.
-  | <var>[<expr> : <expr>]  // Subarray.
-  | <var>[:<wsize> <expr> : <expr>]  // Subarray.
-  | <var>.[<expr> : <expr>]  // Unscaled subarray.
-  | <var>.[:<wsize> <expr> : <expr>]  // Unscaled subarray.
-  | <op1> <expr>  // Unary operation.
-  | <expr> <op2> <expr>  // Binary operation.
-  | <expr> ? <expr> : <expr>  // Conditional.
-  | (<int><sign><int>)[<expr>, ..., <expr>] // Packing.
-  | (<expr>)
-```
-
-At source level, Jasmin program contain expressions whose concrete syntax is described below.
-
-Expressions are made of:
-
-  - constants (`true`, `false`,  `42`, `0xabcd`);
-  - packs (`(4u2)[0, 3, 2, 1]`);
-  - string literals (`"Hello World!"`);
-  - variables (`x`);
-  - parenthesized subexpressions (`(e)`);
-  - memory loads (`[:u16 p + 2 * i]`);
-  - array accesses (`x[i]`, `x.[i]`, `x[:u16 i]`);
-  - unary operators (`- e`);
-  - binary operators (`e - f`);
-  - conditional expressions (`c ? th : el`);
-  - function calls (`f(x, y)`);
-  - primitive instructions (`#copy_32(t)`).
+a.[i]         /* byte at offset i, read as declared type (u64) */
+a.[:u16 i]    /* byte at offset i, read as u16 */
+```
+
+The `.` before the bracket switches to unscaled mode: the index `i` is a
+byte offset into the array. For example, `a.[1]` on a `u64[10]` array reads
+8 bytes starting at byte offset 1.
+
+### Subarray access
+
+```
+a[i:N]        /* N elements starting at index i */
+a[:u16 i:N]   /* N u16 elements starting at index i */
+a.[i:N]       /* N elements starting at byte offset i */
+a.[:u16 i:N]  /* N u16 elements starting at byte offset i */
+```
+
+Subarrays extract a contiguous slice of the array. The length `N` must be
+a compile-time constant. Subarrays can appear both in expressions and as
+[left-values](lvalues.md).
+
+### Alignment annotations
+
+```
+a[#aligned i:N]
+a[#unaligned i:N]
+```
+
+Subarray accesses can be annotated with `#aligned` or `#unaligned` to indicate
+alignment properties for vector loads/stores.
+
+### Summary
+
+```
+<array-access> ::= <var> <arr-bracket>
+                 | <var> "." <arr-bracket>
+
+<arr-bracket> ::= "[" <alignment>? (":" <word-type>)? <expr> (":" <expr>)? "]"
+
+<alignment> ::= "#aligned" | "#unaligned"
+```
+
+The `.` switches from scaled (element) to unscaled (byte) indexing.
+The optional `:<word-type>` reinterprets the array element type.
+The optional `:<expr>` suffix specifies a subarray length.
+
+Jasmin arrays are fundamentally byte arrays in little-endian order.
+See the [semantics of arrays](../semantics/arrays.md) for details.
+
+## Memory access (loads)
+
+```
+reg u64 x p;
+x = [p + 8];              /* load u64 from address p+8 */
+x = [:u16 p + 2 * i];     /* load u16 from address p+2*i */
+x = [#aligned p];         /* aligned load */
+x = [#unaligned :u128 p]; /* unaligned 128-bit load */
+```
+
+```
+<memory-load> ::= "[" <alignment>? (":" <word-type>)? <expr> "]"
+```
+
+A memory load reads a value from a memory address. The expression inside
+brackets computes the address. The offset is always in bytes.
+
+The optional `:<word-type>` specifies the width of the load (default depends on
+context). The optional `#aligned` or `#unaligned` annotation indicates alignment
+expectations for the load instruction.
+
+## Pack expressions
+
+```
+reg u128 v;
+v = (4u32)[a, b, c, d];       /* pack four u32 values into a u128 */
+v = (16u8)[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15];
+```
+
+```
+<pack-expr> ::= "(" <svsize> ")" "[" <expr> ("," <expr>)* "]"
+```
+
+A pack expression constructs a vector value from a list of element values.
+The `<svsize>` specifies the number of elements, signedness, and element
+bit-width (see [SIMD vector sizes](types.md#simd-vector-sizes)).
+The number of expressions must match the lane count.
+
+The elements are listed in little-endian order: the first element in the list
+occupies the least significant bits of the resulting value.
+For example, `(4u64)[a, b, c, d]` places `a` in the lowest 64 bits and `d`
+in the highest.
+
+## Casts
+
+```
+reg u64 x;
+reg u32 y;
+x = (64u) y;     /* zero-extend u32 to u64 */
+x = (64s) y;     /* sign-extend u32 to u64 */
+y = (32u) x;     /* truncate u64 to u32 */
+
+reg u64 z;
+inline int n;
+n = (int) z;     /* word to unbounded integer */
+z = (sint) n;    /* integer to word (signed interpretation) */
+z = (uint) n;    /* integer to word (unsigned interpretation) */
+```
+
+```
+<cast-expr> ::= "(" <cast> ")" <expr>
+
+<cast> ::= <word-size> <sign>     /* word cast: (64u), (32s), etc. */
+         | "int"                  /* word to int (unsigned) */
+         | "sint"                 /* word to int (signed) */
+         | "uint"                 /* word to int (unsigned, explicit) */
+```
+
+The `<word-size>` is the numeric part of a word type: `8`, `16`, `32`, `64`,
+`128`, or `256`. The `<sign>` is `u` (unsigned/zero-extend) or `s`
+(signed/sign-extend).
+
+Casts between word types perform zero-extension, sign-extension, or truncation
+depending on the relative sizes. `(int)` and `(uint)` convert a word to an
+unbounded integer (unsigned interpretation). `(sint)` converts a word to an
+integer using signed interpretation.
 
 ## Unary operators
 
 ```
-<op1> ::=
-  | !        // Boolean and bitwise negation.
-  | -        // Arithmetic negation.
-  | (<cast>) // Cast.
+reg bool b;
+b = !b;           /* boolean/bitwise negation */
 
-<cast> ::=
-  | <wsize_size><sign>
-  | int
+reg u64 x;
+x = -x;           /* arithmetic negation */
+```
 
 ```
+<unary-expr> ::= <unary-op> <expr>
 
-Unary operators are, by decreasing precedence:
+<unary-op> ::= "!" <castop>?
+             | "-" <castop>?
+```
+
+| Operator | Description |
+|----------|-------------|
+| `!`      | Boolean negation (on `bool`) or bitwise complement (on word types). |
+| `-`      | Arithmetic negation. |
 
-  - zero- or sign-extension (`(16s)e`);
-  - boolean / bitwise negation (`! b`);
-  - opposite (`- e`).
+Both operators accept an optional size/sign annotation (see below).
 
 ## Binary operators
 
 ```
-<op2> ::=
-  | +    // Addition.
-  | -    // Subtraction.
-  | *    // Multiplication.
-  | /    // Integer division.
-  | %    // Modulo.
-  | &    // Bitwise AND.
-  | |    // Bitwise OR.
-  | ^    // Bitwise XOR (exclusive OR).
-
-  | ==   // Equality test.
-  | !=   // Inequality test.
-  | <    // Unsgined less than test.
-  | <s   // Signed less than test.
-  | >    // Unsigned greater than test.
-  | >s   // Signed greater than test.
-  | <=   // Unsigned less than or equal test.
-  | <=s  // Signed less than or equal test.
-  | >=   // Unsigned greater than or equal test.
-  | >=s  // Signed greater than or equal test.
-
-  | <<   // Left shift.
-  | >>   // Right shift.
-  | >>s  // Arithmetic right shift.
-  | <<r  // Left rotation.
-  | >>r  // Right rotation.
-
-  | &&   // Boolean AND.
-  | ||   // Boolean OR.
-```
-
-- `+`: Addition.
-- `<<`: Left shift.
-- `>>`: Right shift.
-- `>>s`: Arithmetic right shift. In ARM-M4, an arithmetic right shift by 0 is
-  compiled to a `MOV`.
-- `<<r`: Left rotation.
-- `>>r`: Right rotation. In ARM-M4, a right rotation by 0 is compiled to a
-  `MOV`.
-
-Binary operators are, by decreasing precedence:
-
-  - multiplication (`x * y`), integer division (`x / y`), and remainder (`x % y`);
-  - addition (`x + y`) and subtraction (`x - y`);
-  - shifts (`x << y`; `x >>s y`) and rotations (`x <<r y`; `x >>r y`);
-  - bitwise and (`x & y`);
-  - bitwise exclusive or (`x ^ y`);
-  - bitwise or (`x | y`);
-  - comparisons (`x < y`; `x >= y`);
-  - equality test (`x == y`; `x != y`);
-  - boolean conjunction (`b && c`);
-  - boolean disjunction (`b || c`).
-
-Note that most operators accept as suffix a size annotation. For instance `+32u` is the 32-bit (unsigned) addition and `+8u16` is the parallel 16-bit (unsigned) addition for vectors of 8 elements (i.e., 128 bit). Said annotation can be limited to a sign annotation, for instance `>>u` is the _logical_ right shift whereas `>>s` is the _arithmetic_ right shift.
+x = a + b;
+x = a >>s 4;     /* arithmetic right shift */
+x = a /s b;      /* signed division */
+x = a +4u64 b;   /* parallel 4-lane u64 addition */
+```
 
-## Array access
+```
+<binary-expr> ::= <expr> <binary-op> <expr>
+
+<binary-op> ::= <op> <castop>?
+```
+
+### Operator list
+
+**Arithmetic:**
+
+| Operator | Description |
+|----------|-------------|
+| `+`      | Addition |
+| `-`      | Subtraction |
+| `*`      | Multiplication |
+| `/`      | Unsigned division |
+| `%`      | Unsigned modulo |
+
+**Bitwise:**
+
+| Operator | Description |
+|----------|-------------|
+| `&`      | Bitwise AND |
+| `\|`     | Bitwise OR |
+| `^`      | Bitwise XOR |
+
+**Shifts and rotations:**
+
+| Operator | Description |
+|----------|-------------|
+| `<<`     | Left shift |
+| `>>`     | Unsigned (logical) right shift |
+| `<<r`    | Left rotation |
+| `>>r`    | Right rotation |
+
+**Comparison:**
+
+| Operator | Description |
+|----------|-------------|
+| `==`     | Equality |
+| `!=`     | Inequality |
+| `<`      | Unsigned less than |
+| `>`      | Unsigned greater than |
+| `<=`     | Unsigned less than or equal |
+| `>=`     | Unsigned greater than or equal |
+
+**Logical:**
+
+| Operator | Description |
+|----------|-------------|
+| `&&`     | Boolean AND (short-circuiting) |
+| `\|\|`   | Boolean OR (short-circuiting) |
+
+### Sign modifiers
+
+Division, modulo, right shift, and comparison operators accept an `s` suffix
+to select signed semantics:
+
+| Unsigned | Signed |
+|----------|--------|
+| `/`      | `/s`   |
+| `%`      | `%s`   |
+| `>>`     | `>>s`  |
+| `<`      | `<s`   |
+| `>`      | `>s`   |
+| `<=`     | `<=s`  |
+| `>=`     | `>=s`  |
+
+### Size and vector annotations
+
+Most operators accept a size annotation as a suffix. This forces the
+operation to be performed at a specific width or in parallel over vector lanes:
+
+- `+32u` -- 32-bit unsigned addition
+- `+8u16` -- parallel addition of 8 unsigned 16-bit lanes (128-bit vector)
+- `>>s` -- signed (arithmetic) right shift at the default width
+- `:u32` -- can be attached to `!` and `-` as well: `!:u32 x`
+
+The annotation follows the operator and precedes the right operand. The syntax
+for annotations is:
 
-For an array
 ```
-stack u64[10] x;
+<castop> ::= <swsize>         /* e.g., 32u, 64s */
+           | <svsize>         /* e.g., 4u64, 8u16 */
+           | ":" <word-type>  /* e.g., :u32 */
 ```
-`x[i]` accesses the i-th element of the array (the first index is 0).
 
-Other indexing syntaxes are available, since Jasmin arrays of any type are
-fundamentally byte arrays.
-Therefore, accesses with a different type than the declared type of the array
-are possible, such as `x[u16 i]` which views `x` as a length 40 array of `u16`
-and accesses the i-th element.
+Where `<swsize>` is `<size><sign>` (like `32u`, `64s`) and `<svsize>` is the
+SIMD vector notation (like `4u64`).
+See [SIMD vector sizes](types.md#simd-vector-sizes).
+
+### Precedence
+
+From highest to lowest precedence:
 
-Further, non-scaled array accesses are also possible:
-`x.[u16 1]` returns the `u16` composed of the second and third bytes of the array.
-The explicit type can also be left out `x.[i]` is equivalent to `x.[u64 i]`.
+| Precedence | Operators |
+|------------|-----------|
+| Highest    | `!`, `-` (unary), casts |
+| 1          | `*`, `/`, `%` |
+| 2          | `+`, `-` |
+| 3          | `<<`, `>>`, `<<r`, `>>r` |
+| 4          | `&` |
+| 5          | `^` |
+| 6          | `\|` |
+| 7          | `<`, `>`, `<=`, `>=` |
+| 8          | `==`, `!=` |
+| 9          | `&&` |
+| 10         | `\|\|` |
+| Lowest     | `? :` (ternary) |
 
-> Note: Jasmin semantics specifies the conversion between bytes and words as little-endian.
+All binary operators are left-associative. The ternary operator is
+right-associative.
 
-## Subarrays
+## Ternary conditional
 
-To facilitate array handling, subarray notation was introduced. Consider the
-following example,
 ```
-a[i:N] = add_array(a[i:N], b[j:N]);
+reg u64 x a b;
+x = (a > b) ? a : b;   /* maximum of a and b */
 ```
-with,
+
 ```
-inline fn add_array(stack u64[N] a b) -> stack u64[N] {
-  inline int i;
-  for i = 0 to N {
-    reg u64 ai bi;
-    ai = a[i];
-    bi = b[i];
-    ai += bi;
-    a[i] = ai;
-  }
-  return a;
-}
+<ternary-expr> ::= <expr> "?" <expr> ":" <expr>
 ```
-Subarrays consists on two elements:
-- index: where the access starts
-- length: amount of elements to access (must be a constant `int`).
 
-Similarly to array indexing, non-scaled subarrays and subarrays with
-type-casting are supported: `a.[i:N]`, `a[u16 i:N]`, `a.[u16 i:N]`.
+The ternary conditional evaluates the condition (first operand) and returns
+the second operand if true, or the third if false.
+
+## Comments
 
-## Memory accesses
+Jasmin supports C-style comments:
 
-Suppose a register `reg u64` whose value is a memory address.
-Then, for loading values from memory the notation is as follows:
 ```
-reg u64 var;
-var = [ptr + offset];
-// or for better understanding
-var = (64u)[ptr + offset];
+/* This is a block comment.
+   It can span multiple lines. */
+
+// This is a line comment.
 ```
-`offset` is measured in bytes.
 
+Block comments can be nested: `/* outer /* inner */ still outer */`.
diff --git a/docs/source/language/syntax/index.md b/docs/source/language/syntax/index.md
index 39be1b22e..e2acd9185 100644
--- a/docs/source/language/syntax/index.md
+++ b/docs/source/language/syntax/index.md
@@ -3,16 +3,39 @@
 Jasmin is a low-level language: it is essentially assembly with variables and
 structured control flow.
 It should be thought of as a tool to help you write assembly: programmers use
-Jasmin to produce specific assembly code in a convenient, safe and secure
+Jasmin to produce specific assembly code in a convenient, safe, and secure
 manner.
-This means that there are special considerations for each architecture.
-You can read these for the [[x86-64|x86-64]] and the [[ARMv7-M|ARMv7-M]] target
-architectures.
+
+This section documents the surface syntax of the language. For the operational
+meaning of each construct, see the [semantics reference](../semantics/index.md).
+For annotations that customize compiler behavior and declare security properties,
+see the [annotations reference](../annotations/index.md).
+
+## Notation conventions
+
+The grammar notation used throughout this reference is an informal BNF:
+
+- `<name>` -- a nonterminal (a syntactic category)
+- `"keyword"` -- a literal keyword or symbol
+- `|` -- alternatives
+- `?` -- optional (zero or one)
+- `*` -- zero or more repetitions
+- `+` -- one or more repetitions
+- `(` `)` -- grouping
+
+Concrete examples always precede the grammar rules.
+
+## Architecture considerations
+
+The core Jasmin syntax is architecture-neutral. Architecture-specific features
+(intrinsic names, available register widths, alignment requirements) are noted
+inline where relevant.
 
 :::{toctree}
 :maxdepth: 2
 
 structure.md
+types.md
 code.md
 expressions.md
 lvalues.md
diff --git a/docs/source/language/syntax/lvalues.md b/docs/source/language/syntax/lvalues.md
index 58a18966b..598f54f97 100644
--- a/docs/source/language/syntax/lvalues.md
+++ b/docs/source/language/syntax/lvalues.md
@@ -1,22 +1,74 @@
 # Left-values
 
-Left-values appear on the left-hand side of [assignments](code.md#assignments) and
-[calls](code).
-A left-value describes the location where a value is stored.
+Left-values (lvalues) describe locations where values can be stored.
+They appear on the left-hand side of [assignments](code.md#assignments)
+and as outputs of function and intrinsic calls.
 
 ```
-<lval> ::=
-  | <var>
-  | (<wsize>)[<var> + <expr>] // Memory access.
-  | (<wsize>)[<var> - <expr>] // Memory access.
-  | <var>[<expr>]  // Array access.
-  | <var>[<wsize> <expr>]  // Array access.
-  | <var>.[<wsize> <expr>]  // Unscaled array access.
-  | <var>[<wsize> <expr> : <expr>]  // Subarray.
-  | <var>.[<wsize> <expr> : <expr>]  // Unscaled subarray.
-  | _ // Ignored value
+<lvalue> ::= "_"
+           | <var>
+           | <var> <arr-bracket>
+           | <var> "." <arr-bracket>
+           | "[" <alignment>? (":" <word-type>)? <expr> "]"
 ```
 
-Left-values syntax is a subset of [expression](expressions), except for `_`
-which corresponds to an ignored value.
+Left-value syntax is a subset of [expression](expressions.md) syntax, with the
+addition of `_` (ignored value) which has no expression counterpart.
 
+## Ignored value
+
+```
+_, _, x = #ADDC_64(x, y);
+_ = f(x);
+```
+
+The underscore `_` discards a value. This is commonly used to ignore
+flags returned by intrinsics or to discard unwanted return values from
+function calls.
+
+## Variable
+
+```
+x = 42;
+A::x = 0;
+```
+
+A simple variable or namespace-qualified name. See [variables](expressions.md#variables).
+
+## Array element and subarray
+
+```
+a[i] = x;            /* scaled element store */
+a[:u16 i] = y;       /* typed element store */
+a.[i] = x;           /* unscaled (byte offset) store */
+a.[:u16 i] = y;      /* unscaled typed store */
+
+a[i:N] = f(a[i:N]);  /* subarray store */
+a.[i:N] = v;         /* unscaled subarray store */
+
+a[#aligned i:N] = v; /* aligned subarray store */
+```
+
+Array left-values use the same syntax as array access in
+[expressions](expressions.md#array-access): scaled vs. unscaled (`.`),
+optional type annotation (`:u16`), optional subarray length (`:N`),
+and optional alignment annotations (`#aligned`, `#unaligned`).
+
+In subarray notation `a[i:N]`, `i` is the starting index (which can be any
+expression) and `N` is the *length* (number of elements), not the end index.
+The length must be a compile-time constant. For example, `a[2:3]` accesses
+3 elements starting at index 2 (i.e., elements 2, 3, and 4).
+
+## Memory store
+
+```
+[p + 8] = x;                 /* store u64 at address p+8 */
+[:u16 p + 2 * i] = y;        /* store u16 at address p+2*i */
+[#aligned p] = v;            /* aligned store */
+[#unaligned :u128 p + off] = v; /* unaligned 128-bit store */
+```
+
+Memory stores use the same bracket syntax as
+[memory loads](expressions.md#memory-access-loads): the expression inside
+brackets computes the target address, with optional alignment and type
+annotations.
diff --git a/docs/source/language/syntax/structure.md b/docs/source/language/syntax/structure.md
index 53deb2dfa..346e53ab9 100644
--- a/docs/source/language/syntax/structure.md
+++ b/docs/source/language/syntax/structure.md
@@ -1,244 +1,325 @@
-# Structure
+# Program structure
 
-A Jasmin program is a collection of:
+A Jasmin source file is a sequence of top-level items:
 
-  - requires;
-  - parameters;
-  - global variables;
-  - types aliases;
-  - functions.
+```
+require "common.jinc"
 
-Each of these can potentially be defined inside a namespace.
+param int N = 10;
 
-## Require
+type word = u64;
+
+u128 pattern = (16u8)[12, 15, 14, 13, 8, 11, 10, 9, 4, 7, 6, 5, 0, 3, 2, 1];
+
+namespace Crypto {
+  export fn process(reg u64 p) { ... }
+}
+```
 
 ```
-require <string>
+<program> ::= <top-level-item>*
+
+<top-level-item> ::= <require>
+                   | <param>
+                   | <type-alias>
+                   | <global>
+                   | <function>
+                   | <namespace>
 ```
+
+## Require
+
 ```
-require <string> ... <string>
+require "utils.jinc"
+require "file1.jinc" "file2.jinc"
+from AES require "aes.jinc"
 ```
+
 ```
-from <ident> require <string> ... <string>
+<require> ::= "require" <string>+
+            | "from" <ident> "require" <string>+
 ```
 
-Since version 2022.04.0, a program may be split into several files using a
-`require` clause. Its simplest form is as follows
+A require clause includes the contents of another file.
+Relative paths are resolved relative to the directory of the current file.
+The required file is treated as if its contents were placed at the location
+of the require clause.
 
-    require "path/file.jinc"
+The `from` variant searches for files in a named location. Named locations
+can be defined in two ways:
 
-Relative paths are resolved relative to the current file.
+- On the command line: `-I AES=actual/path/`
+- Via the environment variable `JASMINPATH`: `export JASMINPATH=AES=actual/path/`
 
-The required file is treated (mostly) as if its contents were put in
-place of the `require` clause.
+Multiple named paths can be specified by repeating `-I` or separating entries
+with `:` in `JASMINPATH`.
 
-TODO: More detail about "mostly"
+Both forms accept multiple file arguments:
+
+```
+require "file1.jinc" "file2.jinc" "file3.jinc"
+from PATH require "file1.jinc" "file2.jinc" "file3.jinc"
+```
+
+:::{note}
+An established practice is to name included files with a `.jinc` suffix.
+However, this is not mandatory. Any name (and thus any suffix) can be used.
+:::
+
+## Parameters
+
+```
+param int ROUNDS = 24;
+param int BLOCK_SIZE = 4 * ROUNDS;
+```
 
-Files can also be searched in named locations, for instance:
+```
+<param> ::= "param" <type> <ident> "=" <expr> ";"
+```
 
-    from AES require "aes.jinc"
+A parameter is a named compile-time constant,
+defined in terms of literals and other parameters.
+Parameters can be used within types (e.g., as the size of an array),
+providing a limited form of genericity.
 
-This clause requires the file `aes.jinc` that is located in a path named `AES`.
-There are two ways to give names to paths in the file-system:
+Parameters are resolved by the compiler right after parsing. They do not appear
+in the formal (Rocq) abstract syntax and have no formal semantics.
 
-  - either on the command-line using the argument `-I AES:actual/path/`;
-  - or using the `JASMINPATH` environment variable, as in
-  `export JASMINPATH=AES=actual/path/`.
+## Type aliases
 
-If several paths must be named, the `-I` argument can be used multiple
-times, and in the environment variable value,
-several `ID=path` pairs can be separated by a colon (`:`).
+```
+type word = u64;
+type block = u32[4];
+```
 
-Both `require` clauses and `from` can take several arguments, as in
 ```
-require "path/file1.jinc" "path/file2.jinc" "path/file3.jinc"
+<type-alias> ::= "type" <ident> "=" <type> ";"
 ```
-and
+
+A type alias introduces an alternative name for a type. The alias can then be
+used anywhere a type is expected:
+
 ```
-from PATH require "file1.jinc" "file2.jinc" "file3.jinc"
+reg word x;
+stack word[4] buf1;
+stack block buf2;
 ```
 
-## Parameters
+Type aliases are resolved at parse time, like parameters. They cannot alias
+storage qualifiers: `type x = reg u64;` is not valid. See [types](types.md) for
+the full set of available types.
+
+## Global variables
 
 ```
-param <type> <ident> = <expr>;
+u128 rotate24pattern = (16u8)[12, 15, 14, 13, 8, 11, 10, 9, 4, 7, 6, 5, 0, 3, 2, 1];
+u64 constant = 0x1234;
 ```
 
-A parameter is a named value. The name can be used within types
-(e.g., as the size of an array):
-as such, they can be used to provide a limited form of genericity.
+```
+<global> ::= <type> <ident> "=" <global-expr> ";"
+
+<global-expr> ::= <expr>
+                | "{" <expr> ("," <expr>)* "}"
+```
 
-Parameters are removed by the compiler right after parsing; in particular,
-they do not appear
-in the Coq abstract syntax. Therefore, they have no formal semantics.
+A global variable is a named read-only value available at runtime.
+Unlike parameters, global values cannot be used as part of a type
+(e.g., as an array size), but they can be accessed during execution.
 
-A parameter is introduced by the `param` keyword, followed by a type, a
-name, and the value. For instance:
+Global variables are stored in the code segment and accessed using PC-relative
+addressing. There is no introducing keyword; a top-level declaration without
+`param`, `fn`, `type`, or `namespace` is parsed as a global.
 
-    param int cROUNDS = 2;
+The brace syntax allows initializing arrays element by element:
 
-## Types Aliases
+```
+u32[4] constants = { 0x61707865, 0x3320646e, 0x79622d32, 0x6b206574 };
+```
 
-Jasmin compiler latest development version (still unreleased) introduced a
-new syntax feature for type definition. A type alias can be defined at top
-level of a program or a namespace. The aim of this feature is to improve
-genericity of Jasmin code. The types aliases are resolved like params,
-during parsing.
+The string syntax can be used to initialize arrays of bytes:
 
-To define a type alias, we introduced the `type` keyword, which is followed
-by a name, and the a type. For example :
 ```
-type reg_size = u64;
+u8[4] bytes = "abcd";
 ```
-Defined types can then be used in programs in place of the compiler types.
+
+:::{caution}
+The strings are not automatically zero-terminated.
+:::
+
+## Functions
+
 ```
-reg reg_size a; //declaring variable a with type reg_size
-reg reg_size[10] b; //declaring an array with elements of type reg_size
+inline
+fn rotate(reg u32 x, inline int bits) -> reg u32 {
+    x = x <<r bits;
+    return x;
+}
+
+export
+fn process(reg u64 ptr) {
+    reg u64 t;
+    t = [ptr];
+    [ptr] = t;
+}
+
+#[returnaddress = stack]
+fn helper(reg u64 x) -> reg u64 {
+    x += 1;
+    return x;
+}
 ```
 
-We can note that the feature doesn't allow definitions like :
 ```
-type x = reg u64;
+<function> ::= <annotations>? <fn-kind>? "fn" <ident>
+               "(" <arg-list> ")" ("->" <result-types>)? <body>
+
+<fn-kind> ::= "inline" | "export"
+
+<arg-list> ::= (<annot-arg> ("," <annot-arg>)*)?
+
+<annot-arg> ::= <annotations>? <storage> <type> <ident>+
+
+<result-types> ::= <annot-result> ("," <annot-result>)*
+
+<annot-result> ::= <annotations>? <storage> <type>
+
+<body> ::= "{" <instr>* <return-stmt>? "}"
+
+<return-stmt> ::= "return" <ident> ("," <ident>)* ";"
 ```
 
-We can consider that the storage type (`reg`, `stack`, `inline` ...) is
-similar to the declaration keyword `let` in other languages (for instance Rust).
-Storage type is thus not a type, and should not be aliased.
+A function is introduced by the `fn` keyword, preceded by an optional
+function kind and optional [annotations](../annotations/index.md).
 
-## Global variables
+### Kinds of functions
 
-A global variable is a named value. Unlike parameters, said value is not
-available at compile-time
-(i.e., it cannot be used as part of a type), but it is available at run-time.
+There are three kinds of functions:
 
-Technically, global variables are stored in the code segment and are accessed
-to using PC-relative addressing mode.
+**`inline`** -- The function is inlined at every call site. Inline functions
+are erased during compilation and produce no standalone assembly code.
 
-There is no keyword to introduce a global variable declaration at the top-level,
-only its type, name, and value. For instance:
+**`export`** -- The function is visible from outside (can be called from C or
+other non-Jasmin code). It follows the platform ABI for argument passing
+and return values.
 
-    u128 rotate24pattern = (16u8)[ 12, 15, 14, 13, 8, 11, 10, 9, 4, 7, 6, 5, 0, 3, 2, 1 ];
+**No keyword (local/subroutine)** -- The function is compiled as a subroutine
+with a Jasmin-internal calling convention. It is not visible to external code
+but is preserved as a separate function in the generated assembly.
 
-In this example, the value is a 128-bit machine-word, described as a vector
-of 16 8-bit machine-words.
+### Arguments and results
 
-## Functions
+Each argument has an [annotation](../annotations/index.md) (optional),
+a [storage qualifier and type](types.md), and one or more names.
+Multiple arguments of the same storage and type can share a declaration:
 
-A function is introduced using the `fn` keyword, followed by the function name,
-the list of its parameters, its return type (if any), and its body.
-The body begins with the declaration of local variables and ends with
-a `return` statement.
+```
+fn f(reg u64 x y, stack u8[32] buf) -> reg u64 { ... }
+```
 
-Here is an example function:
+Result types are declared after `->` and specify the storage and type
+(but not the name) of each result. The names of the returned values
+appear in the `return` statement at the end of the function body.
 
-    inline
-    fn shift(reg u128 x, inline int count) -> reg u128 {
-      reg u128 r;
-      r = #VPSLL_4u32(x, count);
-      return r;
-    }
+:::{attention}
+The `return` statement can only reference variables, not expressions.
+:::
+
+Commas are used to separate result types and returned values.
 
 ```
-export
-fn add(reg u64 x, reg u64 y) -> reg u64 {
-  reg u64 r;
-  r = x;
-  r += y;
-  return r;
+fn min_max (reg u64 n m) -> reg u64, reg u64 {
+  reg u64 min max;
+  if (n < m) { min = n; max = m; } else { min = m; max = n; }
+  return min, max;
 }
 ```
 
-Function definitions can be prefixed with either the `inline` or `export`
-keywords to denote, respectively, that the function will be inlined by the
-compiler or that it will respect a specified calling convention.
-
-Since version 2022.04.0, functions may not be marked
-with `inline` or `export`. Such functions are called local functions, and
-they will be preserved by the compiler but are not visible from the outside
-(i.e., they cannot be called from non-Jasmin code).
+A function with no results omits the `->`:
 
-Function definitions can also be prefixed by annotations.
-Annotations are key-value pairs that customize the behaviour of the compiler,
-for instance to store the return address of a function in a register or in the
-stack.
-For instance,
 ```
-#[returnaddress=stack]
-fn copy_to_memory(reg u64 x, reg u64 p) {
-    [p + 8] = x;
+fn store(reg u64 p, reg u64 v) {
+    [p] = v;
 }
 ```
-is a local function that copies the contents of a register `x` to an address
-(stored in a register `p`) with an offset of 8, and takes its return address
-from the stack.
 
-TODO: Add link to annotation syntax.
 
-### Safety annotations
 
-Function definitions can be annotated with safety contracts, whose syntax is illustrated below.
+### Safety contracts
+
+Functions can be annotated with safety contracts for use with the
+[safety checker](../../tools/safety_checker.md):
 
 ```
 #[safety = {
-   args = {<var>, …, <var>},
-   res = {<var>, …, <var>},
-   requires = <expr_assert>,
-   ensures = <expr_assert>
-  } ]
+    args    = { x, y },
+    res     = { r },
+    requires = x + y < 0xFFFFFFFFFFFFFFFF,
+    ensures  = r == x + y
+}]
+fn add(reg u64 x, reg u64 y) -> reg u64 {
+    reg u64 r;
+    r = x + y;
+    return r;
+}
 ```
 
-Field `args` (resp. `res`) is optional: by default it is filled with the
-function parameters (resp. function returned variables).
-
-[The assertions (`<expr_assert>`) are described in a dedicated section.](./code.md#assertions)
+See the [annotations reference](../annotations/index.md#safety) for details
+on the contract fields.
 
 ## Namespaces
 
-Jasmin features a simple namespace system, with a syntax similar to that of C++.
+```
+namespace Crypto {
+    fn encrypt(reg u64 x) -> reg u64 {
+        return x;
+    }
+}
+
+/* Call from outside: */
+r = Crypto::encrypt(x);
+```
 
-A namespace is opened with the keyword `namespace`. It is followed by its name,
-and curly brackets enclosing the definitions placed inside the namespace.
-For instance,
 ```
-namespace A {
-  u32 g = 1;
+<namespace> ::= "namespace" <ident> "{" <top-level-item>* "}"
+```
 
-  fn f (reg u32 x) -> reg u32 {
-    return x;
-  }
+A namespace groups top-level items under a common prefix.
+Items inside a namespace are referenced from outside using `::`:
+
+```
+namespace A {
+    u32 g = 1;
+    fn f(reg u32 x) -> reg u32 { return x; }
 }
+
+/* Access: A::g, A::f */
 ```
-defines a global variable called `g` and a function called `f` inside a namespace called `A`.
 
-Referring to an object outside the namespace where it was defined can be done using `::`.
-In the last example, one would write `A::g` and `A::f`.
+Namespaces can be nested:
 
-Namespaces can be nested. For instance,
 ```
 namespace A {
-  namespace B {
-    fn f (reg u32 x) -> reg u32 {
-      return x;
+    namespace B {
+        fn f(reg u32 x) -> reg u32 { return x; }
     }
-  }
 }
+/* Access: A::B::f */
 ```
-defines `f` inside the namespace `B`, which is itself inside the namespace `A`. To refer to `f` outside `A`,
-one would write `A::B::f`.
 
-A namespace can be closed and reopened, but accesses to objects defined in previous blocks
-of the same namespace must be prefixed.
-For instance,
+A namespace can be closed and reopened, but items defined in a previous block
+of the same namespace must be accessed with the full prefix:
+
 ```
 namespace A {
-  u32 g = 1;
+    u32 g = 1;
 }
 
 namespace A {
-  u32 g2 = A::g; // g needs to be prefixed
+    u32 g2 = A::g;  /* A::g must be qualified */
 }
 ```
 
-Defining an export function inside a namespace has an impact on its label in the assembly produced
-by the compiler. The rule of thumb is: `::` are replaced with `__`.
-For instance, a function `A::B::f` will have symbol `A__B__f`.
+Export functions inside namespaces have their `::` separators replaced with
+`__` in the generated assembly symbol. For example, `A::B::f` becomes
+`A__B__f`.
diff --git a/docs/source/language/syntax/types.md b/docs/source/language/syntax/types.md
new file mode 100644
index 000000000..3ec3904d2
--- /dev/null
+++ b/docs/source/language/syntax/types.md
@@ -0,0 +1,203 @@
+# Types and storage
+
+Every variable in Jasmin has a type and a storage class.
+The type determines what values the variable can hold;
+the storage class determines where it lives at runtime (register, stack, etc.).
+
+## Types
+
+```
+<type> ::= "bool"
+         | "int"
+         | <word-type>
+         | <wint-type>
+         | <array-type>
+         | <ident>
+```
+
+### Boolean
+
+```
+reg bool b;
+b = true;
+```
+
+The type `bool` represents Boolean values. Its only values are `true` and `false`.
+
+### Unbounded integers
+
+```
+param int N = 10;
+inline int i;
+```
+
+The type `int` represents mathematical (unbounded) integers.
+Variables of type `int` must be known at compile time:
+they can only appear with the `inline` or `param` storage.
+
+### Word types
+
+```
+reg u64 x;
+stack u128 v;
+```
+
+```
+<word-type> ::= "u8" | "u16" | "u32" | "u64" | "u128" | "u256"
+```
+
+Word types represent fixed-width bit vectors:
+
+| Type   | Width   |
+|--------|---------|
+| `u8`   | 8 bits  |
+| `u16`  | 16 bits |
+| `u32`  | 32 bits |
+| `u64`  | 64 bits |
+| `u128` | 128 bits |
+| `u256` | 256 bits |
+
+Word types have no inherent signedness. Like in assembly (and unlike C), the
+interpretation as signed or unsigned is determined by the operations applied to
+them: for example, `>>` is an unsigned (logical) right shift while `>>s` is a
+signed (arithmetic) right shift; `<` is an unsigned comparison while `<s` is
+signed.
+
+These are the fundamental types that map to machine registers and memory locations.
+
+### Word-sized integers
+
+```
+reg ui64 x;
+reg si32 y;
+```
+
+```
+<wint-type> ::= "ui8" | "ui16" | "ui32" | "ui64" | "ui128" | "ui256"
+              | "si8" | "si16" | "si32" | "si64" | "si128" | "si256"
+```
+
+Word-sized integers are bounded integers that are compiled to machine words.
+Unlike word types, arithmetic on word-sized integers follows integer semantics
+(e.g., overflow is undefined) rather than modular word semantics.
+
+| Unsigned | Signed | Width |
+|----------|--------|-------|
+| `ui8`    | `si8`  | 8 bits |
+| `ui16`   | `si16` | 16 bits |
+| `ui32`   | `si32` | 32 bits |
+| `ui64`   | `si64` | 64 bits |
+| `ui128`  | `si128` | 128 bits |
+| `ui256`  | `si256` | 256 bits |
+
+See the [semantics of scalar types](../semantics/scalar_types.md)
+for details on overflow behavior and conversion rules.
+
+### Array types
+
+```
+stack u64[10] a;
+reg u8[32] key;
+stack u32[N] buf;   /* N is a param */
+```
+
+An array type is written as a base type followed by a size in brackets:
+
+```
+<array-type> ::= (<word-type> | <ident>) "[" <expr> "]"
+```
+
+The base type is either a word type or an alias to a word type.
+The size must be a compile-time constant expression
+(a literal, a `param`, or an expression involving only these).
+Arrays are fundamentally contiguous sequences of bytes in memory;
+the element type determines the default access granularity.
+
+See the [semantics of arrays](../semantics/arrays.md) for details on
+access patterns and type punning.
+
+### Type aliases
+
+A type alias (an ident) can be used anywhere a type is expected:
+
+```
+type word = u64;
+reg word x;       /* equivalent to: reg u64 x */
+```
+
+Such aliases can be defined using `type` declarations
+(see [type aliases](structure.md#type-aliases)).
+Type aliases are resolved at parse time and do not introduce new types.
+
+## Storage qualifiers
+
+Every variable declaration must specify a storage class:
+
+```
+reg u64 x;                /* register */
+stack u8[32] buf;         /* array in stack */
+inline int i;             /* compile-time constant */
+global u64 g;             /* global data */
+reg ptr u8[32] ptr;       /* pointer to array (the pointer lives in a register) */
+stack ptr u8[32] ptr;     /* pointer to array (the pointer lives in the stack) */
+```
+
+```
+<storage> ::= "reg" <ptr>?
+            | "stack" <ptr>?
+            | "inline"
+            | "global"
+
+<ptr> ::= <writable>? "ptr"
+<writable> ::= "const" | "mut"
+```
+
+### `reg`
+
+The variable lives in a machine register. Register variables are the most common
+in Jasmin. The register allocator assigns physical registers.
+
+### `stack`
+
+The variable lives on the stack frame. Stack variables are accessed via
+stack-relative addressing.
+
+### `inline`
+
+The variable is a compile-time constant. It must be assigned a value that
+can be fully evaluated at compile time. Inline variables are erased during
+compilation. The loop variable of a `for` loop is implicitly `inline int`.
+
+### `global`
+
+The variable is a read-only global constant. Global variables are compile-time
+constants whose values are emitted as bytes in the `.data` section of the
+generated assembly. They are accessed via PC-relative addressing and cannot be
+modified at runtime.
+
+### `reg ptr` and `stack ptr`
+
+Register and stack variables can hold *pointers* to arrays:
+
+```
+reg ptr u64[10] p;           /* pointer to array, default mutability */
+reg const ptr u64[10] p;     /* read-only pointer */
+reg mut ptr u64[10] p;       /* mutable pointer */
+stack ptr u64[10] sp;        /* stack pointer to array */
+```
+
+A pointer variable does not hold the array data itself; it holds a reference to
+an array that lives elsewhere (typically passed as a function argument).
+The `const` qualifier prevents writing through the pointer;
+`mut` explicitly marks it as writable (this is also the default when neither
+`const` nor `mut` is specified).
+
+:::{important}
+The storage modifiers can be seen as hints to the compiler.
+They do not carry any semantical meaning,
+actually they do not even appear in Jasmin's formal semantics.
+In particular, `reg ptr` and `stack ptr` are just arrays
+semantically-speaking.
+See the [semantics of arrays](../semantics/arrays.md)
+for more details on this.
+:::
diff --git a/opam b/opam
index faf09f088..f934cc7e1 100644
--- a/opam
+++ b/opam
@@ -20,7 +20,7 @@ install: [
   make "PREFIX=%{prefix}%" "install"
 ]
 depends: [
-  "ocaml" { >= "4.12" & build }
+  "ocaml" { >= "4.14" & build }
   "batteries" {>= "3.5"}
   "cmdliner" {>= "1.1" & build }
   "dune" {>= "3.7"}