Add a conference tutorial (#299)

* Start working on the tutorial * Improve scalar_tac, progress, introduce delaboration for scalars and work on the tutorial * Remove List.len and use List.length instead * Start working on a bignum library for the tutorial * Add some missing changes * Add support for scalar negation * Add missing files for the tutorial * Update the charon pin * Add alloc.vec.Vec.resize in the Lean library * Update the code for the bignums * Update progress to use simp on the preconditions * Add definition for overflowing_add to the Lean library * Make the trait implementations reducible * Regenerate the files * Update progress to better control the instantiation of meta-variables If there are meta-variables in a precondition, progress will apply an assumption (which instantiates the meta-variables) only if there is a unique assumption matching the precondition. * Improve progress a bit * Fix issues in Primitives.{v,fst} * Make good progress on the tutorial * Make minor modifications to scalar_tac * Fix the proofs of the hashmap * Regenerate the files * Start working on a forward saturation function * Make good progress on the forward saturation function * Add a missing file * Add tactics to normalize scalar goals * Improve the saturation tactic to allow erasing rules and using local rules * Print more informative error messages when saturation patterns are not valid * Drastically improve scalar_tac * Update the proofs in the tutorial * Move and update lemmas * Start replacing the List functions which use integers * Finish replacing the list functions in the Lean library * Start updating the examples * Update the proofs of the hashmap * Update the BaseTutorial * Reduce the proof time of the hashmap and the AVL * Update the tutorial * Make minor modifications * Introduce a dcases tactic and update the tutorial * Fix an issue with the Primitives.fst file * Finish the tutorial * Fix an issue with the tutorial * Fix an issue with Primitives.v * Make minor modifications * Make more minor modifications
AeneasVerif · Aug 19, 2024 · b1ca1ff · b1ca1ff
1 parent b92ed2a
commit b1ca1ff
Show file tree

Hide file tree

Showing 80 changed files with 5,896 additions and 2,497 deletions.
diff --git a/README.md b/README.md
@@ -114,7 +114,7 @@ support for partial functions and extrinsic proofs of termination (see
 and tactics specialized for monadic programs (see
 `./backends/lean/Base/Progress/Progress.lean` and `./backends/hol4/primitivesLib.sml`).
 
-A tutorial for the Lean backend is available [here](./tests/lean/Tutorial.lean).
+A (basic) tutorial for the Lean backend is available [here](./tests/lean/BaseTutorial.lean).
 
 ## Quick start for Nix users
 

diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
@@ -254,11 +254,12 @@ Definition scalar_rem {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty
 
 Definition scalar_neg {ty} (x: scalar ty) : result (scalar ty) := mk_scalar ty (-(to_Z x)).
 
-Axiom scalar_xor : forall ty, scalar ty -> scalar ty -> scalar ty. (* TODO *)
-Axiom scalar_or : forall ty, scalar ty -> scalar ty -> scalar ty. (* TODO *)
-Axiom scalar_and : forall ty, scalar ty -> scalar ty -> scalar ty. (* TODO *)
-Axiom scalar_shl : forall ty0 ty1, scalar ty0 -> scalar ty1 -> result (scalar ty0). (* TODO *)
-Axiom scalar_shr : forall ty0 ty1, scalar ty0 -> scalar ty1 -> result (scalar ty0). (* TODO *)
+Axiom scalar_xor : forall {ty}, scalar ty -> scalar ty -> scalar ty. (* TODO *)
+Axiom scalar_or : forall {ty}, scalar ty -> scalar ty -> scalar ty. (* TODO *)
+Axiom scalar_and : forall {ty}, scalar ty -> scalar ty -> scalar ty. (* TODO *)
+Axiom scalar_shl : forall {ty0 ty1}, scalar ty0 -> scalar ty1 -> result (scalar ty0). (* TODO *)
+Axiom scalar_shr : forall {ty0 ty1}, scalar ty0 -> scalar ty1 -> result (scalar ty0). (* TODO *)
+Axiom scalar_not : forall {ty}, scalar ty -> scalar ty. (* TODO *)
 
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
 (* TODO: check the semantics of casts in Rust *)
@@ -288,7 +289,6 @@ Definition scalar_eqb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool :=
 Definition scalar_neqb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool :=
   negb (Z.eqb (to_Z x) (to_Z y)) .
 
-
 (** The scalar types *)
 Definition isize := scalar Isize.
 Definition i8    := scalar I8.
@@ -451,6 +451,20 @@ Definition i64_shr {ty} := @scalar_shr I64 ty.
 Definition i128_shr {ty} := @scalar_shr I128 ty.
 Definition isize_shr {ty} := @scalar_shr Isize ty.
 
+(** Not *)
+Definition u8_not := @scalar_not U8.
+Definition u16_not := @scalar_not U16.
+Definition u32_not := @scalar_not U32.
+Definition u64_not := @scalar_not U64.
+Definition u128_not := @scalar_not U128.
+Definition usize_not := @scalar_not Usize.
+Definition i8_not := @scalar_not I8.
+Definition i16_not := @scalar_not I16.
+Definition i32_not := @scalar_not I32.
+Definition i64_not := @scalar_not I64.
+Definition i128_not := @scalar_not I128.
+Definition isize_not := @scalar_not Isize.
+
 (** Small utility *)
 Definition usize_to_nat (x: usize) : nat := Z.to_nat (to_Z x).
 

diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
@@ -267,6 +267,8 @@ let scalar_shr (#ty0 #ty1 : scalar_ty)
     (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) =
   admit()
 
+let scalar_not #ty (x : scalar ty) : scalar ty = admit()
+
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
 // TODO: check the semantics of casts in Rust
 let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
@@ -465,6 +467,20 @@ let i64_shr #ty = scalar_shr #I64 #ty
 let i128_shr #ty = scalar_shr #I128 #ty
 let isize_shr #ty = scalar_shr #Isize #ty
 
+/// Not
+let u8_not = scalar_not #U8
+let u16_not = scalar_not #U16
+let u32_not = scalar_not #U32
+let u64_not = scalar_not #U64
+let u128_not = scalar_not #U128
+let usize_not = scalar_not #Usize
+let i8_not = scalar_not #I8
+let i16_not = scalar_not #I16
+let i32_not = scalar_not #I32
+let i64_not = scalar_not #I64
+let i128_not = scalar_not #I128
+let isize_not = scalar_not #Isize
+
 (*** core *)
 
 /// Trait declaration: [core::clone::Clone]

diff --git a/backends/lean/Base.lean b/backends/lean/Base.lean
@@ -1,8 +1,9 @@
 import Base.Arith
 import Base.Diverge
-import Base.IList
+import Base.List
 import Base.Primitives
 import Base.Progress
 import Base.SimpLemmas
 import Base.Utils
+import Base.Saturate
 import Base.Termination
diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean
@@ -1,3 +1,4 @@
 import Base.Arith.Int
-import Base.Arith.Scalar
 import Base.Arith.Lemmas
+import Base.Arith.Scalar
+import Base.Arith.ScalarNF
diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean
@@ -68,4 +68,43 @@ theorem to_int_sub_to_nat_lt (x y : ℤ) (x' : ℕ)
 -- righ-hand side, meaning the rewriting can be applied to `n` itself.
 theorem ofNat_instOfNatNat_eq (n : Nat) : @OfNat.ofNat Nat n (instOfNatNat n) = n := by rfl
 
+
+/-- Small helper
+
+    We used to use this for the list definitions, as some definitions like `index` used to
+    manipulate integers and not natural numbers.
+
+    We cover a set of cases which might imply inequality, to make sure that using
+    this as the precondition of a `simp` lemma will allow the lemma to get correctly
+    triggered.
+    TODO: there should be something more systematic to do, with discharged procedures
+    or simprocs I guess. -/
+@[simp]
+abbrev Int.not_eq (i j : Int) : Prop :=
+  i ≠ j ∨ j ≠ i ∨ i < j ∨ j < i
+
+theorem Int.not_eq_imp_not_eq {i j} : Int.not_eq i j → i ≠ j := by
+  intro h g
+  simp_all
+
+@[simp]
+abbrev Nat.not_eq (i j : Nat) : Prop :=
+  i ≠ j ∨ j ≠ i ∨ i < j ∨ j < i
+
+theorem Nat.not_eq_imp_not_eq {i j} : Nat.not_eq i j → i ≠ j := by
+  intro h g
+  simp_all
+
+@[simp]
+theorem Nat.le_imp_le_equiv_eq (i j : Nat) (h0 : i ≤ j) : j ≤ i ↔ i = j := by
+  omega
+
+@[simp]
+theorem Int.le_imp_le_equiv_eq (i j : Int) (h0 : i ≤ j) : j ≤ i ↔ i = j := by
+  omega
+
+example (i : Int) (j : Nat) (h : i ≤ j) (h2 : j ≤ i) :
+  i = j := by
+  simp_all
+
 end Arith
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
@@ -7,6 +7,7 @@ import Mathlib.Tactic.Ring.RingNF
 import Base.Utils
 import Base.Arith.Base
 import Base.Arith.Init
+import Base.Saturate
 
 namespace Arith
 
@@ -17,6 +18,10 @@ open Lean Lean.Elab Lean.Meta Lean.Elab.Tactic
 
 attribute [aesop (rule_sets := [Aeneas.ScalarTac]) unfold norm] Function.comp
 
+/-
+-- DEPRECATED: `int_tac` and `scalar_tac` used to rely on `aesop`. As there are performance issues
+-- with the saturation tactic for now we use our own tactic. We will revert once the performance
+-- is improved.
 /-- The `int_tac` attribute used to tag forward theorems for the `int_tac` and `scalar_tac` tactics. -/
 macro "int_tac" pat:term : attr =>
   `(attr|aesop safe forward (rule_sets := [$(Lean.mkIdent `Aeneas.ScalarTac):ident]) (pattern := $pat))
@@ -28,6 +33,19 @@ macro "scalar_tac" pat:term : attr =>
 /-- The `nonlin_scalar_tac` attribute used to tag forward theorems for the `int_tac` and `scalar_tac` tactics. -/
 macro "nonlin_scalar_tac" pat:term : attr =>
   `(attr|aesop safe forward (rule_sets := [$(Lean.mkIdent `Aeneas.ScalarTacNonLin):ident]) (pattern := $pat))
