Axiom · dark
Views and lifetimes
A view is a compiler-known borrowed range, not ordinary pointer arithmetic.
view<T> may lower to pointer + length in an ABI, but the semantic model also knows its region, range, lifetime, and permission.
Read-only borrow
Borrowed sequenceAxiom
1contains_zero(view<const u8> data) -> bool:2 for const u8 b in data:3 if b == 0:4 RETURN true5 RETURN false1
The element type is read-only.
2
Iteration creates no mutable alias.
3
A normal test.
5
No manual pointer arithmetic is exposed.
Mutable borrow
Effect inferenceAxiom
1zero(view<u8> data):2 for usize i = 0; i < data.size(); i = i + 1:3 data[i] = 01
The view carries write permission.
2
Loop bounds are visible.
3
The compiler can infer write region(data).
Dangling views are compile errors
Expected compile-time errorAxiom
1bad -> view<const u8>:2 const u8 local[] = { 1, 2, 3 }3 RETURN local1
The function promises to return a borrow.
2
The storage belongs to the local scope.
3
The returned view would outlive that region, so compilation fails.
Two mutable views
They can coexist only when the compiler proves their ranges do not overlap. Two disjoint slices are fine; two unknown overlapping slices are not.