From be14c6af915b865258de6631ee89a2ef81e02b49 Mon Sep 17 00:00:00 2001 From: Ryan Lahfa Date: Mon, 26 Aug 2024 16:40:36 +0200 Subject: [PATCH] chore(docs/user): empty the plan and keep a simple good example Adds the TODO list for infrastructure. Signed-off-by: Ryan Lahfa --- docs/user/TODO.md | 8 ++ docs/user/src/SUMMARY.md | 17 --- docs/user/src/lean/basics/factorial.lean | 168 +++++++++++++++++++++++ 3 files changed, 176 insertions(+), 17 deletions(-) create mode 100644 docs/user/TODO.md diff --git a/docs/user/TODO.md b/docs/user/TODO.md new file mode 100644 index 000000000..a847e8da2 --- /dev/null +++ b/docs/user/TODO.md @@ -0,0 +1,8 @@ +# TODO list for this sub-project + +## Scaffolding + +This project makes use of the Lean flake, but this flake will be soon deprecated and be development-only. + +To overcome this problem, there's a need of https://github.com/oxalica/rust-overlay but for Lean, so that release candidates and various +versions can be selected without a compilation cost by reusing Lean pre-built binaries, i.e. wrapping Lean binaries in FODs in that repository. diff --git a/docs/user/src/SUMMARY.md b/docs/user/src/SUMMARY.md index cb14fb09f..6741ea873 100644 --- a/docs/user/src/SUMMARY.md +++ b/docs/user/src/SUMMARY.md @@ -8,20 +8,3 @@ - [Getting started]() - [Factorial function](./lean/basics/factorial.lean.md) -- [Defining Binary Search Trees in Rust](./rust/bst_def.md) - - [Extracting to Lean]() - - [Panic-freedomness]() -- [Specifying Invariants in Lean]() - - [Invariants of a binary search tree](./lean/bst/invariants.md) - - [Picking mathematical representations](./lean/bst/math-repr.md) -- [Verifying `Find` Operation]() - - [What does it mean to be in a tree?](./lean/bst/set_of_values.md) - - [Dealing with Loops](./lean/bst/loops.md) - - [Applying Known Specifications: `progress` tactic](./lean/bst/progress.md) -- [Verifying Insert Operation]() - - [Dealing with Large Proofs]() - - [Dealing with Symmetry]() -- [Verifying Height Operation](./lean/bst/height.md) - - [Dealing with Termination Issues](./lean/bst/termination.md) - - [Dealing with Machine Integers: `scalar_tac` Tactic](./lean/bst/scalars.md) - - [Refining the Translation](./lean/bst/refining.md) diff --git a/docs/user/src/lean/basics/factorial.lean b/docs/user/src/lean/basics/factorial.lean index c25fa7d54..17beaf1a9 100644 --- a/docs/user/src/lean/basics/factorial.lean +++ b/docs/user/src/lean/basics/factorial.lean @@ -1,4 +1,5 @@ import Base +import Mathlib.Data.Nat.Factorial.Basic /-! @@ -26,3 +27,170 @@ divergent def factorial (n : U64) : Result U64 := n * i1 end factorial + +/-! + +We will need some lemmas on factorials lifted to ℤ and U64 +to prove theorems about factorial. + +This will be useful to introduce arithmetic work in Aeneas. + +First, we would like to prove that the factorial of natural number as integers possess +the recursive property of factorials. +-/ + +lemma Int.mul_factorial_pred: ∀ {n: ℤ}, 0 < n → n * (n - 1).toNat.factorial = n.toNat.factorial := by + intro n n_pos + -- This is a generic tactic to lift types to another types while discharging conditions, e.g. positivity, etc. + lift (n: ℤ) to ℕ + -- `omega` is another generic tactic to close arithmetic goals automatically, `linarith` is another option + -- for linear arithmetic. + omega + -- `simp` here is used as a normalization tactic, then we normalize the casts themselves + -- and finally, we use the natural number version of the recursive property. + -- `exact_mod_cast` is a "here's the term modulo casts" tactic. + simp; norm_cast; exact Nat.mul_factorial_pred (by exact_mod_cast n_pos) + + +lemma U64.mul_factorial_pred: ∀ {n: U64}, 0#u64 < n → (n: ℤ) * (n.toNat - 1).factorial = n.toNat.factorial := by + intro n n_pos + -- `convert` is a "here's the term, please match it as much as you can and let me discharge the differences". + convert (Int.mul_factorial_pred _) + . simp + . scalar_tac + +/-! + +We will need a mathematical theorem relating machine integers +as Rust cannot compute factorials larger than 2^64 - 1 using u64s. + +As factorial is a nice function, i.e. is increasing, we can just reduce +the proof to proving that our domain's max value fits in a U64, i.e. 20! ≤ 2^64 - 1. + +In Lean, certain goals can be "decided", e.g. we can just use a fast algorithm +to produce a proof certificate that something is true. +-/ +theorem factorial_bounds: ∀ {n: ℕ}, n ≤ 20 → n.factorial ≤ U64.max := by + intro n n_pos + -- Our strategy will be to write this in ℕ to reuse natural number theorems. + rw [U64.max] + norm_cast + -- We use transitivity of ≤ to use the natural number theorem _and_ decision. + transitivity + . exact Nat.factorial_le n_pos + . decide + +/-! + +We define a restricted scalar factorial to U64. +To construct a scalar, we need to prove that it fits both of the ends of the scalar. +For unsigned scalar, we only need to prove positivity _and_ it fits the max. + +We leave the problem to `scalar_tac`, an Aeneas tactic that performs pre-processing step +and knows facts about scalars to discharge scalar-related goals. This tactic calls internally `omega`, +so it is _at least_ powerful as `omega`. + +For the upper-bound, we reuse our just-proven theorem. +-/ +def scalar_factorial {n: ℕ} (bounds: n ≤ 20): U64 := + Scalar.ofIntCore n.factorial ⟨ by scalar_tac, factorial_bounds bounds ⟩ + +/-! + +We are ready to create the specification of factorial. + +That is, under the precondition of having an integer smaller than 20, the Rust's extracted factorial function +coincides with the theoretical scalar factorial function lifted from the mathematical scalar factorial function. + +Nonetheless, we will not be able to finish the formalization with the proposed signature. + +`@[pspec]`, a decorator, marks the following theorem as a specification, which can be searched by Aeneas tactics on specifications. +-/ + +@[pspec] +theorem factorial_spec_mistaken: ∀ (n: ℕ), + (bounds: n ≤ 20) → + -- We cast the input natural number it in a scalar. + factorial.factorial (Scalar.ofIntCore n ⟨ by scalar_tac, by scalar_tac ⟩) = Result.ok (scalar_factorial bounds) := by + intro n bounds + -- We unfold the Rust definition. + rw [factorial.factorial] + -- Distinguish the trivial case and the complicated case. + by_cases hzero : n = 0 + . + -- We let Lean reduce this to a trivial equation. + simp [hzero, scalar_factorial] + . + -- We simplify the branching using our negation hypothesis. + simp [hzero] + /- + Here, we need to reuse a specification on scalar substraction regarding `n - 1` + `k` will be the new integer in the context and `Hk` the term that links `k` + to its value. + This specification can be discovered automatically and pasted by `progress?`. + `progress` is one of the Aeneas tactics on specifications. + -/ + progress with Primitives.U64.sub_spec as ⟨ k, Hk ⟩ + -- We have a problem here, the goal ask us to reuse our specification + -- but with a `k`, not with a `Scalar.ofIntCore ...` + -- rw [Hk] + -- progress with factorial_spec + stop + +/-! +In general, specifications in Aeneas are written with an existential-style, that is, we will write there's a result +to some operation and we will attach additional conditions to the value of the result. + +This avoids to depend on things like proofs of boundness of a given scalar which could be arbitrary. + +Here's a fixed proposal. +-/ + +@[pspec] +theorem factorial_spec: ∀ (n: U64), (bounds: n.val ≤ 20) → ∃ v, factorial.factorial n = Result.ok v ∧ v.val = n.val.toNat.factorial := by + intro n bounds + rw [factorial.factorial] + by_cases hzero : n = 0#u64 + . + -- We let Lean reduce this to a trivial equation. + simp [hzero, scalar_factorial] + . + -- We simplify the branching using our negation hypothesis. + simp [hzero] + -- Here, we need to reuse a specification on scalar substraction regarding `n - 1` + -- `k` will be the new integer in the context and `Hk` the term that links `k` + -- to its value. + -- This specification can be discovered automatically and pasted by `progress?`. + progress with Primitives.U64.sub_spec as ⟨ k, Hk ⟩ + -- Here, we have the recursive call to `factorial` + -- Lean will figure out automatically that calling ourselves with a smaller argument + -- is sufficient to prove termination of this specification proof. + progress with factorial_spec as ⟨ p, Hp ⟩ + -- We still need to prove that np is a valid U64 scalar + -- and its value is what is expected. + progress with Primitives.U64.mul_spec as ⟨ y, Hy ⟩ + -- We replace our collected equalities in the previous progresses. + . + rw [Hp, Hk] + -- We do various wrangling with the equalities to simplify + -- their casts, their form, remove the definitions (U64.max). + simp only [Scalar.ofInt_val_eq, Int.pred_toNat] + -- We leave it to Aeneas automation to discharge the non-negativity of the scalar. + rw [U64.mul_factorial_pred (by scalar_tac)] + simp only [U64.toNat] + -- Our original bound live in ℤ, we need it in ℕ, let's lift it quickly. + have bounds' : n.toNat ≤ 20 := by { + -- Let's lift the goal, i.e. the inequality in ℕ, to ℤ and conclude immediately. + zify; simp [bounds] + } + exact factorial_bounds bounds' + . rw [Hy, Hp, Hk] + simp only [Scalar.ofInt_val_eq, Int.pred_toNat] + rw [U64.mul_factorial_pred (by scalar_tac)] +-- We need to prove that we are calling the specification with a smaller scalar. +-- Let's prove it over the cast to natural numbers. +termination_by n => n.val.toNat +decreasing_by + simp_wf -- We simplify the well-founded relation definition. + rw [Hk] -- Inject the definition of `k`. + simp -- Let a Lean tactic conclude trivially.