+-/
+
+/-- The `int_tac` attribute used to tag forward theorems for the `int_tac` and `scalar_tac` tactics. -/
+macro "int_tac" pat:term : attr =>
+  `(attr|aeneas_saturate (set := $(Lean.mkIdent `Aeneas.ScalarTac)) (pattern := $pat))
+
+/-- The `scalar_tac` attribute used to tag forward theorems for the `int_tac` and `scalar_tac` tactics. -/
+macro "scalar_tac" pat:term : attr =>
+  `(attr|aeneas_saturate (set := $(Lean.mkIdent `Aeneas.ScalarTac)) (pattern := $pat))
+
+/-- The `nonlin_scalar_tac` attribute used to tag forward theorems for the `int_tac` and `scalar_tac` tactics. -/
+macro "nonlin_scalar_tac" pat:term : attr =>
+  `(attr|aeneas_saturate (set := $(Lean.mkIdent `Aeneas.ScalarTacNonLin)) (pattern := $pat))
 
 -- This is useful especially in the termination proofs
 attribute [scalar_tac a.toNat] Int.toNat_eq_max
@@ -73,72 +91,81 @@ def intTacSimpRocs : List Name := [``Int.reduceNegSucc, ``Int.reduceNeg]
 
 /-- Apply the scalar_tac forward rules -/
 def intTacSaturateForward : Tactic.TacticM Unit := do
