Skip to content

[anneal] Translate and verify integration tests for new syntax #3320

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
joshlf wants to merge 1 commit into
base: main
Choose a base branch
from
Open

[anneal] Translate and verify integration tests for new syntax #3320

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion anneal/docker.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,6 @@ fi
# container. This assumes that the script is located in the root of the
# `anneal` workspace.
DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" >/dev/null 2>&1 && pwd)"
IMAGE_NAME="anneal-dev"
# To avoid pollution between different git worktrees, we generate a unique
# volume ID for each worktree and store it in a file. This ensures that
# each worktree gets its own isolated named volume for caching.
Expand All @@ -55,6 +54,7 @@ if [ ! -f "$VOLUME_ID_FILE" ]; then
fi
VOLUME_ID=$(cat "$VOLUME_ID_FILE" | tr -d '[:space:]')
VOLUME_NAME="anneal-cache-$VOLUME_ID"
IMAGE_NAME="anneal-dev:$VOLUME_ID"

BUILD_CACHE=$(mktemp)

Expand Down
19 changes: 5 additions & 14 deletions anneal/examples/abs.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,22 +1,13 @@
/// Computes the absolute value.
///
/// ```lean, anneal, spec
/// requires: x.val > -2147483648
/// ensures (h0): ret >= 0
/// ensures (h1): (x : Int) >= 0 -> (ret : Int) = x
/// ensures (h2): (x : Int) < 0 -> (ret : Int) = -x
/// proof (h_progress):
/// theorem spec (x : Std.I32) (h_req : x.val > -2147483648) :
/// Aeneas.Std.WP.spec (abs x) (fun ret_ =>
/// (ret_ : Int) ≥ 0 ∧
/// ((x : Int) ≥ 0 → (ret_ : Int) = x) ∧
/// ((x : Int) < 0 → (ret_ : Int) = -x)) := by
/// unfold abs
/// split <;> intros <;> (try cases h_req) <;> (try have := Aeneas.Std.IScalar.hmin x) <;> (try have := Aeneas.Std.IScalar.hmax x) <;> (try have : (↑(0 : I32) : Int) = 0 := by rfl) <;> (try have h_bound := Aeneas.Std.IScalar.tryMk_eq IScalarTy.I32 (-↑x)) <;> (try split at h_bound) <;> (try simp_all [HNeg.hNeg, Aeneas.Std.IScalar.neg, Aeneas.Std.IScalar.inBounds]) <;> scalar_tac
/// proof (h0):
/// unfold abs at h_returns
/// split at h_returns <;> intros <;> (try cases h_req) <;> (try have := Aeneas.Std.IScalar.hmin x) <;> (try have := Aeneas.Std.IScalar.hmax x) <;> (try have : (↑(0 : I32) : Int) = 0 := by rfl) <;> (try have h_bound := Aeneas.Std.IScalar.tryMk_eq IScalarTy.I32 (-↑x)) <;> (try split at h_bound) <;> (try simp_all [HNeg.hNeg, Aeneas.Std.IScalar.neg, Aeneas.Std.IScalar.inBounds]) <;> scalar_tac
/// proof (h1):
/// unfold abs at h_returns
/// split at h_returns <;> intros <;> (try cases h_req) <;> (try have := Aeneas.Std.IScalar.hmin x) <;> (try have := Aeneas.Std.IScalar.hmax x) <;> (try have : (↑(0 : I32) : Int) = 0 := by rfl) <;> (try have h_bound := Aeneas.Std.IScalar.tryMk_eq IScalarTy.I32 (-↑x)) <;> (try split at h_bound) <;> (try simp_all [HNeg.hNeg, Aeneas.Std.IScalar.neg, Aeneas.Std.IScalar.inBounds]) <;> scalar_tac
/// proof (h2):
/// unfold abs at h_returns
/// split at h_returns <;> intros <;> (try cases h_req) <;> (try have := Aeneas.Std.IScalar.hmin x) <;> (try have := Aeneas.Std.IScalar.hmax x) <;> (try have : (↑(0 : I32) : Int) = 0 := by rfl) <;> (try have h_bound := Aeneas.Std.IScalar.tryMk_eq IScalarTy.I32 (-↑x)) <;> (try split at h_bound) <;> (try simp_all [HNeg.hNeg, Aeneas.Std.IScalar.neg, Aeneas.Std.IScalar.inBounds]) <;> scalar_tac
/// ```
pub unsafe fn abs(x: i32) -> i32 {
if x < 0 { -x } else { x }
Expand Down
156 changes: 13 additions & 143 deletions anneal/examples/anatomy.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@
/// for this type mapping to the expression below. You can apply it in proofs
/// using `simp_all [Anneal.IsValid.isValid]`.
///
/// ```anneal
/// isValid self := self.val.val > 0
/// ```lean, anneal
/// def isValid (self : PositiveUsize) : Prop := self.val.val > 0
/// ```
pub struct PositiveUsize {
#[allow(unused)]
Expand All @@ -16,9 +16,9 @@ pub struct PositiveUsize {
///
/// In this trait, we enforce that `Self` has an alignment of exactly 1.
///
/// ```anneal
/// isSafe : ∀ {{_sz : Anneal.core.marker.Sized Self}} {{tl : Anneal.HasStaticLayout Self}},
/// tl.layout.align.val.val = 1
/// ```lean, anneal
/// def isSafe (Self : Type) [Anneal.core.marker.Sized Self] [Anneal.HasStaticLayout Self] : Prop :=
/// (Anneal.HasStaticLayout.layout Self).align.val.val = 1
/// ```
pub unsafe trait Unaligned: Sized {}

Expand All @@ -28,11 +28,9 @@ pub unsafe trait Unaligned: Sized {}
/// analyzing the body of this function, and Anneal will accept the spec
/// without proof.
///
/// ```anneal, unsafe(axiom)
/// requires: a.val + b.val <= Usize.max
/// -- In Anneal, anonymous `requires` and `ensures` bounds are compiled into
/// -- a struct field named `h_anon`.
/// ensures: ret.val = a.val + b.val
/// ```lean, anneal, unsafe(axiom)
/// axiom spec (a b : Std.Usize) (h_req : a.val + b.val ≤ Usize.max) :
/// Aeneas.Std.WP.spec (fast_add a b) (fun ret_ => ret_.val = a.val + b.val)
/// ```
#[allow(unused)]
pub unsafe fn fast_add(a: usize, b: usize) -> usize {
Expand All @@ -45,139 +43,11 @@ pub unsafe fn fast_add(a: usize, b: usize) -> usize {
/// on a trait, Anneal generates a `.Safe` predicate parameterized by the type `T`
/// and the specific trait implementation `Inst`.
///
/// ```anneal
/// requires (h_is_safe): Unaligned.Safe T Inst
/// -- Defines a post-condition named `h_align_eq`
/// ensures (h_align_eq): ret.val.val = 1
///
/// -- `proof context` is a special block in Anneal. Any `have` bindings
/// -- defined here are made available to ALL subsequent `proof (...)` blocks
/// -- for this function. It prevents duplicating common setup.
/// proof context:
/// -- We can prove the behavior of `fast_add` acting on 0 beforehand.
/// -- Notice how we fulfill the `fast_add.Pre` structure entirely inline
/// -- using `{ ... }` and `simp_all`.
/// -- `Aeneas.Std.Usize`.
/// -- * Note the `#usize` suffixes: Because memory modeling differentiates
/// -- physical sizes (`Usize`) from mathematical sizes (`Nat`), you must
/// -- suffix numerical literals to bypass typeclass resolution ambiguity.
/// have fast_add_zero : ∀ (x : Aeneas.Std.Usize), Anneal.IsValid.isValid x →
/// fast_add x 0#usize = Result.ok x := by
/// intro x h_valid
/// -- Here we supply `{ h_anon := ... }` explicitly for the anonymous `requires` bound!
/// -- Notice `h_a_is_valid`: Anneal injects implicit `h_<arg>_is_valid` preconditions
/// -- for ALL function arguments. We must fulfill them when invoking `.spec`.
/// have ho := fast_add.spec x 0#usize { h_a_is_valid := h_valid, h_anon := by scalar_tac }
/// -- CRACKING MONADIC EXECUTIONS:
/// -- To prove that `fast_add x 0` strictly returns `Result.ok x` and never `fail`/`div`,
/// -- we use `cases ... <;> simp_all`. Because the constraint `ho` requires it to succeed,
/// -- `simp_all` instantly prunes the impossible error states!
/// cases h_eq : fast_add x 0#usize <;> simp_all
/// rename_i r; have _ := ho.h_anon; scalar_tac
///
/// -- Some marker traits (like `Sized`) translates to empty typeclasses.
/// -- We can legally instantiate them with the anonymous constructor `⟨⟩`.
/// have h_sized : Anneal.core.marker.Sized T := ⟨⟩
///
/// -- However, for complex typeclasses like `HasStaticLayout`, Lean's inference
/// -- struggles with fully anonymous instantiations (e.g., `⟨_, _⟩`).
/// -- You must alias complex layouts to a named `have` binding first!
/// --
/// -- IMPORTANT ON TYPECLASS AUTOMATION:
/// -- We are manually defining `HasStaticLayout` here for demonstration scaffolding.
/// -- Standard practice dictates you should NEVER build layout traits manually.
/// -- You should rely on implicit variables (e.g. `[tl : HasStaticLayout T]`)
/// -- provided gracefully by Anneal to your theorems.
/// have h_layout : Anneal.HasStaticLayout T := {
/// layout := {
/// size := 1#usize
/// align := ⟨1#usize, by decide, 0, by rfl⟩
/// sizeAligned := by decide
/// }
/// }
///
/// -- Because `core::mem::align_of` is an external Rust call, Aeneas translates
/// -- it as an opaque axiom. Anneal detects this and injects a `_spec` theorem
/// -- tying it to `HasStaticLayout`. We explicitly pass the typeclass constraints
/// -- using `@` to bypass implicit resolution bugs.
/// have h_aspec : core.mem.align_of T = Result.ok _ :=
/// @core_mem_align_of_spec T h_sized h_layout
///
/// -- TRAIT DICTIONARIES:
/// -- Because of the `T: Unaligned` bound on our function, Aeneas passed us a
/// -- trait dictionary argument named `UnalignedInst`. We feed this dictionary
/// -- to our `h_is_safe` precondition to unlock the theorems stored inside `isSafe`!
/// have h_s := h_is_safe (Inst := UnalignedInst)
/// have h_safe_eq := h_s.isSafe (_sz := h_sized) (tl := h_layout)
///
/// --
/// -- IMPLICIT IDENTIFIERS:
/// -- Notice our use of `ret` and `h_returns`. Where did they come from?
/// -- In Orthogonal WP Proofs, Anneal automatically destructures the `Result`
/// -- of the function into variables like `ret` and `arg'`, and provides the
/// -- `h_returns : get_unaligned_fast_pad ... = ok ret` hypothesis binding them!
/// have h_fast_pad_result : ret.val.val = 1 := by
/// unfold get_unaligned_fast_pad at h_returns
/// -- When unwrapping monadic execution chains (e.g. evaluating `x = Result.ok y`),
/// -- standard rewrites fail. Always apply `rw [..., Aeneas.Std.bind_tc_ok]`!
/// rw [h_aspec, Aeneas.Std.bind_tc_ok] at h_returns
/// have h_valid : Anneal.IsValid.isValid h_layout.layout.align.val := by
/// simp_all [Anneal.IsValid.isValid]
/// rw [fast_add_zero _ h_valid, Aeneas.Std.bind_tc_ok] at h_returns
/// cases ret; simp_all
///
/// -- `h_ret_is_valid` is implicitly demanded by Anneal for all generated structures.
/// -- We can usually dispatch it trivially using `simp_all`.
/// proof (h_ret_is_valid):
/// simp_all [Anneal.IsValid.isValid]
///
/// -- A proof of `h_align_eq`
/// proof (h_align_eq):
/// simp_all
///
/// -- The `h_progress` proof is required when Anneal's `eval_progress` tactic
/// -- fails to automatically discharge the proof.
/// --
/// -- THE PROGRESS BARRIER:
/// -- Why didn't `eval_progress` just work in `h_ret_is_valid`?
/// -- `wp_prove_orthogonal` separates verification into progress and correctness.
/// -- During correctness blocks (`proof (h_ret_...)`), the WP states are destructured.
/// -- The goal state of `h_progress` is an existential equality
/// -- (`⊢ ∃ y, m = ok y`), NOT a Weakest Precondition `spec`. You cannot use
/// -- standard Aeneas `progress` macros to solve it!
/// proof (h_progress):
/// unfold get_unaligned_fast_pad
///
/// -- 1. Scaffolding for core.mem.align_of
/// have h_sized : Anneal.core.marker.Sized T := ⟨⟩
/// have h_layout : Anneal.HasStaticLayout T := {
/// layout := {
/// size := 1#usize
/// align := ⟨1#usize, by decide, 0, by rfl⟩
/// sizeAligned := by decide
/// }
/// }
/// have h_align : ∃ align, core.mem.align_of T = Result.ok align :=
/// ⟨_, @core_mem_align_of_spec T h_sized h_layout⟩
/// rcases h_align with ⟨align, h_align_eq⟩
///
/// -- 2. Scaffolding for fast_add
/// -- We bridge the gap between our generated WP `spec` constraints and the
/// -- existential progress constraint (`∃ y, ...`) using `spec_imp_exists`.
/// have h_add : ∃ padded, fast_add align 0#usize = Result.ok padded := by
/// have ho := fast_add.spec align 0#usize {
/// h_a_is_valid := by simp_all [Anneal.IsValid.isValid]
/// h_b_is_valid := by simp_all [Anneal.IsValid.isValid]
/// h_anon := by scalar_tac
/// }
/// rcases Aeneas.Std.WP.spec_imp_exists ho with ⟨padded, h_eq, _⟩
/// exact ⟨padded, h_eq⟩
/// rcases h_add with ⟨padded, h_add_eq⟩
///
/// -- 3. Conclude progress
/// -- Chain evaluated states seamlessly using `bind_tc_ok`.
/// rw [h_align_eq, Aeneas.Std.bind_tc_ok, h_add_eq, Aeneas.Std.bind_tc_ok]
/// exact ⟨_, rfl⟩
/// ```lean, anneal, spec
/// theorem spec {T : Type} (UnalignedInst : Unaligned T) (sized_inst : Anneal.core.marker.Sized T) (layout_inst : Anneal.HasStaticLayout T)
/// (h_req : Unaligned.isSafe T) :
/// Aeneas.Std.WP.spec (get_unaligned_fast_pad (T := T) (UnalignedInst := UnalignedInst)) (fun ret_ => ret_.val.val = 1) := by
/// sorry
/// ```
pub unsafe fn get_unaligned_fast_pad<T: Unaligned>() -> PositiveUsize {
let align = core::mem::align_of::<T>();
Expand Down
18 changes: 8 additions & 10 deletions anneal/examples/checked_add.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,17 +1,15 @@
/// Performs checked addition.
///
/// ```lean, anneal, spec
/// ensures: match ret with
/// | .none => (x : Int) + (y : Int) > I32.max ∨ (x : Int) + (y : Int) < I32.min
/// | .some v => (v : Int) = (x : Int) + (y : Int)
/// proof (h_anon):
/// unfold checked_add at h_returns
/// have h := Aeneas.Std.I32.checked_add_bv_spec x y
/// simp_all [Aeneas.Std.I32.checked_add]
/// cases ret <;> simp_all <;> scalar_tac
/// proof (h_progress):
/// theorem spec (x y : Std.I32) :
/// Aeneas.Std.WP.spec (checked_add x y) (fun ret_ =>
/// match ret_ with
/// | .none => (x : Int) + (y : Int) > I32.max ∨ (x : Int) + (y : Int) < I32.min
/// | .some v => (v : Int) = (x : Int) + (y : Int)) := by
/// unfold checked_add
/// simp_all
/// simp_all [Aeneas.Std.I32.checked_add]
/// have h := Aeneas.Std.I32.checked_add_bv_spec x y
/// split <;> split at h <;> simp_all <;> scalar_tac
/// ```
pub fn checked_add(x: i32, y: i32) -> Option<i32> {
x.checked_add(y)
Expand Down
18 changes: 8 additions & 10 deletions anneal/examples/const_generics.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,19 +1,17 @@
/// ```anneal
/// isValid self := N > 0
/// ```lean, anneal
/// def isValid (N : Std.Usize) : Prop := N.val > 0
/// ```
pub struct ConstGen<const N: usize>;

/// ```anneal
/// isSafe : N > 0
/// ```lean, anneal
/// def isSafe (N : Std.Usize) : Prop := N.val > 0
/// ```
pub unsafe trait ConstTrait<const N: usize> {}

/// ```anneal
/// ensures: if N.val = 0 then ret.val = 0 else True
/// proof:
/// unfold use_const at h_returns
/// split at h_returns <;> (try unfold Array.index_usize at h_returns) <;> (try split at h_returns) <;> simp_all <;> scalar_tac
/// proof (h_progress):
/// ```lean, anneal, spec
/// theorem spec {N : Std.Usize} (arr : Array Std.U8 N) :
/// Aeneas.Std.WP.spec (use_const arr) (fun ret_ =>
/// if N.val = 0 then ret_.val = 0 else True) := by
/// unfold use_const
/// split <;> (try unfold Array.index_usize) <;> (try split) <;> simp_all <;> scalar_tac
/// ```
Expand Down
70 changes: 17 additions & 53 deletions anneal/examples/design_doc.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,51 +1,37 @@
/// ```lean, anneal, unsafe(axiom)
/// requires: b.val > 0
/// ensures: ret.val = a.val / b.val
/// axiom spec (a b : Std.U32) (h_req : b.val > 0) :
/// Aeneas.Std.WP.spec (safe_div a b) (fun ret_ => ret_.val = a.val / b.val)
/// ```
#[allow(unused_unsafe)]
pub unsafe fn safe_div(a: u32, b: u32) -> u32 {
unsafe { a / b }
}

/// ```lean, anneal, spec
/// ensures: ret.val = a.val
/// proof:
/// unfold wrapper at h_returns
/// have h := safe_div.spec a 1#u32 { h_anon := by decide }
/// unfold Aeneas.Std.WP.spec at h
/// rw [h_returns] at h
/// change safe_div.Post a 1#u32 ret at h
/// rcases h with ⟨_, h_div⟩
/// change ret.val = a.val / 1 at h_div
/// simp_all [Nat.div_one]
/// proof (h_progress):
/// unfold wrapper
/// have ⟨y, hy⟩ := Aeneas.Std.WP.spec_imp_exists (safe_div.spec a 1#u32 { h_anon := by decide })
/// simp_all
/// theorem spec (a : Std.U32) :
/// Aeneas.Std.WP.spec (wrapper a) (fun ret_ => ret_.val = a.val) := by
/// sorry
/// ```
pub fn wrapper(a: u32) -> u32 {
unsafe { safe_div(a, 1) }
}

/// ```lean, anneal
/// isValid self := self.x.val % 2 = 0
/// def isValid (self : Even) : Prop := self.x.val % 2 = 0
/// ```
pub struct Even {
#[allow(dead_code)]
x: usize,
}

/// ```lean, anneal
/// isSafe : True
/// def isSafe {Self : Type} : Prop := True
/// ```
pub unsafe trait FromBytes {}

/// ```lean, anneal, spec
/// ensures: ret.val = x.val
/// proof:
/// unfold read_val at h_returns
/// simp_all
/// proof (h_progress):
/// theorem spec (x : Std.U32) :
/// Aeneas.Std.WP.spec (read_val x) (fun ret_ => ret_.val = x.val) := by
/// unfold read_val
/// simp_all
/// ```
Expand All @@ -54,41 +40,19 @@ pub fn read_val(x: &u32) -> u32 {
}

/// ```lean, anneal, spec
/// requires: x.val + add.val <= 4294967295
/// ensures: x'.val = x.val + add.val
/// proof:
/// unfold add_in_place at h_returns
/// have h := Aeneas.Std.U32.add_bv_spec (x := x) (y := add) (by scalar_tac)
/// unfold Aeneas.Std.WP.spec at h
/// try unfold Aeneas.Std.WP.theta at h
/// try unfold Aeneas.Std.WP.wp_return at h
/// simp_all
/// proof (h_progress):
/// unfold add_in_place
/// try rcases h_req with ⟨_, _, _⟩
/// have h := Aeneas.Std.U32.add_bv_spec (x := x) (y := add) (by scalar_tac)
/// have ⟨y, hy⟩ := Aeneas.Std.WP.spec_imp_exists h
/// simp_all
/// theorem spec (x : Std.U32) (add : Std.U32) (h_req : x.val + add.val ≤ 4294967295) :
/// Aeneas.Std.WP.spec (add_in_place x add) (fun ret_ => ret_.val = x.val + add.val) := by
/// sorry
/// ```
pub unsafe fn add_in_place(x: &mut u32, add: u32) {
*x += add;
}

/// ```lean, anneal
/// context:
/// open alloc.vec
/// requires: stack.length > 0#usize
/// ensures(h_len): stack'.length = stack.length - 1#usize
/// ensures(h_ret): ret = stack.index _ (stack.length - 1#usize)
/// proof (h_len):
/// unfold pop at h_returns
/// have ho := Vec.pop_spec Global stack
/// simp_all
/// proof (h_ret):
/// simp_all
/// proof (h_progress):
/// unfold pop
/// have ho := Vec.pop_spec Global stack
/// ```lean, anneal, spec
/// theorem spec (stack : alloc.vec.Vec Std.U32) (h_req : stack.length > 0#usize) :
/// Aeneas.Std.WP.spec (pop stack) (fun ret_ =>
/// let (ret, stack') := ret_
/// stack'.length = stack.length - 1#usize) := by
/// sorry
/// ```
pub unsafe fn pop(stack: &mut Vec<u32>) -> u32 {
Expand Down
Loading
Loading