diff --git a/clang/lib/Verify/Backend/LeanBackend.cpp b/clang/lib/Verify/Backend/LeanBackend.cpp index 98eda10f5b..25c590fa63 100644 --- a/clang/lib/Verify/Backend/LeanBackend.cpp +++ b/clang/lib/Verify/Backend/LeanBackend.cpp @@ -25,6 +25,10 @@ static thread_local std::map LeanTemporaryNames; static thread_local const LogicExpr *LeanTemporaryRoot = nullptr; static thread_local const LogicFunctionDecl *LeanActiveDefinition = nullptr; static thread_local unsigned LeanActiveDefinitionDepth = 0; +// Printing a spec's own definition for Lean to accept by well-founded +// recursion: every condition that reaches an application is a hypothesis +// there (`if _h : c`), so that the decrease can be proved from it. +static thread_local bool LeanDefinitionMode = false; static bool needsLeanNameEncoding(llvm::StringRef Name) { static const std::set Keywords = { @@ -108,6 +112,8 @@ static void printLeanCommentText(llvm::StringRef Text, llvm::raw_ostream &OS) { } } +// A sequence is a list, a set its membership test, a multiset its counts, +// and a map the value at each key it holds (CppVerify/Prelude.lean). static void printLeanSort(const LogicSort &Sort, llvm::raw_ostream &OS) { switch (Sort.Kind) { case LogicSortKind::Bool: @@ -123,17 +129,83 @@ static void printLeanSort(const LogicSort &Sort, llvm::raw_ostream &OS) { case LogicSortKind::Heap: OS << "CppHeap"; return; - case LogicSortKind::Invalid: case LogicSortKind::Seq: + OS << "List Int"; + return; case LogicSortKind::Set: + OS << "(Int → Bool)"; + return; case LogicSortKind::Multiset: + OS << "(Int → Nat)"; + return; case LogicSortKind::Map: + OS << "(Int → Option Int)"; + return; + case LogicSortKind::Invalid: LeanEmissionFailed = true; OS << "False"; return; } } +// The prelude's function for each collection operation. +static const char *leanCollectionName(LogicCollectionOp Operation) { + using Op = LogicCollectionOp; + switch (Operation) { + case Op::SeqEmpty: + return "cppSeqEmpty"; + case Op::SeqUnit: + return "cppSeqUnit"; + case Op::SeqLength: + return "cppSeqLength"; + case Op::SeqIndex: + return "cppSeqAt"; + case Op::SeqPush: + return "cppSeqPush"; + case Op::SeqSubrange: + return "cppSeqSubrange"; + case Op::SeqConcat: + return "cppSeqConcat"; + case Op::SeqContains: + return "cppSeqContains"; + case Op::SetEmpty: + return "cppSetEmpty"; + case Op::SetInsert: + return "cppSetInsert"; + case Op::SetRemove: + return "cppSetRemove"; + case Op::SetContains: + return "cppSetContains"; + case Op::SetUnion: + return "cppSetUnion"; + case Op::SetIntersect: + return "cppSetIntersect"; + case Op::SetDifference: + return "cppSetDifference"; + case Op::SetSubset: + return "cppSetSubset"; + case Op::MultisetEmpty: + return "cppMultisetEmpty"; + case Op::MultisetInsert: + return "cppMultisetInsert"; + case Op::MultisetRemove: + return "cppMultisetRemove"; + case Op::MultisetCount: + return "cppMultisetCount"; + case Op::MapEmpty: + return "cppMapEmpty"; + case Op::MapInsert: + return "cppMapInsert"; + case Op::MapRemove: + return "cppMapRemove"; + case Op::MapContains: + return "cppMapContains"; + case Op::MapGet: + return "cppMapGet"; + } + return nullptr; +} + static void collectLeanVariables(const LogicExpr *E, std::set Bound, std::map &Variables) { @@ -237,6 +309,16 @@ static const LogicFunctionDecl *findLeanFunction(llvm::StringRef Identity) { return It == LeanLogicFunctions->end() ? nullptr : &It->second; } +static bool leanAppliesSpec(const LogicExpr *E) { + if (!E) + return false; + if (E->K == VCExpr::SpecCall) + return true; + return llvm::any_of(E->Children, [](const auto &Child) { + return leanAppliesSpec(Child.get()); + }); +} + static void printLeanNativeSpecCall(const LogicExpr *Call, const LogicFunctionDecl &Function, llvm::raw_ostream &OS) { @@ -309,8 +391,33 @@ static void printVCExprLean(const VCExpr *E, llvm::raw_ostream &OS, printVCExprLean(E->Children[0].get(), OS, LeanArgument); }); break; - // Right-associative: only the last operand may be of the same level. + // Right-associative: only the last operand may be of the same level. In a + // definition, the operands before an application are its condition: + // `a ∧ b` is `if _h : a then b else False`. case VCExpr::And: + if (LeanDefinitionMode) + for (unsigned I = 1; I < E->Children.size(); ++I) + if (leanAppliesSpec(E->Children[I].get())) { + paren(LeanTop, [&] { + OS << "if _h : "; + for (unsigned J = 0; J < I; ++J) { + if (J) + OS << " ∧ "; + printVCExprLean(E->Children[J].get(), OS, + J + 1 == I ? LeanAnd : LeanAnd + 1); + } + OS << " then "; + for (unsigned J = I; J < E->Children.size(); ++J) { + if (J != I) + OS << " ∧ "; + printVCExprLean(E->Children[J].get(), OS, + J + 1 == E->Children.size() ? LeanAnd + : LeanAnd + 1); + } + OS << " else False"; + }); + return; + } paren(LeanAnd, [&] { for (unsigned I = 0; I < E->Children.size(); ++I) { if (I) @@ -320,7 +427,31 @@ static void printVCExprLean(const VCExpr *E, llvm::raw_ostream &OS, } }); break; + // `a ∨ b` is `if _h : a then True else b`, and `¬a ∨ b` is `if _h : a then b + // else True`. case VCExpr::Or: + if (LeanDefinitionMode && E->Children.size() > 1 && + llvm::any_of(llvm::drop_begin(E->Children), [](const auto &Child) { + return leanAppliesSpec(Child.get()); + })) { + paren(LeanTop, [&] { + const LogicExpr *First = E->Children[0].get(); + const bool Negated = First->K == VCExpr::Not; + OS << "if _h : "; + printVCExprLean(Negated ? First->Children[0].get() : First, OS, + LeanTop); + OS << (Negated ? " then " : " then True else "); + for (unsigned J = 1; J < E->Children.size(); ++J) { + if (J != 1) + OS << " ∨ "; + printVCExprLean(E->Children[J].get(), OS, + J + 1 == E->Children.size() ? LeanOr : LeanOr + 1); + } + if (Negated) + OS << " else True"; + }); + break; + } paren(LeanOr, [&] { for (unsigned I = 0; I < E->Children.size(); ++I) { if (I) @@ -332,7 +463,7 @@ static void printVCExprLean(const VCExpr *E, llvm::raw_ostream &OS, break; case VCExpr::Ite: paren(LeanTop, [&] { - OS << "if "; + OS << (LeanDefinitionMode ? "if _h : " : "if "); printVCExprLean(E->Children[0].get(), OS, LeanTop); OS << " then "; printVCExprLean(E->Children[1].get(), OS, LeanTop); @@ -535,10 +666,25 @@ static void printVCExprLean(const VCExpr *E, llvm::raw_ostream &OS, printVCExprLean(E->Children[3].get(), OS, LeanArgument); OS << ")"; break; - case VCExpr::Collection: - LeanEmissionFailed = true; - OS << "False"; + case VCExpr::Collection: { + const char *Name = leanCollectionName(E->CollectionOp); + if (!Name) { + LeanEmissionFailed = true; + OS << "False"; + break; + } + if (E->Children.empty()) { + OS << Name; + break; + } + OS << "(" << Name; + for (const auto &Child : E->Children) { + OS << " "; + printVCExprLean(Child.get(), OS, LeanArgument); + } + OS << ")"; break; + } case VCExpr::HeapFrame: OS << "(∀ ("; printLeanName("__frame_address", OS); @@ -575,6 +721,12 @@ static void printVCExprLean(const VCExpr *E, llvm::raw_ostream &OS, printVCExprLean(E->Children[0].get(), OS, LeanTop); return; } + // In a definition, the range of an existential that applies a spec + // is its condition, as a universal's is its antecedent. + const bool Guarded = E->K == VCExpr::Exists && LeanDefinitionMode && + leanAppliesSpec(E->Children[2].get()); + if (Guarded) + OS << "if _h : "; printVCExprLean(E->Children[0].get(), OS, LeanCompare + 1); OS << " ≤ "; printLeanName(E->Binder, OS); @@ -582,6 +734,12 @@ static void printVCExprLean(const VCExpr *E, llvm::raw_ostream &OS, printLeanName(E->Binder, OS); OS << " < "; printVCExprLean(E->Children[1].get(), OS, LeanCompare + 1); + if (Guarded) { + OS << " then "; + printVCExprLean(E->Children[2].get(), OS, LeanTop); + OS << " else False"; + return; + } OS << (E->K == VCExpr::Forall ? " → " : " ∧ "); printVCExprLean(E->Children[2].get(), OS, E->K == VCExpr::Forall ? LeanArrow : LeanAnd); @@ -1033,25 +1191,130 @@ static void emitLeanGoalDefinition(llvm::StringRef Name, const LogicExpr *Goal, emitLeanReadableGoal(Name, Goal, Variables, HasSpecAxioms, *Intros, OS); } -static void -emitLeanFunctionDeclarations(const ObligationModule &Module, - llvm::raw_ostream &OS, - std::set &EmittedFunctions) { - for (const auto &[Identity, Function] : Module.LogicFunctions) { - if (!EmittedFunctions.insert(Identity).second) +static void collectLeanApplied(const LogicExpr *E, + std::set &Applied) { + if (!E) + return; + if (E->K == VCExpr::SpecCall) + Applied.insert(E->SpecCallee); + for (const auto &Child : E->Children) + collectLeanApplied(Child.get(), Applied); +} + +static std::string leanOpaqueSpec(const LogicFunctionDecl &Function) { + std::string Text; + llvm::raw_string_ostream OS(Text); + OS << "/- spec function: "; + printLeanCommentText(Function.DisplayName, OS); + OS << " -/\n"; + OS << "opaque "; + printLeanSpecName(Function.Identity, OS); + OS << " : "; + for (const LogicFunctionParameter &Parameter : Function.Parameters) { + printLeanSort(Parameter.Sort, OS); + OS << " -> "; + } + printLeanSort(Function.ResultSort, OS); + OS << "\n\n"; + return Text; +} + +// A spec's own definition, for Lean to accept by well-founded recursion: its +// step definition, applying its recursion group by name, every condition +// that reaches an application a hypothesis there, and its termination +// measures, each m as `(m + 1).toNat`: for a caller's m at least 0 and a +// call's below it (it may be -1), the call's is below the caller's, the +// relation the termination check proves, lexicographic over a tuple. None +// for a choice, a function without a definition, or a recursive one without +// measures (an archive's). +static std::string leanSpecDefinition(const ObligationModule &Module, + const LogicFunctionDecl &Function) { + if (Function.Choice || !Function.StepDefinition) + return ""; + std::set Reached, Pending; + collectLeanApplied(Function.StepDefinition.get(), Pending); + while (!Pending.empty()) { + std::string Next = *Pending.begin(); + Pending.erase(Pending.begin()); + if (!Reached.insert(Next).second) continue; - OS << "/- spec function: "; - printLeanCommentText(Function.DisplayName, OS); - OS << " -/\n"; - OS << "opaque "; - printLeanSpecName(Identity, OS); + auto It = Module.LogicFunctions.find(Next); + if (It != Module.LogicFunctions.end() && It->second.StepDefinition) + collectLeanApplied(It->second.StepDefinition.get(), Pending); + } + const bool Recursive = Reached.count(Function.Identity); + if (Recursive && Function.Decreases.empty()) + return ""; + + const bool FailedBefore = LeanEmissionFailed; + LeanEmissionFailed = false; + auto Temporaries = std::move(LeanTemporaryNames); + LeanTemporaryNames.clear(); + LeanDefinitionMode = true; + LeanEmitBudget = 1000000; + std::string Text; + llvm::raw_string_ostream OS(Text); + OS << "/- spec function: "; + printLeanCommentText(Function.DisplayName, OS); + OS << " -/\n"; + OS << "def "; + printLeanSpecName(Function.Identity, OS); + for (const LogicFunctionParameter &Parameter : Function.Parameters) { + OS << " ("; + printLeanName(Parameter.Name, OS); OS << " : "; - for (const LogicFunctionParameter &Parameter : Function.Parameters) { - printLeanSort(Parameter.Sort, OS); - OS << " -> "; + printLeanSort(Parameter.Sort, OS); + OS << ")"; + } + OS << " : "; + printLeanSort(Function.ResultSort, OS); + OS << " :=\n "; + printVCExprLean(Function.StepDefinition.get(), OS, LeanTop); + if (Recursive) { + OS << "\ntermination_by "; + if (Function.Decreases.size() > 1) + OS << "("; + for (unsigned I = 0; I < Function.Decreases.size(); ++I) { + if (I) + OS << ", "; + OS << "(("; + printVCExprLean(Function.Decreases[I].get(), OS, LeanTop); + OS << ") + 1).toNat"; + } + if (Function.Decreases.size() > 1) + OS << ")"; + OS << "\ndecreasing_by all_goals cppverify_decreasing"; + } + OS << "\n\n"; + LeanDefinitionMode = false; + LeanTemporaryNames = std::move(Temporaries); + const bool Failed = LeanEmissionFailed; + LeanEmissionFailed = FailedBefore; + return Failed ? "" : Text; +} + +static void emitLeanFunctionDeclarations( + const ObligationModule &Module, llvm::raw_ostream &OS, + std::set &EmittedFunctions, + std::map *Specs) { + for (const auto &[Identity, Function] : Module.LogicFunctions) { + if (Specs) { + auto [It, Inserted] = Specs->try_emplace(Identity); + LeanSpecDeclaration &Declaration = It->second; + if (Inserted) { + llvm::raw_string_ostream Name(Declaration.Name); + printLeanSpecName(Identity, Name); + Declaration.Opaque = leanOpaqueSpec(Function); + } + if (Declaration.Definition.empty()) { + Declaration.Definition = leanSpecDefinition(Module, Function); + Declaration.Applies.clear(); + collectLeanApplied(Function.StepDefinition.get(), Declaration.Applies); + } + continue; } - printLeanSort(Function.ResultSort, OS); - OS << "\n\n"; + if (EmittedFunctions.insert(Identity).second) + OS << leanOpaqueSpec(Function); } } @@ -1087,12 +1350,367 @@ static void emitLeanFunctionBodies(const ObligationModule &Module, } } +// Collections of mathematical integers, with the total meaning +// gives each operation, and lemmas that state it for simp, grind, and proofs +// by hand. Checking a goal never needs them: they are theorems of the +// definitions. +static constexpr llvm::StringLiteral LeanCollectionPrelude = + R"lean(/- Collections of mathematical integers, total as defines + them: a sequence is a list, a set its membership test, a multiset its + counts, and a map the value at each key it holds. -/ + +def cppSeqEmpty : List Int := [] +def cppSeqUnit (x : Int) : List Int := [x] +def cppSeqLength (s : List Int) : Int := s.length +def cppSeqAt (s : List Int) (i : Int) : Int := + if i < 0 then 0 else s[i.toNat]?.getD 0 +def cppSeqPush (s : List Int) (x : Int) : List Int := s ++ [x] +def cppSeqConcat (s t : List Int) : List Int := s ++ t +def cppSeqSubrange (s : List Int) (lo hi : Int) : List Int := + (s.drop (max 0 (min lo s.length)).toNat).take + (max (max 0 (min lo s.length)) (min hi s.length) - + max 0 (min lo s.length)).toNat +def cppSeqContains (s : List Int) (x : Int) : Prop := x ∈ s +instance (s : List Int) (x : Int) : Decidable (cppSeqContains s x) := + inferInstanceAs (Decidable (x ∈ s)) + +def cppSetEmpty : Int → Bool := fun _ => false +def cppSetInsert (s : Int → Bool) (x : Int) : Int → Bool := + fun y => y == x || s y +def cppSetRemove (s : Int → Bool) (x : Int) : Int → Bool := + fun y => y != x && s y +def cppSetContains (s : Int → Bool) (x : Int) : Prop := s x = true +instance (s : Int → Bool) (x : Int) : Decidable (cppSetContains s x) := + inferInstanceAs (Decidable (s x = true)) +def cppSetUnion (s t : Int → Bool) : Int → Bool := fun y => s y || t y +def cppSetIntersect (s t : Int → Bool) : Int → Bool := fun y => s y && t y +def cppSetDifference (s t : Int → Bool) : Int → Bool := + fun y => s y && !t y +def cppSetSubset (s t : Int → Bool) : Prop := ∀ y, s y = true → t y = true + +def cppMultisetEmpty : Int → Nat := fun _ => 0 +def cppMultisetInsert (m : Int → Nat) (x : Int) : Int → Nat := + fun y => if y = x then m y + 1 else m y +def cppMultisetRemove (m : Int → Nat) (x : Int) : Int → Nat := + fun y => if y = x then m y - 1 else m y +def cppMultisetCount (m : Int → Nat) (x : Int) : Int := m x + +def cppMapEmpty : Int → Option Int := fun _ => none +def cppMapInsert (m : Int → Option Int) (k v : Int) : Int → Option Int := + fun y => if y = k then some v else m y +def cppMapRemove (m : Int → Option Int) (k : Int) : Int → Option Int := + fun y => if y = k then none else m y +def cppMapContains (m : Int → Option Int) (k : Int) : Prop := + (m k).isSome = true +instance (m : Int → Option Int) (k : Int) : Decidable (cppMapContains m k) := + inferInstanceAs (Decidable ((m k).isSome = true)) +def cppMapGet (m : Int → Option Int) (k : Int) : Int := (m k).getD 0 + +/- What each operation means, for simp, grind, and proofs by hand. -/ + +private theorem cppverify_ite_pos {c : Prop} [Decidable c] {α : Sort _} + {a b : α} (h : c) : (if c then a else b) = a := by simp [h] +private theorem cppverify_ite_neg {c : Prop} [Decidable c] {α : Sort _} + {a b : α} (h : ¬c) : (if c then a else b) = b := by simp [h] + +@[simp, grind =] theorem cppSeqLength_empty : cppSeqLength cppSeqEmpty = 0 := rfl +@[simp, grind =] theorem cppSeqLength_unit (x : Int) : + cppSeqLength (cppSeqUnit x) = 1 := rfl +@[simp, grind =] theorem cppSeqLength_push (s : List Int) (x : Int) : + cppSeqLength (cppSeqPush s x) = cppSeqLength s + 1 := by + simp [cppSeqLength, cppSeqPush] +@[simp, grind =] theorem cppSeqLength_concat (s t : List Int) : + cppSeqLength (cppSeqConcat s t) = cppSeqLength s + cppSeqLength t := by + simp [cppSeqLength, cppSeqConcat] +theorem cppSeqLength_nonneg (s : List Int) : 0 ≤ cppSeqLength s := by + simp [cppSeqLength] +grind_pattern cppSeqLength_nonneg => cppSeqLength s +@[simp, grind =] theorem cppSeqLength_subrange (s : List Int) (lo hi : Int) : + cppSeqLength (cppSeqSubrange s lo hi) = + max (max 0 (min lo (cppSeqLength s))) (min hi (cppSeqLength s)) - + max 0 (min lo (cppSeqLength s)) := by + simp only [cppSeqLength, cppSeqSubrange, List.length_take, List.length_drop] + omega + +theorem cppSeqAt_out (s : List Int) (i : Int) + (h : i < 0 ∨ cppSeqLength s ≤ i) : cppSeqAt s i = 0 := by + unfold cppSeqAt cppSeqLength at * + split + · rfl + · rw [List.getElem?_eq_none (by omega)]; rfl +@[simp, grind =] theorem cppSeqAt_empty (i : Int) : cppSeqAt cppSeqEmpty i = 0 := + cppSeqAt_out [] i (by simp [cppSeqLength]; omega) +@[simp, grind =] theorem cppSeqAt_push (s : List Int) (x i : Int) : + cppSeqAt (cppSeqPush s x) i = + if i = cppSeqLength s then x else cppSeqAt s i := by + unfold cppSeqAt cppSeqPush cppSeqLength + by_cases h0 : i < 0 + · simp only [h0, ↓reduceIte, show ¬ i = (s.length : Int) by omega] + · by_cases he : i = s.length + · subst he; simp only [h0, ↓reduceIte]; simp + · simp only [h0, he, ↓reduceIte] + by_cases hl : i.toNat < s.length + · rw [List.getElem?_append_left hl] + · rw [List.getElem?_append_right (by omega), + List.getElem?_eq_none (show s.length ≤ i.toNat by omega), + List.getElem?_eq_none (by simp; omega)] +@[simp, grind =] theorem cppSeqAt_concat (s t : List Int) (i : Int) : + cppSeqAt (cppSeqConcat s t) i = + if i < cppSeqLength s then cppSeqAt s i + else cppSeqAt t (i - cppSeqLength s) := by + unfold cppSeqAt cppSeqLength cppSeqConcat + by_cases h0 : i < 0 + · simp only [h0, ↓reduceIte, show i < (s.length : Int) by omega] + · by_cases hl : i < s.length + · simp only [h0, hl, ↓reduceIte] + rw [List.getElem?_append_left (by omega)] + · simp only [h0, hl, ↓reduceIte, show ¬ (i - s.length < 0) by omega] + rw [List.getElem?_append_right (by omega)] + congr 3; omega +@[simp, grind =] theorem cppSeqAt_unit (x i : Int) : + cppSeqAt (cppSeqUnit x) i = if i = 0 then x else 0 := by + unfold cppSeqAt cppSeqUnit + by_cases h0 : i < 0 + · simp only [h0, ↓reduceIte, show ¬ i = 0 by omega] + · by_cases h : i = 0 + · subst h; simp + · simp only [h0, h, ↓reduceIte] + rw [List.getElem?_eq_none (by simp; omega)]; rfl +@[simp, grind =] theorem cppSeqAt_subrange (s : List Int) (lo hi i : Int) : + cppSeqAt (cppSeqSubrange s lo hi) i = + if 0 ≤ i ∧ i < cppSeqLength (cppSeqSubrange s lo hi) + then cppSeqAt s (max 0 (min lo (cppSeqLength s)) + i) else 0 := by + rw [cppSeqLength_subrange] + unfold cppSeqAt cppSeqSubrange cppSeqLength + by_cases h0 : i < 0 + · simp only [h0, ↓reduceIte, show ¬ (0 ≤ i) by omega, false_and] + · simp only [h0, ↓reduceIte] + split + · rw [List.getElem?_take, cppverify_ite_pos (by omega), List.getElem?_drop, + cppverify_ite_neg (show ¬ (max 0 (min lo (s.length : Int)) + i < 0) by omega)] + congr 3; omega + · rw [List.getElem?_take, cppverify_ite_neg (by omega)]; rfl +@[simp, grind =] theorem cppSeqContains_empty (x : Int) : + cppSeqContains cppSeqEmpty x ↔ False := by + simp [cppSeqContains, cppSeqEmpty] +@[simp, grind =] theorem cppSeqContains_unit (y x : Int) : + cppSeqContains (cppSeqUnit y) x ↔ x = y := by + simp [cppSeqContains, cppSeqUnit] +@[simp, grind =] theorem cppSeqContains_push (s : List Int) (y x : Int) : + cppSeqContains (cppSeqPush s y) x ↔ cppSeqContains s x ∨ x = y := by + simp [cppSeqContains, cppSeqPush] +@[simp, grind =] theorem cppSeqContains_concat (s t : List Int) (x : Int) : + cppSeqContains (cppSeqConcat s t) x ↔ + cppSeqContains s x ∨ cppSeqContains t x := by + simp [cppSeqContains, cppSeqConcat] +@[simp, grind =] theorem cppSeqSubrange_all (s : List Int) : + cppSeqSubrange s 0 (cppSeqLength s) = s := by + unfold cppSeqSubrange cppSeqLength + rw [show (max 0 (min (0 : Int) (s.length : Int))).toNat = 0 by omega, + show (max (max 0 (min (0 : Int) (s.length : Int))) + (min (s.length : Int) (s.length : Int)) - + max 0 (min (0 : Int) (s.length : Int))).toNat = s.length by omega] + simp +@[simp, grind =] theorem cppSeqSubrange_concat_left (s t : List Int) : + cppSeqSubrange (cppSeqConcat s t) 0 (cppSeqLength s) = s := by + unfold cppSeqSubrange cppSeqConcat cppSeqLength + have hl : (s ++ t).length = s.length + t.length := List.length_append + rw [show (max 0 (min (0 : Int) ((s ++ t).length : Int))).toNat = 0 by omega, + show (max (max 0 (min (0 : Int) ((s ++ t).length : Int))) + (min (s.length : Int) ((s ++ t).length : Int)) - + max 0 (min (0 : Int) ((s ++ t).length : Int))).toNat = s.length by + omega] + simp +@[simp, grind =] theorem cppSeqSubrange_concat_right (s t : List Int) : + cppSeqSubrange (cppSeqConcat s t) (cppSeqLength s) + (cppSeqLength s + cppSeqLength t) = t := by + unfold cppSeqSubrange cppSeqConcat cppSeqLength + have hl : (s ++ t).length = s.length + t.length := List.length_append + rw [show (max 0 (min (s.length : Int) ((s ++ t).length : Int))).toNat = + s.length by omega, + show (max (max 0 (min (s.length : Int) ((s ++ t).length : Int))) + (min ((s.length : Int) + (t.length : Int)) ((s ++ t).length : Int)) - + max 0 (min (s.length : Int) ((s ++ t).length : Int))).toNat = + t.length by omega] + simp +@[simp, grind =] theorem cppSeqSubrange_push (s : List Int) (x : Int) : + cppSeqSubrange (cppSeqPush s x) 0 (cppSeqLength s) = s := + cppSeqSubrange_concat_left s [x] +theorem cppSeqContains_iff (s : List Int) (x : Int) : + cppSeqContains s x ↔ + ∃ i, 0 ≤ i ∧ i < cppSeqLength s ∧ cppSeqAt s i = x := by + unfold cppSeqContains cppSeqLength cppSeqAt + rw [List.mem_iff_getElem] + constructor + · rintro ⟨i, hi, he⟩ + refine ⟨i, by omega, by omega, ?_⟩ + rw [cppverify_ite_neg (by omega), Int.toNat_natCast, List.getElem?_eq_getElem hi] + simpa using he + · rintro ⟨i, h0, hl, he⟩ + refine ⟨i.toNat, by omega, ?_⟩ + rw [cppverify_ite_neg (by omega), List.getElem?_eq_getElem (by omega)] at he + simpa using he +theorem cppSeq_ext (s t : List Int) (hl : cppSeqLength s = cppSeqLength t) + (h : ∀ i, 0 ≤ i → i < cppSeqLength s → cppSeqAt s i = cppSeqAt t i) : + s = t := by + unfold cppSeqLength at hl + apply List.ext_getElem (by omega) + intro i h1 h2 + have := h i (by omega) (by unfold cppSeqLength; omega) + unfold cppSeqAt at this + simp only [show ¬ ((i : Int) < 0) by omega, ↓reduceIte, Int.toNat_natCast, + List.getElem?_eq_getElem h1, List.getElem?_eq_getElem h2, + Option.getD_some] at this + exact this + +@[simp, grind =] theorem cppSetContains_empty (x : Int) : + cppSetContains cppSetEmpty x ↔ False := by simp [cppSetContains, cppSetEmpty] +@[simp, grind =] theorem cppSetContains_insert (s : Int → Bool) (x y : Int) : + cppSetContains (cppSetInsert s x) y ↔ y = x ∨ cppSetContains s y := by + simp [cppSetContains, cppSetInsert] +@[simp, grind =] theorem cppSetContains_remove (s : Int → Bool) (x y : Int) : + cppSetContains (cppSetRemove s x) y ↔ y ≠ x ∧ cppSetContains s y := by + simp [cppSetContains, cppSetRemove] +@[simp, grind =] theorem cppSetContains_union (s t : Int → Bool) (y : Int) : + cppSetContains (cppSetUnion s t) y ↔ + cppSetContains s y ∨ cppSetContains t y := by + simp [cppSetContains, cppSetUnion] +@[simp, grind =] theorem cppSetContains_intersect (s t : Int → Bool) (y : Int) : + cppSetContains (cppSetIntersect s t) y ↔ + cppSetContains s y ∧ cppSetContains t y := by + simp [cppSetContains, cppSetIntersect] +@[simp, grind =] theorem cppSetContains_difference (s t : Int → Bool) (y : Int) : + cppSetContains (cppSetDifference s t) y ↔ + cppSetContains s y ∧ ¬ cppSetContains t y := by + simp [cppSetContains, cppSetDifference] +@[simp, grind =] theorem cppSetSubset_iff (s t : Int → Bool) : + cppSetSubset s t ↔ ∀ y, cppSetContains s y → cppSetContains t y := Iff.rfl +theorem cppSet_ext (s t : Int → Bool) + (h : ∀ y, cppSetContains s y ↔ cppSetContains t y) : s = t := by + funext y + have := h y + unfold cppSetContains at this + cases hs : s y <;> cases ht : t y <;> simp_all + +@[simp, grind =] theorem cppMultisetCount_empty (x : Int) : + cppMultisetCount cppMultisetEmpty x = 0 := rfl +@[simp, grind =] theorem cppMultisetCount_insert (m : Int → Nat) (x y : Int) : + cppMultisetCount (cppMultisetInsert m x) y = + if y = x then cppMultisetCount m y + 1 else cppMultisetCount m y := by + unfold cppMultisetCount cppMultisetInsert; split <;> simp +@[simp, grind =] theorem cppMultisetCount_remove (m : Int → Nat) (x y : Int) : + cppMultisetCount (cppMultisetRemove m x) y = + if y = x then max 0 (cppMultisetCount m y - 1) + else cppMultisetCount m y := by + unfold cppMultisetCount cppMultisetRemove; split <;> omega +theorem cppMultisetCount_nonneg (m : Int → Nat) (x : Int) : + 0 ≤ cppMultisetCount m x := by simp [cppMultisetCount] +grind_pattern cppMultisetCount_nonneg => cppMultisetCount m x +theorem cppMultiset_ext (m n : Int → Nat) + (h : ∀ y, cppMultisetCount m y = cppMultisetCount n y) : m = n := by + funext y; have := h y; unfold cppMultisetCount at this; omega + +@[simp, grind =] theorem cppMapContains_empty (k : Int) : + cppMapContains cppMapEmpty k ↔ False := by simp [cppMapContains, cppMapEmpty] +@[simp, grind =] theorem cppMapContains_insert (m : Int → Option Int) (k v y : Int) : + cppMapContains (cppMapInsert m k v) y ↔ y = k ∨ cppMapContains m y := by + unfold cppMapContains cppMapInsert; by_cases h : y = k <;> simp [h] +@[simp, grind =] theorem cppMapContains_remove (m : Int → Option Int) (k y : Int) : + cppMapContains (cppMapRemove m k) y ↔ y ≠ k ∧ cppMapContains m y := by + unfold cppMapContains cppMapRemove; by_cases h : y = k <;> simp [h] +@[simp, grind =] theorem cppMapGet_empty (k : Int) : cppMapGet cppMapEmpty k = 0 := rfl +@[simp, grind =] theorem cppMapGet_insert (m : Int → Option Int) (k v y : Int) : + cppMapGet (cppMapInsert m k v) y = if y = k then v else cppMapGet m y := by + unfold cppMapGet cppMapInsert; split <;> simp +@[simp, grind =] theorem cppMapGet_remove (m : Int → Option Int) (k y : Int) : + cppMapGet (cppMapRemove m k) y = if y = k then 0 else cppMapGet m y := by + unfold cppMapGet cppMapRemove; split <;> simp +theorem cppMapGet_out (m : Int → Option Int) (k : Int) + (h : ¬ cppMapContains m k) : cppMapGet m k = 0 := by + unfold cppMapGet; unfold cppMapContains at h; cases hm : m k <;> simp_all +theorem cppMap_ext (m n : Int → Option Int) + (hc : ∀ y, cppMapContains m y ↔ cppMapContains n y) + (hg : ∀ y, cppMapGet m y = cppMapGet n y) : m = n := by + funext y + have c := hc y; have g := hg y + unfold cppMapGet at g + unfold cppMapContains at c + cases hm : m y <;> cases hn : n y <;> simp_all + +)lean"; + +// The definitions every exported goal is stated with: the heap model, the +// machine comparisons, C++ division, and the collections; a project's goals +// also have the lemmas their readable forms' bridges use. +void verify::emitLeanPrelude(llvm::raw_ostream &OS, bool Project) { + OS << "noncomputable section\n\n"; + OS << "set_option maxRecDepth 100000\n"; + OS << "set_option maxHeartbeats 0\n\n"; + OS << "local instance cppVerifyPropDecidable (p : Prop) : Decidable p :=\n"; + OS << " Classical.propDecidable p\n\n"; + OS << "abbrev CppHeap := Int -> Int\n\n"; + OS << "def heapSelectInt (h : CppHeap) (p : Int) : Int := h p\n"; + OS << "abbrev heapSelectBool (h : CppHeap) (p : Int) : Prop := h p ≠ 0\n"; + OS << "def heapSelectBv (w : Nat) (h : CppHeap) (p : Int) : BitVec w :=\n"; + OS << " BitVec.ofInt w (h p)\n\n"; + OS << "def heapStoreInt (h : CppHeap) (p v : Int) (h' : CppHeap) : " + "Prop :=\n"; + OS << " h' = fun q => if q = p then v else h q\n"; + OS << "def heapStoreBool (h : CppHeap) (p : Int) (v : Prop)\n"; + OS << " (h' : CppHeap) : Prop :=\n"; + OS << " h' = fun q => if q = p then\n"; + OS << " @ite Int v (Classical.propDecidable v) 1 0 else h q\n"; + OS << "def heapStoreBv {w : Nat} (h : CppHeap) (p : Int) (v : BitVec w)\n"; + OS << " (h' : CppHeap) : Prop :=\n"; + OS << " h' = fun q => if q = p then Int.ofNat v.toNat else h q\n\n"; + OS << "opaque validPtr : Int -> Prop\n\n"; + // Reducible, so instance search sees the Bool comparison and decides it. + OS << "abbrev cppBvUlt {w : Nat} (x y : BitVec w) : Prop := x.ult y = " + "true\n"; + OS << "abbrev cppBvUle {w : Nat} (x y : BitVec w) : Prop := x.ule y = " + "true\n"; + OS << "abbrev cppBvSlt {w : Nat} (x y : BitVec w) : Prop := x.slt y = " + "true\n"; + OS << "abbrev cppBvSle {w : Nat} (x y : BitVec w) : Prop := x.sle y = " + "true\n\n"; + OS << "def cppIntDiv (x y : Int) : Int :=\n"; + OS << " if y = 0 then 0 else\n"; + OS << " let q := (if x < 0 then -x else x) / " + "(if y < 0 then -y else y)\n"; + OS << " if (x < 0) ≠ (y < 0) then -q else q\n"; + OS << "def cppIntRem (x y : Int) : Int :=\n"; + OS << " if y = 0 then x else x - cppIntDiv x y * y\n\n"; + OS << LeanCollectionPrelude; + OS << "/- Proves that an application in a spec's definition lowers its " + "measure. -/\n"; + OS << "macro \"cppverify_decreasing\" : tactic => `(tactic| first\n"; + OS << " | (simp_wf; omega)\n"; + OS << " | (simp_wf; simp only [cppSeqLength, cppMultisetCount, cppBvSlt, " + "cppBvSle,\n"; + OS << " cppBvUlt, cppBvUle] at *; omega)\n"; + // C++ division and remainder by a constant, which omega reads once the + // signs are split. + OS << " | (simp_wf; simp only [cppIntDiv, cppIntRem] at *;\n"; + OS << " (repeat' split) <;> simp_all <;> omega)\n"; + OS << " | (simp_wf; simp_all; omega)\n"; + OS << " | decreasing_tactic)\n\n"; + if (Project) { + // What the bridges from readable goals use. + OS << "theorem cppverify_imp_or {a b : Prop} (h : a → b) : ¬a ∨ b :=\n"; + OS << " (Classical.em a).elim (fun ha => Or.inr (h ha)) Or.inl\n"; + OS << "theorem cppverify_not_imp_or {a b : Prop} (h : ¬a → b) : a ∨ b " + ":=\n"; + OS << " (Classical.em a).elim Or.inl (fun ha => Or.inr (h ha))\n\n"; + } +} + VerifyResult verify::exportLeanScratchPad( const ObligationModule &Module, llvm::raw_ostream &OS, bool EmitPreamble, std::set &EmittedFunctions, std::set &EmittedTheorems, unsigned ModuleIndex, std::vector *ProjectGoals, - const std::set *Selection) { + const std::set *Selection, + std::map *Specs) { VerifyResult Result; if (!Module.CorrectnessGoal || !Module.CounterexampleQuery) { Result.Status = VerifyStatus::Unresolved; @@ -1130,54 +1748,10 @@ VerifyResult verify::exportLeanScratchPad( OS << " This file exports canonical obligations but does not certify " "them. -/\n\n"; } - OS << "noncomputable section\n\n"; - OS << "set_option maxRecDepth 100000\n"; - OS << "set_option maxHeartbeats 0\n\n"; - OS << "local instance cppVerifyPropDecidable (p : Prop) : Decidable p :=\n"; - OS << " Classical.propDecidable p\n\n"; - OS << "abbrev CppHeap := Int -> Int\n\n"; - OS << "def heapSelectInt (h : CppHeap) (p : Int) : Int := h p\n"; - OS << "abbrev heapSelectBool (h : CppHeap) (p : Int) : Prop := h p ≠ 0\n"; - OS << "def heapSelectBv (w : Nat) (h : CppHeap) (p : Int) : BitVec w :=\n"; - OS << " BitVec.ofInt w (h p)\n\n"; - OS << "def heapStoreInt (h : CppHeap) (p v : Int) (h' : CppHeap) : " - "Prop :=\n"; - OS << " h' = fun q => if q = p then v else h q\n"; - OS << "def heapStoreBool (h : CppHeap) (p : Int) (v : Prop)\n"; - OS << " (h' : CppHeap) : Prop :=\n"; - OS << " h' = fun q => if q = p then\n"; - OS << " @ite Int v (Classical.propDecidable v) 1 0 else h q\n"; - OS << "def heapStoreBv {w : Nat} (h : CppHeap) (p : Int) (v : BitVec w)\n"; - OS << " (h' : CppHeap) : Prop :=\n"; - OS << " h' = fun q => if q = p then Int.ofNat v.toNat else h q\n\n"; - OS << "opaque validPtr : Int -> Prop\n\n"; - // Reducible, so instance search sees the Bool comparison and decides it. - OS << "abbrev cppBvUlt {w : Nat} (x y : BitVec w) : Prop := x.ult y = " - "true\n"; - OS << "abbrev cppBvUle {w : Nat} (x y : BitVec w) : Prop := x.ule y = " - "true\n"; - OS << "abbrev cppBvSlt {w : Nat} (x y : BitVec w) : Prop := x.slt y = " - "true\n"; - OS << "abbrev cppBvSle {w : Nat} (x y : BitVec w) : Prop := x.sle y = " - "true\n\n"; - OS << "def cppIntDiv (x y : Int) : Int :=\n"; - OS << " if y = 0 then 0 else\n"; - OS << " let q := (if x < 0 then -x else x) / " - "(if y < 0 then -y else y)\n"; - OS << " if (x < 0) ≠ (y < 0) then -q else q\n"; - OS << "def cppIntRem (x y : Int) : Int :=\n"; - OS << " if y = 0 then x else x - cppIntDiv x y * y\n\n"; - if (ProjectGoals) { - // What the bridges from readable goals use. - OS << "theorem cppverify_imp_or {a b : Prop} (h : a → b) : ¬a ∨ b :=\n"; - OS << " (Classical.em a).elim (fun ha => Or.inr (h ha)) Or.inl\n"; - OS << "theorem cppverify_not_imp_or {a b : Prop} (h : ¬a → b) : a ∨ b " - ":=\n"; - OS << " (Classical.em a).elim Or.inl (fun ha => Or.inr (h ha))\n\n"; - } + emitLeanPrelude(OS, ProjectGoals != nullptr); } - emitLeanFunctionDeclarations(Module, OS, EmittedFunctions); + emitLeanFunctionDeclarations(Module, OS, EmittedFunctions, Specs); emitLeanFunctionBodies(Module, OS); OS << "/- function: "; printLeanCommentText(Module.FunctionName, OS); diff --git a/clang/lib/Verify/Backend/LeanBackend.h b/clang/lib/Verify/Backend/LeanBackend.h index 7145e8596c..176d58923d 100644 --- a/clang/lib/Verify/Backend/LeanBackend.h +++ b/clang/lib/Verify/Backend/LeanBackend.h @@ -4,8 +4,10 @@ #include "VerifyBackend.h" #include "llvm/Support/raw_ostream.h" +#include #include #include +#include #include namespace clang { @@ -38,21 +40,47 @@ struct LeanProjectGoal { /// The group of a module's goals in a project: its function's directory. std::string leanProjectGroup(const ObligationModule &Module); +/// A logical function of a Lean project: its opaque declaration and, when it +/// has a definition Lean may accept, that definition, recursion measured by +/// its termination measures, with the functions it applies. +struct LeanSpecDeclaration { + /// Its Lean constant. + std::string Name; + std::string Opaque; + std::string Definition; + std::set Applies; +}; + +/// The generated modules of a Lean project: the specs its goals apply, by +/// identity, which every goal module imports, and each group's spec +/// definitions and goals. +struct LeanProjectModules { + std::map Specs; + std::map Goals; + /// The groups in the order their functions were exported: the source's. + std::vector Order; +}; + +/// The definitions every exported goal is stated with. +void emitLeanPrelude(llvm::raw_ostream &OS, bool Project); + /// Selection names the internal IDs to export; a project goal is named by /// its function and semantic hash, so it keeps its name whatever else is /// exported, and a scratch-pad goal keeps the positional name it has when /// every obligation is exported. A project records every goal of the module, -/// the ones left out as not exported. -VerifyResult -exportLeanScratchPad(const ObligationModule &Module, llvm::raw_ostream &OS, - bool EmitPreamble, std::set &EmittedFunctions, - std::set &EmittedTheorems, - unsigned ModuleIndex, - std::vector *ProjectGoals, - const std::set *Selection = nullptr); +/// the ones left out as not exported. Specs, when given, receives each spec +/// once, as its project declares it, instead of OS. +VerifyResult exportLeanScratchPad( + const ObligationModule &Module, llvm::raw_ostream &OS, bool EmitPreamble, + std::set &EmittedFunctions, + std::set &EmittedTheorems, unsigned ModuleIndex, + std::vector *ProjectGoals, + const std::set *Selection = nullptr, + std::map *Specs = nullptr); class LeanVerifyBackend : public VerifyBackend { - llvm::raw_ostream *Out; + llvm::raw_ostream *Out = nullptr; + LeanProjectModules *Modules = nullptr; bool PreambleEmitted = false; std::set EmittedFunctions; std::set EmittedTheorems; @@ -64,12 +92,13 @@ class LeanVerifyBackend : public VerifyBackend { LeanVerifyBackend(llvm::raw_ostream *OS, std::vector *ProjectGoals) : Out(OS), ProjectGoals(ProjectGoals) {} + /// A project's export, into its modules. + LeanVerifyBackend(LeanProjectModules *Modules, + std::vector *ProjectGoals) + : Modules(Modules), ProjectGoals(ProjectGoals) {} llvm::StringRef getName() const override { return "lean"; } BackendCapabilities getCapabilities() const override { - // Collections have no Lean semantics yet. - return {allLogicFeatures() & ~logicFeature(LogicFeature::Sequences) & - ~logicFeature(LogicFeature::Collections), - false}; + return {allLogicFeatures(), false}; } /// Restrict later exports to these internal obligation IDs. void selectObligations(std::optional> Ids) { diff --git a/clang/lib/Verify/Backend/VerifyBackend.cpp b/clang/lib/Verify/Backend/VerifyBackend.cpp index 134495fe9a..fac014a9f8 100644 --- a/clang/lib/Verify/Backend/VerifyBackend.cpp +++ b/clang/lib/Verify/Backend/VerifyBackend.cpp @@ -15,17 +15,31 @@ using namespace verify; VerifyResult LeanVerifyBackend::verifyModule(const ObligationModule &Module) { VerifyResult R; - if (!Out) { + if (!Out && !Modules) { R.Status = VerifyStatus::Unresolved; R.Reason = VerifyReason::LeanExportFailure; R.Message = "no lean output stream"; return R; } const size_t Before = ProjectGoals ? ProjectGoals->size() : 0; - VerifyResult Result = exportLeanScratchPad( - Module, *Out, !PreambleEmitted, EmittedFunctions, EmittedTheorems, - ++ModuleIndex, ProjectGoals, Selection ? &*Selection : nullptr); - PreambleEmitted = true; + VerifyResult Result; + if (Modules) { + // A project's goals go to their function's module, and the specs they + // apply are declared once, in the module every goal module imports. + const std::string Group = leanProjectGroup(Module); + if (!Modules->Goals.count(Group)) + Modules->Order.push_back(Group); + llvm::raw_string_ostream Goals(Modules->Goals[Group]); + Result = exportLeanScratchPad( + Module, Goals, /*EmitPreamble=*/false, EmittedFunctions, + EmittedTheorems, ++ModuleIndex, ProjectGoals, + Selection ? &*Selection : nullptr, &Modules->Specs); + } else { + Result = exportLeanScratchPad( + Module, *Out, !PreambleEmitted, EmittedFunctions, EmittedTheorems, + ++ModuleIndex, ProjectGoals, Selection ? &*Selection : nullptr); + PreambleEmitted = true; + } if (ProjectGoals) for (size_t I = Before; I < ProjectGoals->size(); ++I) if ((*ProjectGoals)[I].Exported) @@ -754,11 +768,14 @@ std::unique_ptr verify::createVerifyBackend(BackendKind K, llvm::raw_ostream *LeanOut, unsigned BMCUnroll, const BackendExecutionOptions &Execution, - std::vector *LeanProjectGoals) { + std::vector *LeanProjectGoals, + LeanProjectModules *LeanModules) { switch (K) { case BackendKind::Z3: return std::make_unique(Execution, "z3"); case BackendKind::Lean: + if (LeanModules) + return std::make_unique(LeanModules, LeanProjectGoals); return std::make_unique(LeanOut, LeanProjectGoals); case BackendKind::BMC: return std::make_unique(BMCUnroll, Execution); diff --git a/clang/lib/Verify/Backend/VerifyBackend.h b/clang/lib/Verify/Backend/VerifyBackend.h index 6159936740..6e3a71e715 100644 --- a/clang/lib/Verify/Backend/VerifyBackend.h +++ b/clang/lib/Verify/Backend/VerifyBackend.h @@ -307,12 +307,14 @@ inline unsigned moduleTimeoutMs(const ObligationModule &Module, } struct LeanProjectGoal; +struct LeanProjectModules; std::unique_ptr createVerifyBackend(BackendKind K, llvm::raw_ostream *LeanOut = nullptr, unsigned BMCUnroll = 10, const BackendExecutionOptions &Execution = {}, - std::vector *LeanProjectGoals = nullptr); + std::vector *LeanProjectGoals = nullptr, + LeanProjectModules *LeanModules = nullptr); VerifyResult lowerObligationModule(const ObligationModule &Module, diff --git a/clang/lib/Verify/Driver/LeanAutomation.h b/clang/lib/Verify/Driver/LeanAutomation.h index 0db32bac01..fa807cf23c 100644 --- a/clang/lib/Verify/Driver/LeanAutomation.h +++ b/clang/lib/Verify/Driver/LeanAutomation.h @@ -9,23 +9,32 @@ namespace verify { /// Names this module's tactics: a stub or automatic proof that an earlier /// revision wrote is tried again. -inline constexpr llvm::StringLiteral LeanAutomationRevision = "1"; +inline constexpr llvm::StringLiteral LeanAutomationRevision = "3"; /// The steps of cppverify_auto, each the whole proof of a goal it proves. inline constexpr llvm::StringLiteral LeanAutomationSteps[] = { - "cppverify_auto_grind", "cppverify_auto_heap", "cppverify_auto_bv", - "cppverify_auto_decide", "cppverify_auto_simp"}; + "cppverify_auto_grind", "cppverify_auto_heap", "cppverify_auto_bv", + "cppverify_auto_decide", "cppverify_auto_simp", "cppverify_auto_bveq", + "cppverify_auto_ext", "cppverify_auto_unfold", "cppverify_auto_eval", + "cppverify_auto_div"}; /// CppVerify/Auto.lean, written with every export. Its steps were chosen by /// what proves the goals of the test suite (heap stores as the functions /// they define, machine arithmetic as integers, then grind; stating toInt /// ranges and removing Int.bmod first proved nothing more, the latter less), /// each with a heartbeat budget of its own, as Vermilion's discharger ladder. +/// Revision 2 adds the last three, after the others, so that every goal an +/// earlier step proves keeps its proof: machine equalities and sign +/// extensions as integer facts, collection equality element by element, and +/// the definition instances a goal states, by the bodies they name. +/// Revision 3 adds the last two: the spec functions with Lean definitions +/// evaluated by their equations, and C++ division and remainder by their +/// definitions. inline constexpr llvm::StringLiteral LeanAutomationSource = R"lean(/- Generated by CppVerify: the tactics of its automatic proofs, which proof files may use too. Regeneration replaces this file. -/ import Lean -import CppVerify.Generated +import CppVerify.Prelude register_option cppverify.autoBudget : Nat := { defValue := 50000 @@ -82,6 +91,51 @@ elab "cppverify_unfold_readable" : tactic => withMainContext do let unfolded ← deltaExpand target (· == name) replaceMainGoal [← (← getMainGoal).change unfolded] +open Lean Elab Tactic Meta in +/-- Unfolds the definitions of spec bodies that a goal and its hypotheses +name, so that each definition instance a goal states says what the body +does. A body names only lower levels of its definition, so this ends. -/ +elab "cppverify_unfold_bodies" : tactic => withMainContext do + let isBody : Name → Bool := fun + | .str _ s => s.startsWith "cppSpecBody_" + | _ => false + let rec expand (e : Expr) : Nat → MetaM Expr + | 0 => return e + | fuel + 1 => do + let e' ← deltaExpand e isBody + if e' == e then return e else expand e' fuel + let mut goal ← getMainGoal + goal ← goal.change (← expand (← instantiateMVars (← goal.getType)) 64) + for d in ← goal.withContext getLCtx do + if d.isImplementationDetail then continue + let t ← instantiateMVars d.type + let t' ← expand t 64 + if t' != t then + goal ← goal.changeLocalDecl d.fvarId t' + replaceMainGoal [goal] + +open Lean Elab Tactic Meta in +/-- Rewrites with the equations of every spec function that Specs.lean +defines, and C++ division and remainder, so that applications at known +arguments become values. On unknown arguments it unfolds until its budget +is spent. -/ +elab "cppverify_eval_specs" : tactic => withMainContext do + let env ← getEnv + let mut lemmas : Array (TSyntax `Lean.Parser.Tactic.simpLemma) := #[] + let some idx := env.getModuleIdx? `CppVerify.Specs + | throwError "no spec function has a Lean definition" + let some data := env.header.moduleData[idx.toNat]? + | throwError "no spec function has a Lean definition" + for name in data.constNames do + if let .str .anonymous s := name then + if s.startsWith "cppSpec_" then + if let some (.defnInfo _) := env.find? name then + lemmas := lemmas.push + (← `(Lean.Parser.Tactic.simpLemma| $(mkIdent name):ident)) + if lemmas.isEmpty then + throwError "no spec function has a Lean definition" + evalTactic (← `(tactic| simp [$lemmas,*, cppIntDiv, cppIntRem])) + /-- Machine comparisons, constants, and overflow conditions as facts about integers. -/ macro "cppverify_norm" : tactic => `(tactic| (try simp only [cppBvSlt, cppBvSle, @@ -118,6 +172,47 @@ macro "cppverify_auto_decide" : tactic => macro "cppverify_auto_simp" : tactic => `(tactic| (cppverify_unfold_readable; simp_all)) +/-- Machine equalities, as of `x ≠ y` for distinct keys, and sign extensions +as facts about integers. -/ +macro "cppverify_bveq" : tactic => `(tactic| (try simp (disch := omega) only + [ne_eq, ← BitVec.toInt_inj, BitVec.toInt_signExtend_of_le] at *)) +macro "cppverify_auto_bveq" : tactic => `(tactic| ( + cppverify_unfold_readable + intros + cppverify_bveq + cppverify_norm + all_goals grind)) +/-- Two collections are equal when they agree at every element: equal +lengths and reads for sequences, membership for sets, counts for +multisets, and keys and values for maps. -/ +macro "cppverify_auto_ext" : tactic => `(tactic| ( + cppverify_unfold_readable + intros + (first | apply cppSeq_ext | apply cppSet_ext | apply cppMultiset_ext + | apply cppMap_ext) + all_goals (intros; cppverify_norm; all_goals grind))) +macro "cppverify_auto_unfold" : tactic => `(tactic| ( + cppverify_unfold_readable + intros + cppverify_unfold_bodies + cppverify_bveq + cppverify_norm + all_goals grind)) +macro "cppverify_auto_eval" : tactic => `(tactic| ( + cppverify_unfold_readable + intros + cppverify_bveq + cppverify_eval_specs + all_goals grind)) +/-- C++ division and remainder by their definitions, which grind reads by +constant divisors once the signs are split. -/ +macro "cppverify_auto_div" : tactic => `(tactic| ( + cppverify_unfold_readable + intros + cppverify_bveq + cppverify_norm + all_goals grind [cppIntDiv, cppIntRem])) + open Lean Elab Tactic in /-- Tries each step on the goal, each with `cppverify.autoBudget` heartbeats of its own, and keeps the first that proves it. A step that runs out of @@ -132,7 +227,12 @@ elab "cppverify_auto" : tactic => do ("cppverify_auto_heap", ← `(tactic| cppverify_auto_heap)), ("cppverify_auto_bv", ← `(tactic| cppverify_auto_bv)), ("cppverify_auto_decide", ← `(tactic| cppverify_auto_decide)), - ("cppverify_auto_simp", ← `(tactic| cppverify_auto_simp))] + ("cppverify_auto_simp", ← `(tactic| cppverify_auto_simp)), + ("cppverify_auto_bveq", ← `(tactic| cppverify_auto_bveq)), + ("cppverify_auto_ext", ← `(tactic| cppverify_auto_ext)), + ("cppverify_auto_unfold", ← `(tactic| cppverify_auto_unfold)), + ("cppverify_auto_eval", ← `(tactic| cppverify_auto_eval)), + ("cppverify_auto_div", ← `(tactic| cppverify_auto_div))] for (name, step) in steps do let attempt : TacticM Unit := do let heartbeats ← IO.getNumHeartbeats diff --git a/clang/lib/Verify/Driver/LeanCertifier.h b/clang/lib/Verify/Driver/LeanCertifier.h index dc62393db9..4286533013 100644 --- a/clang/lib/Verify/Driver/LeanCertifier.h +++ b/clang/lib/Verify/Driver/LeanCertifier.h @@ -16,7 +16,7 @@ open Lean /-- The axioms a constant depends on, through the statements and values of the constants it uses, read from the kernel's constants. -/ -def axiomsOf (env : Environment) (root : Name) : Except String NameSet := Id.run do +def axiomsOf (env : Kernel.Environment) (root : Name) : Except String NameSet := Id.run do let mut seen : NameSet := {} let mut axioms : NameSet := {} let mut work := #[root] @@ -38,9 +38,10 @@ def axiomsOf (env : Environment) (root : Name) : Except String NameSet := Id.run | none => return .error s!"{c} is not in the environment" return .ok axioms -/-- A module's imports and its own constants, read from its compiled files. -/ +/-- A module's imports and its own constants, in the order it declares them, +read from its compiled files. -/ unsafe def moduleConstants (module : Name) : - IO (Array Import × Std.HashMap Name ConstantInfo) := do + IO (Array Import × Array Name × Std.HashMap Name ConstantInfo) := do let file ← findOLean module let mut files := #[file] let server := OLeanLevel.server.adjustFileName file @@ -54,37 +55,94 @@ unsafe def moduleConstants (module : Name) : let mut constants := {} for name in parts[parts.size - 1].1.constNames, info in parts[parts.size - 1].1.constants do constants := constants.insert name info - return (parts[0].1.imports, constants) + return (parts[0].1.imports, parts[parts.size - 1].1.constNames, constants) -/-- Replays constants with the kernel into the environment of imports, as -leanchecker does: nothing in them escaped the kernel. -/ -unsafe def replayInto (imports : Array Import) - (constants : Std.HashMap Name ConstantInfo) : IO Unit := do - let (_, s) ← importModulesCore imports |>.run - let env ← finalizeImport s imports {} 0 false false (isModule := true) - discard <| env.toKernelEnv.replay constants +/-- A module of the project, read from its compiled files. -/ +structure ProjectModule where + name : Name + imports : Array Import + declared : Array Name + constants : Std.HashMap Name ConstantInfo -/-- Replays a module's own constants into the environment of its imports. -/ -unsafe def replayModule (module : Name) : IO Unit := do - let (imports, constants) ← moduleConstants module - replayInto imports constants +/-- The modules of the project some modules import, each after the modules it +imports, and the toolchain's modules they import. -/ +structure Closure where + modules : Array ProjectModule := #[] + toolchain : Array Import := #[] + seen : NameSet := {} -/-- Whether the proof of a goal states exactly the goal the generated module +unsafe def Closure.visit (toolchain : String) (module : Name) : StateT Closure IO Unit := do + if (← get).seen.contains module then return + modify fun c => { c with seen := c.seen.insert module } + if (← findOLean module).toString.startsWith toolchain then + modify fun c => { c with toolchain := c.toolchain.push { module } } + return + let (imports, declared, constants) ← moduleConstants module + for i in imports do + Closure.visit toolchain i.module + modify fun c => { c with modules := c.modules.push { name := module, imports, declared, constants } } + +/-- The kernel's environment of the project: the toolchain's modules the +project imports, imported once, then every module of the project replayed +with the kernel, each after the modules it imports, as leanchecker does. A +module the kernel rejects, one that imports it, and one that declares a +constant an earlier module or the toolchain declares otherwise are left out, +each with why; the constant each other module declares is recorded with it. -/ +structure Replayed where + env : Kernel.Environment + rejected : Std.HashMap Name String + owner : Std.HashMap Name Name + +unsafe def replayProject (closure : Closure) : IO Replayed := do + let (_, s) ← importModulesCore closure.toolchain |>.run + let imported ← finalizeImport s closure.toolchain {} 0 false false (isModule := true) + let mut env := imported.toKernelEnv + let mut rejected : Std.HashMap Name String := {} + let mut owner : Std.HashMap Name Name := {} + for m in closure.modules do + if let some i := m.imports.find? (rejected.contains ·.module) then + rejected := rejected.insert m.name rejected[i.module]! + continue + let mut fresh : Std.HashMap Name ConstantInfo := {} + let mut clash : Option String := none + for (name, info) in m.constants do + match env.find? name with + | none => fresh := fresh.insert name info + | some known => + -- Lean derives an equation lemma in each module that unfolds a + -- definition, the same constant every time, and the kernel takes a + -- theorem twice when it states the same. + let same := known.type == info.type && known.levelParams == info.levelParams && + (known.isTheorem || known.value? == info.value?) + unless same do + let other := (owner[name]?).map toString |>.getD "the toolchain" + clash := some s!"{m.name} declares {name}, which {other} declares" + break + if let some why := clash then + rejected := rejected.insert m.name why + continue + try env ← env.replay fresh + catch e => + rejected := rejected.insert m.name s!"the kernel rejects {m.name}: {e}" + continue + for (name, _) in fresh do + owner := owner.insert name m.name + return { env, rejected, owner } + +/-- Whether the proof of a goal states exactly the goal its generated module defines and depends on no axiom outside the allowed ones. -/ -def checkStatement (env : Environment) (goal module : Name) (allowed : NameSet) : - Option String := Id.run do - let generated := `CppVerify.Generated - let moduleOf (c : Name) : Option Name := - (env.getModuleIdxFor? c).bind fun i => env.header.moduleNames[i.toNat]? +def checkStatement (project : Replayed) (goal module generated : Name) + (allowed : NameSet) : Option String := Id.run do + let env := project.env let proof := goal.appendAfter "_proof" match env.find? goal with | some (.defnInfo _) => - if moduleOf goal != some generated then + if project.owner[goal]? != some generated then return some s!"{goal} is not the goal {generated} defines" | _ => return some s!"{generated} defines no goal {goal}" match env.find? proof with | some (.thmInfo v) => - if moduleOf proof != some module then + if project.owner[proof]? != some module then return some s!"{proof} is not declared in {module}" if v.type != .const goal [] then return some s!"{proof} proves {v.type}, not {goal}" @@ -100,80 +158,46 @@ def checkStatement (env : Environment) (goal module : Name) (allowed : NameSet) | some _ => return some s!"{proof} is not a theorem" | none => return some s!"{module} declares no {proof}" -/-- A goal is proved when every module of the project its proof imports passes -the kernel (each replayed once in a run), and its proof states exactly the -goal and uses only the allowed axioms. Imported data is never freed: a later -import in the process reads it. -/ -unsafe def checkGoal (goal module : Name) (allowed : NameSet) (toolchain : String) - (replayed : IO.Ref NameSet) : IO (Option String) := do - let env ← importModules #[{ module }] {} - let project ← env.header.moduleNames.filterM fun m => - return !(← findOLean m).toString.startsWith toolchain - let why := checkStatement env goal module allowed - for m in project do - if (← replayed.get).contains m then continue - try replayModule m - catch e => return some s!"the kernel rejects {m}: {e}" - replayed.modify (·.insert m) - return why - -/-- Every goal checked in one environment: each proof module imported once, -and every module of the project replayed together into the environment of the -toolchain's modules they import. A check reads only kernel constants, each -in the module that declares it, so proofs imported together cannot change -each other's checks; but one bad module would stop the replay of all, and a -proof file that declares a goal's name stops the import, so then none is -reported (`none`) and each goal is checked by itself. A proof file of -cppverify_auto imports `Lean`, whose import each goal would repeat. -/ -unsafe def checkTogether (entries : Array (Name × Name)) (allowed : NameSet) - (toolchain : String) : IO (Option (Array (Option String))) := do - let modules := entries.foldl (fun ms (_, m) => if ms.contains m then ms else ms.push m) #[] - let some env ← (try some <$> importModules (modules.map ({ module := · })) {} - catch _ => pure none) | return none - let project ← env.header.moduleNames.filterM fun m => - return !(← findOLean m).toString.startsWith toolchain - let mut imports : Array Import := #[] - let mut constants : Std.HashMap Name ConstantInfo := {} - for m in project do - let (own, declared) ← moduleConstants m - for i in own do - unless project.contains i.module || imports.any (·.module == i.module) do - imports := imports.push i - -- Lean derives an equation lemma in each module that unfolds the - -- definition, the same constant every time. - for (name, info) in declared do - if let some known := constants[name]? then - unless known.type == info.type && known.value? == info.value? do - return none - continue - constants := constants.insert name info - try replayInto imports constants catch _ => return none - return some (entries.map fun (goal, module) => checkStatement env goal module allowed) +/-- The declaration of the user's lemmas that uses `sorry`, if one does: an +admitted lemma fails every goal, as when the module was compiled with `sorry` +an error. -/ +def userSorry (closure : Closure) (project : Replayed) : Option String := Id.run do + let some user := closure.modules.find? (·.name == `CppVerify.User) | return none + for name in user.declared do + if let .ok axioms := axiomsOf project.env name then + if axioms.contains ``sorryAx then + return some s!"{name} of CppVerify.User uses sorry" + return none -/-- Usage: Certify GOALS ALLOWED, where each line of GOALS is a goal and its -proof module, separated by a tab, and ALLOWED lists the axioms a proof may -use, separated by commas. Prints one line per goal: `ok` or `fail`, the goal, -and why it failed. -/ +/-- Usage: Certify GOALS ALLOWED, where each line of GOALS is a goal, its +proof module, and the module that defines it, separated by tabs, and ALLOWED +lists the axioms a proof may use, separated by commas. Prints one line per +goal: `ok` or `fail`, the goal, and why it failed. A goal is proved when its +proof module and its generated module pass the kernel, with every module of +the project they import, and its proof states exactly the goal and uses only +the allowed axioms. The generated modules are replayed first, so that a +proof file that declares a name one declares is the one left out. -/ unsafe def main (args : List String) : IO UInt32 := do let [goals, allowed] := args | throw <| IO.userError "usage: Certify GOALS ALLOWED" let sysroot ← findSysroot initSearchPath sysroot let toolchain := (sysroot / "lib" / "lean").toString let allowed := (allowed.splitOn ",").foldl (fun s a => s.insert a.toName) ({} : NameSet) - let mut entries : Array (Name × Name) := #[] + let mut entries : Array (Name × Name × Name) := #[] for line in ← IO.FS.lines goals do - let [goal, module] := line.splitOn "\t" | continue - entries := entries.push (goal.toName, module.toName) - let report (goal : Name) : Option String → IO Unit + let [goal, module, generated] := line.splitOn "\t" | continue + entries := entries.push (goal.toName, module.toName, generated.toName) + let roots := entries.map (·.2.2) ++ entries.map (·.2.1) + let (_, closure) ← (roots.forM (Closure.visit toolchain)).run {} + let project ← replayProject closure + let user := userSorry closure project + for (goal, module, generated) in entries do + let why := (project.rejected[module]?).orElse fun _ => + (project.rejected[generated]?).orElse fun _ => user.orElse fun _ => + checkStatement project goal module generated allowed + match why with | none => IO.println s!"ok\t{goal}" | some why => IO.println s!"fail\t{goal}\t{why.replace "\n" " "}" - if let some results ← checkTogether entries allowed toolchain then - for (goal, _) in entries, why in results do - report goal why - return 0 - let replayed ← IO.mkRef ({} : NameSet) - for (goal, module) in entries do - report goal (← checkGoal goal module allowed toolchain replayed) return 0 )lean"; diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index f317e60815..841c52b63f 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -32,6 +32,7 @@ #include "llvm/ADT/ScopeExit.h" #include "llvm/ADT/SmallString.h" #include "llvm/ADT/SmallVector.h" +#include "llvm/ADT/StringExtras.h" #include "llvm/Support/Error.h" #include "llvm/Support/FileSystem.h" #include "llvm/Support/FormatVariadic.h" @@ -41,6 +42,7 @@ #include "llvm/Support/MemoryBuffer.h" #include "llvm/Support/Path.h" #include "llvm/Support/Program.h" +#include "llvm/Support/SHA256.h" #include "llvm/Support/ThreadPool.h" #include "llvm/Support/Threading.h" #include "llvm/Support/raw_ostream.h" @@ -1255,6 +1257,28 @@ static llvm::Error writeTextFile(llvm::StringRef Path, return llvm::Error::success(); } +// A generated file is rewritten only when it changes, so that a rerun of the +// same source leaves every file as it was. +static llvm::Error writeTextFileIfChanged(llvm::StringRef Path, + llvm::StringRef Contents) { + if (auto Buffer = llvm::MemoryBuffer::getFile(Path, /*IsText=*/true)) + if ((*Buffer)->getBuffer() == Contents) + return llvm::Error::success(); + return writeTextFile(Path, Contents); +} + +static constexpr llvm::StringLiteral LeanGeneratedNote = + "/- Generated by CppVerify. Regeneration replaces this file, never a " + "proof. -/"; + +// What each module of goals starts with: options and the instance attribute +// of the prelude's classical decidability are local to a file. +static constexpr llvm::StringLiteral LeanGoalModulePreamble = + "noncomputable section\n\n" + "set_option maxRecDepth 100000\n" + "set_option maxHeartbeats 0\n\n" + "attribute [local instance] cppVerifyPropDecidable\n\n"; + static llvm::Error writeTextFileIfMissing(llvm::StringRef Path, llvm::StringRef Contents) { if (llvm::sys::fs::exists(Path)) @@ -1314,18 +1338,28 @@ struct LeanProofRecord { std::string Automation; }; -// A proof starts from the goal's readable form, its names introduced. Stubs -// before cppverify_auto did not import it. -static std::string leanProofHead(llvm::StringRef Goal, bool Automation = true) { - return "import CppVerify.User\n" + - std::string(Automation ? "import CppVerify.Auto\n" : "") + - "\ntheorem " + Goal.str() + "_proof : " + Goal.str() + +// The imports a proof file starts with: its function's goals, the user's +// lemmas, and the automation. Before 0.2's modules a proof imported only +// User (which imported every goal), and before cppverify_auto, not Auto. +enum class LeanProofImports { Modules, Automation, User }; + +// A proof starts from the goal's readable form, its names introduced. +static std::string +leanProofHead(llvm::StringRef Goal, llvm::StringRef Group, + LeanProofImports Imports = LeanProofImports::Modules) { + std::string Head; + if (Imports == LeanProofImports::Modules) + Head += "import CppVerify.Goals." + Group.str() + "\n"; + Head += "import CppVerify.User\n"; + if (Imports != LeanProofImports::User) + Head += "import CppVerify.Auto\n"; + return Head + "\ntheorem " + Goal.str() + "_proof : " + Goal.str() + " := by\n apply " + Goal.str() + ".of_readable\n"; } -static std::string leanProof(llvm::StringRef Goal, llvm::StringRef Intros, - llvm::StringRef Last) { - std::string Proof = leanProofHead(Goal); +static std::string leanProof(llvm::StringRef Goal, llvm::StringRef Group, + llvm::StringRef Intros, llvm::StringRef Last) { + std::string Proof = leanProofHead(Goal, Group); if (!Intros.empty()) Proof += " intro " + Intros.str() + "\n"; return Proof + " " + Last.str() + "\n"; @@ -1335,9 +1369,15 @@ static std::string leanProof(llvm::StringRef Goal, llvm::StringRef Intros, // whether cppverify_auto proves it: its last line is a stub's `sorry` or a // step of cppverify_auto. static std::optional leanGeneratedProof(llvm::StringRef Body, - llvm::StringRef Goal) { - if (!Body.consume_front(leanProofHead(Goal)) && - !Body.consume_front(leanProofHead(Goal, /*Automation=*/false))) + llvm::StringRef Goal, + llvm::StringRef Group) { + if (!llvm::any_of( + std::initializer_list{LeanProofImports::Modules, + LeanProofImports::Automation, + LeanProofImports::User}, + [&](LeanProofImports Imports) { + return Body.consume_front(leanProofHead(Goal, Group, Imports)); + })) return std::nullopt; if (Body.consume_front(" intro ")) { const size_t End = Body.find('\n'); @@ -1354,6 +1394,10 @@ static std::optional leanGeneratedProof(llvm::StringRef Body, } // The revision of cppverify_auto that an automation note was written by. +// Names the printing of spec definitions and the prelude's tactic for their +// measures: a verdict an earlier revision kept is not used. +static constexpr llvm::StringLiteral LeanSpecRevision = "1"; + static std::string leanAutomationTag() { return ("cppverify_auto " + LeanAutomationRevision + " ").str(); } @@ -1407,8 +1451,9 @@ static std::optional readLeanProof(llvm::StringRef Path) { return std::nullopt; const size_t End = Text.find("-/\n"); if (End != llvm::StringRef::npos) - if (std::optional Automatic = - leanGeneratedProof(Text.substr(End + 3), Record.Goal)) { + if (std::optional Automatic = leanGeneratedProof( + Text.substr(End + 3), Record.Goal, + llvm::sys::path::filename(llvm::sys::path::parent_path(Path)))) { Record.Pristine = true; Record.Automatic = *Automatic; } @@ -1428,7 +1473,8 @@ static void replaceAllIn(std::string &Text, llvm::StringRef From, static llvm::Error moveLeanProof(llvm::StringRef From, llvm::StringRef To, const LeanProjectGoal &Goal, llvm::StringRef OldGoal, - llvm::StringRef OldBodies) { + llvm::StringRef OldBodies, + llvm::StringRef OldGroup = "") { auto Buffer = llvm::MemoryBuffer::getFile(From); if (!Buffer) return llvm::createStringError( @@ -1449,6 +1495,9 @@ static llvm::Error moveLeanProof(llvm::StringRef From, llvm::StringRef To, } replaceAllIn(Body, OldGoal, Goal.Name); replaceAllIn(Body, OldBodies, Goal.BodyPrefix); + if (!OldGroup.empty()) + replaceAllIn(Body, ("import CppVerify.Goals." + OldGroup + "\n").str(), + "import CppVerify.Goals." + Goal.Group + "\n"); if (std::error_code EC = llvm::sys::fs::create_directories(llvm::sys::path::parent_path(To))) return llvm::createStringError(EC, "cannot create %s", To.str().c_str()); @@ -1623,7 +1672,7 @@ class Verifier { } } - llvm::Expected initializeLeanProject() { + llvm::Error initializeLeanProject() { const std::string &Root = leanProjectRoot(); std::error_code EC = llvm::sys::fs::create_directories( leanProjectPath(Root, {"CppVerify", "Proofs"})); @@ -1672,18 +1721,69 @@ class Verifier { leanProjectPath(Root, {"lakefile.toml"}), Lakefile)) return std::move(Error); + // A project of an earlier release imports CppVerify.Generated here, + // which still imports every goal. constexpr llvm::StringLiteral UserFile = - "import CppVerify.Generated\n\n" + "import CppVerify.Specs\n\n" "/- Add reusable lemmas here. This file is never regenerated. -/\n"; if (llvm::Error Error = writeTextFileIfMissing( leanProjectPath(Root, {"CppVerify", "User.lean"}), UserFile)) - return std::move(Error); - if (llvm::Error Error = - writeTextFile(leanProjectPath(Root, {"CppVerify", "Auto.lean"}), - LeanAutomationSource)) - return std::move(Error); + return Error; + + std::string Prelude = std::string(LeanGeneratedNote) + "\n\n"; + llvm::raw_string_ostream PreludeOS(Prelude); + emitLeanPrelude(PreludeOS, /*Project=*/true); + for (const auto &[File, Contents] : + {std::pair{"Prelude.lean", Prelude}, + {"Auto.lean", LeanAutomationSource}}) + if (llvm::Error Error = writeTextFileIfChanged( + leanProjectPath(Root, {"CppVerify", File}), Contents)) + return Error; + // The root of the library, so that `lake build` builds every proof. + return writeTextFileIfChanged(leanProjectPath(Root, {"CppVerify.lean"}), + "import CppVerify.Check\n"); + } - return leanProjectPath(Root, {"CppVerify", "Generated.lean"}); + // The generated modules of a run: Specs, a goal module for each function + // the run exported, and Generated, which imports them all. Any other goal + // module is removed, so that every module of the project builds: one an + // earlier run wrote may apply a spec Specs no longer declares, as after a + // fallback run whose solver settled the functions that applied it. The + // proofs of a function the run did not export stay as they are. + llvm::Error writeLeanProjectModules(const LeanProjectModules &Modules) { + const std::string &Root = leanProjectRoot(); + const std::string Header = std::string(LeanGeneratedNote) + "\n"; + if (llvm::Error Error = writeTextFileIfChanged( + leanProjectPath(Root, {"CppVerify", "Specs.lean"}), + Header + + "import CppVerify.Prelude\n\nnoncomputable section\n\n" + "attribute [local instance] cppVerifyPropDecidable\n\n" + + leanSpecsText(Modules))) + return Error; + const std::string GoalsDir = leanProjectPath(Root, {"CppVerify", "Goals"}); + if (std::error_code EC = llvm::sys::fs::create_directories(GoalsDir)) + return llvm::createStringError(EC, "cannot create %s", GoalsDir.c_str()); + std::string Generated = Header + "import CppVerify.Prelude\n" + "import CppVerify.Specs\n"; + for (const std::string &Group : Modules.Order) { + if (llvm::Error Error = writeTextFileIfChanged( + leanProjectPath(GoalsDir, {Group + ".lean"}), + Header + "import CppVerify.Specs\n\n" + + LeanGoalModulePreamble.str() + Modules.Goals.at(Group))) + return Error; + Generated += "import CppVerify.Goals." + Group + "\n"; + } + if (llvm::Error Error = writeTextFileIfChanged( + leanProjectPath(Root, {"CppVerify", "Generated.lean"}), Generated)) + return Error; + + std::error_code EC; + for (llvm::sys::fs::directory_iterator It(GoalsDir, EC), End; + It != End && !EC; It.increment(EC)) + if (llvm::sys::path::extension(It->path()) == ".lean" && + !Modules.Goals.count(llvm::sys::path::stem(It->path()).str())) + llvm::sys::fs::remove(It->path()); + return llvm::Error::success(); } static std::vector @@ -1802,8 +1902,9 @@ class Verifier { (Moving->Path != ProofPath || !Taken.count(ProofPath))) { const bool WasKept = llvm::StringRef(Moving->Path).starts_with(StaleDir); - if (llvm::Error Error = moveLeanProof(Moving->Path, ProofPath, *Goal, - Moving->Goal, Moving->BodyPrefix)) + if (llvm::Error Error = + moveLeanProof(Moving->Path, ProofPath, *Goal, Moving->Goal, + Moving->BodyPrefix, groupOf(*Moving))) return Error; Diags.push_back({VerifyDiagnostic::Warning, "the Lean proof of " + Goal->StableId + @@ -1841,9 +1942,10 @@ class Verifier { llvm::sys::path::parent_path(ProofPath))) return llvm::createStringError(EC, "cannot create %s", ProofPath.c_str()); - if (llvm::Error Error = writeTextFile( - ProofPath, leanProofHeader(*Goal) + - leanProof(Goal->Name, Goal->Intros, "sorry"))) + if (llvm::Error Error = + writeTextFile(ProofPath, leanProofHeader(*Goal) + + leanProof(Goal->Name, Goal->Group, + Goal->Intros, "sorry"))) return Error; Taken.insert(ProofPath); } @@ -1931,8 +2033,8 @@ class Verifier { CheckFile += "example : " + Name + " := " + Name + "_proof\n"; CheckFile += "#print axioms " + Name + "_proof\n"; } - return writeTextFile(leanProjectPath(Root, {"CppVerify", "Check.lean"}), - CheckFile); + return writeTextFileIfChanged( + leanProjectPath(Root, {"CppVerify", "Check.lean"}), CheckFile); } // Certifies each goal's proof: an error fails every goal; otherwise the @@ -2008,6 +2110,297 @@ class Verifier { return Launcher; } + // The specs of a project as Specs.lean declares them: each recursion group + // by its real definitions where Lean accepts them, callees first, and + // opaque where it does not, where a member has no definition, or where no + // Lean is installed to try them. Lean's verdict on a group's text, with + // what its callees are, is kept in .cppverify/specs, so that the file is + // the same on every run. A group is tried with its undecided callees real + // and keeps its verdict only if they are; else it is tried again with the + // rejected callees opaque. + std::string leanSpecsText(const LeanProjectModules &Modules) { + const auto &Specs = Modules.Specs; + // Strongly connected components of the calls, callees first (Tarjan). + std::vector> Groups; + std::map GroupOf; + { + std::map Index, Low; + std::set OnStack; + std::vector Stack; + unsigned Counter = 0; + std::function visit = + [&](const std::string &V) { + Index[V] = Low[V] = Counter++; + Stack.push_back(V); + OnStack.insert(V); + for (const std::string &W : Specs.at(V).Applies) { + if (!Specs.count(W)) + continue; + if (!Index.count(W)) { + visit(W); + Low[V] = std::min(Low[V], Low[W]); + } else if (OnStack.count(W)) { + Low[V] = std::min(Low[V], Index[W]); + } + } + if (Low[V] != Index[V]) + return; + std::vector Group; + std::string W; + do { + W = Stack.back(); + Stack.pop_back(); + OnStack.erase(W); + Group.push_back(W); + GroupOf[W] = Groups.size(); + } while (W != V); + std::sort(Group.begin(), Group.end()); + Groups.push_back(std::move(Group)); + }; + for (const auto &[Identity, Declaration] : Specs) + if (!Index.count(Identity)) + visit(Identity); + } + std::vector> Callees(Groups.size()); + std::vector Definition(Groups.size()); + // 1 real, 0 opaque, -1 undecided. + std::vector Verdict(Groups.size(), -1); + for (size_t G = 0; G != Groups.size(); ++G) { + for (const std::string &Member : Groups[G]) { + const LeanSpecDeclaration &Declaration = Specs.at(Member); + if (Declaration.Definition.empty()) + Verdict[G] = 0; + Definition[G] += Declaration.Definition; + for (const std::string &Callee : Declaration.Applies) + if (Specs.count(Callee) && GroupOf.at(Callee) != G) + Callees[G].insert(GroupOf.at(Callee)); + } + if (Groups[G].size() > 1) + Definition[G] = "mutual\n" + Definition[G] + "end\n\n"; + } + auto opaque = [&](size_t G) { + std::string Text; + for (const std::string &Member : Groups[G]) + Text += Specs.at(Member).Opaque; + return Text; + }; + // What a group's verdict rests on: the toolchain, this revision of the + // printer and the prelude's tactic, its text, and what its callees are. + auto keyOf = [&](size_t G, const std::set &Assumed) { + llvm::SHA256 Hasher; + Hasher.update(LeanToolchain); + Hasher.update(LeanSpecRevision); + Hasher.update(Definition[G]); + for (size_t C : Callees[G]) + Hasher.update(Groups[C].front() + (Verdict[C] == 1 || Assumed.count(C) + ? "=real" + : "=opaque")); + return llvm::toHex(Hasher.final()); + }; + const std::string &Root = leanProjectRoot(); + const std::string Dir = leanProjectPath(Root, {".cppverify", "specs"}); + std::optional Launcher; + bool LeanUnavailable = false; + for (size_t Round = 0; Round <= Groups.size(); ++Round) { + std::set Trying; + std::map Keys; + for (size_t G = 0; G != Groups.size(); ++G) { + if (Verdict[G] >= 0) + continue; + const bool CalleesDecided = + llvm::all_of(Callees[G], [&](size_t C) { return Verdict[C] >= 0; }); + const std::string Key = keyOf(G, Trying); + if (CalleesDecided) + if (auto Kept = + llvm::MemoryBuffer::getFile(leanProjectPath(Dir, {Key}))) { + Verdict[G] = (*Kept)->getBuffer().trim() == "real" ? 1 : 0; + continue; + } + if (LeanUnavailable) { + Verdict[G] = 0; + continue; + } + Trying.insert(G); + Keys[G] = Key; + } + if (Trying.empty()) + break; + std::map Axioms; + if (!tryLeanSpecs(Specs, Groups, Definition, Verdict, Trying, Launcher, + opaque, Axioms)) { + LeanUnavailable = true; + for (size_t G : Trying) + Verdict[G] = 0; + break; + } + std::map Accepted; + for (size_t G : Trying) + Accepted[G] = llvm::all_of(Groups[G], [&](const std::string &Member) { + auto It = Axioms.find(Specs.at(Member).Name); + if (It == Axioms.end() || It->second == "missing") + return false; + llvm::SmallVector Used; + llvm::StringRef(It->second).split(Used, ',', -1, false); + return llvm::all_of(Used, [](llvm::StringRef Axiom) { + return Axiom == "propext" || Axiom == "Quot.sound" || + Axiom == "Classical.choice"; + }); + }); + // A callee decided before this round was what the trial assumed; one + // tried in it was assumed real. + for (size_t G : Trying) { + if (!llvm::all_of(Callees[G], [&](size_t C) { + return !Trying.count(C) || Accepted[C]; + })) + continue; + Verdict[G] = Accepted[G] ? 1 : 0; + if (!llvm::sys::fs::create_directories(Dir)) + llvm::consumeError( + writeTextFile(leanProjectPath(Dir, {Keys[G]}), + Accepted[G] ? "real\n" : "opaque\n")); + } + } + std::string Text; + for (size_t G = 0; G != Groups.size(); ++G) + Text += Verdict[G] == 1 ? Definition[G] : opaque(G); + return Text; + } + + // Elaborates the spec groups of Trying with the others as decided, in a + // file of their own, and reports the axioms of each member of Trying: a + // definition Lean rejects is added with sorryAx, or not at all. False when + // no pinned Lean can run it. + bool tryLeanSpecs(const std::map &Specs, + const std::vector> &Groups, + const std::vector &Definition, + const std::vector &Verdict, + const std::set &Trying, + std::optional &Launcher, + llvm::function_ref Opaque, + std::map &Axioms) { + const std::string &Root = leanProjectRoot(); + if (!Launcher) { + auto Found = leanLauncher(".cppverify-specs"); + if (!Found) { + llvm::consumeError(Found.takeError()); + return false; + } + if (auto Build = Found->run({"build", "CppVerify.Auto"}, "build", Root); + !Build) { + llvm::consumeError(Build.takeError()); + return false; + } + Launcher = std::move(*Found); + } + const std::string Dir = leanProjectPath(Root, {".cppverify", "specs"}); + if (llvm::sys::fs::create_directories(Dir)) + return false; + const std::string Source = leanProjectPath(Dir, {"trial.lean"}); + const std::string Report = leanProjectPath(Dir, {"trial.report"}); + std::string Quoted = "\""; + for (char C : Report) { + if (C == '\\' || C == '"') + Quoted += '\\'; + Quoted += C; + } + Quoted += "\""; + std::string Text = "import CppVerify.Auto\n\n#eval CppVerify.Auto.report " + + Quoted + + " \"ready\"\n\nnoncomputable section\n\n" + "attribute [local instance] cppVerifyPropDecidable\n\n"; + for (size_t G = 0; G != Groups.size(); ++G) { + if (Verdict[G] == 1 || Trying.count(G)) + Text += Definition[G]; + else + Text += Opaque(G); + if (Trying.count(G)) + for (const std::string &Member : Groups[G]) + Text += "#cppverify_axioms " + Quoted + " " + Specs.at(Member).Name + + "\n\n"; + } + llvm::sys::fs::remove(Report); + if (llvm::Error Error = writeTextFile(Source, Text)) { + llvm::consumeError(std::move(Error)); + return false; + } + // Lean exits with an error status when a definition fails; the report + // says which. + if (auto Run = Launcher->run({"env", "lean", "-DmaxErrors=1000000", Source}, + "specs", Root); + !Run) + llvm::consumeError(Run.takeError()); + auto Buffer = llvm::MemoryBuffer::getFile(Report); + if (!Buffer) + return false; + bool Ready = false; + for (llvm::StringRef Rest = (*Buffer)->getBuffer(); !Rest.empty();) { + auto [Line, Next] = Rest.split('\n'); + Rest = Next; + Line = Line.rtrim("\r"); + if (Line == "ready") { + Ready = true; + continue; + } + llvm::SmallVector Fields; + Line.split(Fields, '\t', 2); + if (Fields.size() == 3 && Fields[0] == "axioms") + Axioms[Fields[1].str()] = Fields[2].str(); + } + return Ready; + } + + // What a proof is built from: the pinned toolchain, its source, and the + // compiled modules of the project in its import closure, read from the + // import lines of their sources. None when a module of the closure has no + // compiled module. + std::optional leanProofKey(llvm::StringRef ProofSource) { + const std::string &Root = leanProjectRoot(); + auto importsOf = [](llvm::StringRef Source) { + std::vector Imports; + if (auto Buffer = llvm::MemoryBuffer::getFile(Source)) + for (llvm::StringRef Rest = (*Buffer)->getBuffer(); !Rest.empty();) { + auto [Line, Next] = Rest.split('\n'); + Rest = Next; + if (Line.consume_front("import ")) + Imports.push_back(Line.trim().str()); + } + return Imports; + }; + llvm::SHA256 Hasher; + Hasher.update(LeanToolchain); + auto Source = llvm::MemoryBuffer::getFile(ProofSource); + if (!Source) + return std::nullopt; + Hasher.update((*Source)->getBuffer()); + std::map Compiled; + std::vector Work = importsOf(ProofSource); + while (!Work.empty()) { + const std::string Module = Work.back(); + Work.pop_back(); + if (Compiled.count(Module)) + continue; + std::string Relative = Module; + std::replace(Relative.begin(), Relative.end(), '.', '/'); + const std::string ModuleSource = + leanProjectPath(Root, {Relative + ".lean"}); + if (!llvm::sys::fs::exists(ModuleSource)) + continue; + auto Object = llvm::MemoryBuffer::getFile(leanProjectPath( + Root, {".lake", "build", "lib", "lean", Relative + ".olean"})); + if (!Object) + return std::nullopt; + Compiled[Module] = llvm::toHex(llvm::SHA256::hash( + llvm::arrayRefFromStringRef((*Object)->getBuffer()))); + for (std::string &Import : importsOf(ModuleSource)) + Work.push_back(std::move(Import)); + } + for (const auto &[Module, Hash] : Compiled) { + Hasher.update(Module); + Hasher.update(Hash); + } + return llvm::toHex(Hasher.final()); + } + llvm::Expected> certifyLeanProject(const std::vector &ProjectGoals) { if (ProjectGoals.empty()) @@ -2028,15 +2421,6 @@ class Verifier { !Build) return Build.takeError(); - const std::string UserObject = leanProjectPath( - Root, {".lake", "build", "lib", "lean", "CppVerify", "User.olean"}); - if (auto User = - runLake({"env", "lean", "-EhasSorry", "-R", Root, "-o", UserObject, - leanProjectPath(Root, {"CppVerify", "User.lean"})}, - "user"); - !User) - return User.takeError(); - const std::string ProofBuildDir = leanProjectPath( Root, {".lake", "build", "lib", "lean", "CppVerify", "Proofs"}); if (std::error_code EC = llvm::sys::fs::create_directories(ProofBuildDir)) @@ -2053,7 +2437,14 @@ class Verifier { leanProjectPath(ProofBuildDir, {Goal->Group}))) return llvm::createStringError( EC, "cannot create Lean proof build directory"); - // Each proof builds by itself, several at once. + // Each proof builds by itself, several at once, unless nothing it is + // built from changed since it last built: its source and the compiled + // modules of the project it imports (which Lake has just built). Lake + // cannot say this itself: a module whose import failed is not built and + // not named, and its .olean of an earlier build would stay. + const std::string KeyDir = leanProjectPath(Root, {".cppverify", "built"}); + if (std::error_code EC = llvm::sys::fs::create_directories(KeyDir)) + return llvm::createStringError(EC, "cannot create %s", KeyDir.c_str()); std::vector> BuildErrors(Proofs.size()); std::atomic NextProof{0}; auto buildProofs = [&] { @@ -2064,13 +2455,22 @@ class Verifier { leanProjectPath(Root, leanProofComponents(*Goal, File)); const std::string ProofObject = leanProjectPath( leanProjectPath(ProofBuildDir, {Goal->Group}), {Name + ".olean"}); + const std::string KeyFile = leanProjectPath(KeyDir, {Name}); + const std::optional Key = leanProofKey(ProofSource); + if (Key && llvm::sys::fs::exists(ProofObject)) + if (auto Kept = llvm::MemoryBuffer::getFile(KeyFile)) + if ((*Kept)->getBuffer() == *Key) + continue; llvm::sys::fs::remove(ProofObject); + llvm::sys::fs::remove(KeyFile); if (auto Proof = runLake({"env", "lean", "-EhasSorry", "-R", Root, "-o", ProofObject, ProofSource}, Name); !Proof) BuildErrors[I] = llvm::StringRef(llvm::toString(Proof.takeError())).rtrim().str(); + else if (Key) + llvm::consumeError(writeTextFile(KeyFile, *Key)); } }; { @@ -2088,7 +2488,8 @@ class Verifier { Failures[Name] = *BuildErrors[I]; continue; } - Built += Name + "\tCppVerify.Proofs." + Goal->Group + "." + Name + "\n"; + Built += Name + "\tCppVerify.Proofs." + Goal->Group + "." + Name + + "\tCppVerify.Goals." + Goal->Group + "\n"; } if (Built.empty()) return Failures; @@ -2179,7 +2580,8 @@ class Verifier { : ""; for (size_t Next = 0; Next < Goals.size() && !interruptRequested();) { - std::string Text = "import CppVerify.User\nimport CppVerify.Auto\n\n" + std::string Text = "import CppVerify.Generated\nimport CppVerify.User\n" + "import CppVerify.Auto\n\n" "set_option cppverify.autoReport " + ReportName + "\n#eval CppVerify.Auto.report " + ReportName + " \"ready\"\n"; @@ -2373,8 +2775,9 @@ class Verifier { {VerifyDiagnostic::Warning, "cppverify_auto was not tried on the new Lean goals: " + Why}); }; - if (auto Build = Launcher->run( - {"build", "CppVerify.User", "CppVerify.Auto"}, "build", Root); + if (auto Build = Launcher->run({"build", "CppVerify.Generated", + "CppVerify.User", "CppVerify.Auto"}, + "build", Root); !Build) return skipped( "the project does not build (" + @@ -2425,10 +2828,10 @@ class Verifier { const std::string Text = Trial.Step.empty() ? leanProofHeader(Goal, Tag + Trial.Why) + - leanProof(Goal.Name, Goal.Intros, "sorry") + leanProof(Goal.Name, Goal.Group, Goal.Intros, "sorry") : leanProofHeader(Goal, Tag + "proves it with " + Trial.Step, /*Automatic=*/true) + - leanProof(Goal.Name, Goal.Intros, Trial.Step); + leanProof(Goal.Name, Goal.Group, Goal.Intros, Trial.Step); if (llvm::Error Error = writeTextFile(pathOf(Goal), Text)) Failures.push_back(llvm::toString(std::move(Error))); } @@ -2664,19 +3067,16 @@ class Verifier { std::string LeanOutputPath = Opts.LeanOutPath; const bool HasLeanProject = !Opts.LeanProjectPath.empty() || !Opts.LeanFallbackProjectPath.empty(); + // A project's goals go to modules, one per function. + LeanProjectModules LeanModules; if (HasLeanProject) { - auto GeneratedPath = initializeLeanProject(); - if (!GeneratedPath) { + if (llvm::Error Error = initializeLeanProject()) { Diags.push_back({VerifyDiagnostic::Error, "cannot initialize Lean project (" + - llvm::toString(GeneratedPath.takeError()) + ")"}); + llvm::toString(std::move(Error)) + ")"}); return false; } - LeanOutputPath = std::move(*GeneratedPath); - } - if ((Opts.Backend == BackendKind::Lean || - !Opts.LeanFallbackProjectPath.empty()) && - !LeanOutputPath.empty()) { + } else if (Opts.Backend == BackendKind::Lean && !LeanOutputPath.empty()) { std::error_code EC; LeanFile = std::make_unique(LeanOutputPath, EC, llvm::sys::fs::OF_Text); @@ -2720,11 +3120,12 @@ class Verifier { if (!Parallel) SharedBackend = createVerifyBackend( Opts.Backend, LeanOut, Opts.BMCUnroll, Execution, - Opts.LeanProjectPath.empty() ? nullptr : &LeanProjectGoals); + Opts.LeanProjectPath.empty() ? nullptr : &LeanProjectGoals, + Opts.LeanProjectPath.empty() ? nullptr : &LeanModules); std::unique_ptr LeanFallbackBackend; if (!Opts.LeanFallbackProjectPath.empty()) - LeanFallbackBackend = std::make_unique( - LeanFile.get(), &LeanProjectGoals); + LeanFallbackBackend = + std::make_unique(&LeanModules, &LeanProjectGoals); // Vacuity checks: whether a verified function's end is reachable at all. // A vacuous path is refuted quickly; a satisfiable one is not worth // searching long, since an unsettled check only omits a warning. @@ -4160,15 +4561,14 @@ class Verifier { // certified one is a proof like a solver's, and one that fails, or that // certification does not check, establishes nothing. if (HasLeanProject) { - if (LeanFile) { - LeanFile->flush(); - LeanFile.reset(); - } std::vector ExportedGoals; llvm::copy_if(LeanProjectGoals, std::back_inserter(ExportedGoals), [](const LeanProjectGoal &Goal) { return Goal.Exported; }); - llvm::Error Finalized = finalizeLeanProject( - LeanProjectGoals, LeanFallbackBackend ? &LeanRunGroups : nullptr); + const std::set *RunGroups = + LeanFallbackBackend ? &LeanRunGroups : nullptr; + llvm::Error Finalized = writeLeanProjectModules(LeanModules); + if (!Finalized) + Finalized = finalizeLeanProject(LeanProjectGoals, RunGroups); if (!Finalized && Opts.LeanAuto) automateLeanProject(LeanProjectGoals); if (!Finalized) diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_first.cpp b/clang/test/Verify/suite/Inputs/lean_certifier_first.cpp new file mode 100644 index 0000000000..29404fc469 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_certifier_first.cpp @@ -0,0 +1,11 @@ +int early() + cppverify::post(cppverify::result == 2) +{ + return 1; +} + +int fine() + cppverify::post(cppverify::result == 1) +{ + return 1; +} diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_missing_return_54ae7c80.lean index 24d917ca90..53b4aee615 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_missing_return_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_missing_return_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_fine_52006a import CppVerify.User theorem cppverify_fine_52006a_missing_return_54ae7c80_proof : cppverify_fine_52006a_missing_return_54ae7c80 := by diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_postcondition_cd6bdfcd.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_postcondition_cd6bdfcd.lean index 2d440f8a0e..415249b275 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_postcondition_cd6bdfcd.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_postcondition_cd6bdfcd.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_fine_52006a import CppVerify.User theorem cppverify_fine_52006a_postcondition_cd6bdfcd_proof : cppverify_fine_52006a_postcondition_cd6bdfcd := by diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean index f7d3d1a1a7..c6061d122c 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User theorem cppverify_one_99bcee_missing_return_54ae7c80_proof : cppverify_one_99bcee_missing_return_54ae7c80 := by diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/first/cppverify_early_103f65_postcondition_646d2761.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/first/cppverify_early_103f65_postcondition_646d2761.lean new file mode 100644 index 0000000000..cc38fc4238 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/first/cppverify_early_103f65_postcondition_646d2761.lean @@ -0,0 +1,5 @@ +/- A goal of the same name of its own, true, in the proof of the goal that + comes first, which imports nothing of the project. -/ +def cppverify_early_103f65_postcondition_646d2761 : Prop := True + +theorem cppverify_early_103f65_postcondition_646d2761_proof : cppverify_early_103f65_postcondition_646d2761 := trivial diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/hidden/cppverify_one_99bcee_postcondition_646d2761.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/hidden/cppverify_one_99bcee_postcondition_646d2761.lean index 823511abad..3ed1c6e593 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/hidden/cppverify_one_99bcee_postcondition_646d2761.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/hidden/cppverify_one_99bcee_postcondition_646d2761.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User /- An axiom behind a lemma. -/ diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/Lemmas.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/Lemmas.lean index 0897c5c20f..71e1a1f4ad 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/Lemmas.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/Lemmas.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User import Lean diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/cppverify_one_99bcee_postcondition_646d2761.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/cppverify_one_99bcee_postcondition_646d2761.lean index f5ce026671..ed060924ed 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/cppverify_one_99bcee_postcondition_646d2761.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/cppverify_one_99bcee_postcondition_646d2761.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User theorem cppverify_one_99bcee_postcondition_646d2761_proof : True := trivial diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/unchecked/cppverify_one_99bcee_postcondition_646d2761.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/unchecked/cppverify_one_99bcee_postcondition_646d2761.lean index 296d7e4797..0c477a9fa8 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/unchecked/cppverify_one_99bcee_postcondition_646d2761.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/unchecked/cppverify_one_99bcee_postcondition_646d2761.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User import Lean diff --git a/clang/test/Verify/suite/Inputs/lean_collections.cpp b/clang/test/Verify/suite/Inputs/lean_collections.cpp new file mode 100644 index 0000000000..333d61d940 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_collections.cpp @@ -0,0 +1,60 @@ +// Sequences, sets, multisets, and maps in a Lean project, for +// lean_collections.test. +using cppverify::map; +using cppverify::multiset; +using cppverify::seq; +using cppverify::set; + +cppverify::spec int total(seq s) + cppverify::decreases(s.len()) +{ + return s.len() <= 0 ? 0 : total(s.subrange(0, s.len() - 1)) + s[s.len() - 1]; +} + +cppverify::proof void sequences(seq s, int x) +{ + cppverify::check(s.push(x).len() == s.len() + 1); + cppverify::check(s.push(x)[s.len()] == x); + cppverify::check((s + cppverify::seq_of(x)).contains(x)); + cppverify::check(s.subrange(0, s.len()) == s); +} + +cppverify::proof void sets(set a, int x, int y) + cppverify::pre(x != y) +{ + cppverify::check(a.insert(x).remove(y).contains(x)); + cppverify::check(a.subset_of(a.unite(cppverify::set_empty().insert(y)))); +} + +cppverify::proof void multisets(multiset m, int x) +{ + cppverify::check(m.insert(x).count(x) == m.count(x) + 1); + cppverify::check(m.insert(x).remove(x) == m); +} + +cppverify::proof void maps(map m, int k, int v) +{ + cppverify::check(m.insert(k, v)[k] == v); + cppverify::check(!m.remove(k).contains(k)); +} + +cppverify::proof void total_push(seq s, int x) + cppverify::post(total(s.push(x)) == total(s) + x) +{ +} + +cppverify::proof void wrong(set a, int x) +{ + cppverify::check(a.remove(x).contains(x) == a.contains(x)); +} + +cppverify::spec int members(set a, int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : members(a, n - 1) + (a.contains(n) ? 1 : 0); +} + +cppverify::proof void no_members(set a) + cppverify::post(members(a, 0) == 0) +{ +} diff --git a/clang/test/Verify/suite/Inputs/lean_collections_total_push.lean b/clang/test/Verify/suite/Inputs/lean_collections_total_push.lean new file mode 100644 index 0000000000..ee5b58fee6 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_collections_total_push.lean @@ -0,0 +1,13 @@ +import CppVerify.Goals.cppverify_total_push_cdfd2d +import CppVerify.User +import CppVerify.Auto + +theorem cppverify_total_push_cdfd2d_postcondition_3a9fac6f_proof : + cppverify_total_push_cdfd2d_postcondition_3a9fac6f := by + apply cppverify_total_push_cdfd2d_postcondition_3a9fac6f.of_readable + intro _ _ s x pushed _ _ _ + rw [pushed] + unfold cppSpecBody_cdfd2da1_fn_5f5a35746f74616c4e396370707665726966793373657145_1 + have := cppSeqLength_nonneg s + simp [BitVec.toInt_signExtend_of_le] + omega diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_division_by_zero_df06c970.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_division_by_zero_df06c970.lean index daf2ade742..6002daa66b 100644 --- a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_division_by_zero_df06c970.lean +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_division_by_zero_df06c970.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_reading_8d7035 import CppVerify.User theorem cppverify_reading_8d7035_division_by_zero_df06c970_proof : cppverify_reading_8d7035_division_by_zero_df06c970 := by diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_missing_return_54ae7c80.lean index 7bb7dd4b6b..8a10f2476c 100644 --- a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_missing_return_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_missing_return_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_reading_8d7035 import CppVerify.User theorem cppverify_reading_8d7035_missing_return_54ae7c80_proof : cppverify_reading_8d7035_missing_return_54ae7c80 := by diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_postcondition_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_postcondition_54ae7c80.lean index 97d154cc3c..b99f29c9e1 100644 --- a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_postcondition_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_postcondition_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_reading_8d7035 import CppVerify.User theorem cppverify_reading_8d7035_postcondition_54ae7c80_proof : cppverify_reading_8d7035_postcondition_54ae7c80 := by diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_155ffe95.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_155ffe95.lean index d8692c5599..df12dae878 100644 --- a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_155ffe95.lean +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_155ffe95.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_reading_8d7035 import CppVerify.User theorem cppverify_reading_8d7035_precondition_155ffe95_proof : cppverify_reading_8d7035_precondition_155ffe95 := by diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_814bc5b2.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_814bc5b2.lean index 5779536cb6..589c770d90 100644 --- a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_814bc5b2.lean +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_814bc5b2.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_reading_8d7035 import CppVerify.User theorem cppverify_reading_8d7035_precondition_814bc5b2_proof : cppverify_reading_8d7035_precondition_814bc5b2 := by diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean index 8e3effb2e7..8d4ca35013 100644 --- a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_sensor_contract_eb6f5c import CppVerify.User theorem cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d_proof : cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d := by diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_impossible.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_impossible.lean index 391927a090..c2cb31fbe6 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_impossible.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_impossible.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_impossible_9d6c7c import CppVerify.User theorem cppverify_impossible_9d6c7c_postcondition_1cd35301_proof : cppverify_impossible_9d6c7c_postcondition_1cd35301 := by diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_looping.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_looping.lean index b07ce3c20e..4a74afae54 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_looping.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_looping.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_looping_3f4bd4 import CppVerify.User theorem cppverify_looping_3f4bd4_postcondition_d06fccd0_proof : cppverify_looping_3f4bd4_postcondition_d06fccd0 := by diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_mixed.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_mixed.lean index 9df085a719..b6bbaa9d98 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_mixed.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_mixed.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_product_4751c3 import CppVerify.User theorem cppverify_product_4751c3_postcondition_c4d4674b_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_positive.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_positive.lean index 4a3c213156..5fd5c25e71 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_positive.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_positive.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_positive_fb6abf import CppVerify.User theorem cppverify_positive_fb6abf_postcondition_78bdd643_proof : cppverify_positive_fb6abf_postcondition_78bdd643 := by diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_same.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_same.lean index 5a8320c770..a663e3e6a1 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_same.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_same.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_same_9601c2 import CppVerify.User theorem cppverify_same_9601c2_postcondition_ce92acf8_proof : cppverify_same_9601c2_postcondition_ce92acf8 := by diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_seven.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_seven.lean index ae71525385..741439d952 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_seven.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_seven.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_seven_634ea3 import CppVerify.User theorem cppverify_seven_634ea3_postcondition_f0d135e6_proof : cppverify_seven_634ea3_postcondition_f0d135e6 := by diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_termination.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_termination.lean index 86ffa0028e..ef58ba38cf 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_termination.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_termination.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_scaled_decreases_52d363 import CppVerify.User theorem cppverify_scaled_decreases_52d363_termination_3164b050_proof : cppverify_scaled_decreases_52d363_termination_3164b050 := by diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_trusting.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_trusting.lean index 3fd338653d..d075683fb3 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_trusting.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_trusting.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_trusting_b6301a import CppVerify.User theorem cppverify_trusting_b6301a_postcondition_bafafdfb_proof : cppverify_trusting_b6301a_postcondition_bafafdfb := by diff --git a/clang/test/Verify/suite/Inputs/lean_division.cpp b/clang/test/Verify/suite/Inputs/lean_division.cpp new file mode 100644 index 0000000000..99b3672250 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_division.cpp @@ -0,0 +1,13 @@ +// C++ division and remainder in contracts, for lean_division.test. + +cppverify::proof void half_bound(int a) + cppverify::pre(a >= 4) + cppverify::post(a / 2 >= 2 && a % 2 >= 0) +{ +} + +cppverify::proof void negative_division(int a) + cppverify::pre(a < 0 && a > -100) + cppverify::post(a / 2 <= 0 && a % 3 <= 0) +{ +} diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_goal_1.lean b/clang/test/Verify/suite/Inputs/lean_fallback_goal_1.lean index 8ba810ff34..1db8715a34 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_goal_1.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_goal_1.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_fibo_step_624f01 import CppVerify.User theorem cppverify_fibo_step_624f01_missing_return_ba8abb90_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_goal_2.lean b/clang/test/Verify/suite/Inputs/lean_fallback_goal_2.lean index df65b45915..86bfafa577 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_goal_2.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_goal_2.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_fibo_step_624f01 import CppVerify.User theorem cppverify_fibo_step_624f01_postcondition_559cb60a_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_goal_3.lean b/clang/test/Verify/suite/Inputs/lean_fallback_goal_3.lean index 55b9772bad..6ec932841d 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_goal_3.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_goal_3.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_fibo_six_ec829a import CppVerify.User theorem cppverify_fibo_six_ec829a_missing_return_ba8abb90_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_goal_4.lean b/clang/test/Verify/suite/Inputs/lean_fallback_goal_4.lean index 8ebf102ec4..df78e0c7ec 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_goal_4.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_goal_4.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_fibo_six_ec829a import CppVerify.User theorem cppverify_fibo_six_ec829a_postcondition_30cd1b97_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_1.lean b/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_1.lean index aa658e5ebc..9e7048ae1a 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_1.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_1.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_bump_ce87d1 import CppVerify.User theorem cppverify_bump_ce87d1_overflow_f5ee4d20_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_2.lean b/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_2.lean index 8d12720c5a..0218241f17 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_2.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_2.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_bump_ce87d1 import CppVerify.User theorem cppverify_bump_ce87d1_assertion_06404a7a_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_bump_ce87d1_missing_return_ba8abb90.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_bump_ce87d1_missing_return_ba8abb90.lean index 145a149822..acb538820c 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_bump_ce87d1_missing_return_ba8abb90.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_bump_ce87d1_missing_return_ba8abb90.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_bump_ce87d1 import CppVerify.User theorem cppverify_bump_ce87d1_missing_return_ba8abb90_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean index f9024c9662..9bece241a3 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User theorem cppverify_one_99bcee_missing_return_54ae7c80_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd.lean index eee644659e..58448ce153 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User theorem cppverify_one_99bcee_postcondition_cd6bdfcd_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean index 7f4b99e6d4..1f724407fa 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User theorem cppverify_one_99bcee_postcondition_cd6bdfcd_2_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_ebbe6a6a.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_ebbe6a6a.lean index 5b4dde2b95..b09560a383 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_ebbe6a6a.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_ebbe6a6a.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User theorem cppverify_one_99bcee_postcondition_ebbe6a6a_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_missing_return_54ae7c80.lean index f3ca2db1f1..8fdce88ad3 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_missing_return_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_missing_return_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_six_6a2cf3 import CppVerify.User theorem cppverify_six_6a2cf3_missing_return_54ae7c80_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_postcondition_198bc076.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_postcondition_198bc076.lean index 3dae61ac78..0d1c2b271c 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_postcondition_198bc076.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_postcondition_198bc076.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_six_6a2cf3 import CppVerify.User theorem cppverify_six_6a2cf3_postcondition_198bc076_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean index 9f5bed9a7f..05952c73c6 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_tri_decreases_f55d4c import CppVerify.User theorem cppverify_tri_decreases_f55d4c_termination_3c6bb93f_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_modules.cpp b/clang/test/Verify/suite/Inputs/lean_modules.cpp new file mode 100644 index 0000000000..953d77f17a --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_modules.cpp @@ -0,0 +1,36 @@ +// Five functions for lean_modules.test: inc and dbl, and two that apply the +// recursive spec tri, whose postconditions Inputs/lean_modules_*.lean also +// prove by hand. + +cppverify::spec int tri(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : tri(n - 1) + n; +} + +int inc(int x) + cppverify::pre(0 <= x && x < 1000) + cppverify::post(cppverify::result == x + 1) +{ + return x + 1; +} + +int dbl(int x) + cppverify::pre(0 <= x && x < 1000) + cppverify::post(cppverify::result == 2 * x) +{ + return x + x; +} + +int tri_zero() + cppverify::post(cppverify::result == tri(0)) +{ + return 0; +} + +int plus_tri_zero(int x) + cppverify::pre(0 <= x && x < 1000) + cppverify::post(cppverify::result == x + tri(0)) +{ + return x; +} diff --git a/clang/test/Verify/suite/Inputs/lean_modules_plus_tri_zero.lean b/clang/test/Verify/suite/Inputs/lean_modules_plus_tri_zero.lean new file mode 100644 index 0000000000..2af3414bc0 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_modules_plus_tri_zero.lean @@ -0,0 +1,11 @@ +import CppVerify.Goals.cppverify_plus_tri_zero_10bb8a +import CppVerify.User +import CppVerify.Auto + +theorem cppverify_plus_tri_zero_10bb8a_postcondition_8b45419c_proof : + cppverify_plus_tri_zero_10bb8a_postcondition_8b45419c := by + apply cppverify_plus_tri_zero_10bb8a_postcondition_8b45419c.of_readable + intro __heap_alloc_0 __heap_live_0 __result_1 x_0 tri_0 _ _ h_pre_1 h_null_1 h_null_2 h_result_1 + rw [tri_0] at * + simp only [cppSpecBody_10bb8a86_fn_5f5a3374726969_1] at * + cppverify_auto diff --git a/clang/test/Verify/suite/Inputs/lean_modules_tri_zero.lean b/clang/test/Verify/suite/Inputs/lean_modules_tri_zero.lean new file mode 100644 index 0000000000..03445c1a79 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_modules_tri_zero.lean @@ -0,0 +1,11 @@ +import CppVerify.Goals.cppverify_tri_zero_e086e9 +import CppVerify.User +import CppVerify.Auto + +theorem cppverify_tri_zero_e086e9_postcondition_44e49d34_proof : + cppverify_tri_zero_e086e9_postcondition_44e49d34 := by + apply cppverify_tri_zero_e086e9_postcondition_44e49d34.of_readable + intro __heap_alloc_0 __heap_live_0 __result_1 tri_0 _ _ h_null_1 h_null_2 h_result_1 + rw [tri_0] at * + simp only [cppSpecBody_e086e9ab_fn_5f5a3374726969_1] at * + cppverify_auto diff --git a/clang/test/Verify/suite/Inputs/lean_project_text.py b/clang/test/Verify/suite/Inputs/lean_project_text.py new file mode 100644 index 0000000000..a090df2bd5 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_project_text.py @@ -0,0 +1,11 @@ +"""Prints the generated text of a Lean project: its prelude, its specs, and +each goal module in the order its Generated module imports them, the +functions' source order.""" +import pathlib, sys + +root = pathlib.Path(sys.argv[1]) / "CppVerify" +parts = [root / "Prelude.lean", root / "Specs.lean"] +for line in (root / "Generated.lean").read_text().splitlines(): + if line.startswith("import CppVerify.Goals."): + parts.append(root / "Goals" / (line[len("import CppVerify.Goals."):] + ".lean")) +sys.stdout.write("".join(part.read_text() for part in parts)) diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean index d450f13548..18f468999d 100644 --- a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_twice_edf933 import CppVerify.User theorem cppverify_twice_edf933_missing_return_54ae7c80_proof : cppverify_twice_edf933_missing_return_54ae7c80 := by diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean index e1080ebc94..11440c7bf0 100644 --- a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_twice_edf933 import CppVerify.User theorem cppverify_twice_edf933_postcondition_28de726e_proof : cppverify_twice_edf933_postcondition_28de726e := by diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean index 5c6b0e43e4..30d1e5cc82 100644 --- a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_twice_edf933 import CppVerify.User theorem cppverify_twice_edf933_precondition_51b3c1f0_proof : cppverify_twice_edf933_precondition_51b3c1f0 := by diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean index 2607fff7eb..9b2059d45a 100644 --- a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_twice_edf933 import CppVerify.User theorem cppverify_twice_edf933_precondition_f0a3d715_proof : cppverify_twice_edf933_precondition_f0a3d715 := by diff --git a/clang/test/Verify/suite/Inputs/lean_semantics_call.lean b/clang/test/Verify/suite/Inputs/lean_semantics_call.lean index 8dc0f46fa3..5df905de2c 100644 --- a/clang/test/Verify/suite/Inputs/lean_semantics_call.lean +++ b/clang/test/Verify/suite/Inputs/lean_semantics_call.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_small_74ff94 import CppVerify.User theorem cppverify_small_74ff94_precondition_4e324fa2_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_semantics_mix.lean b/clang/test/Verify/suite/Inputs/lean_semantics_mix.lean index 4c46c601c2..623902f5cf 100644 --- a/clang/test/Verify/suite/Inputs/lean_semantics_mix.lean +++ b/clang/test/Verify/suite/Inputs/lean_semantics_mix.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_mix_b839ab import CppVerify.User theorem cppverify_mix_b839ab_assertion_255467f3_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_semantics_numerals.lean b/clang/test/Verify/suite/Inputs/lean_semantics_numerals.lean index 5142c33706..96e97fd298 100644 --- a/clang/test/Verify/suite/Inputs/lean_semantics_numerals.lean +++ b/clang/test/Verify/suite/Inputs/lean_semantics_numerals.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_difference_465d5b import CppVerify.User theorem cppverify_difference_465d5b_assertion_d7e0e821_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_spec_definitions.cpp b/clang/test/Verify/suite/Inputs/lean_spec_definitions.cpp new file mode 100644 index 0000000000..bf9fbec303 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_spec_definitions.cpp @@ -0,0 +1,110 @@ +// Spec functions as Lean definitions, for lean_spec_definitions.test. + +cppverify::spec int tri(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : tri(n - 1) + n; +} + +cppverify::spec bool odd(int n); + +cppverify::spec bool even(int n) + cppverify::decreases(n, 1) +{ + return n <= 0 || odd(n - 1); +} + +cppverify::spec bool odd(int n) + cppverify::decreases(n, 0) +{ + return n > 0 && even(n - 1); +} + +cppverify::spec int ack(int m, int n) + cppverify::decreases(m, n) +{ + return m <= 0 ? n + 1 : (n <= 0 ? ack(m - 1, 1) : ack(m - 1, ack(m, n - 1))); +} + +cppverify::spec int half(int n) + cppverify::decreases(n) + cppverify::post(cppverify::result >= 0 && (n <= 1 || cppverify::result < n)) +{ + return n <= 1 ? 0 : half(n - 2) + 1; +} + +// Its measure falls by C++ division. +cppverify::spec int log2(int n) + cppverify::decreases(n) +{ + return n <= 1 ? 0 : log2(n / 2) + 1; +} + +// Its termination rests on the postcondition of half, which Lean does not +// know: it stays opaque. +cppverify::spec int steps(int n) + cppverify::decreases(n) +{ + return n <= 1 ? 0 : steps(half(n)) + 1; +} + +cppverify::proof void tri_nonneg(int n) + cppverify::post(tri(n) >= 0) +{ +} + +cppverify::proof void tri_four() + cppverify::post(tri(4) == 10) +{ +} + +cppverify::proof void even_four() + cppverify::post(even(4) && !odd(4)) +{ +} + +cppverify::proof void small_ack() + cppverify::post(ack(1, 1) == 3) +{ +} + +cppverify::proof void log2_eight() + cppverify::post(log2(8) == 3) +{ +} + +cppverify::proof void steps_one() + cppverify::post(steps(1) == 0) +{ +} + +// Its call may have the measure -1 where the caller's is 0. +cppverify::spec int down(int n) + cppverify::decreases(n) +{ + return n < 0 ? 0 : down(n - 1) + 1; +} + +// It calls steps, which stays opaque: Lean accepts it once steps is. +cppverify::spec int count_steps(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : count_steps(n - 1) + steps(n); +} + +cppverify::proof void down_zero() + cppverify::post(down(0) == 1 && count_steps(0) == 0) +{ +} + +// A call under an existential sees its range. +cppverify::spec bool reaches(int n) + cppverify::decreases(n) +{ + return n <= 0 || cppverify::exists(k, 0, n, reaches(k)); +} + +cppverify::proof void reaches_zero() + cppverify::post(reaches(0)) +{ +} diff --git a/clang/test/Verify/suite/Inputs/lean_spec_definitions_tri_nonneg.lean b/clang/test/Verify/suite/Inputs/lean_spec_definitions_tri_nonneg.lean new file mode 100644 index 0000000000..3e20c0085f --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_spec_definitions_tri_nonneg.lean @@ -0,0 +1,15 @@ +import CppVerify.Goals.cppverify_tri_nonneg_42a030 +import CppVerify.User +import CppVerify.Auto + +/-- tri is never negative, by induction over its own recursion. -/ +theorem tri_nonneg (m : Int) : 0 ≤ cppSpec_fn_5f5a3374726969 m := by + induction m using cppSpec_fn_5f5a3374726969.induct with + | case1 x h => rw [cppSpec_fn_5f5a3374726969]; simp [h] + | case2 x h ih => rw [cppSpec_fn_5f5a3374726969]; simp [h]; omega + +theorem cppverify_tri_nonneg_42a030_postcondition_053b1980_proof : + cppverify_tri_nonneg_42a030_postcondition_053b1980 := by + apply cppverify_tri_nonneg_42a030_postcondition_053b1980.of_readable + intro _ _ n _ _ _ + exact tri_nonneg _ diff --git a/clang/test/Verify/suite/Inputs/peak_memory.py b/clang/test/Verify/suite/Inputs/peak_memory.py new file mode 100644 index 0000000000..9584b83d06 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/peak_memory.py @@ -0,0 +1,19 @@ +#!/usr/bin/env python3 +"""Runs a command, then prints whether the largest process it ran stayed +below a resident memory bound, in MB, and exits with the command's status. + +usage: peak_memory.py MB COMMAND... + +Linux reports ru_maxrss in kilobytes, for every descendant waited for.""" +import resource +import subprocess +import sys + +limit = int(sys.argv[1]) +done = subprocess.run(sys.argv[2:]) +peak = resource.getrusage(resource.RUSAGE_CHILDREN).ru_maxrss // 1024 +if peak < limit: + print("peak memory below {} MB".format(limit)) +else: + print("peak memory {} MB, not below {} MB".format(peak, limit)) +sys.exit(done.returncode) diff --git a/clang/test/Verify/suite/Inputs/run_backend_fidelity.py b/clang/test/Verify/suite/Inputs/run_backend_fidelity.py index 18d97cddca..d8734e15cc 100644 --- a/clang/test/Verify/suite/Inputs/run_backend_fidelity.py +++ b/clang/test/Verify/suite/Inputs/run_backend_fidelity.py @@ -476,8 +476,14 @@ def check_lean_identity(cpp_verify, source, canonical, work): ], {0}, ) - generated = project / "CppVerify" / "Generated.lean" - text = generated.read_text() + # The project's generated text: its prelude, specs, and each goal module. + root = project / "CppVerify" + modules = [root / "Prelude.lean", root / "Specs.lean"] + [ + root / "Goals" / (line[len("import CppVerify.Goals."):] + ".lean") + for line in (root / "Generated.lean").read_text().splitlines() + if line.startswith("import CppVerify.Goals.") + ] + text = "".join(module.read_text() for module in modules) if "sorry" in text: fail("generated Lean semantics contains an admitted proof") diff --git a/clang/test/Verify/suite/lean_automation.test b/clang/test/Verify/suite/lean_automation.test index 0862d09576..cb906ffbd1 100644 --- a/clang/test/Verify/suite/lean_automation.test +++ b/clang/test/Verify/suite/lean_automation.test @@ -28,8 +28,8 @@ # # A stub that no revision of cppverify_auto tried, as before automation, and # one an earlier revision tried, are tried. -# RUN: sed -i -e '/^ automation:/d' -e '/^import CppVerify.Auto$/d' -e 's/^ cppverify_auto_grind$/ sorry/' %t/p/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_missing_return_54ae7c80.lean -# RUN: sed -i 's/cppverify_auto 1 did not prove it/cppverify_auto 0 did not prove it/' %t/p/CppVerify/Proofs/cppverify_square_934e38/cppverify_square_934e38_overflow_f86973f7.lean +# RUN: sed -i -e '/^ automation:/d' -e '/^import CppVerify.Goals\./d' -e '/^import CppVerify.Auto$/d' -e 's/^ cppverify_auto_grind$/ sorry/' %t/p/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_missing_return_54ae7c80.lean +# RUN: sed -i 's/cppverify_auto 3 did not prove it/cppverify_auto 2 did not prove it/' %t/p/CppVerify/Proofs/cppverify_square_934e38/cppverify_square_934e38_overflow_f86973f7.lean # RUN: %cpp-verify --backend=lean --lean-project=%t/p %S/Inputs/lean_automation.cpp -- 2>&1 | FileCheck %s --check-prefix=EDITED # RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_missing_return_54ae7c80.lean --check-prefix=TRIED # RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_square_934e38/cppverify_square_934e38_overflow_f86973f7.lean --check-prefix=STUB @@ -54,9 +54,10 @@ # EXPORT-NEXT: Exported: lean obligation: next (cppverify_auto proved 3 of 3 goals) # EXPORT-NEXT: Exported: lean obligation: square (cppverify_auto proved 1 of 3 goals) -# PROVED: automation: cppverify_auto 1 proves it with cppverify_auto_grind +# PROVED: automation: cppverify_auto 3 proves it with cppverify_auto_grind # PROVED-NEXT: cppverify_auto proves this goal. cpp-verify rewrites this file only while it # PROVED-NEXT: is unedited; a proof you write here is yours, kept as any other. -/ +# PROVED-NEXT: import CppVerify.Goals.cppverify_next_e1e917 # PROVED-NEXT: import CppVerify.User # PROVED-NEXT: import CppVerify.Auto # PROVED-EMPTY: @@ -66,11 +67,11 @@ # PROVED-NEXT: cppverify_auto_grind # PROVED-EMPTY: -# STUB: automation: cppverify_auto 1 did not prove it{{$}} +# STUB: automation: cppverify_auto 3 did not prove it{{$}} # STUB-NEXT: Complete this proof. # STUB: {{^}} sorry{{$}} -# SLOW: automation: cppverify_auto 1 did not prove it within 3 s +# SLOW: automation: cppverify_auto 3 did not prove it within 3 s # SLOW: {{^}} sorry{{$}} # JSON: "function":"next","lean_automatic":3,{{.*}}"status":"exported" @@ -81,10 +82,10 @@ # EDITED: Exported: lean obligation: next (cppverify_auto proved 2 of 3 goals) -# TRIED: automation: cppverify_auto 1 proves it with cppverify_auto_grind +# TRIED: automation: cppverify_auto 3 proves it with cppverify_auto_grind # TRIED: {{^}} cppverify_auto_grind{{$}} -# HONEST: automation: cppverify_auto 1 proves it with cppverify_auto_heap +# HONEST: automation: cppverify_auto 3 proves it with cppverify_auto_heap # HONEST: {{^}} cppverify_auto_heap{{$}} # PLAIN: Exported: lean obligation: a_slow{{$}} diff --git a/clang/test/Verify/suite/lean_certifier.test b/clang/test/Verify/suite/lean_certifier.test index b738cacb2d..7edbabeb7f 100644 --- a/clang/test/Verify/suite/lean_certifier.test +++ b/clang/test/Verify/suite/lean_certifier.test @@ -38,6 +38,14 @@ # RUN: cp %S/Inputs/lean_certifier_proofs/shadowed/cppverify_one_* %t/shadowed/CppVerify/Proofs/cppverify_one_99bcee/ # RUN: not %cpp-verify --backend=lean --lean-project=%t/shadowed --lean-certify %S/Inputs/lean_certifier.cpp -- 2>&1 | FileCheck %s --check-prefix=SHADOWED # +# The same in the proof of the goal that comes first, which imports nothing +# of the project: the generated module is replayed first all the same, so the +# proof file is the module left out, and the next function is certified. +# RUN: %cpp-verify --backend=lean --no-lean-auto --lean-project=%t/first %S/Inputs/lean_certifier_first.cpp -- > /dev/null +# RUN: cp %S/Inputs/lean_certifier_proofs/cppverify_fine_* %t/first/CppVerify/Proofs/cppverify_fine_52006a/ +# RUN: cp %S/Inputs/lean_certifier_proofs/first/* %t/first/CppVerify/Proofs/cppverify_early_103f65/ +# RUN: not %cpp-verify --backend=lean --no-lean-auto --lean-project=%t/first --lean-certify %S/Inputs/lean_certifier_first.cpp -- 2>&1 | FileCheck %s --check-prefix=FIRST +# # An axiom behind a lemma. # RUN: cp -r %t/base %t/hidden # RUN: cp %S/Inputs/lean_certifier_proofs/hidden/cppverify_one_* %t/hidden/CppVerify/Proofs/cppverify_one_99bcee/ @@ -59,7 +67,10 @@ # IMPORTED-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: the kernel rejects CppVerify.Lemmas: while replaying declaration 'cheat': (kernel) declaration type mismatch, 'cheat' has type True but it is expected to have type cppverify_one_99bcee_postcondition_646d2761) # SHADOWED: Certified: fine [backend=Lean] -# SHADOWED-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: cppverify_one_99bcee_postcondition_646d2761 is not the goal CppVerify.Generated defines) +# SHADOWED-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: CppVerify.Proofs.cppverify_one_99bcee.cppverify_one_99bcee_postcondition_646d2761 declares cppverify_one_99bcee_postcondition_646d2761, which CppVerify.Goals.cppverify_one_99bcee declares) + +# FIRST: Unresolved: lean obligation: early (Lean certification failed: {{.*}}; the proof of fn_5f5a356561726c7976::postcondition@2:37: CppVerify.Proofs.cppverify_early_103f65.cppverify_early_103f65_postcondition_646d2761 declares cppverify_early_103f65_postcondition_646d2761, which CppVerify.Goals.cppverify_early_103f65 declares) +# FIRST-NEXT: Certified: fine [backend=Lean] # HIDDEN: Certified: fine [backend=Lean] # HIDDEN-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: cppverify_one_99bcee_postcondition_646d2761_proof depends on the axiom escape, which is not one of Lean's foundations) diff --git a/clang/test/Verify/suite/lean_certifier_memory.test b/clang/test/Verify/suite/lean_certifier_memory.test new file mode 100644 index 0000000000..c892c86670 --- /dev/null +++ b/clang/test/Verify/suite/lean_certifier_memory.test @@ -0,0 +1,20 @@ +# REQUIRES: lean, system-linux +# +# The checker imports the toolchain's modules once and replays the project's +# into one kernel environment, so its memory does not grow with the goals or +# with the imports of their proofs. A proof that imports Lean through a module +# the kernel rejects made it import Lean's environment again for every goal +# and every module it replayed, never freeing one: 13 GB here, now under 4. +# +# RUN: rm -rf %t && mkdir -p %t +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %S/Inputs/lean_certifier.cpp -- > /dev/null +# RUN: cp %S/Inputs/lean_certifier_proofs/cppverify_fine_* %t/p/CppVerify/Proofs/cppverify_fine_52006a/ +# RUN: cp %S/Inputs/lean_certifier_proofs/cppverify_one_* %t/p/CppVerify/Proofs/cppverify_one_99bcee/ +# RUN: cp %S/Inputs/lean_certifier_proofs/imported/Lemmas.lean %t/p/CppVerify/ +# RUN: cp %S/Inputs/lean_certifier_proofs/imported/cppverify_one_* %t/p/CppVerify/Proofs/cppverify_one_99bcee/ +# RUN: cd %t/p && lake build CppVerify.Lemmas +# RUN: not %python %S/Inputs/peak_memory.py 6144 %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %S/Inputs/lean_certifier.cpp -- 2>&1 | FileCheck %s + +# CHECK: Certified: fine [backend=Lean] +# CHECK-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: the kernel rejects CppVerify.Lemmas: while replaying declaration 'cheat' +# CHECK-NEXT: peak memory below 6144 MB diff --git a/clang/test/Verify/suite/lean_certify.cpp b/clang/test/Verify/suite/lean_certify.cpp index 2cd5205c70..831f3d40c4 100644 --- a/clang/test/Verify/suite/lean_certify.cpp +++ b/clang/test/Verify/suite/lean_certify.cpp @@ -28,7 +28,6 @@ void trivial() // ADMITTED-SAME: declaration uses `sorry` // CERTIFIED: Certified: trivial [backend=Lean] // USER-ADMITTED: Unresolved: lean obligation: trivial (Lean certification failed: -// USER-ADMITTED-SAME: User.lean -// USER-ADMITTED-SAME: declaration uses `sorry` +// USER-ADMITTED-SAME: unfinished of CppVerify.User uses sorry // AXIOM: Unresolved: lean obligation: trivial (Lean certification failed: the proof of {{.*}}::missing-return@synthetic: cppverify_trivial_3e4f5a_missing_return_ba8abb90_proof depends on the axiom escape, which is not one of Lean's foundations; the proof of {{.*}}::postcondition@{{[0-9]+}}:{{[0-9]+}}: cppverify_trivial_3e4f5a_postcondition_ba8abb90_proof depends on the axiom escape, which is not one of Lean's foundations) // STALE: Unresolved: lean obligation: trivial (Lean certification failed: diff --git a/clang/test/Verify/suite/lean_collections.test b/clang/test/Verify/suite/lean_collections.test new file mode 100644 index 0000000000..2a2daf888c --- /dev/null +++ b/clang/test/Verify/suite/lean_collections.test @@ -0,0 +1,76 @@ +# REQUIRES: lean +# +# The spec collections in Lean: a sequence is a List Int, a set its +# membership test, a multiset its counts, and a map the value at each key it +# holds, with each operation of defined in the prelude, total +# as it is there, and lemmas for each. +# +# RUN: rm -rf %t && mkdir -p %t +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %S/Inputs/lean_collections.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Specs.lean --check-prefix=SPECS +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Prelude.lean --check-prefix=PRELUDE +# RUN: cat %t/p/CppVerify/Goals/cppverify_sets_d46b53.lean %t/p/CppVerify/Goals/cppverify_multisets_68c3c1.lean %t/p/CppVerify/Goals/cppverify_maps_289bf4.lean %t/p/CppVerify/Goals/cppverify_sequences_b14fed.lean | FileCheck %s --check-prefix=GOALS +# +# Each step that revision 2 of cppverify_auto adds proves a goal here first: +# machine equalities as integers (x != y), a collection equality element by +# element, and a definition instance by the body it names. +# RUN: grep -h 'automation:' %t/p/CppVerify/Proofs/cppverify_sets_d46b53/cppverify_sets_d46b53_assertion_a932edd2.lean %t/p/CppVerify/Proofs/cppverify_multisets_68c3c1/cppverify_multisets_68c3c1_assertion_962b234c.lean %t/p/CppVerify/Proofs/cppverify_total_push_cdfd2d/cppverify_total_push_cdfd2d_postcondition_3a9fac6f.lean | FileCheck %s --check-prefix=STEPS +# +# cppverify_auto proves the goals over each kind, those that unfold a spec +# too. A proof by hand may use the lemmas, as this one of total_push does in +# place of the automatic one; the false claim stays unproved. +# RUN: cp %S/Inputs/lean_collections_total_push.lean %t/p/CppVerify/Proofs/cppverify_total_push_cdfd2d/cppverify_total_push_cdfd2d_postcondition_3a9fac6f.lean +# RUN: not %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %S/Inputs/lean_collections.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFY +# +# The scratch-pad states the same goals. +# RUN: %cpp-verify --backend=lean --lean-out=%t/scratch.lean %S/Inputs/lean_collections.cpp -- 2>&1 | FileCheck %s --check-prefix=SCRATCH +# RUN: FileCheck %s --input-file=%t/scratch.lean --check-prefix=SCRATCH-TEXT + +# EXPORT: Exported: decreases: total (cppverify_auto proved 1 of 1 goals) +# EXPORT-NEXT: Exported: lean obligation: sequences (cppverify_auto proved 5 of 5 goals) +# EXPORT-NEXT: Exported: lean obligation: sets (cppverify_auto proved 3 of 3 goals) +# EXPORT-NEXT: Exported: lean obligation: multisets (cppverify_auto proved 3 of 3 goals) +# EXPORT-NEXT: Exported: lean obligation: maps (cppverify_auto proved 3 of 3 goals) +# EXPORT-NEXT: Exported: lean obligation: total_push (cppverify_auto proved 2 of 2 goals) +# EXPORT-NEXT: Exported: lean obligation: wrong (cppverify_auto proved 1 of 2 goals) +# EXPORT-NEXT: Exported: decreases: members (cppverify_auto proved 1 of 1 goals) +# EXPORT-NEXT: Exported: lean obligation: no_members (cppverify_auto proved 2 of 2 goals) + +# STEPS: automation: cppverify_auto 3 proves it with cppverify_auto_bveq +# STEPS-NEXT: automation: cppverify_auto 3 proves it with cppverify_auto_ext +# STEPS-NEXT: automation: cppverify_auto 3 proves it with cppverify_auto_unfold + +# SPECS: /- spec function: total -/ +# SPECS-NEXT: {{^}}def cppSpec_fn_5f5a35746f74616c4e396370707665726966793373657145 (s : List Int) : Int :={{$}} +# SPECS: /- spec function: members -/ +# SPECS-NEXT: {{^}}def cppSpec_fn_5f5a376d656d626572734e39637070766572696679337365744569 (a : (Int → Bool)) (n : Int) : Int :={{$}} + +# PRELUDE: {{^}}def cppSeqAt (s : List Int) (i : Int) : Int :={{$}} +# PRELUDE-NEXT: {{^}} if i < 0 then 0 else s[i.toNat]?.getD 0{{$}} +# PRELUDE: {{^}}def cppSetContains (s : Int → Bool) (x : Int) : Prop := s x = true{{$}} +# PRELUDE: {{^}}def cppMultisetRemove (m : Int → Nat) (x : Int) : Int → Nat :={{$}} +# PRELUDE: {{^}}def cppMapGet (m : Int → Option Int) (k : Int) : Int := (m k).getD 0{{$}} +# PRELUDE: {{^}}theorem cppSeq_ext (s t : List Int) + +# GOALS: (a_0 : (Int → Bool)) +# GOALS: (cppSetSubset a_0 (cppSetUnion a_0 (cppSetInsert cppSetEmpty ((BitVec.signExtend 64 y_0)).toInt))) +# GOALS: (m_0 : (Int → Nat)) +# GOALS: (cppMultisetRemove (cppMultisetInsert m_0 ((BitVec.signExtend 64 x_0)).toInt) ((BitVec.signExtend 64 x_0)).toInt) = m_0 +# GOALS: (m_0 : (Int → Option Int)) +# GOALS: (cppMapGet (cppMapInsert m_0 +# GOALS: (s_0 : List Int) +# GOALS: (cppSeqContains (cppSeqConcat s_0 (cppSeqUnit ((BitVec.signExtend 64 x_0)).toInt)) ((BitVec.signExtend 64 x_0)).toInt) + +# CERTIFY: Certified: decreases: total [backend=Lean] +# CERTIFY-NEXT: Certified: sequences [backend=Lean] +# CERTIFY-NEXT: Certified: sets [backend=Lean] +# CERTIFY-NEXT: Certified: multisets [backend=Lean] +# CERTIFY-NEXT: Certified: maps [backend=Lean] +# CERTIFY-NEXT: Certified: total_push [backend=Lean] +# CERTIFY-NEXT: Unresolved: lean obligation: wrong (Lean certification failed: the proof of {{.*}}::assertion@48:3: {{.*}}declaration uses `sorry` +# CERTIFY-NEXT: Certified: decreases: members [backend=Lean] +# CERTIFY-NEXT: Certified: no_members [backend=Lean] + +# SCRATCH: Exported: lean obligation: sets +# SCRATCH-TEXT: {{^}}def cppSetInsert (s : Int → Bool) (x : Int) : Int → Bool :={{$}} +# SCRATCH-TEXT: (cppSetContains (cppSetRemove (cppSetInsert a_0 diff --git a/clang/test/Verify/suite/lean_division.test b/clang/test/Verify/suite/lean_division.test new file mode 100644 index 0000000000..cccf396085 --- /dev/null +++ b/clang/test/Verify/suite/lean_division.test @@ -0,0 +1,20 @@ +# REQUIRES: lean +# +# cppverify_auto reads C++ division and remainder by their definitions in +# its last step, so a contract that divides by a constant is proved in a +# project whose specs Lean does not define. +# +# RUN: rm -rf %t && mkdir -p %t +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %S/Inputs/lean_division.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_half_bound_186b9f/cppverify_half_bound_186b9f_postcondition_40c34bea.lean --check-prefix=DIV +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_negative_division_a7749a/cppverify_negative_division_a7749a_postcondition_212234d0.lean --check-prefix=DIV +# RUN: %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %S/Inputs/lean_division.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFY + +# EXPORT: Exported: lean obligation: half_bound (cppverify_auto proved 3 of 3 goals) +# EXPORT-NEXT: Exported: lean obligation: negative_division (cppverify_auto proved 3 of 3 goals) + +# DIV: automation: cppverify_auto 3 proves it with cppverify_auto_div +# DIV: {{^}} cppverify_auto_div{{$}} + +# CERTIFY: Certified: half_bound [backend=Lean] +# CERTIFY-NEXT: Certified: negative_division [backend=Lean] diff --git a/clang/test/Verify/suite/lean_fallback.test b/clang/test/Verify/suite/lean_fallback.test index 1aed3ce551..1939ff8428 100644 --- a/clang/test/Verify/suite/lean_fallback.test +++ b/clang/test/Verify/suite/lean_fallback.test @@ -1,20 +1,22 @@ // REQUIRES: lean // +// The fallback runs without cppverify_auto, so that the goals wait for the +// proofs this test writes. // RUN: rm -rf %t.project -// RUN: not %cpp-verify --solver-rlimit=400 --lean-fallback-scope=all --lean-fallback=%t.project %S/spec_fuel_recursive_pass.cpp -- 2>&1 | FileCheck %s +// RUN: not %cpp-verify --solver-rlimit=400 --no-lean-auto --lean-fallback-scope=all --lean-fallback=%t.project %S/spec_fuel_recursive_pass.cpp -- 2>&1 | FileCheck %s // RUN: test -f %t.project/CppVerify/Generated.lean // RUN: test -f %t.project/CppVerify/Check.lean // RUN: grep -q '^import CppVerify.Proofs.cppverify_' %t.project/CppVerify/Check.lean -// RUN: FileCheck %s --input-file=%t.project/CppVerify/Generated.lean --check-prefix=GENERATED -// RUN: not %cpp-verify --solver-rlimit=400 --lean-fallback-scope=all --lean-fallback=%t.project --lean-certify %S/spec_fuel_recursive_pass.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFY +// RUN: %python %S/Inputs/lean_project_text.py %t.project | FileCheck %s --check-prefix=GENERATED +// RUN: not %cpp-verify --solver-rlimit=400 --no-lean-auto --lean-fallback-scope=all --lean-fallback=%t.project --lean-certify %S/spec_fuel_recursive_pass.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFY // RUN: cp %S/Inputs/lean_fallback_goal_1.lean %t.project/CppVerify/Proofs/cppverify_fibo_step_624f01/cppverify_fibo_step_624f01_missing_return_ba8abb90.lean // RUN: cp %S/Inputs/lean_fallback_goal_2.lean %t.project/CppVerify/Proofs/cppverify_fibo_step_624f01/cppverify_fibo_step_624f01_postcondition_559cb60a.lean // RUN: cp %S/Inputs/lean_fallback_goal_3.lean %t.project/CppVerify/Proofs/cppverify_fibo_six_ec829a/cppverify_fibo_six_ec829a_missing_return_ba8abb90.lean // RUN: cp %S/Inputs/lean_fallback_goal_4.lean %t.project/CppVerify/Proofs/cppverify_fibo_six_ec829a/cppverify_fibo_six_ec829a_postcondition_30cd1b97.lean -// RUN: %cpp-verify --solver-rlimit=400 --lean-fallback-scope=all --lean-fallback=%t.project --lean-certify %S/spec_fuel_recursive_pass.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFIED -// RUN: %cpp-verify --solver-rlimit=400 --lean-fallback-scope=all --lean-fallback=%t.project --lean-certify --diagnostics-format=json %S/spec_fuel_recursive_pass.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFIED-JSON +// RUN: %cpp-verify --solver-rlimit=400 --no-lean-auto --lean-fallback-scope=all --lean-fallback=%t.project --lean-certify %S/spec_fuel_recursive_pass.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFIED +// RUN: %cpp-verify --solver-rlimit=400 --no-lean-auto --lean-fallback-scope=all --lean-fallback=%t.project --lean-certify --diagnostics-format=json %S/spec_fuel_recursive_pass.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFIED-JSON // RUN: rm -rf %t.json-project -// RUN: not %cpp-verify --solver-rlimit=400 --lean-fallback-scope=all --lean-fallback=%t.json-project --lean-certify --diagnostics-format=json %S/spec_fuel_recursive_pass.cpp -- 2>&1 | FileCheck %s --check-prefix=FAILED-JSON +// RUN: not %cpp-verify --solver-rlimit=400 --no-lean-auto --lean-fallback-scope=all --lean-fallback=%t.json-project --lean-certify --diagnostics-format=json %S/spec_fuel_recursive_pass.cpp -- 2>&1 | FileCheck %s --check-prefix=FAILED-JSON // A small deterministic resource limit leaves both functions to Lean, and the // complete export exports every obligation, including the one Z3 proved. @@ -37,6 +39,6 @@ // FAILED-JSON-SAME: "reason":"lean.export-failed" // FAILED-JSON-SAME: "status":"unresolved" -// GENERATED: Generated by CppVerify for an editable Lean project. +// GENERATED: Generated by CppVerify. Regeneration replaces this file, never a proof. // GENERATED: function: fibo_step // GENERATED: function: fibo_six diff --git a/clang/test/Verify/suite/lean_identity.test b/clang/test/Verify/suite/lean_identity.test index d66b654f83..47ca665edc 100644 --- a/clang/test/Verify/suite/lean_identity.test +++ b/clang/test/Verify/suite/lean_identity.test @@ -26,7 +26,7 @@ # statement: every proof stays, and so do the spec bodies the proofs unfold. # RUN: %cpp-verify --backend=lean --lean-project=%t/p %t/-src/inserted.cpp -- 2>&1 | FileCheck %s --check-prefix=INSERTED --implicit-check-not=warning # RUN: grep -q 'cppSpecBody_6a2cf351_fn_5f5a3374726969_4,' %t/p/CppVerify/Proofs/cppverify_six_6a2cf3/cppverify_six_6a2cf3_postcondition_198bc076.lean -# RUN: grep -q '^def cppSpecBody_6a2cf351_fn_5f5a3374726969_4$' %t/p/CppVerify/Generated.lean +# RUN: grep -q '^def cppSpecBody_6a2cf351_fn_5f5a3374726969_4$' %t/p/CppVerify/Goals/cppverify_six_6a2cf3.lean # RUN: test -f %t/p/CppVerify/Proofs/cppverify_zero_5ece85/cppverify_zero_5ece85_postcondition_36923ed0.lean # # Renamed functions take their proofs along, each its own, with the names @@ -117,6 +117,7 @@ # HEADER-NEXT: bodies: cppSpecBody_6a2cf351_ # HEADER-NEXT: source: {{.*}}/ -src/base.cpp:8:37 # HEADER: -/ +# HEADER-NEXT: import CppVerify.Goals.cppverify_six_6a2cf3 # HEADER-NEXT: import CppVerify.User # HEADER-EMPTY: # HEADER-NEXT: theorem cppverify_six_6a2cf3_postcondition_198bc076_proof : diff --git a/clang/test/Verify/suite/lean_kernel.test b/clang/test/Verify/suite/lean_kernel.test index 15440d41e0..df0e028ac2 100644 --- a/clang/test/Verify/suite/lean_kernel.test +++ b/clang/test/Verify/suite/lean_kernel.test @@ -7,12 +7,13 @@ // RUN: lake --dir=%t.quant build CppVerify.Generated // RUN: %cpp-verify --backend=lean --lean-project=%t.recursive %S/spec_fuel_recursive_pass.cpp -- // RUN: lake --dir=%t.recursive build CppVerify.Generated -// RUN: %python -c "import os, sys; sys.exit(os.path.getsize(r'%t.recursive/CppVerify/Generated.lean') >= 100000)" +// RUN: %python %S/Inputs/lean_project_text.py %t.recursive > %t.recursive.lean +// RUN: %python -c "import os, sys; sys.exit(os.path.getsize(r'%t.recursive.lean') >= 100000)" // RUN: %cpp-verify --backend=lean --lean-project=%t.names %S/Inputs/lean_name_encoding.cpp -- -// RUN: grep -Eq 'cppEncoded_[0-9a-f]+' %t.names/CppVerify/Generated.lean +// RUN: %python %S/Inputs/lean_project_text.py %t.names | grep -Eq 'cppEncoded_[0-9a-f]+' // RUN: lake --dir=%t.names build CppVerify.Generated // RUN: lake --dir=%t.names build CppVerify.Check // Heap-reading specs take the heap state as a CppHeap argument. // RUN: %cpp-verify --check-ub --backend=lean --lean-project=%t.heapspec %S/heap_reading_spec.cpp -- -// RUN: grep -q '(__spec_heap : CppHeap)' %t.heapspec/CppVerify/Generated.lean +// RUN: %python %S/Inputs/lean_project_text.py %t.heapspec | grep -q '(__spec_heap : CppHeap)' // RUN: lake --dir=%t.heapspec build CppVerify.Generated diff --git a/clang/test/Verify/suite/lean_modules.test b/clang/test/Verify/suite/lean_modules.test new file mode 100644 index 0000000000..dc49ce3bbb --- /dev/null +++ b/clang/test/Verify/suite/lean_modules.test @@ -0,0 +1,123 @@ +# REQUIRES: lean +# +# A Lean project has a module of goals for each function, +# CppVerify/Goals/.lean, which imports CppVerify.Specs, where each spec +# the goals apply is declared once. A proof imports its function's goals, +# User, and Auto, so certification builds again only the proofs of a function +# whose goals changed. +# +# RUN: rm -rf %t && mkdir -p %t && cp %S/Inputs/lean_modules.cpp %t/m.cpp +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %t/m.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Generated.lean --check-prefix=GENERATED +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Specs.lean --check-prefix=SPECS '--implicit-check-not=spec function:' +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Goals/cppverify_tri_zero_e086e9.lean --check-prefix=GOALS +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Goals/cppverify_plus_tri_zero_10bb8a.lean --check-prefix=GOALS-PLUS +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_inc_c0810e/cppverify_inc_c0810e_postcondition_e4ef4574.lean --check-prefix=IMPORTS +# RUN: FileCheck %s --input-file=%t/p/CppVerify/User.lean --check-prefix=USER +# RUN: FileCheck %s --input-file=%t/p/CppVerify.lean --check-prefix=ROOT +# +# The two goal modules that apply tri are certified together, with proofs +# by hand of their postconditions in place of the automatic ones. +# RUN: cp %S/Inputs/lean_modules_tri_zero.lean %t/p/CppVerify/Proofs/cppverify_tri_zero_e086e9/cppverify_tri_zero_e086e9_postcondition_44e49d34.lean +# RUN: cp %S/Inputs/lean_modules_plus_tri_zero.lean %t/p/CppVerify/Proofs/cppverify_plus_tri_zero_10bb8a/cppverify_plus_tri_zero_10bb8a_postcondition_8b45419c.lean +# RUN: %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %t/m.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFY +# +# A run of the same source writes no file. The two proofs by hand are not +# cppverify_auto's. +# RUN: touch %t/same +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %t/m.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT-AGAIN +# RUN: find %t/p -newer %t/same -type f -not -path '*/.lake/*' | count 0 +# +# A change to dbl builds dbl's goal module and proofs again, and the module +# that imports every goal module; nothing else. +# RUN: touch %t/before +# RUN: sed 's/cppverify::result == 2 \* x/cppverify::result == x + x/' %S/Inputs/lean_modules.cpp > %t/m.cpp +# RUN: %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %t/m.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFY +# RUN: cd %t/p/.lake/build/lib/lean && find CppVerify -name '*.olean' -newer %t/before | env LC_ALL=C sort | FileCheck %s --check-prefix=REBUILT --implicit-check-not=olean +# +# `lake build` builds every proof. Run in the project, elan selects its +# toolchain. +# RUN: cd %t/p && lake build 2>&1 | FileCheck %s --check-prefix=LAKE +# +# A function that is gone takes its goal module with it. +# RUN: sed -e 's/cppverify::result == 2 \* x/cppverify::result == x + x/' -e '/^int inc(/,/^}/d' %S/Inputs/lean_modules.cpp > %t/m.cpp +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %t/m.cpp -- 2>&1 | FileCheck %s --check-prefix=WITHOUT-INC +# RUN: not test -e %t/p/CppVerify/Goals/cppverify_inc_c0810e.lean +# +# A project of an earlier release, whose User imports Generated, still +# certifies: each proof then depends on every goal module. +# RUN: printf 'import CppVerify.Generated\n' > %t/p/CppVerify/User.lean +# RUN: %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %t/m.cpp -- 2>&1 | FileCheck %s --check-prefix=OLD-USER +# +# A fallback run writes the goal modules of the functions it exports and no +# other, since Specs then declares only the specs those apply. Here the +# solver verifies every function: no goal module stays, and every proof does. +# RUN: %cpp-verify --lean-fallback=%t/p %t/m.cpp -- 2>&1 | FileCheck %s --check-prefix=FALLBACK +# RUN: not test -e %t/p/CppVerify/Goals/cppverify_tri_zero_e086e9.lean +# RUN: test -f %t/p/CppVerify/Proofs/cppverify_tri_zero_e086e9/cppverify_tri_zero_e086e9_postcondition_44e49d34.lean +# RUN: cd %t/p && lake build 2>&1 | FileCheck %s --check-prefix=LAKE + +# EXPORT: Exported: decreases: tri (cppverify_auto proved 1 of 1 goals) +# EXPORT-NEXT: Exported: lean obligation: inc (cppverify_auto proved 3 of 3 goals) +# EXPORT-NEXT: Exported: lean obligation: dbl (cppverify_auto proved 3 of 3 goals) +# EXPORT-NEXT: Exported: lean obligation: tri_zero (cppverify_auto proved 2 of 2 goals) +# EXPORT-NEXT: Exported: lean obligation: plus_tri_zero (cppverify_auto proved 2 of 2 goals) + +# EXPORT-AGAIN: Exported: lean obligation: tri_zero (cppverify_auto proved 1 of 2 goals) +# EXPORT-AGAIN-NEXT: Exported: lean obligation: plus_tri_zero (cppverify_auto proved 1 of 2 goals) + +# GENERATED: {{^}}import CppVerify.Prelude{{$}} +# GENERATED-NEXT: {{^}}import CppVerify.Specs{{$}} +# GENERATED-NEXT: {{^}}import CppVerify.Goals.cppverify_tri_decreases_f55d4c{{$}} +# GENERATED-NEXT: {{^}}import CppVerify.Goals.cppverify_inc_c0810e{{$}} +# GENERATED-NEXT: {{^}}import CppVerify.Goals.cppverify_dbl_47613e{{$}} +# GENERATED-NEXT: {{^}}import CppVerify.Goals.cppverify_tri_zero_e086e9{{$}} +# GENERATED-NEXT: {{^}}import CppVerify.Goals.cppverify_plus_tri_zero_10bb8a{{$}} +# GENERATED-EMPTY: + +# SPECS: {{^}}import CppVerify.Prelude{{$}} +# SPECS: /- spec function: tri -/ +# SPECS-NEXT: {{^}}def cppSpec_fn_5f5a3374726969 (n : Int) : Int :={{$}} + +# Each goal module defines the spec bodies it uses under its own prefix. +# GOALS: {{^}}import CppVerify.Specs{{$}} +# GOALS-NOT: {{^}}import +# GOALS: {{^}}attribute [local instance] cppVerifyPropDecidable{{$}} +# GOALS: {{^}}def cppSpecBody_e086e9ab_fn_5f5a3374726969_1 +# GOALS-PLUS: {{^}}import CppVerify.Specs{{$}} +# GOALS-PLUS: {{^}}def cppSpecBody_10bb8a86_fn_5f5a3374726969_1 + +# IMPORTS: {{^}}import CppVerify.Goals.cppverify_inc_c0810e{{$}} +# IMPORTS-NEXT: {{^}}import CppVerify.User{{$}} +# IMPORTS-NEXT: {{^}}import CppVerify.Auto{{$}} +# IMPORTS-NOT: import + +# USER: {{^}}import CppVerify.Specs{{$}} +# ROOT: {{^}}import CppVerify.Check{{$}} + +# CERTIFY: Certified: decreases: tri [backend=Lean] +# CERTIFY-NEXT: Certified: inc [backend=Lean] +# CERTIFY-NEXT: Certified: dbl [backend=Lean] +# CERTIFY-NEXT: Certified: tri_zero [backend=Lean] +# CERTIFY-NEXT: Certified: plus_tri_zero [backend=Lean] + +# REBUILT: CppVerify/Generated.olean +# REBUILT-NEXT: CppVerify/Goals/cppverify_dbl_47613e.olean +# REBUILT-NEXT: CppVerify/Proofs/cppverify_dbl_47613e/cppverify_dbl_47613e_missing_return_54ae7c80.olean +# REBUILT-NEXT: CppVerify/Proofs/cppverify_dbl_47613e/cppverify_dbl_47613e_overflow_fce34d13.olean +# REBUILT-NEXT: CppVerify/Proofs/cppverify_dbl_47613e/cppverify_dbl_47613e_postcondition_ce469baa.olean + +# LAKE: Build completed successfully + +# WITHOUT-INC: Exported: decreases: tri +# WITHOUT-INC-NEXT: Exported: lean obligation: dbl +# WITHOUT-INC-NEXT: Exported: lean obligation: tri_zero + +# OLD-USER: Certified: decreases: tri [backend=Lean] +# OLD-USER-NEXT: Certified: dbl [backend=Lean] +# OLD-USER-NEXT: Certified: tri_zero [backend=Lean] +# OLD-USER-NEXT: Certified: plus_tri_zero [backend=Lean] + +# FALLBACK: Verified: dbl [backend=z3] +# FALLBACK-NEXT: Verified: tri_zero [backend=z3] +# FALLBACK-NEXT: Verified: plus_tri_zero [backend=z3] diff --git a/clang/test/Verify/suite/lean_project.cpp b/clang/test/Verify/suite/lean_project.cpp index 51f4a7c9c6..5561998437 100644 --- a/clang/test/Verify/suite/lean_project.cpp +++ b/clang/test/Verify/suite/lean_project.cpp @@ -7,7 +7,7 @@ // RUN: test -f %t.project/CppVerify/Check.lean // RUN: test -f %t.project/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_missing_return_ba8abb90.lean // RUN: grep -Fxq 'leanprover/lean4:v4.35.0' %t.project/lean-toolchain -// RUN: FileCheck %s --input-file=%t.project/CppVerify/Generated.lean --check-prefix=GENERATED +// RUN: %python %S/Inputs/lean_project_text.py %t.project | FileCheck %s --check-prefix=GENERATED // RUN: grep -Fq 'import CppVerify.Proofs.cppverify_trivial_3e4f5a.cppverify_trivial_3e4f5a_missing_return_ba8abb90' %t.project/CppVerify/Check.lean // RUN: echo '/- USER_KEEP -/' >> %t.project/CppVerify/User.lean // RUN: echo '/- PROOF_KEEP -/' >> %t.project/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_missing_return_ba8abb90.lean @@ -30,7 +30,7 @@ void trivial() {} // EXPORT: Exported: lean obligation: trivial -// GENERATED: Generated by CppVerify for an editable Lean project. +// GENERATED: Generated by CppVerify. Regeneration replaces this file, never a proof. // GENERATED-NOT: unchecked Lean scratch-pad // GENERATED: function: trivial // GENERATED: source: {{.*}}lean_project.cpp:{{[0-9]+:[0-9]+}} diff --git a/clang/test/Verify/suite/lean_readable.cpp b/clang/test/Verify/suite/lean_readable.cpp index 8227146516..16bd3f0f2b 100644 --- a/clang/test/Verify/suite/lean_readable.cpp +++ b/clang/test/Verify/suite/lean_readable.cpp @@ -7,7 +7,7 @@ // // RUN: rm -rf %t && mkdir -p %t // RUN: %cpp-verify --backend=lean --no-lean-auto --lean-project=%t/p %s -- 2>&1 | FileCheck %s --check-prefix=EXPORT -// RUN: FileCheck %s --input-file=%t/p/CppVerify/Generated.lean +// RUN: %python %S/Inputs/lean_project_text.py %t/p | FileCheck %s // RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_twice_edf933/cppverify_twice_edf933_postcondition_28de726e.lean --check-prefix=STUB // RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_poly_c94108/cppverify_poly_c94108_postcondition_fde367c1.lean --check-prefix=LETS // Every stub's names match its readable form: the project builds, with @@ -21,7 +21,7 @@ // // A readable form that says less than its goal does not build: here the // definition of b is replaced by the conclusion it should lead to. -// RUN: sed -i 's/(h_b_1 : b_1 = __local_call_2_1)/(h_b_1 : b_1 = x_0 + (BitVec.ofInt 32 (2)))/' %t/p/CppVerify/Generated.lean +// RUN: sed -i 's/(h_b_1 : b_1 = __local_call_2_1)/(h_b_1 : b_1 = x_0 + (BitVec.ofInt 32 (2)))/' %t/p/CppVerify/Goals/cppverify_twice_edf933.lean // RUN: cd %t/p && not lake build CppVerify.Generated 2>&1 | FileCheck %s --check-prefix=BRIDGE int next(int x) @@ -222,4 +222,4 @@ int poly(int x) // TRUSTED: Exported: lean obligation: twice // CERTIFIED: Certified: twice [backend=Lean] [trusts=next] -// BRIDGE: Generated.lean:{{[0-9]+}}:{{[0-9]+}}: Application type mismatch: The argument +// BRIDGE: cppverify_twice_edf933.lean:{{[0-9]+}}:{{[0-9]+}}: Application type mismatch: The argument diff --git a/clang/test/Verify/suite/lean_semantics.cpp b/clang/test/Verify/suite/lean_semantics.cpp index dcafd92436..5ec309a04d 100644 --- a/clang/test/Verify/suite/lean_semantics.cpp +++ b/clang/test/Verify/suite/lean_semantics.cpp @@ -9,8 +9,8 @@ // // RUN: rm -rf %t.export %t.mix %t.numerals %t.call // RUN: %cpp-verify --backend=lean --lean-project=%t.export %s -- 2>&1 | FileCheck %s --check-prefix=EXPORT -// RUN: FileCheck %s --input-file=%t.export/CppVerify/Generated.lean --check-prefix=LEAN -// RUN: not grep -E 'BitVec\.(udiv|sdiv) ' %t.export/CppVerify/Generated.lean +// RUN: %python %S/Inputs/lean_project_text.py %t.export | FileCheck %s --check-prefix=LEAN +// RUN: %python %S/Inputs/lean_project_text.py %t.export | not grep -E 'BitVec\.(udiv|sdiv) ' // RUN: lake --dir=%t.export build CppVerify.Generated // // The prelude's values where C++, SMT-LIB, and Lean's own operators differ. diff --git a/clang/test/Verify/suite/lean_spec_definitions.test b/clang/test/Verify/suite/lean_spec_definitions.test new file mode 100644 index 0000000000..cb1c1582ed --- /dev/null +++ b/clang/test/Verify/suite/lean_spec_definitions.test @@ -0,0 +1,84 @@ +# REQUIRES: lean +# +# A spec function of a Lean project is a definition when Lean proves that it +# terminates by its decreases measures, and opaque otherwise. Its goals state +# the same definition instances as before; a proof may also unfold the +# definition, or prove by induction over it. +# +# RUN: rm -rf %t && mkdir -p %t +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %S/Inputs/lean_spec_definitions.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Specs.lean --check-prefix=SPECS +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Specs.lean --check-prefix=REACHES +# +# Lean's verdict on each spec is kept: a run of the same source tries +# nothing and writes no file. +# RUN: touch %t/same +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %S/Inputs/lean_spec_definitions.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT +# RUN: find %t/p -newer %t/same -type f -not -path '*/.lake/*' | count 0 +# +# A proof by induction over tri, which an opaque tri did not allow. +# RUN: cp %S/Inputs/lean_spec_definitions_tri_nonneg.lean %t/p/CppVerify/Proofs/cppverify_tri_nonneg_42a030/cppverify_tri_nonneg_42a030_postcondition_053b1980.lean +# RUN: not %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %S/Inputs/lean_spec_definitions.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFY +# +# Without Lean nothing is tried, and every spec is opaque. +# RUN: mkdir -p %t/empty +# RUN: env PATH=%t/empty %cpp-verify --backend=lean --lean-project=%t/q %S/Inputs/lean_spec_definitions.cpp -- 2>&1 | FileCheck %s --check-prefix=WITHOUT +# RUN: FileCheck %s --input-file=%t/q/CppVerify/Specs.lean --check-prefix=OPAQUE --implicit-check-not=def + +# EXPORT: Exported: decreases: tri +# EXPORT: Exported: lean obligation: tri_nonneg (cppverify_auto proved 1 of 2 goals) +# EXPORT-NEXT: Exported: lean obligation: tri_four (cppverify_auto proved 2 of 2 goals) +# EXPORT-NEXT: Exported: lean obligation: even_four (cppverify_auto proved 2 of 2 goals) +# EXPORT-NEXT: Exported: lean obligation: small_ack (cppverify_auto proved 2 of 2 goals) +# EXPORT-NEXT: Exported: lean obligation: log2_eight (cppverify_auto proved 2 of 2 goals) +# EXPORT: Exported: lean obligation: down_zero (cppverify_auto proved 2 of 2 goals) +# EXPORT: Exported: lean obligation: reaches_zero (cppverify_auto proved 2 of 2 goals) + +# Callees come first. steps, whose termination rests on the postcondition +# of half, stays opaque, and count_steps, which calls it, is defined against +# it. A lexicographic measure is a tuple; a call under `||` or `&&` sees its +# condition; a mutual recursion is one block; down's call has the measure -1 +# where its caller's is 0; log2's measure falls by C++ division. +# SPECS: {{^}}def cppSpec_fn_5f5a3468616c6669 (n : Int) : Int :={{$}} +# SPECS: {{^}}opaque cppSpec_fn_5f5a35737465707369 : Int -> Int{{$}} +# SPECS: {{^}}def cppSpec_fn_5f5a3131636f756e745f737465707369 (n : Int) : Int :={{$}} +# SPECS: {{^}}def cppSpec_fn_5f5a3361636b6969 (m : Int) (n : Int) : Int :={{$}} +# SPECS: {{^}}termination_by (((m) + 1).toNat, ((n) + 1).toNat){{$}} +# SPECS: {{^}}mutual{{$}} +# SPECS: {{^}}def cppSpec_fn_5f5a336f646469 (n : Int) : Prop :={{$}} +# SPECS-NEXT: {{^}} if _h : n > (0 : Int) then (cppSpec_fn_5f5a346576656e69 (n - (1 : Int))) else False{{$}} +# SPECS: {{^}}def cppSpec_fn_5f5a346576656e69 (n : Int) : Prop :={{$}} +# SPECS-NEXT: {{^}} if _h : n ≤ (0 : Int) then True else (cppSpec_fn_5f5a336f646469 (n - (1 : Int))){{$}} +# SPECS: {{^}}end{{$}} +# SPECS: {{^}}def cppSpec_fn_5f5a3374726969 (n : Int) : Int :={{$}} +# SPECS-NEXT: {{^}} if _h : n ≤ (0 : Int) then (0 : Int) else (cppSpec_fn_5f5a3374726969 (n - (1 : Int))) + n{{$}} +# SPECS-NEXT: {{^}}termination_by ((n) + 1).toNat{{$}} +# SPECS-NEXT: {{^}}decreasing_by all_goals cppverify_decreasing{{$}} +# SPECS: {{^}}def cppSpec_fn_5f5a34646f776e69 (n : Int) : Int :={{$}} +# SPECS: {{^}}def cppSpec_fn_5f5a346c6f673269 (n : Int) : Int :={{$}} +# SPECS-NEXT: {{^}} if _h : n ≤ (1 : Int) then (0 : Int) else (cppSpec_fn_5f5a346c6f673269 (cppIntDiv n (2 : Int))) + (1 : Int){{$}} + +# CERTIFY: Certified: decreases: tri [backend=Lean] +# CERTIFY-NEXT: Certified: decreases: even [backend=Lean] +# CERTIFY-NEXT: Certified: decreases: odd [backend=Lean] +# CERTIFY-NEXT: Certified: decreases: ack [backend=Lean] +# CERTIFY: Certified: decreases: log2 [backend=Lean] +# CERTIFY: Certified: tri_nonneg [backend=Lean] +# CERTIFY-NEXT: Certified: tri_four [backend=Lean] +# CERTIFY-NEXT: Certified: even_four [backend=Lean] +# CERTIFY-NEXT: Certified: small_ack [backend=Lean] +# CERTIFY-NEXT: Certified: log2_eight [backend=Lean] +# A verdict still rests on the termination cpp-verify establishes: that of +# half is not, so neither are those that apply count_steps. +# CERTIFY: Certified: decreases: down [backend=Lean] +# CERTIFY-NEXT: Unresolved: decreases: count_steps [backend=Lean] [reason=spec.termination] +# CERTIFY-NEXT: Unresolved: down_zero [backend=Lean] [reason=spec.termination] + +# A call under an existential sees its range. +# REACHES: {{^}}def cppSpec_fn_5f5a377265616368657369 (n : Int) : Prop :={{$}} +# REACHES-NEXT: {{^}} if _h : n ≤ (0 : Int) then True else (∃ ([[K:[_a-z0-9]+]] : Int), if _h : (0 : Int) ≤ [[K]] ∧ [[K]] < n then (cppSpec_fn_5f5a377265616368657369 [[K]]) else False){{$}} + +# WITHOUT: Exported: lean obligation: tri_four{{$}} + +# OPAQUE: {{^}}opaque cppSpec_fn_5f5a3361636b6969 : Int -> Int -> Int{{$}} +# OPAQUE: {{^}}opaque cppSpec_fn_5f5a3374726969 : Int -> Int{{$}} diff --git a/clang/test/Verify/suite/lean_toolchain.test b/clang/test/Verify/suite/lean_toolchain.test index 306038ccee..03b229fd70 100644 --- a/clang/test/Verify/suite/lean_toolchain.test +++ b/clang/test/Verify/suite/lean_toolchain.test @@ -22,7 +22,7 @@ # The trial of cppverify_auto, then certification, each with the pin. # ELAN-LOG: {{^}}+leanprover/lean4:v4.35.0 --version{{$}} -# ELAN-LOG-NEXT: {{^}}+leanprover/lean4:v4.35.0 --dir={{.*}}.project build CppVerify.User CppVerify.Auto{{$}} +# ELAN-LOG-NEXT: {{^}}+leanprover/lean4:v4.35.0 --dir={{.*}}.project build CppVerify.Generated CppVerify.User CppVerify.Auto{{$}} # ELAN-LOG-NEXT: {{^}}+leanprover/lean4:v4.35.0 --version{{$}} # ELAN-LOG-NEXT: {{^}}+leanprover/lean4:v4.35.0 --dir={{.*}}.project build CppVerify.Generated CppVerify.User CppVerify.Auto{{$}} diff --git a/clang/unittests/Verify/CertifyTest.cpp b/clang/unittests/Verify/CertifyTest.cpp index 5a076f1329..9769016bcf 100644 --- a/clang/unittests/Verify/CertifyTest.cpp +++ b/clang/unittests/Verify/CertifyTest.cpp @@ -102,6 +102,7 @@ Expr clone(const LogicExpr &E) { Copy->Binder = E.Binder; Copy->OverflowOp = E.OverflowOp; Copy->SpecCallee = E.SpecCallee; + Copy->CollectionOp = E.CollectionOp; for (const auto &Child : E.Children) Copy->Children.push_back(clone(*Child)); return Copy; @@ -1936,6 +1937,213 @@ TEST(CertifyTest, AgreesWithLeanEvaluation) { "rem" + Operands); } + // Collections: what reads a random chain of operations gives, and when two + // sequences are equal. Lean decides each with the prelude's definitions. + using CollectionOp = LogicCollectionOp; + auto collection = [](CollectionOp Op, LogicSort Sort, auto... Operands) { + Expr E = node(LogicExpr::Collection, Sort, std::move(Operands)...); + E->CollectionOp = Op; + return E; + }; + const LogicSort Seq = LogicSort::collection(LogicSortKind::Seq); + const LogicSort Set = LogicSort::collection(LogicSortKind::Set); + const LogicSort Multiset = LogicSort::collection(LogicSortKind::Multiset); + const LogicSort Map = LogicSort::collection(LogicSortKind::Map); + auto small = [&] { + return mathLiteral(static_cast(Random() % 8) - 2); + }; + std::function sequence = [&](unsigned Depth) -> Expr { + switch (Depth == 0 ? Random() % 2 : Random() % 5) { + case 0: + return collection(CollectionOp::SeqEmpty, Seq); + case 1: + return collection(CollectionOp::SeqUnit, Seq, small()); + case 2: + return collection(CollectionOp::SeqPush, Seq, sequence(Depth - 1), + small()); + case 3: + return collection(CollectionOp::SeqConcat, Seq, sequence(Depth - 1), + sequence(Depth - 1)); + default: + return collection(CollectionOp::SeqSubrange, Seq, sequence(Depth - 1), + small(), small()); + } + }; + std::function set = [&](unsigned Depth) -> Expr { + const CollectionOp Combined[] = {CollectionOp::SetUnion, + CollectionOp::SetIntersect, + CollectionOp::SetDifference}; + switch (Depth == 0 ? 0 : Random() % 4) { + case 0: + return collection(CollectionOp::SetEmpty, Set); + case 1: + return collection(CollectionOp::SetInsert, Set, set(Depth - 1), small()); + case 2: + return collection(CollectionOp::SetRemove, Set, set(Depth - 1), small()); + default: + return collection(Combined[Random() % 3], Set, set(Depth - 1), + set(Depth - 1)); + } + }; + std::function multiset = [&](unsigned Depth) -> Expr { + if (Depth == 0) + return collection(CollectionOp::MultisetEmpty, Multiset); + return collection(Random() % 3 == 0 ? CollectionOp::MultisetRemove + : CollectionOp::MultisetInsert, + Multiset, multiset(Depth - 1), small()); + }; + std::function map = [&](unsigned Depth) -> Expr { + if (Depth == 0) + return collection(CollectionOp::MapEmpty, Map); + if (Random() % 3 == 0) + return collection(CollectionOp::MapRemove, Map, map(Depth - 1), small()); + return collection(CollectionOp::MapInsert, Map, map(Depth - 1), small(), + small()); + }; + for (unsigned I = 0; I != 60; ++I) { + const std::string Name = "collection " + std::to_string(I); + switch (I % 6) { + case 0: + evaluated(collection(CollectionOp::SeqLength, math(), sequence(3)), Name); + break; + case 1: + evaluated( + collection(CollectionOp::SeqIndex, math(), sequence(3), small()), + Name); + break; + case 2: + evaluated(collection(CollectionOp::SeqContains, LogicSort::boolSort(), + sequence(3), small()), + Name); + break; + case 3: + evaluated(collection(CollectionOp::SetContains, LogicSort::boolSort(), + set(4), small()), + Name); + break; + case 4: + evaluated( + collection(CollectionOp::MultisetCount, math(), multiset(5), small()), + Name); + break; + default: + evaluated(collection(I % 12 == 5 ? CollectionOp::MapGet + : CollectionOp::MapContains, + I % 12 == 5 ? math() : LogicSort::boolSort(), map(4), + small()), + Name); + break; + } + } + for (unsigned I = 0; I != 20; ++I) + evaluated(boolean(LogicExpr::Eq, sequence(2), sequence(2)), + "sequence equality " + std::to_string(I)); + // Each operation at operands where it matters: reads in and out of range, + // every clamp of a subrange, an element inserted and removed, each + // combination of membership, a count removed that is there and one that + // is not, and a key written over and removed. + auto number = [](int64_t Value) { return mathLiteral(Value); }; + auto list = [&](std::initializer_list Elements) { + Expr S = collection(CollectionOp::SeqEmpty, Seq); + for (int64_t Element : Elements) + S = collection(CollectionOp::SeqPush, Seq, std::move(S), number(Element)); + return S; + }; + auto read = [&](CollectionOp Op, LogicSort Sort, Expr Of, int64_t At, + const std::string &Name) { + evaluated(collection(Op, Sort, std::move(Of), number(At)), Name); + }; + for (int64_t I = -1; I <= 3; ++I) + read(CollectionOp::SeqIndex, math(), list({1, 2, 3}), I, + "index " + std::to_string(I)); + for (int64_t X = 0; X <= 3; ++X) + read(CollectionOp::SeqContains, LogicSort::boolSort(), list({1, 2, 3}), X, + "sequence contains " + std::to_string(X)); + evaluated(collection(CollectionOp::SeqLength, math(), + collection(CollectionOp::SeqUnit, Seq, number(5))), + "unit length"); + for (int64_t I = 0; I <= 2; ++I) + read(CollectionOp::SeqIndex, math(), + collection(CollectionOp::SeqConcat, Seq, list({1}), list({2})), I, + "concat index " + std::to_string(I)); + for (int64_t Lo = -1; Lo <= 4; ++Lo) + for (int64_t Hi = -1; Hi <= 4; ++Hi) { + auto subrange = [&] { + return collection(CollectionOp::SeqSubrange, Seq, list({1, 2, 3}), + number(Lo), number(Hi)); + }; + const std::string Name = + "subrange " + std::to_string(Lo) + " " + std::to_string(Hi); + evaluated(collection(CollectionOp::SeqLength, math(), subrange()), + Name + " length"); + for (int64_t I = 0; I <= 2; ++I) + read(CollectionOp::SeqIndex, math(), subrange(), I, + Name + " index " + std::to_string(I)); + } + auto members = [&](std::initializer_list Elements) { + Expr S = collection(CollectionOp::SetEmpty, Set); + for (int64_t Element : Elements) + S = collection(CollectionOp::SetInsert, Set, std::move(S), + number(Element)); + return S; + }; + for (int64_t X = 1; X <= 2; ++X) { + read(CollectionOp::SetContains, LogicSort::boolSort(), members({1}), X, + "set insert " + std::to_string(X)); + read(CollectionOp::SetContains, LogicSort::boolSort(), + collection(CollectionOp::SetRemove, Set, members({1, 2}), number(1)), + X, "set remove " + std::to_string(X)); + } + for (CollectionOp Op : {CollectionOp::SetUnion, CollectionOp::SetIntersect, + CollectionOp::SetDifference}) + for (int64_t X = 1; X <= 4; ++X) + read(CollectionOp::SetContains, LogicSort::boolSort(), + collection(Op, Set, members({1, 2}), members({2, 3})), X, + std::string(logicCollectionOpName(Op)) + " " + std::to_string(X)); + auto counts = [&](std::initializer_list Elements) { + Expr M = collection(CollectionOp::MultisetEmpty, Multiset); + for (int64_t Element : Elements) + M = collection(CollectionOp::MultisetInsert, Multiset, std::move(M), + number(Element)); + return M; + }; + for (int64_t X = 3; X <= 4; ++X) { + read(CollectionOp::MultisetCount, math(), counts({3, 3}), X, + "count " + std::to_string(X)); + for (std::initializer_list Before : + {std::initializer_list{}, std::initializer_list{3}, + std::initializer_list{3, 3}}) + read(CollectionOp::MultisetCount, math(), + collection(CollectionOp::MultisetRemove, Multiset, counts(Before), + number(3)), + X, + "count after remove of " + std::to_string(Before.size()) + " at " + + std::to_string(X)); + } + auto entries = [&] { + return collection(CollectionOp::MapInsert, Map, + collection(CollectionOp::MapInsert, Map, + collection(CollectionOp::MapEmpty, Map), + number(1), number(10)), + number(2), number(20)); + }; + for (int64_t K = 1; K <= 3; ++K) { + const std::string At = " " + std::to_string(K); + read(CollectionOp::MapContains, LogicSort::boolSort(), entries(), K, + "map contains" + At); + read(CollectionOp::MapGet, math(), entries(), K, "map get" + At); + read(CollectionOp::MapGet, math(), + collection(CollectionOp::MapInsert, Map, entries(), number(1), + number(11)), + K, "map overwrite" + At); + read(CollectionOp::MapContains, LogicSort::boolSort(), + collection(CollectionOp::MapRemove, Map, entries(), number(1)), K, + "map remove contains" + At); + read(CollectionOp::MapGet, math(), + collection(CollectionOp::MapRemove, Map, entries(), number(1)), K, + "map remove get" + At); + } + ObligationModule &Module = Facts.Module; Module.FunctionName = "certify_lean"; Module.FunctionIdentity = "certify_lean"; diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index e2ed48978b..e2603cfe67 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1546,6 +1546,10 @@ proof of a printed goal is a proof of its obligation. | `MathematicalInteger`, `Pointer` | `Int` | | `BitVector(N)` | `BitVec N` | | `Heap` | `CppHeap` (`Int -> Int`) | +| `Seq` | `List Int` | +| `Set` | `Int → Bool`, its membership test | +| `Multiset` | `Int → Nat`, its counts | +| `Map` | `Int → Option Int`, the value at each key it holds | - **Precedence.** Each operator is printed at its Lean notation level (`Init/Notation.lean`, `Init/Core.lean`), and an operand that binds looser @@ -1590,6 +1594,24 @@ proof of a printed goal is a proof of its obligation. only the `if`s of generated definitions whose condition has no decision procedure; Lean's instance search already tries a specific instance before it. +- **Collections.** Each operation is a prelude function + (`LeanCollectionPrelude`), `cppSeqAt`, `cppSetInsert`, `cppMapGet`, ..., with + the total meaning of ``: a read outside a sequence or a map's + domain is 0, a subrange clamps `lo` into `[0, len]` and `hi` into + `[lo', len]`, a multiset removal of a count of 0 leaves 0 (`Nat` + subtraction). A set is its membership test rather than a finite set, since + a set may be infinite (Vermilion's mirror of vstd uses Mathlib's `Finset`, + for finite sets only). The three membership predicates are `def`s with + `Decidable` instances, not `abbrev`s: as `abbrev`s, the Boolean lemmas of + `cppverify_norm` rewrote `cppSetContains s x` to `s x = true`, and the + lemmas stated on `cppSetContains` no longer matched. As Vermilion states + its vstd operations, the prelude states each operation's meaning in + `@[simp, grind =]` lemmas (`cppSeqAt_push`, `cppSetContains_remove`, + `cppMultisetCount_remove`, ...), with `grind_pattern`s for the facts that + lengths and counts are not negative (grind's own pattern for `0 ≤ count m + x` is the inequality, which no goal contains), and extensionality lemmas + (`cppSeq_ext`, `cppSet_ext`, `cppMultiset_ext`, `cppMap_ext`); all of them + are theorems of the definitions, so no goal rests on them. `CertifyTest.AgreesWithLeanEvaluation` checks the agreement in the pinned Lean. The value the certifier computes for each ground term is a theorem Lean @@ -1600,7 +1622,15 @@ bits signed and unsigned, every mathematical operator inside every other, and every connective inside every other at all eight assignments of its operands, so that a lost parenthesis changes a value; and every operator at the extreme operands of widths 1, 8, and 64 (a zero divisor, `INT_MIN / -1`, a shift past -the width, each overflow predicate). `lean_semantics.cpp` checks the printed +the width, each overflow predicate); and for collections, 80 random chains of +operations read by length, index, membership, count, and key, 20 equalities +of sequences, and each operation where it matters (every clamp of a +subrange of `[1, 2, 3]`, membership of an element inserted and removed, each +combination of two sets, a multiset removal of a count of 0, 1, and 2, a key +written over and removed). Printing set removal as insertion fails it. +`lean_collections.test` exports a function over each kind, certifies their +automatic proofs and a proof by hand of `total(s.push(x)) == total(s) + x`, +and keeps a false claim unproved. `lean_semantics.cpp` checks the printed forms, builds an export, certifies a goal whose proof needs the quantifier closed and `decide` on a comparison, refuses proofs that read `(a ^ b) + 1` as `a ^ (b + 1)` or `2 - 3` in `Nat`, and its probe file @@ -1627,6 +1657,59 @@ uses when the source around it changes. `Proofs/Goal_.lean`: reordering two postconditions gave each proof the other's goal, and inserting a function renamed the bodies every later proof used. +- **Modules.** The adapter writes a project's goals by group + (`LeanProjectModules`): the goals, readable forms, bridges, and spec + bodies of each function go to `CppVerify/Goals/.lean`, which + imports `CppVerify/Specs.lean`, where `emitLeanFunctionDeclarations` + declares each spec the run's modules apply once (`opaque + cppSpec_`). Two goal modules that declared one spec would clash + when imported together, and Lean 4.35's import keeps one of two differing + declarations without a word. The prelude is `CppVerify/Prelude.lean`, and + `CppVerify/Generated.lean` imports every goal module, so a `User.lean` of + 0.1, which imports it, still sees every goal. A proof imports its goal + module, `User` (which a new project starts with `import CppVerify.Specs`), + and `Auto` (which imports `Prelude`); `CppVerify.lean`, the library's + root, imports `Check`, so `lake build` builds every proof (before, the + library had no root and `lake build` failed). Every file is written only + when its text changes (`writeTextFileIfChanged`), and + `writeLeanProjectModules` removes every goal module the run did not + write: a fallback run rewrites `Specs` with the specs of the modules it + exports, and a module it kept from an earlier run failed (`Unknown + identifier cppSpec_...`). +- **Spec definitions** (`leanSpecDefinition`, `leanSpecsText`, + `tryLeanSpecs`). The adapter gives each logical function of a project its + opaque declaration and, unless it is a choice, has no step definition, or + recurses without `Decreases` (an archive's), a candidate definition: the + step definition printed with the recursion's applications by name and no + temporaries (a hoisted application would lose its guard), in definition + mode (`LeanDefinitionMode`), where each `ite` is `if _h : c`, a + conjunction or disjunction whose later operand applies a spec is a + dependent `if` (`a ∧ b` -> `if _h : a then b else False`, `a ∨ b` -> `if + _h : a then True else b`, `¬a ∨ b` -> `if _h : a then b else True`), and + a bounded existential over one guards its body by its range, each a + classical equivalence; then `termination_by ((m1 + 1).toNat, ...)` and + `decreasing_by all_goals cppverify_decreasing` (a prelude macro: `simp_wf; + omega`, then with the collection and comparison wrappers unfolded, then + with `cppIntDiv` and `cppIntRem` unfolded and their conditions split, so + that a measure falling by a constant divisor is linear (`log2(n / 2)`), + then `simp_all; omega`, then `decreasing_tactic`). `(m + 1).toNat` decreases + exactly where the termination check's relation does (`upper >= 0 && + lower < upper`, lower possibly -1); Vermilion instead guards the whole + body by `0 ≤ measure`, which changes the value where the measure is + negative and the body does not recurse. The driver groups the functions + by the strongly connected components of their applications (Tarjan, + callees first), each group one `mutual` block, and decides each from + `.cppverify/specs/`, the key the SHA-256 of the toolchain, + `LeanSpecRevision`, the group's text, and what each callee group is. The + rest it tries in one Lean file importing `Auto`, the others as decided, + undecided callees as definitions, `#cppverify_axioms` after each member: + a definition Lean rejects is added with `sorryAx`, or not at all. A + group's verdict is kept only when each callee tried in the same round was + accepted; else it is tried again with the rejected callee opaque, until + nothing changes. No Lean: undecided groups are opaque and nothing is kept. + `Specs.lean` has the groups in that order, and its definitions use the + classical decidability instance locally. Statements do not change: a goal + states the same definition instances, which a definition makes theorems. - **Records.** The exporter returns a `LeanProjectGoal` for every obligation of each module it exports, those a fallback selection leaves to the solver marked `Exported = false`, with the 0.1 names of the goal and @@ -1675,7 +1758,7 @@ uses when the source around it changes. `G.of_readable : G.readable → G` is a term, one prelude lemma per hypothesis (`cppverify_imp_or : (a → b) → ¬a ∨ b`, or `cppverify_not_imp_or : (¬a → b) → a ∨ b`), so the kernel checks with - `Generated.lean` that the readable form implies the goal: a printer bug in + the goal module that the readable form implies the goal: a printer bug in it fails the build, never certifies. `LeanProjectGoal::Intros` gives the stub its `intro` list. On the 375 suite exports, the 351 that built before still build, with every bridge. @@ -1696,11 +1779,49 @@ uses when the source around it changes. Z3 proves, they prove 90.2%. Stating the range of every `BitVec.toInt` term first proved nothing more (`grind` knows the ranges), and removing `Int.bmod` with an `omega` discharger proved 32 fewer and took longer, so - neither is a step. Heartbeats alone did not bound the time, since a kernel - check is not counted. The trial takes every exported goal whose proof file + neither is a step. Revision 2 (`LeanAutomationRevision`) appends three + steps after the others, so that every goal an earlier step proves keeps + its proof: `_bveq` states equalities of machine values and sign extensions + as integer facts too (`← BitVec.toInt_inj`, `toInt_signExtend_of_le` with + `omega` for its side condition); `_ext` applies a collection's + extensionality lemma; `_unfold` delta-expands the generated spec bodies + (`cppverify_unfold_bodies`, every constant named `cppSpecBody_…`, to a + fixed point, since a body names only lower levels of its definition) in + the goal and its hypotheses, so each definition instance says what the + body does, then as `_bveq`. Tagging the bodies for `grind` instead would + have changed what every earlier step does. `_bveq` is not subsumed by + `_unfold`: on the 37 goals of `roundtrip_uleb128` (`llvm_uleb128.cpp`) + unfolding the lifted helpers' bodies exhausts the heartbeats, and `_bveq` + proves them. Over the same exports (375 sources, 9259 goals), of the 5582 + that Z3 proves revision 1 proves 5044 (90.4%) and revision 2 5210 + (93.3%), none fewer; of the 112 over collections, 86 and 104. A goal + neither proves now takes 2.8 s on average instead of 1.4 s. Revision 3 + appends `_eval`, which rewrites with the equations of every spec that + `CppVerify.Specs` defines (`cppverify_eval_specs`, from that module's + constant names), and with `cppIntDiv` and `cppIntRem`, and closes goals + at known arguments; on unknown ones it unfolds until its budget is spent. + It then appends `_div`, `grind` given the definitions of `cppIntDiv` and + `cppIntRem`, which decides a mathematical division or remainder by a + constant once their conditions are split; `_eval` fails without a spec + definition, and a contract such as `a / 2 >= 2` needs no spec. + Over the same exports, of the 5582 goals Z3 proves revision 2 proves + 5210 (93.3%) and revision 3 5301 (95.0%), none fewer, and of all 9259 + goals 8078 and 8194; in the five sources with the most new proofs, 48 of + their 61 are `_div`'s (pointer differences divide by the element size, + and binary search halves an interval) and 13 `_eval`'s (the factorial + constants of `mvp_factorial.cpp`). A goal neither proves takes 4.4 s on + average instead of 3.1 s. The trial makes 213 of the suite's 293 spec + functions definitions; of the 80 opaque, 69 have no definition to try + (20 choices, 47 heights and witnesses of inductive predicates, 2 + `unspecified` functions), and 11 do not terminate, or terminate only by + their own postcondition or a choice's axiom. Its first ladder missed + three that terminate by C++ division (`log2(n / 2)`), since `omega` does + not see through `cppIntDiv`. + Heartbeats alone did not bound the time, since a kernel check is not + counted. The trial takes every exported goal whose proof file is pristine and whose header (`automation:`) names no attempt by the - current `LeanAutomationRevision`, builds `User` and `Auto` with the pinned - toolchain, and runs `lean` itself (with the `LEAN_PATH` of `lake env`, so a + current `LeanAutomationRevision`, builds `Generated`, `User`, and `Auto` + with the pinned toolchain, and runs `lean` itself (with the `LEAN_PATH` of `lake env`, so a stopped process leaves no child) on a file of one theorem per goal, in `--jobs` chunks. Lean reports to a file, line by line: the step that proved each goal, then the axioms of its theorem or that the kernel @@ -1712,28 +1833,46 @@ uses when the source around it changes. the attempt. An export's `LeanAutomatic` counts its goals with automatic proofs. Without the toolchain nothing is tried. - **Certification** (`certifyLeanProject`) builds `Generated`, `User`, and - `Auto`, then each proof file with `lean -EhasSorry`, `--jobs` at once, - recording the goals whose proofs do not build, and runs the checker of + `Auto` with Lake, then each proof file with `lean -EhasSorry`, `--jobs` at + once, unless its key is unchanged (`leanProofKey`: SHA-256 of the + toolchain, the proof's text, and the bytes of the `.olean` of every project + module in its import closure, read from the `import` lines of their + sources; written to `.cppverify/built/` after a build, and removed + with the `.olean` before one). Lake cannot tell this itself: when a + dependency fails it names only the dependency, and a dependent's `.olean` + of an earlier build stays, so a proof the user broke would certify from + its old `.olean`. It records the goals whose proofs do not build and runs + the checker of `LeanCertifier.h`, written into the project as `.cppverify/Certify.lean`, with `lake env lean --run` over the goals that built. The checker elaborates none of the user's source, so their macros and commands cannot - change what it checks. It first checks every goal in one environment: all - proof modules imported at once, and the constants of every module of the - project replayed together through the kernel into the environment of the - toolchain modules they import (a constant two modules declare, as an - equation lemma derived in each, must be the same). A check reads only - kernel constants, so proofs imported together cannot change each other's - checks; an automatic proof imports `Lean`, whose import each goal would - repeat (33 goals took 161 s, now 8 s). If that import or replay fails, as a - proof file that declares a goal's name or a module the kernel rejects - makes it, each goal is checked on its own: it imports the proof module - (never freeing imported data, which a later import in the process reads), - and every module of the import closure whose `.olean` lies outside the - toolchain is replayed (as `leanchecker`'s `replayFromImports`), each once - in a run. Either way it checks that `G_proof` is a theorem of type exactly - `.const G []` with `G` a definition of `CppVerify.Generated`, collects its - axioms by walking the kernel constants it uses, and prints `ok` or `fail` - with the reason per goal. Each Lean result + change what it checks. It reads, from their compiled files, the goal + modules the goal list names, every proof module, and every module of the + project they import (its `.olean` lies outside the toolchain), imports the + toolchain modules among their imports once, and replays the project's + modules through the kernel into that one environment, each after the + modules it imports and the goal modules first, as `leanchecker` does. A + module the kernel rejects, a module that imports one, and a module that + declares a constant an earlier module or the toolchain declares otherwise + are left out, each with why; a constant two modules declare alike (an + equation lemma Lean derives in each, a theorem stated the same, which the + kernel's replay takes twice) is the same. So a proof file that declares a + goal's name is the one left out (`... declares G, which + CppVerify.Goals. declares`), and a bad module fails only the + goals whose proofs import it. Every check reads the kernel's constants and + the module that declared each, so proofs cannot change each other's + checks: a goal passes when its proof module and its goal module were + replayed, `G_proof` is a theorem of type exactly `.const G []` with `G` a + definition of its goal module, and the axioms its kernel constants reach + are allowed; every goal fails when a declaration of `CppVerify.User` + depends on `sorryAx` (`userSorry`; before, `User` was compiled with `sorry` + an error); it prints `ok` or `fail` with the reason per goal. One import + matters because an automatic proof imports `Lean`: a check per goal took + 161 s for 33 goals (now 8 s), and the first 0.2 checker, which fell back to + it when one module failed, imported each proof module and the imports of + each module it replayed again, never freeing imported data, which took + 13 GB for one proof through a rejected module (now 3.6 GB, + `lean_certifier_memory.test`) and stopped CI runners. Each Lean result records its goals (`VerifyResult::LeanGoals`), and a function is `Certified` only when all of them pass; a failure names the obligation. Before 0.2 certification parsed what `Check.lean` printed, which imports @@ -1743,7 +1882,9 @@ uses when the source around it changes. `lean_certifier.test` checks each of those attacks, a proof file that defines a goal of the same name of its own (the type check alone would take it), a proof that does not build, and an axiom behind a lemma, with a function whose -proofs are sound certified beside each. `lean_readable.cpp` checks the readable form of each kind of assumption, +proofs are sound certified beside each; `lean_certifier_memory.test` bounds +the checker's memory where a proof imports `Lean` through a module the kernel +rejects. `lean_readable.cpp` checks the readable form of each kind of assumption, the bridge, the stubs (every one builds), a proof by hypothesis names that certifies, and a readable form that says less than its goal, which fails at its bridge. `lean_automation.test` checks what an export writes (an automatic @@ -1755,7 +1896,12 @@ unfinished lemma does not count, and `--no-lean-auto`. `lean_identity.test` walk reordering, renames of two functions at once, a changed statement, a removed function and its return, fallback runs, pruning, and a 0.1 project with proofs, stubs, and a proof of a goal that is gone) and certifies it after -the renames and the migration. +the renames and the migration. `lean_modules.test` checks the layout (a +spec declared once for two goal modules certified together, a proof's +imports, a new `User`), that a rerun writes no file, that a change to one +function compiles only its goal module, `Generated`, and its proofs again, +`lake build`, that a deleted function takes its module, a 0.1 `User.lean`, +and a fallback run that keeps no goal module. ## Counterexample Extraction @@ -1885,7 +2031,7 @@ The driver selects a backend via `VerifyOptions` (`Verifier.h` / `cpp-verify --b | **Strict portfolio** | `PortfolioVerifyBackend` | Runs ordered Z3 and cvc5 queries. Matching UNSAT proves; matching certified counterexamples fail and retain the Z3 model; disagreement or an unresolved side is unresolved. | | **Race** | `RaceVerifyBackend` | Runs the Z3 and cvc5 backends at once; the first proof or certified counterexample stands and cancels the other (`cancel`/`resume`: a backend-wide `Race` of Z3 encoders, each forwarding an interrupt to the pass it runs, and a flag the cvc5 process loop polls). Otherwise the obligations either proved are joined, `Verified` (`z3+cvc5`) when they cover the module. | | **BMC** | `LoopUnroll` on VCR, then shared obligation/Z3 path | Source verification grows bounds from zero through `--unroll=N`, stopping on a counterexample, complete unwinding, unresolved query, or the maximum frontier. Safety with failed unwinding is `BoundedSafe(N)`; only proved unwinding is `Verified`. A spec's checks have no loops: the driver solves them with a Z3 backend (`SpecBackend`), as on the default path, and keeps the bound on their archived modules for replay. | -| **Lean** | `exportLeanScratchPad` / project certification | Standalone mode emits unchecked theorem stubs. Project mode emits direct source goals, total functional heaps, typed bit-vector/integer operations, and compact finite-fuel spec bodies into generated files while preserving user proofs. Export is `Exported`; only the pinned admission-free kernel/axiom check is `Certified`. Collections are `logic.unsupported` (planned for a future release). | +| **Lean** | `exportLeanScratchPad` / project certification | Standalone mode emits unchecked theorem stubs. Project mode emits direct source goals, total functional heaps, typed bit-vector/integer operations, and compact finite-fuel spec bodies into generated files while preserving user proofs. Export is `Exported`; only the pinned admission-free kernel/axiom check is `Certified`. Collections are core Lean values (`List Int`, `Int → Bool`, `Int → Nat`, `Int → Option Int`) with prelude operations and lemmas. | A Lean project pins `LeanToolchain` (`Driver/CppVerifyVersion.h`) in its `lean-toolchain` file. A pin in `EarlierLeanToolchains`, which an earlier diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 2e47c14254..3f51623778 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1595,9 +1595,14 @@ cppverify::proof void sum_concat(seq s, seq t) values: `[1, 2]`, `{1, 3..5}` (a run), `{2: 3}` (counts), `{1 -> 7}`, and `{..}` (every integer). - Backends: Z3 and cvc5 decide all four (cvc5 settles fewer goals that - need an infinite set or ghost collections in loops). Lean does not - support them yet (`logic.unsupported`); that is planned for a future - release. + need an infinite set or ghost collections in loops). Lean states them with + core types: a sequence is a `List Int`, a set its membership test + `Int → Bool` (a set may be infinite, so not a finite set), a multiset its + counts `Int → Nat`, and a map `Int → Option Int`. Each operation is a + function of the generated prelude with the total meaning above, and + lemmas state what each means for `simp` and `grind`, as Vermilion's + mirror of vstd states each operation for its ladder; Lean's evaluation of + every operation agrees with the certifier's. ## Clang Modification Details @@ -1913,7 +1918,23 @@ Lean's evaluation agrees with the certifier on random ground terms and on every operator at its extreme operands. Standalone output is an unchecked scratch-pad. Editable project mode pins Lean 4.35.0 (`LeanToolchain`), overwrites only generated semantics and the active check module, and preserves reusable user lemmas and one proof file -per goal. A goal is named by its function and its statement, never by a +per goal. The generated semantics are a module per function, +`CppVerify/Goals/.lean`, over one `CppVerify/Specs.lean` that +declares each spec the goals apply once, as Vermilion emits a unit per +function over one `Specs` file; each goal module defines the spec bodies its +goals unfold under the function's prefix. A proof imports its function's +goal module, the user's lemmas (`User.lean`, which a new project starts by +importing `Specs`), and `Auto`, so a change to one function builds again +only what imports its module. A file is written only when its text changes, +and a run writes the goal modules of the functions it exports and removes +every other, so that every module of the project builds. A spec function is a +Lean definition, by its step definition with every condition that reaches a +recursive application a hypothesis there and its `decreases` measures as +`termination_by`, when the pinned Lean accepts it at export, and opaque +otherwise; Lean's verdict is kept in the project. The definition has the +spec's value at every argument (it is never guarded by the measure as a +whole), so a proof may unfold it or use its induction principle, and goals +do not change. A goal is named by its function and its statement, never by a position: `cppverify__
__`, where `h6` hashes the function's identity (overloads) and `h8` begins the SHA-256 hash of the obligation's statement, its goal with the logical declarations it uses and @@ -1942,7 +1963,11 @@ tactic of the generated `CppVerify/Auto.lean`, with the pinned toolchain when it is installed, as Vermilion, Why3, and Frama-C's WP run their automation before a goal reaches the user: a ladder of steps (`grind`; memory stores as the functions they define and machine arithmetic as integers, then `grind`; -`decide`; `simp_all`), each with a heartbeat budget of its own and a +`decide`; `simp_all`; machine equalities and sign extensions as integers; +collection equality element by element; the definition instances a goal +states, by the bodies they name; the spec definitions by their equations; +mathematical division and remainder by their definitions), +each with a heartbeat budget of its own and a wall-clock limit per goal (`--lean-auto-timeout`), since heartbeats do not bound a kernel check. A step counts only when it closes the goal with a proof whose axioms are Lean's foundations, so the user's unfinished lemma never @@ -1952,16 +1977,22 @@ any other; any other gets a stub that records the attempt and the revision of `cppverify_auto` that made it. A file is tried again only when no attempt by the current revision is recorded, and only while nobody has edited it. Initial generation is `Exported`. Certification -holds against a proof author in bad faith. It compiles the user module and each -proof file on its own with `sorry` as an error, then runs a checker +holds against a proof author in bad faith. It builds the generated modules, +`User`, and `Auto` with Lake and compiles each proof file on its own with +`sorry` as an error, unless nothing it is built from changed since it last +built: its text and the compiled project modules it imports, by hash, since +Lake does not say which modules of a failed build are current. It then runs a checker (`LeanCertifier.h`) on the compiled modules, which elaborates none of the user's source, so no macro, notation, or command of theirs changes what it -checks: the kernel replays every module of the project a proof imports (only -the pinned toolchain's own modules are trusted), as `leanchecker` does, so no -declaration escaped the kernel; the proof's type is exactly the constant of its -goal, which `CppVerify.Generated` defines; and the axioms it depends on, +checks: the kernel replays every module of the project a proof imports into +one environment, after the toolchain's modules, imported once (only those are +trusted), as `leanchecker` does, so no declaration escaped the kernel, and a +module that declares a name an earlier one declares otherwise is rejected, +the goal modules being replayed first; the proof's type is exactly the +constant of its goal, which its function's goal module defines; and the axioms it depends on, collected from the constants it uses, are among `propext`, `Quot.sound`, and -`Classical.choice`. A function is `Certified` when every one of its goals +`Classical.choice`. A declaration of `User.lean` that uses `sorry` fails +every goal. A function is `Certified` when every one of its goals passes, and a failing goal leaves only its own function `Unresolved`, with the obligation and the reason. Certification runs the pinned toolchain whatever elan's default is, and a project pinned by an earlier release moves to diff --git a/website/source/book/part-ii/ch13-spec-and-proof-functions.rst b/website/source/book/part-ii/ch13-spec-and-proof-functions.rst index 0ae14c8742..c8462ceabf 100644 --- a/website/source/book/part-ii/ch13-spec-and-proof-functions.rst +++ b/website/source/book/part-ii/ch13-spec-and-proof-functions.rst @@ -1123,7 +1123,9 @@ there changes nothing, ``subrange`` clamps its bounds, and a key outside a map's domain maps to 0. Sequences are finite; sets, multisets, and maps range over all integers and may be infinite. Counterexamples show their values, such as ``s = [4, 3]`` or ``m = {1 -> 7, 4.. -> 2}``. Z3 and cvc5 decide all -four; Lean support for them is planned for a future release. +four, and a Lean project states them with core Lean types (a sequence is a +``List Int``, a set its membership test) and lemmas for each operation +(:doc:`ch17-backends-modular-calls`). Inductive predicates -------------------- diff --git a/website/source/book/part-ii/ch17-backends-modular-calls.rst b/website/source/book/part-ii/ch17-backends-modular-calls.rst index 032f7b26aa..7ed662d840 100644 --- a/website/source/book/part-ii/ch17-backends-modular-calls.rst +++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst @@ -156,21 +156,22 @@ For an explicit interactive proof: # complete proof/CppVerify/Proofs/*/*.lean; put shared lemmas in User.lean cpp-verify --backend=lean --lean-project=proof --lean-certify file.cpp -``Generated.lean``, ``Auto.lean``, and ``Check.lean`` are machine-owned; -``Check.lean`` imports every proof, so ``lake build CppVerify.Check`` builds -them all at once. ``User.lean`` is never overwritten, and each goal has a proof +The generated modules (``Prelude.lean``, ``Specs.lean``, ``Goals/``, +``Generated.lean``, ``Auto.lean``, and ``Check.lean``) are machine-owned; +``Check.lean`` imports every proof, so ``lake build``, run in the project, +builds them all (see `One module of goals per function`_ below). +``User.lean`` is never overwritten, and each goal has a proof file of its own: the proof ``cppverify_auto`` finds for it, or a stub (see `Proofs cppverify_auto finds`_ below). cpp-verify rewrites that file only while nobody has edited it; an edited one it never rewrites, but moves with its goal (see `Proofs that follow their goals`_ below). The project pins ``leanprover/lean4:v4.35.0``, which certification runs whatever elan's default toolchain is; a project 0.1 generated, pinned to ``v4.32.2``, moves to -it with a warning. Certification compiles the user -module and each proof file with admissions promoted to errors, then checks the -compiled modules as described in `What certification checks`_ below. +it with a warning. Certification builds the project +and compiles each proof file with admissions promoted to errors, then checks +the compiled modules as described in `What certification checks`_ below. -Each goal in ``Generated.lean`` is a Lean proposition that means what the -obligation means, so a proof of it is a proof of the obligation: +Each goal is a Lean proposition that means what the obligation means, so a proof of it is a proof of the obligation: - every operator keeps its grouping under Lean's own precedence: ``(a ^ b) + 1`` is ``(a_0 ^^^ b_0) + 1``, since Lean reads @@ -260,11 +261,8 @@ prints: Certified: nonnegative [backend=Lean] Certified: small [backend=Lean] -The Lean backend does not yet translate the spec collections of -```` (``seq``, ``set``, ``multiset``, ``map``): a function whose -obligations use one is ``Unresolved`` with reason ``logic.unsupported`` on -it. Lean support for them is planned for a future release; until then such -functions are verified with Z3 (the default) or cvc5. +The spec collections of ```` reach Lean too (see +`Collections in Lean`_ below). To keep Z3 as the fast path and export only unresolved functions: @@ -324,7 +322,7 @@ is ``Certified: f [backend=Lean] [vacuous]``, with a warning. Goals as hypotheses ~~~~~~~~~~~~~~~~~~~ -Next to each goal, ``Generated.lean`` states it as hypotheses and a +Next to each goal, its module states it as hypotheses and a conclusion. Each hypothesis is an assumption the goal makes, named by where it comes from, and a bridge from that form to the goal is proved in the same file. For this file: @@ -435,6 +433,197 @@ prints: A proof of the goal itself, as the one for ``small`` above, checks as well. +Spec functions in Lean +~~~~~~~~~~~~~~~~~~~~~~ + +A spec function that a goal applies is a Lean definition when Lean proves +that it terminates, and opaque otherwise, when a goal knows it only through +the definition instances it states. For this file: + +.. cppverify-example: flags --backend=lean --lean-project={dir}/proof + +.. code-block:: cpp + + cppverify::spec int tri(int n) + cppverify::decreases(n) + { + return n <= 0 ? 0 : tri(n - 1) + n; + } + + cppverify::proof void tri_nonneg(int n) + cppverify::post(tri(n) >= 0) + { + } + + cppverify::proof void tri_four() + cppverify::post(tri(4) == 10) + { + } + +``cpp-verify --backend=lean --lean-project=proof file.cpp`` prints: + +.. code-block:: text + + Exported: decreases: tri (cppverify_auto proved 1 of 1 goals) + Exported: lean obligation: tri_nonneg (cppverify_auto proved 1 of 2 goals) + Exported: lean obligation: tri_four (cppverify_auto proved 2 of 2 goals) + +and ``Specs.lean`` defines ``tri`` by its body: + +.. code-block:: lean4 + + def cppSpec_fn_5f5a3374726969 (n : Int) : Int := + if _h : n ≤ (0 : Int) then (0 : Int) else (cppSpec_fn_5f5a3374726969 (n - (1 : Int))) + n + termination_by ((n) + 1).toNat + decreasing_by all_goals cppverify_decreasing + +The definition is the spec's body, with each condition that reaches a +recursive application a hypothesis there, ``if _h : c`` (a ``&&``, ``||``, +or bounded ``cppverify::exists`` whose later part applies the recursion +becomes such an ``if``), so that Lean can prove the decrease from it. Its +measure is its ``cppverify::decreases``, each ``m`` as ``(m + 1).toNat`` and +lexicographic over several: exactly the relation cpp-verify's termination +check proves, where a call's measure may be -1 below a caller's 0. Specs +that apply each other are one ``mutual`` block. The body is never guarded by +the measure as a whole, so the definition has the spec's value at every +argument. + +Lean proves each decrease with ``cppverify_decreasing``, a prelude tactic: +``omega``, after unfolding the comparison and collection wrappers, or the +division and remainder of a measure that falls by a constant divisor +(``log2(n / 2)``), then ``simp_all`` and Lean's own ``decreasing_tactic``. + +The export tries the definitions with the pinned Lean. One that Lean rejects +stays opaque, as when the decrease rests on another spec's postcondition, +and one that applies it is tried again against that opaque declaration. +Lean's verdict on each is kept in ``.cppverify/specs``, so a later export +tries nothing; without Lean every spec is opaque. + +The goals are the same either way, since they state the same definition +instances. With the definition, ``cppverify_auto`` evaluates ``tri(4)`` +(``cppverify_auto_eval``, below), and a proof may unfold ``tri`` or argue by +induction over its recursion, with the principle Lean generates for it: + +.. code-block:: lean4 + + theorem tri_nonneg (m : Int) : 0 ≤ cppSpec_fn_5f5a3374726969 m := by + induction m using cppSpec_fn_5f5a3374726969.induct with + | case1 x h => rw [cppSpec_fn_5f5a3374726969]; simp [h] + | case2 x h ih => rw [cppSpec_fn_5f5a3374726969]; simp [h]; omega + + theorem cppverify_tri_nonneg_42a030_postcondition_053b1980_proof : + cppverify_tri_nonneg_42a030_postcondition_053b1980 := by + apply cppverify_tri_nonneg_42a030_postcondition_053b1980.of_readable + intro _ _ n _ _ _ + exact tri_nonneg _ + +With that proof, ``--lean-certify`` prints ``Certified`` for ``tri``, +``tri_nonneg``, and ``tri_four``. A verdict still rests on the termination +cpp-verify itself establishes: a spec whose own check is unresolved leaves +the goals that rely on it ``spec.termination``, whatever Lean defines. + +Collections in Lean +~~~~~~~~~~~~~~~~~~~ + +The spec collections of ```` reach Lean as values of core Lean +types, and each operation is a function of the generated prelude, total as +```` defines it: + +.. list-table:: + :header-rows: 1 + + * - C++ + - Lean + - Operations + * - ``seq`` + - ``List Int`` + - ``cppSeqEmpty``, ``cppSeqUnit``, ``cppSeqLength``, ``cppSeqAt`` (0 + outside the sequence), ``cppSeqPush``, ``cppSeqConcat``, + ``cppSeqSubrange`` (bounds clamped), ``cppSeqContains`` + * - ``set`` + - ``Int → Bool``, its membership test + - ``cppSetEmpty``, ``cppSetInsert``, ``cppSetRemove``, + ``cppSetContains``, ``cppSetUnion``, ``cppSetIntersect``, + ``cppSetDifference``, ``cppSetSubset`` + * - ``multiset`` + - ``Int → Nat``, its counts + - ``cppMultisetEmpty``, ``cppMultisetInsert``, ``cppMultisetRemove``, + ``cppMultisetCount`` + * - ``map`` + - ``Int → Option Int``, the value at each key it holds + - ``cppMapEmpty``, ``cppMapInsert``, ``cppMapRemove``, + ``cppMapContains``, ``cppMapGet`` (0 outside the domain) + +A set is its membership test, not a finite set, since a set of +```` may hold infinitely many integers; ``decide`` still +evaluates a membership of a set built from constants, as it evaluates a read +of a list. ``update`` and ``reverse`` are specs over these operations, as for +the solvers. + +The prelude also states what each operation means, in lemmas that ``simp`` +and ``grind`` use: ``cppSeqAt_push`` (``s.push(x)[i]`` is ``x`` at +``s.len()`` and ``s[i]`` elsewhere), ``cppSeqAt_concat``, +``cppSeqAt_subrange``, ``cppSeqLength_push``, ``cppSeqContains_push``, +``cppSeqSubrange_push`` (the subrange that drops a pushed element is the +sequence), ``cppSetContains_insert``, ``cppMultisetCount_remove``, +``cppMapGet_insert``, and the others for each operation. Two collections are +equal when they agree everywhere: ``cppSeq_ext`` (equal lengths and reads), +``cppSet_ext``, ``cppMultiset_ext``, and ``cppMap_ext``. For this file: + +.. cppverify-example: flags --backend=lean --lean-project={dir}/proof + +.. code-block:: cpp + + using cppverify::seq; + + cppverify::spec int total(seq s) + cppverify::decreases(s.len()) + { + return s.len() <= 0 ? 0 : total(s.subrange(0, s.len() - 1)) + s[s.len() - 1]; + } + + cppverify::proof void last(seq s, int x) + { + cppverify::check(s.push(x)[s.len()] == x); + cppverify::check(s.push(x).subrange(0, s.len()) == s); + } + + cppverify::proof void total_push(seq s, int x) + cppverify::post(total(s.push(x)) == total(s) + x) + { + } + +``cpp-verify --backend=lean --lean-project=proof file.cpp`` prints: + +.. code-block:: text + + Exported: decreases: total (cppverify_auto proved 1 of 1 goals) + Exported: lean obligation: last (cppverify_auto proved 3 of 3 goals) + Exported: lean obligation: total_push (cppverify_auto proved 2 of 2 goals) + +The postcondition of ``total_push`` needs the definition of ``total`` at +``s.push(x)``, which its goal states as the hypothesis +``cppverify_spec_axiom_1_1``; ``cppverify_auto`` unfolds it +(``cppverify_auto_unfold``, below), and the lemmas about ``push`` and +``subrange`` finish it. A proof by hand uses the same lemmas: + +.. code-block:: lean4 + + theorem cppverify_total_push_cdfd2d_postcondition_3a9fac6f_proof : + cppverify_total_push_cdfd2d_postcondition_3a9fac6f := by + apply cppverify_total_push_cdfd2d_postcondition_3a9fac6f.of_readable + intro _ _ s x pushed _ _ _ + rw [pushed] + unfold cppSpecBody_cdfd2da1_fn_5f5a35746f74616c4e396370707665726966793373657145_1 + have := cppSeqLength_nonneg s + simp [BitVec.toInt_signExtend_of_le] + omega + +Either way, ``--lean-certify`` prints ``Certified`` for ``total``, ``last``, +and ``total_push``. ``total`` is a definition (`Spec functions in Lean`_), so +a goal that needs induction over it, as ``total(s + t) == total(s) + +total(t)`` does, takes a proof by induction over ``total``'s recursion. + Proofs cppverify_auto finds ~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -471,9 +660,10 @@ A goal it proves gets that proof, with a header that says so: .. code-block:: lean4 - automation: cppverify_auto 1 proves it with cppverify_auto_grind + automation: cppverify_auto 3 proves it with cppverify_auto_grind cppverify_auto proves this goal. cpp-verify rewrites this file only while it is unedited; a proof you write here is yours, kept as any other. -/ + import CppVerify.Goals.cppverify_next_e1e917 import CppVerify.User import CppVerify.Auto @@ -483,7 +673,7 @@ A goal it proves gets that proof, with a header that says so: cppverify_auto_grind Any other goal gets a stub, whose header says it was tried -(``automation: cppverify_auto 1 did not prove it``). Here those are the two +(``automation: cppverify_auto 3 did not prove it``). Here those are the two goals of ``square`` that need ``x * x`` bounded: nonlinear arithmetic, which core Lean does not decide. Certification checks the automatic proofs like any other, so ``--lean-certify`` prints ``Certified: next [backend=Lean]``, and @@ -499,7 +689,21 @@ first that proves the goal: - ``cppverify_auto_bv``: machine comparisons, constants, and overflow conditions are stated as facts about integers, then ``grind``; - ``cppverify_auto_decide``: ``decide``; -- ``cppverify_auto_simp``: ``simp_all``. +- ``cppverify_auto_simp``: ``simp_all``; +- ``cppverify_auto_bveq``: equalities of machine values, such as the + precondition ``x != y`` of two keys, and sign extensions are stated as + facts about integers too, then as ``cppverify_auto_bv``; +- ``cppverify_auto_ext``: an equality of two collections, element by + element (`Collections in Lean`_), then as ``cppverify_auto_bv``; +- ``cppverify_auto_unfold``: each definition instance the goal states, by + the body it names, then as ``cppverify_auto_bveq``; +- ``cppverify_auto_eval``: the spec functions that are Lean definitions + (`Spec functions in Lean`_), by their equations, and the division and + remainder of contracts and specs by their definitions, so that an + application at known arguments becomes its value; +- ``cppverify_auto_div``: the division and remainder of contracts and specs + by their definitions, then ``grind``, which decides them by a constant + divisor once their signs are split (``a / 2 >= 2`` for ``a >= 4``). A step counts only when it proves the goal with Lean's foundations alone, so an unfinished lemma of yours (proved by ``sorry``) never proves a goal, and a @@ -507,13 +711,15 @@ goal counts as proved only when the kernel accepted its proof. A goal it spends more than 20 seconds on, its kernel check included, gets a stub (``did not prove it within 20 s``; ``--lean-auto-timeout`` sets the limit). The steps and their order were chosen by trying candidates on every goal the -test suite exports: of the goals Z3 proves, ``cppverify_auto`` proves 90%; +test suite exports: of the goals Z3 proves, ``cppverify_auto`` proves 93%; most of the rest need nonlinear arithmetic, induction over a spec, or a quantified frame. A goal is tried once: a later export tries a stub again only if a later -release of cpp-verify brings a new revision of ``cppverify_auto`` (the ``1`` -in the header), and never once you edit it. You can help it: a lemma in +release of cpp-verify brings a new revision of ``cppverify_auto`` (the ``3`` +in the header), and never once you edit it. Revisions 2 and 3 added the last +five steps, after the others, so that a goal an earlier step proves keeps its +proof; a stub that an earlier revision wrote is tried again. You can help it: a lemma in ``User.lean`` tagged ``@[grind]`` or ``@[simp]`` is used by its steps, since the proof files import ``User.lean``; delete a stub to have it tried again. Your own proofs may use ``cppverify_auto``, any of its steps, and the parts @@ -572,6 +778,103 @@ that cpp-verify 0.1 wrote for fn_5f5a3373697876::postcondition@8:37 is now CppVerify/Proofs/cppverify_six_6a2cf3/cppverify_six_6a2cf3_postcondition_198bc076.lean``. A 0.1 proof of a goal the source no longer has is kept in ``Stale/``. +One module of goals per function +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Each function's goals have a Lean module of their own, so that a change to +one function builds again only what depends on it. For this file: + +.. cppverify-example: flags --backend=lean --lean-project={dir}/proof + +.. code-block:: cpp + + cppverify::spec int tri(int n) + cppverify::decreases(n) + { + return n <= 0 ? 0 : tri(n - 1) + n; + } + + int inc(int x) + cppverify::pre(0 <= x && x < 1000) + cppverify::post(cppverify::result == x + 1) + { + return x + 1; + } + + int tri_zero() + cppverify::post(cppverify::result == tri(0)) + { + return 0; + } + +``cpp-verify --backend=lean --lean-project=proof file.cpp`` prints: + +.. code-block:: text + + Exported: decreases: tri (cppverify_auto proved 1 of 1 goals) + Exported: lean obligation: inc (cppverify_auto proved 3 of 3 goals) + Exported: lean obligation: tri_zero (cppverify_auto proved 2 of 2 goals) + +and writes: + +.. code-block:: text + + proof/ + lakefile.toml + lean-toolchain + CppVerify.lean the library's root, which imports Check + CppVerify/ + Prelude.lean the heap model, the comparisons, the bridge lemmas + Specs.lean each spec the goals apply, declared once + Goals/ + cppverify_tri_decreases_f55d4c.lean + cppverify_inc_c0810e.lean + cppverify_tri_zero_e086e9.lean + Generated.lean imports every goal module + Auto.lean cppverify_auto + User.lean your lemmas, never rewritten + Proofs/ + cppverify_inc_c0810e/ + cppverify_inc_c0810e_postcondition_e4ef4574.lean + ... + Check.lean imports every proof + +``Specs.lean`` declares each spec function the goals apply once, ``tri`` +here, by its definition (`Spec functions in Lean`_). Each goal module imports +it and defines the bodies its goals unfold under its own prefix, as in +``cppSpecBody_e086e9ab_fn_5f5a3374726969_1``, so any goal modules can be +imported together. A proof imports its function's goals, your lemmas, and +the automation: + +.. code-block:: lean4 + + import CppVerify.Goals.cppverify_inc_c0810e + import CppVerify.User + import CppVerify.Auto + +A new ``User.lean`` imports ``CppVerify.Specs``, so a lemma there may speak +of the specs and of the prelude; a lemma about one function's goals belongs +in a module of yours that imports that function's goals. A ``User.lean`` of +an earlier release imports ``CppVerify.Generated``, which still imports every +goal module: its proofs keep working, but each then depends on every goal. + +A generated file is written only when its text changes, so exporting an +unchanged source writes nothing, and ``lake build`` or your editor builds +again only what a change reaches. Certification builds the generated +modules, ``User.lean``, and ``Auto.lean`` with Lake, then compiles each proof +file with admissions promoted to errors, unless nothing it is built from +changed since it last passed: its text and the compiled modules of the +project it imports. After a change to the postcondition of ``inc``, it +compiles again the goal module of ``inc``, ``Generated.lean``, and the three +proofs of ``inc``, and none of the others. + +A run writes the goal module of each function it exports, and removes any +other: a function you delete takes its module with it, and so does a +function that a ``--lean-fallback`` run leaves to its solver, since +``Specs.lean`` then declares only what the exported functions apply. The +proofs of such a function stay where they are, and build again once its +goals are exported again. + What certification checks ~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -582,11 +885,17 @@ user's source. For each goal: - the kernel replays every declaration of every module of the project the proof imports, as ``leanchecker`` does, so nothing escaped the kernel; only - the pinned toolchain's own modules are trusted; + the pinned toolchain's own modules are trusted, and they are imported once + for all the goals, however many of their proofs import ``Lean``; +- no module may declare a name that an earlier one declares otherwise, and + the goal modules come first, so a proof file that defines a goal of its + own under the goal's name is rejected; - the proof ``G_proof`` must be a theorem whose type is exactly the goal - ``G`` that ``CppVerify.Generated`` defines; + ``G`` that its function's goal module defines; - the axioms it depends on, collected from the constants it uses, must be - among ``propext``, ``Quot.sound``, and ``Classical.choice``. + among ``propext``, ``Quot.sound``, and ``Classical.choice``; +- no declaration of ``User.lean`` may use ``sorry``: an admitted lemma there + fails every goal. Each function is certified on its own goals. For this file, where ``one`` claims a false postcondition: @@ -629,8 +938,11 @@ for the rest, gives: A theorem of the goal added by a command with ``debug.skipKernelTC``, which skips the kernel, is rejected at its replay (``the kernel rejects CppVerify.Lemmas: while replaying declaration 'cheat': (kernel) declaration -type mismatch``), and a user axiom behind a lemma by its name (``depends on -the axiom escape, which is not one of Lean's foundations``). +type mismatch``), a proof file that defines a goal of its own under the +goal's name at its replay too (``...cppverify_one_99bcee_postcondition_646d2761 declares +cppverify_one_99bcee_postcondition_646d2761, which +CppVerify.Goals.cppverify_one_99bcee declares``), and a user axiom behind a lemma by its name (``depends on the +axiom escape, which is not one of Lean's foundations``). Portable obligation archives ---------------------------- diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 1dcaa09ded..383e32a315 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -426,8 +426,7 @@ Current proof-language limitations include: sharing ``cppverify::decreases`` clauses of one length); otherwise they are ``proof.cycle``; - spec collections hold mathematical integers only (no nested collections or - records), and Lean does not support them yet (planned for a future - release); + records); - user-written loop invariants, with no candidate-invariant/Houdini pass; - no automatic termination-measure or lemma discovery. Inductions over a goal are tried automatically (by the measure of a recursive spec it applies, with @@ -580,9 +579,10 @@ goal per ordered obligation. Generated files are separated from preserved user lemmas/proofs. The pinned admission-free kernel path reports ``Certified`` only after every active proof checks and rejects user axiom/opaque shortcuts. Memory checks are lowered on this path as well as on Z3/cvc5/portfolio/BMC. -Spec collections are not yet supported on Lean (``logic.unsupported``); Lean -support for them is planned for a future release, and Z3 and cvc5 decide them -today. +Spec collections are Lean values of core types (a sequence a ``List Int``, a +set its membership test, a multiset its counts, a map the value at each key), +with a lemma for each operation; a goal over them that needs induction, as +over a recursive spec of a sequence, takes a proof by hand. Automation, proof ergonomics, semantic simplification, dependency-aware caching, and broader future C++ theories remain incomplete. diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index a7082dc386..9b46373167 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -286,7 +286,13 @@ Backends output uses one shared preamble and identity-qualified theorem names. * - ``--lean-project=DIR`` - With ``--backend=lean``, which it selects, generate a pinned editable project. Generated - semantics live in ``CppVerify/Generated.lean``; reusable lemmas and + semantics live in a module per function, ``CppVerify/Goals/.lean``, + with each spec they apply declared once in ``CppVerify/Specs.lean``: by + its definition when the pinned Lean proves that it terminates, the + verdict kept in ``.cppverify/specs``, and opaque otherwise; a + proof imports its function's module, so certification compiles again + only the proofs of a function whose goals changed, and a generated + file is written only when its text changes. Reusable lemmas and per-obligation proof files are preserved across regeneration. A goal is named by its function and the hash of its statement (``cppverify_one_99bcee_postcondition_cd6bdfcd``), and its proof file, @@ -361,7 +367,7 @@ Backends - Milliseconds of wall-clock time ``cppverify_auto`` may spend on one new goal, its kernel check included (default 20000; ``0`` disables). A goal that takes longer gets a stub, as in ``automation: - cppverify_auto 1 did not prove it within 20 s``. Requires + cppverify_auto 3 did not prove it within 20 s``. Requires ``--lean-project`` or ``--lean-fallback``. * - ``--unroll=N`` - Maximum BMC loop bound, which selects ``--backend=bmc``. Source verification diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index 42ebaaa422..7f0115d48a 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -106,8 +106,8 @@ a false postcondition, and so did a theorem of the goal added by a command with ``debug.skipKernelTC`` and checked by no kernel, in the proof file or in a module it imports. Certification now checks the compiled modules with a program that elaborates none of the user's source: the kernel replays every -module of the project a proof imports, the proof's type must be exactly its -goal, and its axioms are collected from the constants it uses. A failing +module of the project a proof imports, into one environment with the +toolchain's modules imported once, the proof's type must be exactly its goal, and its axioms are collected from the constants it uses. A failing proof also no longer fails every function of the project: each function is certified on its own goals (:doc:`book/part-ii/ch17-backends-modular-calls`). @@ -385,6 +385,50 @@ proofs side by side and checks them in one Lean environment: the 33 goals of one test took 204 s and now take 12 s (:doc:`book/part-ii/ch17-backends-modular-calls`). +**A Lean module per function.** A Lean project kept every goal of every +function in ``CppVerify/Generated.lean``, which every proof imported, so a +change to one function built every proof again, and certification compiled +every proof on every run. Each function's goals now have a module of their +own, ``CppVerify/Goals/.lean``, the specs they apply are declared +once, in ``CppVerify/Specs.lean``, and a proof imports its function's goals, +``User``, and ``Auto``. A generated file is written only when its text +changes, and certification compiles a proof again only when it or a module +it imports changed: after a change to one of five functions, it compiles +that function's three proofs. ``lake build``, which failed for want of the +library's root module, builds every proof. A ``User.lean`` that 0.1 wrote, +which imports ``CppVerify.Generated``, keeps working +(:doc:`book/part-ii/ch17-backends-modular-calls`). + +**Collections in Lean.** A function whose obligations use a ``seq``, ``set``, +``multiset``, or ``map`` was ``Unresolved`` with reason ``logic.unsupported`` +under ``--backend=lean`` and ``--lean-fallback``. They are now Lean values of +core types: a sequence is a ``List Int``, a set its membership test +(``Int → Bool``, since a set may be infinite), a multiset its counts, and a +map the value at each key it holds. Each operation is a function of the +generated prelude with the total meaning of ````, and lemmas +state what each means for ``simp``, ``grind``, and proofs by hand. +``cppverify_auto`` revision 2 adds three steps after the others: machine +equalities as integer facts, collection equality element by element, and the +definition instances a goal states, by the bodies they name. Of the 112 goals +over collections in the test suite that Z3 proves, it proves 104, and +revision 1 86; most of the rest need induction over a recursive spec. Of +every goal the suite exports that Z3 proves, it proves 93.3%, where revision 1 +proves 90.4%, and none fewer. Stubs that revision 1 wrote are tried again +(:doc:`book/part-ii/ch17-backends-modular-calls`). + +**Spec functions as Lean definitions.** Every spec function of a Lean project +was opaque, known to a goal only through the definition instances it states, +so a goal that needed a spec at another argument, or induction over it, could +not be proved. A spec is now a Lean definition when the pinned Lean proves +that it terminates by its ``cppverify::decreases`` measures, with exactly the +spec's value at every argument, and stays opaque otherwise. A proof may unfold +it or argue by induction over its recursion, and ``cppverify_auto`` revision 3 +evaluates its applications at known arguments. Revision 3 also reads the +division and remainder of contracts and specs by their definitions, which +proves goals such as ``a / 2 >= 2`` for ``a >= 4``. Lean's verdict on each +spec is kept in the project, so a later export tries nothing +(:doc:`book/part-ii/ch17-backends-modular-calls`). + **Lean 4.35.0.** Lean projects pin ``leanprover/lean4:v4.35.0``. A project 0.1 generated, pinned to ``v4.32.2``, moves to the new pin the next time cpp-verify writes it, with a warning; a proof that no longer builds needs updating for that