+  /-
   let options : Aesop.Options := {}
   -- Use a forward max depth of 0 to prevent recursively applying forward rules on the assumptions
   -- introduced by the forward rules themselves.
-  let options ← options.toOptions' (some 0)
+  let options ← options.toOptions' (some 0)-/
   -- We always use the rule set `Aeneas.ScalarTac`, but also need to add other rule sets locally
   -- activated by the user. The `Aeneas.ScalarTacNonLin` rule set has a special treatment as
   -- it is activated through an option.
   let ruleSets :=
     let ruleSets := `Aeneas.ScalarTac :: (← scalarTacRuleSets.get)
     if scalarTac.nonLin.get (← getOptions) then `Aeneas.ScalarTacNonLin :: ruleSets
     else ruleSets
-  evalAesopSaturate options ruleSets.toArray
+  -- TODO
+  -- evalAesopSaturate options ruleSets.toArray
+  Saturate.evalSaturate ruleSets
+
+-- For debugging
+elab "int_tac_saturate" : tactic =>
+  intTacSaturateForward
 
-/- Boosting a bit the `omega` tac.
+/-  Boosting a bit the `omega` tac.
+
+    - `extraPrePreprocess`: extra-preprocessing to be done *before* this preprocessing
+    - `extraPreprocess`: extra-preprocessing to be done *after* this preprocessing
  -/
-def intTacPreprocess (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM Unit := do
+def intTacPreprocess (extraPrePreprocess extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM Unit := do
   Tactic.withMainContext do
+  -- Pre-preprocessing
+  extraPrePreprocess
   -- Apply the forward rules
   intTacSaturateForward
   -- Extra preprocessing
   extraPreprocess
   -- Reduce all the terms in the goal - note that the extra preprocessing step
-  -- might have proven the goal, hence the `Tactic.allGoals`
+  -- might have proven the goal, hence the `allGoals`
   let dsimp :=
-    Tactic.allGoals do tryTac (
+    allGoalsNoRecover do tryTac (
       -- We set `simpOnly` at false on purpose.
-      dsimpAt false {} intTacSimpRocs
+      -- Also, we need `zetaDelta` to inline the let-bindings (otherwise, omega doesn't always manages
+      -- to deal with them)
+      dsimpAt false {zetaDelta := true} intTacSimpRocs
         -- Declarations to unfold
         []
         -- Theorems
         []
         [] Tactic.Location.wildcard)
   dsimp
   -- More preprocessing: apply norm_cast to the whole context
-  Tactic.allGoals (Utils.tryTac (Utils.normCastAtAll))
+  allGoalsNoRecover (Utils.tryTac (Utils.normCastAtAll))
   -- norm_cast does weird things with negative numbers so we reapply simp
   dsimp
-  -- Int.subNatNat is very annoying - TODO: there is probably something more general thing to do
-  Utils.tryTac (
+  allGoalsNoRecover do Utils.tryTac (
     Utils.simpAt true {}
                -- Simprocs
                []
                -- Unfoldings
                []
                 -- Simp lemmas
-                [``Int.subNatNat_eq_coe]
+                [-- Int.subNatNat is very annoying - TODO: there is probably something more general thing to do
+                 ``Int.subNatNat_eq_coe,
+                 -- We also need this, in case the goal is: ¬ False
+                 ``not_false_eq_true]
                 -- Hypotheses
                 [] .wildcard)
-  -- We also need this, in case the goal is: ¬ False
-  Tactic.allGoals do tryTac (
-    Utils.simpAt true {}
-               -- Simprocs
-               intTacSimpRocs
-               -- Unfoldings
-               []
-                -- Simp lemmas
-                [``not_false_eq_true]
-                -- Hypotheses
-                []
-                (.targets #[] true)
-  )
 
 elab "int_tac_preprocess" : tactic =>
-  intTacPreprocess (do pure ())
+  intTacPreprocess (do pure ()) (do pure ())
 
-def intTac (tacName : String) (splitGoalConjs : Bool) (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM Unit := do
+/-- - `splitAllDisjs`: if true, also split all the matches/if then else in the context (note that
+      `omega` splits the *disjunctions*)
+    - `splitGoalConjs`: if true, split the goal if it is a conjunction so as to introduce one
+      subgoal per conjunction.
+-/
+def intTac (tacName : String) (splitAllDisjs splitGoalConjs : Bool)
+  (extraPrePreprocess extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM Unit := do
   Tactic.withMainContext do
   Tactic.focus do
   let g ← Tactic.getMainGoal
@@ -148,19 +175,50 @@ def intTac (tacName : String) (splitGoalConjs : Bool) (extraPreprocess :  Tactic
   Tactic.setGoals [g]
   -- Preprocess - wondering if we should do this before or after splitting
   -- the goal. I think before leads to a smaller proof term?
-  Tactic.allGoals (intTacPreprocess extraPreprocess)
+  allGoalsNoRecover (intTacPreprocess extraPrePreprocess extraPreprocess)
   -- Split the conjunctions in the goal
-  if splitGoalConjs then Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
-  -- Call omega
-  Tactic.allGoals do
-    try do Tactic.Omega.omegaTactic {}
+  if splitGoalConjs then allGoalsNoRecover (Utils.repeatTac Utils.splitConjTarget)
+  /- If we split the disjunctions, split then use simp_all. Otherwise only use simp_all.
+     Note that simp_all is very useful here as a "congruence" procedure. Note however that we
+     only activate a very restricted set of simp lemmas (otherwise it can be very expensive,
+     and have surprising behaviors). -/
+  allGoalsNoRecover do
+    try do
+      let simpThenOmega := do
+        /- IMPORTANT: we put a quite low number for `maxSteps`.
+           There are two reasons.
+           First, `simp_all` seems to loop at times, so by controling the maximum number of steps
+           we make sure it doesn't exceed the maximum number of heart beats (or worse, overflows the
+           stack).
+           Second, this makes the tactic very snappy.
+         -/
+        Utils.tryTac (
+          -- TODO: is there a simproc to simplify propositional logic?
+          Utils.simpAll {failIfUnchanged := false, maxSteps := 75} true [``reduceIte] []
+            [``and_self, ``false_implies, ``true_implies, ``Prod.mk.injEq, ``not_false_eq_true,
+             ``true_and, ``and_true, ``false_and, ``and_false, ``true_or, ``or_true,
+             ``false_or, ``or_false] [])
+        allGoalsNoRecover (do
+          trace[Arith] "Goal after simplification: {← getMainGoal}"
+          Tactic.Omega.omegaTactic {})
+      if splitAllDisjs then do
+        /- In order to improve performance, we first try to prove the goal without splitting. If it
+           fails, we split. -/
+        try
+          trace[Arith] "First trying to solve the goal without splitting"
+          simpThenOmega
+        catch _ =>
+          trace[Arith] "First attempt failed: splitting the goal and retrying"
+          splitAll (allGoalsNoRecover simpThenOmega)
+      else
+        simpThenOmega
     catch _ =>
       let g ← Tactic.getMainGoal
-      throwError "{tacName} failed to prove the goal below.\n\nNote that {tacName} is equivalent to:\n  {tacName}_preprocess; omega\n\nGoal: \n{g}"
+      throwError "{tacName} failed to prove the goal below.\n\nNote that {tacName} is equivalent to:\n  {tacName}_preprocess; split_all <;> simp_all only <;> omega\n\nGoal: \n{g}"
 
 elab "int_tac" args:(" split_goal"?): tactic =>
-  let split := args.raw.getArgs.size > 0
-  intTac "int_tac" split (do pure ())
+  let splitConjs := args.raw.getArgs.size > 0
+  intTac "int_tac" true splitConjs (do pure ()) (do pure ())
 
 -- For termination proofs
 syntax "int_decr_tac" : tactic
@@ -177,6 +235,9 @@ macro_rules
 example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y := by
   int_tac split_goal
 
+--example (x y : Int) : x + y ≥ 2 := by
+--  int_tac split_goal
+
 -- Checking that things happen correctly when there are several disjunctions
 example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y ∧ x + y ≥ 2 := by
   int_tac split_goal
@@ -198,4 +259,8 @@ example (x y : Int) (h : x + y = 3) :
   intro z
   omega
 
+-- Checking that we manage to split the cases/if then else
+example (x : Int) (b : Bool) (h : if b then x ≤ 0 else x ≤ 0) : x ≤ 0 := by
+  int_tac
+
 end Arith