diff --git a/CMakeLists.txt b/CMakeLists.txt index e07b2e5..65bc82a 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -57,6 +57,7 @@ add_executable(crabber src/crabir_builder.cpp src/analyzer.cpp src/json_export.cpp + src/lean_verify.cpp src/domains/boxes_domain.cpp src/domains/dis_interval_domain.cpp src/domains/interval_domain.cpp @@ -68,6 +69,44 @@ add_executable(crabber src/domains/zones_domain.cpp ) target_link_libraries(crabber PRIVATE ${CRAB_LIBS}) + +# --verify-with-lean: after the analysis, ask the Lean development in lean/ to +# prove the exported invariants sound. +# +# Configure-time rather than a runtime flag, for two reasons. It means the +# option exists only in a build that can actually honour it -- in particular the +# wasm build, which has no toolchain to call, does not carry code for a +# capability a browser cannot have. And it removes any need to discover lake or +# the project directory at run time. +set(LAKE_EXECUTABLE "" CACHE FILEPATH + "Path to lake. Enables crabber's --verify-with-lean option.") + +if (LAKE_EXECUTABLE) + if (NOT EXISTS "${LAKE_EXECUTABLE}") + message(FATAL_ERROR "LAKE_EXECUTABLE does not exist: ${LAKE_EXECUTABLE}") + endif() + + # Build the Lean library as part of the normal build. Knowing where lake lives + # is not the same as the library having been built, and a crabber that can + # find lake but meets missing .olean files reports a confusing failure that + # looks nothing like a proof not going through. + add_custom_target(lean_library ALL + COMMAND "${LAKE_EXECUTABLE}" build + WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}/lean" + COMMENT "Building the Lean verification library") + add_dependencies(crabber lean_library) + + target_compile_definitions(crabber PRIVATE + CRABBER_WITH_LEAN=1 + CRABBER_LAKE="${LAKE_EXECUTABLE}" + CRABBER_LEAN_PROJECT="${CMAKE_CURRENT_SOURCE_DIR}/lean") + + message(STATUS "Lean verification enabled: ${LAKE_EXECUTABLE}") +else () + message(STATUS "Lean verification disabled " + "(set -DLAKE_EXECUTABLE=$(which lake) to enable)") +endif() + install(TARGETS crabber DESTINATION bin) install(DIRECTORY include/crabber DESTINATION include) diff --git a/README.md b/README.md index 7fc6d1d..7ca0bac 100644 --- a/README.md +++ b/README.md @@ -279,3 +279,139 @@ TestResult run_program(std::istream &is, ``` +# Verifying the analysis with Lean # + +Abstract interpretation is sound *by construction*: the theory guarantees that +the computed invariants over-approximate the reachable states — provided the +domains, their transfer functions, and the fixpoint engine are implemented +correctly. That proviso carries most of the weight. An abstract domain is +thousands of lines of C++, and a bug in a join, a widening, or a single transfer +function yields an invariant that is unsound while looking entirely ordinary. +Soundness in theory says nothing about *this* run of *this* implementation. + +`--verify-with-lean` checks that run. Crabber exports the analyzed CFG together +with the inferred invariants as JSON, and a Lean 4 development in +[`lean/`](lean/) reads that document and tries to prove the results sound — so +an implementation bug surfaces as a failed proof rather than as a wrong answer +nobody notices. + +``` bash +crabber samples/test-1.crabir -d int --verify-with-lean +``` + +``` +### LEAN VERIFICATION ### +could not verify foo : omega could not prove the goal: +proved bar : invariants sound, all assertions proved +``` + +Enabled at configure time: + +``` bash +cmake -DLAKE_EXECUTABLE=$(which lake) ../ +``` + +## What "proved" means ## + +For that CFG, Lean's kernel has accepted a proof of two things: + +- every state the program can reach at a block satisfies the invariant Crab + printed for that block, under the concrete semantics of CrabIR; +- no execution can reach an assertion whose condition is false. + +Crucially, **nothing about Crab is modelled**. The fixpoint engine, widening, +and the abstract domains are not formalized — only Crab's *output* is checked, +per program. That is what makes the result independent of which domain produced +it, and what keeps the proof effort bounded. + +## Which CFGs are checked ## + +A file may hold several CFGs, and only the **roots of the call graph** — those +nothing calls — are checked. A CFG that is called is reported as `not checked` +rather than passed over silently. + +The reason is that a callee's invariants are not properties of the callee. Crab's +top-down inter-procedural analysis derives them from the call sites, so in + +``` +main() { ... inc(7) ... } inc(a) { ... } +``` + +Crab may infer `a >= 5` at `inc`'s entry — true only because of how `main` calls +it. The theorem Lean proves quantifies over *every* initial state, which is a +strictly stronger claim than Crab made. Checking `inc` in isolation would ask a +question Crab never answered, and fail for a reason that says nothing about the +analysis. + +Verifying the conditional claim Crab actually made needs the calling context +modelled, which is future work. Until then the check stays where the two +questions coincide. + +## Which statements are modelled ## + +The Lean semantics covers the integer core and the whole boolean fragment: + +| Modelled | | +|---|---| +| `assign`, `havoc`, `assume`, `assert` | Integers are unbounded `Int`, not machine words — measured against the analyser, `x:i8 := 127; x := x+1` yields 128. An `assert` is check-then-assume. | +| `bool_assign_cst`, `bool_assign_var`, `bool_binop`, `bool_assume`, `bool_assert`, `bool_select` | Booleans live in their own store, as `Bool` rather than as 0/1 integers. Crab exports boolean facts as `b = 1`; the reader turns those back into boolean claims. | + +| Not modelled — refused by name, so a CFG using one is reported `not attempted` | | +|---|---| +| `binop`, `select`, `cast` | Multiplication and division of variables are outside what `omega` decides, and Crab's four division operators differ in rounding. `cast` is why `samples/test-6.crabir` cannot be checked despite being a boolean program; `samples/test-bool-1.crabir` is the cast-free equivalent. | +| `callsite` | Needs a call rule and the interprocedural summaries — see above. | +| the four array statements, and the reference/region family | Need select/store reasoning in the assertion language. | + +Nothing is ever silently skipped: dropping a statement would weaken every proof +obligation in its block, so an unmodelled construct fails the read and names +itself in the report. + +## What is trusted, and what is not ## + +The point of the exercise is that the list of trusted things is short and +explicit. + +| Trusted — a bug here could certify a false invariant | | +|---|---| +| The Lean model of CrabIR's semantics | The substantive one. It *is* the claim about what a CrabIR program means; nothing can prove it right. | +| The exporter | Crab's rendering of an abstract state as linear constraints, and crabber's JSON around it. | +| The JSON reader on the Lean side | Mitigated: it writes what it read back out and compares against the input, so a dropped statement or misread coefficient is reported rather than believed. | +| Crabber's own report | Printing "proved" only says crabber ran Lean and Lean agreed. To rely on it, run `lake build` in `lean/` yourself. | + +| Not trusted — proved, or checked by the kernel | | +|---|---| +| The verification conditions and the weakest-precondition calculus | Proved sound once, for all programs. | +| The soundness meta-theorem and assertion safety | Proved once. | +| Every per-program proof | Found by tactics, then checked by Lean's kernel. A tactic can fail to find a proof; it cannot produce a wrong one. | + +## Reading a negative result ## + +`could not verify` is a statement about the proof attempt, **not** about Crab. +It may mean the invariant is genuinely not inductive — or only that the proof +search was too weak, or that the program contains an assertion Crab itself could +not establish. The check is sound but incomplete, and its output is worded to +keep that distinction visible. + +When the arithmetic is what ran out, the report also shows the assignment it +could not rule out, in the program's own variables: + +``` +could not verify octagons : omega could not prove the goal + cannot rule out : 101 ≤ y ≤ 200 +``` + +That is **not** a counterexample to the invariant — the state may well be +unreachable. It says where the reasoning stopped, which is usually the quickest +way to see whether a fact is missing or the invariant is genuinely too weak. + +To investigate further, keep the intermediate files and ask for Lean's full +output: + +``` bash +crabber samples/test-2.crabir --verify-with-lean --lean-keep-temp --lean-show-output +``` + +This reports the exported JSON, the generated Lean file, and the exact command +that re-runs it. That file is all Lean was given, so it can be opened in an +editor, its tactics taken apart, and the failing goal inspected directly. + diff --git a/include/crabber/lean_verify.hpp b/include/crabber/lean_verify.hpp new file mode 100644 index 0000000..5e3c5b6 --- /dev/null +++ b/include/crabber/lean_verify.hpp @@ -0,0 +1,135 @@ +#pragma once +/** + * Ask the Lean development to prove the exported invariants sound. + * + * `--print-invariants-to-json` writes a document holding the analyzed CFG and, + * for every block, the invariant Crab inferred for it. That document is the + * only thing that crosses between the two sides: this code writes it, Lean + * reads it, and nothing about the program travels any other way. + * + * What happens per CFG is that a two-line Lean file is written, + * + * crab_program "" cfg "" + * crab_verify + * + * and checked with `lake env lean`. The first line reads the document while the + * file is being elaborated and installs the program and the invariants as Lean + * data; the second generates the proof obligations and discharges them. Success + * means Lean's kernel accepted a proof that every reachable state satisfies the + * invariant Crab printed for its block, and that no assertion can fail. + * + * What this does *not* do is make crabber's report trustworthy on its own. + * Printing "proved" only says Lean was run and agreed; a bug here could print + * it without running anything. The claim rests on the Lean development, and + * anyone who wants to rely on it should run `lake build` themselves. + * + * Nor is a failure evidence that Crab is wrong. Lean's arithmetic may simply be + * too weak, the program may use constructs the Lean semantics does not model, + * or an assertion may be one Crab itself could not prove. The verdicts below + * keep those apart, and the wording of each is chosen so that a negative result + * never reads as a claim about Crab. + * + * Available only when the build was configured with a path to `lake` (see + * `LAKE_EXECUTABLE` in CMakeLists.txt). Without it `leanAvailable()` is false + * and the option reports how to enable it. + */ + +#include +#include + +namespace crabber { + +class CrabIrBuilder; + +struct LeanVerifyOpts { + /** Run the check after the analysis. */ + bool enabled = false; + /** + * Elaboration budget, as Lean heartbeats rather than seconds. + * + * A wall-clock timeout would make the outcome depend on how loaded the + * machine is, so the same program could verify on one run and "fail" on the + * next. Heartbeats are deterministic, and exhausting them is reported by Lean + * as an ordinary diagnostic, which is why `Exhausted` can be told apart from + * a proof that genuinely did not go through. + */ + unsigned heartbeats = 400000; + /** + * Keep the exported JSON and the generated Lean file, and report where they + * are. + * + * This is the whole debugging story for a CFG that does not go through. The + * two files are exactly what Lean saw, so re-running the printed command + * reproduces the failure with nothing in between -- and the Lean file can + * then be edited, its tactics taken apart, and the failing goal inspected in + * an editor. + */ + bool keep_temp = false; + /** Print Lean's complete output for a CFG that was not proved. */ + bool show_output = false; +}; + +enum class LeanVerdict { + /** Lean proved the invariants sound and every assertion unfailable. */ + Proved, + /** The program uses a construct the Lean semantics does not model. */ + OutOfScope, + /** Lean did not find a proof. Not a claim that Crab is wrong. */ + Unproved, + /** The elaboration budget ran out before Lean finished. */ + Exhausted, + /** + * Not a root of the call graph, so not checked. + * + * Reported rather than passed over in silence: a CFG present in the file and + * absent from the results would otherwise look like an oversight. + */ + Skipped, +}; + +struct LeanResult { + std::string cfg_name; + LeanVerdict verdict; + /** Lean's own first line of output, kept for the unproved cases. */ + std::string detail; + /** Everything Lean printed. Empty when it printed nothing. */ + std::string output; + /** + * The counterexample the arithmetic decision procedure reported, if it did, + * rewritten in terms of the program's own variables. + * + * Not a counterexample to the invariant: it describes an assignment the proof + * search could not rule out, which may well be unreachable. It is a pointer to + * where the reasoning ran out, and usually the fastest way to see whether the + * gap is a missing fact or a genuinely weak invariant. + */ + std::string counterexample; + /** Where the generated Lean file was left, when it was kept. */ + std::string lean_file; +}; + +/** Whether this build can call Lean at all. */ +bool leanAvailable(); + +/** The Lean development this build was configured against. */ +std::string leanProjectDir(); + +/** The command that re-runs one kept Lean file by hand. */ +std::string leanReproduceCommand(const std::string &leanFile); + +/** Why not, when it cannot -- suitable for showing to a user. */ +std::string leanUnavailableReason(); + +/** + * Check every CFG in `jsonPath`, which must be a document written by + * `--print-invariants-to-json`. One result per CFG, in the order the call graph + * gives them. + */ +std::vector verifyWithLean(const std::string &jsonPath, + const CrabIrBuilder &crabIR, + const LeanVerifyOpts &opts); + +/** One line describing a result, for the report. */ +std::string describe(const LeanResult &r); + +} // namespace crabber diff --git a/lean/.gitignore b/lean/.gitignore new file mode 100644 index 0000000..adc56b3 --- /dev/null +++ b/lean/.gitignore @@ -0,0 +1,10 @@ +# Lake build artifacts: .olean/.ilean/.c outputs, and any fetched dependencies +# under .lake/packages. Entirely regenerated by `lake build`. +/.lake/ + +# Scratch analyses, written here when sweeping crabber over the samples: +# crabber .crabir -d --print-invariants-to-json lean/exports/.json +# Regenerable, and committing them would only invite drift from the exporter. +# The one document a build actually needs is a fixture, and lives next to the +# sample that reads it, under CrabberJson/Samples/. +/exports/ \ No newline at end of file diff --git a/lean/CheckJson.lean b/lean/CheckJson.lean new file mode 100644 index 0000000..c54c7e9 --- /dev/null +++ b/lean/CheckJson.lean @@ -0,0 +1,86 @@ +import CrabberJson +/- +# `checkjson` — run the reader over exported documents + + lake exe checkjson out1.json out2.json … + +For each file: parse it, read it into the wire types, confirm that writing those +back out reproduces the input, and convert every cfg in it to the `Cfg` and +`Label → Assn` the proof library consumes. Reports one line per cfg and exits +non-zero if anything failed. + +This is how the reader is exercised against the whole sample suite without +writing a per-program Lean file for each. A program using constructs outside the +modelled fragment is *expected* to fail here, with the construct named; that is +the reader refusing to silently drop it. + +## This program proves nothing + +Worth stating plainly, because "check" is a word the proof side has a claim on. +Nothing here constructs a verification condition, runs a tactic, or produces a +theorem. `ok` means *this export can be read and converted* — it says nothing +about whether Crab's invariants are sound or its assertions hold. + +Where proving actually happens is `lake build`: the per-program files under +`CrabberJson/Samples/` are elaborated, `crab_vc` searches for the proofs, and +Lean's kernel checks them. That is the whole design — proofs are found and +checked offline, once per program, and no binary ever decides anything at run +time. (Building *this* executable does cause those proofs to be checked, since +it imports them, but that is a build dependency, not something it does when run.) + +The one future exception is the reflective checker sketched for the playground, +where a compiled Lean function would render a verdict in a browser. That would be +a different binary, and it would carry a soundness theorem of its own. +-/ + +open CrabberJson + +/-- Run the reader over one file. Returns whether it succeeded. + + With `dump`, also prints the converted program block by block, which is what + lets a generated file be compared against a hand transcription. -/ +def checkFile (path : System.FilePath) (dump : Bool) : IO Bool := do + let text ← IO.FS.readFile path + match Lean.Json.parse text >>= readChecked with + | .error e => + IO.println s!"FAIL {path}\n {e}" + return false + | .ok d => + let mut ok := true + -- One CFG at a time, each parsed and round-tripped on its own, so a CFG + -- the library cannot model is reported against itself rather than taking + -- its neighbours down with it. + for name in d.cfgNames do + match d.rawCfg name >>= cfgChecked >>= WCfg.toProgram with + | .error e => + IO.println s!"FAIL {path} [{name}]\n {e}" + ok := false + | .ok p => + let stmts := p.labels.foldl (fun n l => n + (p.cfg.body l).length) 0 + -- `analysis` is carried as raw JSON, so the domain is dug out here + -- rather than modelled; it is reporting, not something a proof needs. + let domain := (d.analysis.getObjValAs? String "domain").toOption.getD "?" + IO.println s!"ok {path} [{p.name}] \ + {p.labels.length} blocks, {stmts} statements, \ + entry {p.entry}, domain {domain}" + if dump then + for l in p.labels do + IO.println s!" {l}" + IO.println s!" body {repr (p.cfg.body l)}" + IO.println s!" succs {repr (p.cfg.succ l)}" + IO.println s!" inv {repr (p.inv l)}" + return ok + +def main (args : List String) : IO UInt32 := do + let dump := args.contains "--dump" + let files := args.filter (· != "--dump") + if files.isEmpty then + IO.println "usage: checkjson [--dump] …" + return 1 + let mut failures := 0 + for a in files do + unless ← checkFile ⟨a⟩ dump do + failures := failures + 1 + IO.println s!"\n{files.length - failures} of {files.length} documents read and \ + round-tripped; {failures} failed" + return if failures == 0 then 0 else 1 diff --git a/lean/Crabber.lean b/lean/Crabber.lean new file mode 100644 index 0000000..59d8877 --- /dev/null +++ b/lean/Crabber.lean @@ -0,0 +1,45 @@ +/- +# Crabber — proving Crab's invariants in Lean 4 + +Root module: importing `Crabber` pulls in the whole library. + +## What this library does + +Crab is an abstract interpreter for CrabIR. For a given program it computes an +invariant for every basic block. This library checks that output: given the +program and the invariants as data, it produces a machine-checked proof that +they really are invariants — every state the program can reach at a block +satisfies the invariant claimed there — and that assertions Crab reported as +safe can never fail. + +It does **not** model Crab itself. No fixpoint engine, no widening, no abstract +domain is formalised here. That is what keeps the job tractable, and it means +the proof is indifferent to which domain produced the invariants. + +## Reading order + + Syntax — CrabIR programs as data + State — concrete states; meaning of expressions } trusted + Semantics — Exec / Step / Reachable: what a program *does* } + Assn — invariants as data, and their meaning } trusted + WP — the weakest-precondition calculus + soundness } proved + VC — the per-block obligation + the adapter lemma } proved + Soundness — inductive_sound and assert_safe } proved + Tactic — `crab_vc`, the automation (untrusted) + Samples/* — one file per analysed program (data + theorems; these will be + machine generated from Crab's JSON export, hand-written for now) + +"Trusted" means a bug there could let us prove something false, because those +files *are* the claim about what CrabIR means. "Proved" means a bug there can +only make a true statement unprovable — the kernel rejects a bad proof. +-/ +import Crabber.Syntax +import Crabber.State +import Crabber.Assn +import Crabber.Semantics +import Crabber.WP +import Crabber.VC +import Crabber.Soundness +import Crabber.Tactic +import Crabber.Samples.Test1Bar +import Crabber.Samples.Test1Foo diff --git a/lean/Crabber/Assn.lean b/lean/Crabber/Assn.lean new file mode 100644 index 0000000..80e0831 --- /dev/null +++ b/lean/Crabber/Assn.lean @@ -0,0 +1,106 @@ +import Crabber.State +/- +# Crabber.Assn — invariants as data, and what they mean + +The assertion language is a **disjunction of conjunctions of linear +constraints** — exactly what every Crab abstract domain can export, via its +"convert to a disjunctive linear constraint system" operation. Keeping it as +*data* rather than as a Lean predicate matters for two reasons: it arrives from +a parser, and we want to print it back verbatim when a proof obligation fails. + +**Trusted.** The meaning function below is our claim about what Crab's exported +constraints mean. +-/ + +namespace Crabber + +/-! ## Atoms + +One conjunct of an exported invariant. Crab's disjuncts mix two kinds of claim, +and they are told apart by the `type` tag the export puts on every constraint. + +**Why booleans are their own atom rather than `1·b = 1`.** Crab writes boolean +facts as 0/1 linear constraints, so reading them as ordinary `LinCon`s over a +variable that happens to be boolean would typecheck and would even be +*consistent* — but it would commit the state to representing booleans as +integers, which `Syntax.lean` argues against at length. Measured across every +domain crabber offers, a bool-tagged constraint is only ever `1·b = 0` or +`1·b = 1`, so this atom is exactly as expressive as what Crab actually emits, and +the reader refuses any other bool-tagged shape by name rather than guessing. + +The payoff is on both sides of a goal: a boolean fact arrives as +`σ.bools "b" = true`, which `simp` consumes directly, and the integer half stays +free of `if … then 1 else 0` terms that `omega` would have to be walked past. -/ + +/-- One conjunct of an invariant. -/ +inductive Atom where + /-- An integer linear constraint. -/ + | lin (c : LinCon) + /-- `x` is `v` — the export's `1·x = 1` and `1·x = 0`, with `x` boolean. -/ + | bool (x : Var) (v : Bool) + deriving Repr + +/-- What an atom claims about a state. Each kind reads its own store, and only + its own store. -/ +def Atom.holds : Atom → State → Prop + | .lin c => fun σ => c.holds σ + | .bool x v => fun σ => σ.bools x = v + +/-- A conjunction of atoms: one "disjunct" in the export. -/ +abbrev Conj := List Atom + +/-- An invariant: a disjunction of conjunctions, read as "or of ands". -/ +abbrev Assn := List Conj + +/-- A conjunction holds when *every* atom in it holds. + + `∀ c ∈ k, …` is Lean's bounded quantifier, sugar for `∀ c, c ∈ k → …`. + Writing it this way rather than folding `∧` over the list is what makes the + degenerate cases below come out right with no special handling. -/ +def Conj.holds (k : Conj) (σ : State) : Prop := ∀ a ∈ k, a.holds σ + +/-- An invariant holds when *some* disjunct holds. -/ +def Assn.holds (A : Assn) (σ : State) : Prop := ∃ k ∈ A, Conj.holds k σ + +/-- Notation `⟦A⟧ σ` — "state σ satisfies invariant A". + + The bridge from invariant *data* to an actual proposition about a state. -/ +notation:max "⟦" A "⟧" => Assn.holds A + +/-! ## The two degenerate invariants + +Crab's JSON marks "everything" and "nothing" explicitly, because an empty list +is ambiguous on the wire. In Lean no such ambiguity exists — the list encoding +gives both, and each falls out of the definitions above with no special case. -/ + +/-- Bottom: the invariant of an unreachable block. Crab prints these rather than + omitting them, so that a block being unreachable is a claim we can check. + No disjuncts, so `∃ k ∈ [], …` is false. -/ +def Assn.bot : Assn := [] + +/-- Top: no information. One disjunct, itself empty, so `∃ k ∈ [[]], ∀ c ∈ [], …` + reduces to `∀ c ∈ [], …`, vacuously true. -/ +def Assn.top : Assn := [[]] + +/-- Bottom really is unsatisfiable. + + Stated so that the reasoning about unreachable blocks is a fact in Lean + rather than a comment: a block Crab marked unreachable gets `False` as its + invariant, so its own proof obligation holds vacuously and the burden shifts + to its *predecessors*, which must then show the block cannot be entered — + which is exactly the claim Crab is making there. -/ +theorem Assn.not_holds_bot (σ : State) : ¬ ⟦Assn.bot⟧ σ := by + -- `rintro` introduces the hypothesis and destructs it in one step: + -- a proof of `∃ k ∈ [], …` would have to supply a member of `[]`. + rintro ⟨k, hk, -⟩ + -- `simp at hk` reduces `k ∈ []` to `False`, closing the goal. + simp [Assn.bot] at hk + +/-- Top really is satisfied by every state. -/ +theorem Assn.holds_top (σ : State) : ⟦Assn.top⟧ σ := by + -- Provide the witness `[]` for the existential; the inner `∀ c ∈ []` is then + -- vacuous. `⟨_, _, _⟩` is anonymous-constructor notation: it builds the + -- ∃-proof from its parts. + exact ⟨[], by simp [Assn.top], by simp [Conj.holds]⟩ + +end Crabber diff --git a/lean/Crabber/Attr.lean b/lean/Crabber/Attr.lean new file mode 100644 index 0000000..4ff13ac --- /dev/null +++ b/lean/Crabber/Attr.lean @@ -0,0 +1,12 @@ +import Lean +/- +# Crabber.Attr — the `@[crab]` simp set + +Lean requires an attribute to be *registered* in a module that is imported by +the modules using it, so this one-line file exists on its own. + +`@[crab]` marks the per-program definitions (`prog`, `body`, `succ`, `inv`, …) +that `crab_vc` must unfold. Keeping them in a named simp set rather than the +default one means a generated program cannot perturb unrelated proofs. +-/ +register_simp_attr crab diff --git a/lean/Crabber/Samples/Test1Bar.lean b/lean/Crabber/Samples/Test1Bar.lean new file mode 100644 index 0000000..d23654a --- /dev/null +++ b/lean/Crabber/Samples/Test1Bar.lean @@ -0,0 +1,206 @@ +import Crabber.Soundness +import Crabber.Tactic +/- +# `samples/test-1.crabir`, cfg `bar`, under `-d int` + +This is the **per-program** artifact — the only part that will eventually be +machine generated, from the two JSON documents: + + crabber samples/test-1.crabir -d int --cfg-to-json - + crabber samples/test-1.crabir -d int --print-invariants-to-json - + +The source program is a counting loop: + + start: y := 0 goto loop + loop: y := y + 1 if (y <= 9) goto loop else goto out + out: assert(y == 10) + +Note the CFG below is the one **Crab analysed**, not the source text: the +conditional has been compiled into the two `edge-loop-*` blocks that carry the +guards. That is why the export walks the analyser's final graph — a +transcription of the source would not line up with the invariant labels. + +Everything here is data plus `by crab_vc`. There is no reasoning about `Step`, +`Reachable`, or induction anywhere in this file; all of that lives once in +`Crabber/Soundness.lean` and `Crabber/VC.lean`. +-/ + +namespace Crabber +namespace Test1Bar + +/-! ## The program (from `--cfg-to-json`) + +`@[crab]` puts each definition in the simp set `crab_vc` unfolds. -/ + +/-- `y ≥ k`, exported by Crab in normalised form as `-1·y ≤ -k`. -/ +@[crab] def yGeq (k : Int) : LinCon := { op := .le, terms := [(-1, "y")], const := -k } + +/-- `y ≤ k`, exported as `1·y ≤ k`. -/ +@[crab] def yLeq (k : Int) : LinCon := { op := .le, terms := [(1, "y")], const := k } + +/-- `y = 10` — the asserted condition in block `out`. -/ +@[crab] def yEq10 : LinCon := { op := .eq, terms := [(1, "y")], const := 10 } + +/-- Block bodies. The final `_ => []` is what makes this a *total* function, + as `Cfg` requires: every label naming no block gets an empty body. -/ +@[crab] def bodyOf : Label → List Stmt + | "start" => [.assign "y" { terms := [], const := 0 }] + | "loop" => [.assign "y" { terms := [(1, "y")], const := 1 }] + | "edge-loop-loop" => [.assume (yLeq 9)] + | "edge-loop-out" => [.assume (yGeq 10)] + | "out" => [.assert yEq10] + | _ => [] + +/-- Successor lists, likewise total. -/ +@[crab] def succOf : Label → List Label + | "start" => ["loop"] + | "loop" => ["edge-loop-loop", "edge-loop-out"] + | "edge-loop-loop" => ["loop"] + | "edge-loop-out" => ["out"] + | _ => [] + +/-- The CFG. -/ +@[crab] def prog : Cfg := { entry := "start", body := bodyOf, succ := succOf } + +/-! ## The invariants (from `--print-invariants-to-json`) + +Transcribed verbatim from the JSON. Crab's `int` domain found, for cfg `bar`: + +| block | exported constraints | i.e. | +|------------------|-------------------------------|-----------| +| `start` | `{"kind":"true"}` | ⊤ | +| `loop` | `-y ≤ 0`, `y ≤ 9` | 0 ≤ y ≤ 9 | +| `edge-loop-loop` | `-y ≤ -1`, `y ≤ 10` | 1 ≤ y ≤ 10| +| `edge-loop-out` | `-y ≤ -1`, `y ≤ 10` | 1 ≤ y ≤ 10| +| `out` | `-y ≤ -10`, `y ≤ 10` | y = 10 | +-/ + +/-- The annotation. Unknown labels get `Assn.bot`: they are unreachable, and + the lemma covering unnamed labels proves their obligation without looking + at the invariant at all. -/ +@[crab] def inv : Label → Assn + | "start" => Assn.top + | "loop" => [[.lin (yGeq 0), .lin (yLeq 9)]] + | "edge-loop-loop" => [[.lin (yGeq 1), .lin (yLeq 10)]] + | "edge-loop-out" => [[.lin (yGeq 1), .lin (yLeq 10)]] + | "out" => [[.lin (yGeq 10), .lin (yLeq 10)]] + | _ => Assn.bot + +/-! ## One verification condition per block + +Each `theorem` below has a *type* which is an instance of the `VC` schema, and +a *proof* which is one tactic call. Written out, the obligations are: + + start ∀ σ, True → 0 ≤ 0 ≤ 9 (after y := 0) + loop ∀ σ, 0 ≤ y ≤ 9 → 1 ≤ y+1 ≤ 10 (after y := y+1) + edge-loop-loop ∀ σ, 1 ≤ y ≤ 10 → (y ≤ 9 → 0 ≤ y ≤ 9) + edge-loop-out ∀ σ, 1 ≤ y ≤ 10 → (y ≥ 10 → 10 ≤ y ≤ 10) + out ∀ σ, 10 ≤ y ≤ 10 → (y = 10 ∧ True) + +`start` and `loop` are deterministic, so the weakest precondition is pure +substitution and no quantifier survives. The two edge blocks gain exactly one +arrow each, from their `assume`. `out` has no successors, so its postcondition +is `True` and all that remains is the assert's own obligation — an assert both +checks and filters, so it contributes a conjunct rather than an antecedent. -/ + +theorem vc_start : VC prog inv "start" := by crab_vc +theorem vc_loop : VC prog inv "loop" := by crab_vc +theorem vc_edge_loop_loop : VC prog inv "edge-loop-loop" := by crab_vc +theorem vc_edge_loop_out : VC prog inv "edge-loop-out" := by crab_vc +theorem vc_out : VC prog inv "out" := by crab_vc + +/-! ## Bundling the VCs + +`consecution_of_VC` wants `∀ B, VC prog inv B` — over *every* string. The five +theorems above cover the named blocks; `VC_of_unknown` covers all the rest at +once. The case analysis that joins them is mechanical, which is the point: it +is generated, not designed. -/ + +/-- Every label is one of the five blocks, or names no block at all. + + `by_cases h : B = "start"` splits on a decidable proposition, giving the + `h` branch and the `¬h` branch. In the final branch the five negated + equations sit in the context, and `simp` discharges the side conditions of + `bodyOf`'s and `succOf`'s catch-all equations from them automatically. -/ +theorem label_cases (B : Label) : + B = "start" ∨ B = "loop" ∨ B = "edge-loop-loop" ∨ B = "edge-loop-out" + ∨ B = "out" ∨ (prog.body B = [] ∧ prog.succ B = []) := by + by_cases h1 : B = "start"; · exact .inl h1 + by_cases h2 : B = "loop"; · exact .inr (.inl h2) + by_cases h3 : B = "edge-loop-loop"; · exact .inr (.inr (.inl h3)) + by_cases h4 : B = "edge-loop-out"; · exact .inr (.inr (.inr (.inl h4))) + by_cases h5 : B = "out"; · exact .inr (.inr (.inr (.inr (.inl h5)))) + exact .inr (.inr (.inr (.inr (.inr + ⟨by simp [prog, bodyOf], by simp [prog, succOf]⟩)))) + +/-- **Every** label's verification condition holds. + + `rcases … with rfl | rfl | …` destructs the disjunction, and each `rfl` + *substitutes* the equation — so in the first branch the goal literally + becomes `VC prog inv "start"`, which `vc_start` proves. -/ +theorem vc_all (B : Label) : VC prog inv B := by + rcases label_cases B with rfl | rfl | rfl | rfl | rfl | ⟨hb, hs⟩ + · exact vc_start + · exact vc_loop + · exact vc_edge_loop_loop + · exact vc_edge_loop_out + · exact vc_out + · exact VC_of_unknown _ _ _ hb hs + +/-! ## The entry obligation -/ + +/-- Every initial state satisfies the invariant at the entry block. + + Crab claims ⊤ at `start`, so this is immediate — but it is not vacuous in + general: a domain that inferred something at entry would have to justify it + against `InitState`. -/ +theorem initiation : ∀ σ : State, InitState prog σ → ⟦inv prog.entry⟧ σ := by + intro σ _ + exact Assn.holds_top σ + +/-! ## The assertion obligation -/ + +/-- At every statement in every block, the block's invariant implies that + statement's obligation after running the statements before it. + + **One line, and that is the point.** This used to be the longest proof in + the file: a case split over all six label cases, then — for each — an attempt + to refute the split `pre ++ s :: post` statement by statement, with only + block `out` surviving to say anything. + + None of that was necessary. `wpStmt` puts an assert's obligation into the + precondition as a conjunct, so it is already inside `VC prog inv "out"`, + which `vc_all` proved above; `chk_of_VC` is the general lemma that takes it + back out. The work is real, it just is not per-program. + + Kept as a named theorem rather than inlined into `bar_verified` because + `Walkthrough.lean` refers to it when pulling the chain apart, and because + naming it keeps the four premises of the argument visible in one file. -/ +theorem chk : ∀ (L : Label) (pre : List Stmt) (s : Stmt) (post : List Stmt), + prog.body L = pre ++ s :: post → + ∀ σ : State, ⟦inv L⟧ σ → wp pre (fun τ => s.obligation τ) σ := + chk_of_VC prog inv vc_all + +/-! ## The result -/ + +/-- **The theorem.** + + In English: *the invariants Crab inferred for cfg `bar` of + `samples/test-1.crabir` under `-d int` are genuine invariants of the + program, and the program's assertion can never fail.* + + Read the two halves as: + * `InvariantOf prog inv` — every state reachable at a block satisfies the + invariant Crab printed there; + * `¬ AssertFails prog` — no execution reaches `assert(y == 10)` with `y` + different from 10. Crab reported this assert **safe**; this is the + machine-checked confirmation. + + Trusted for this claim: the Lean semantics of CrabIR (`Semantics.lean` and + `State.lean`), the transcription of the program above, and Crab's invariant + export. Not trusted, because proved: everything else. -/ +theorem bar_verified : InvariantOf prog inv ∧ ¬ AssertFails prog := + verified prog inv initiation vc_all + +end Test1Bar +end Crabber diff --git a/lean/Crabber/Samples/Test1Foo.lean b/lean/Crabber/Samples/Test1Foo.lean new file mode 100644 index 0000000..16775b5 --- /dev/null +++ b/lean/Crabber/Samples/Test1Foo.lean @@ -0,0 +1,141 @@ +import Crabber.Soundness +import Crabber.Tactic +/- +# `samples/test-1.crabir`, cfg `foo`, under `-d int` — the *unsafe* companion + +`foo` is `bar` with the assertion negated: + + out: assert(x != 10) + +and the source marks it `EXPECT_EQ(false, …)` — Crab reports this assert as an +**error**, not as safe. Formalising it is the sharpest available check that +the development is not vacuous, because it separates the two halves of +`verified`: + + * the **invariants** are still perfectly sound — Crab's fixpoint is correct + about the reachable states — and we prove `InvariantOf` below exactly as + for `bar`; + * the **assertion obligation** is not merely hard, it is *false*, and we + prove its negation. Crab's verdict and Lean's agree. + +See `Test1Bar.lean` for the commentary on the shared structure; this file only +annotates what differs. +-/ + +namespace Crabber +namespace Test1Foo + +@[crab] def xGeq (k : Int) : LinCon := { op := .le, terms := [(-1, "x")], const := -k } +@[crab] def xLeq (k : Int) : LinCon := { op := .le, terms := [(1, "x")], const := k } + +/-- The asserted condition: `x != 10`. Note `op := .ne` — this is the only + structural difference from `bar`. -/ +@[crab] def xNe10 : LinCon := { op := .ne, terms := [(1, "x")], const := 10 } + +@[crab] def bodyOf : Label → List Stmt + | "start" => [.assign "x" { terms := [], const := 0 }] + | "loop" => [.assign "x" { terms := [(1, "x")], const := 1 }] + | "edge-loop-loop" => [.assume (xLeq 9)] + | "edge-loop-out" => [.assume (xGeq 10)] + | "out" => [.assert xNe10] + | _ => [] + +@[crab] def succOf : Label → List Label + | "start" => ["loop"] + | "loop" => ["edge-loop-loop", "edge-loop-out"] + | "edge-loop-loop" => ["loop"] + | "edge-loop-out" => ["out"] + | _ => [] + +@[crab] def prog : Cfg := { entry := "start", body := bodyOf, succ := succOf } + +/-- `.lin` wraps a linear constraint as an invariant atom; the other atom is the + boolean one, which this program has no use for. -/ +@[crab] def inv : Label → Assn + | "start" => Assn.top + | "loop" => [[.lin (xGeq 0), .lin (xLeq 9)]] + | "edge-loop-loop" => [[.lin (xGeq 1), .lin (xLeq 10)]] + | "edge-loop-out" => [[.lin (xGeq 1), .lin (xLeq 10)]] + | "out" => [[.lin (xGeq 10), .lin (xLeq 10)]] + | _ => Assn.bot + +/-! ## Which obligations hold, and which does not + +All four *non-assert* blocks verify exactly as in `bar`: Crab's invariants are +genuinely consecutive, and the analysis is not wrong about the reachable +states. -/ + +theorem vc_start : VC prog inv "start" := by crab_vc +theorem vc_loop : VC prog inv "loop" := by crab_vc +theorem vc_edge_loop_loop : VC prog inv "edge-loop-loop" := by crab_vc +theorem vc_edge_loop_out : VC prog inv "edge-loop-out" := by crab_vc + +/-- A state in which every integer variable is 10. + + `⟨…⟩` is anonymous-constructor notation for the record `State`: one constant + map per store. The boolean one is irrelevant here — this program has no + booleans — but `State` has two fields, so it must be given. -/ +def sigma10 : State := ⟨fun _ => 10, fun _ => false⟩ + +/-- **Block `out`'s verification condition is false.** + + In English: *there is a state satisfying the invariant Crab printed at + `out` in which the assertion `x != 10` does not hold* — so no proof of + `VC prog inv "out"` can exist. + + This is not a limitation of `omega` or of `crab_vc`. We prove the + **negation**, so the claim is unconditional: `x = 10` is exactly what Crab + inferred at `out`, and `x != 10` is exactly what the program asserts there. + Crab reports this assertion as an *error*; Lean agrees, and the source file + marks it `EXPECT_EQ(false, …)`. + + `Nat`/`Int` note: `simp` reduces the goal to `¬(10 ≠ 10)`, closed by `rfl` + inside `simp`. -/ +theorem vc_out_false : ¬ VC prog inv "out" := by + -- Assume the VC held, and instantiate it at the offending state. + intro h + have hpre : ⟦inv "out"⟧ sigma10 := by + simp [crab, sigma10, Assn.holds, Conj.holds, Atom.holds, LinCon.holds, LinCon.lhs, + LinExp.eval] + have hbad := h sigma10 hpre + -- `hbad` unfolds to `xNe10.holds sigma10 ∧ True`, i.e. `(10 : Int) ≠ 10`. + simp [crab, sigma10, LinCon.holds, LinCon.lhs, LinExp.eval] at hbad + +/-! ## What this shows about the design + +`bar` and `foo` differ in exactly one character of the CrabIR source, and the +development separates them exactly where it should: four VCs pass in both, and +the fifth passes in `bar` and is *refutable* in `foo`. + +It also exposes a design point worth settling deliberately. Defining the +weakest precondition of an assert as `⟦c⟧ ∧ Q` carries the assertion obligation +**inside** the per-block verification condition. The consequence is visible +right here: because `VC prog inv "out"` is false, `vc_all` is unprovable for +`foo`, and so `InvariantOf prog inv` cannot be derived — *even though the +invariants themselves are perfectly sound*. Block `out` has no successors, so +consecution at `out` is vacuous; only the assert makes its VC fail. + +Both readings are sound with respect to `Exec` — a failing assert has no +successor state either way — so this is a genuine choice, not a bug: + + * **`∧` (as specified, and as implemented here)** — one obligation per block + covers both invariant preservation and assertion safety. Simpler pipeline, + but "the invariants are sound" is only provable for programs whose + assertions all pass. + * **`→` (assume-flavoured)** — the VC would then prove invariant soundness + alone, with assertion safety left entirely to `chk`. `foo` would get its + `InvariantOf` theorem, and the two claims could be reported independently: + *"invariants sound; 1 of 2 assertions proved"*. + +The `∧` reading has since been leaned on further: `chk_of_VC` *derives* the +assertion obligations from the verification conditions, so a per-program file no +longer proves them separately at all. That is a second thing switching to `→` +would cost — `chk_of_VC` becomes false, and generated files need their `chk` +back. It does not change the argument above, only its price. + +Worth settling before any bulk run over the sample suite, since it changes what +can be reported for programs with deliberately failing assertions — and the +suite is full of them. -/ + +end Test1Foo +end Crabber diff --git a/lean/Crabber/Samples/Walkthrough.lean b/lean/Crabber/Samples/Walkthrough.lean new file mode 100644 index 0000000..0c7bb03 --- /dev/null +++ b/lean/Crabber/Samples/Walkthrough.lean @@ -0,0 +1,291 @@ +import Crabber.Samples.Test1Bar +/- +# Crabber.Walkthrough — `Test1Bar` proved again, one step at a time + +`Test1Bar.lean` proves each block with `by crab_vc`, a single macro. That +is what you want in a *generated* file, and useless for learning: stepping into +it shows the goal before and `True` after, with nothing in between. + +Here the macro is **unrolled**, so you can watch the machinery run. + +## How to use it + +1. Open the InfoView: command palette → **"Lean 4: Infoview: Toggle"** (⌃⇧↩). +2. Put the cursor at the **end of a tactic line** to see the state *after* that + tactic. Arrow down one line at a time. +3. Hover any identifier for its docstring; **F12** jumps to its definition. + +**Start with block `start` below.** It is the only one whose goal fits on a +screen at every stage. + +Everything here is an `example` (an anonymous theorem), so nothing clashes with +`Test1Bar.lean` and nothing depends on it. + +This file is **not** imported by `Crabber.lean` and is not part of the committed +library — it is a local teaching copy. So `lake build` does *not* check it. +After changing anything in the library, check it by hand: + + lake env lean Crabber/Samples/Walkthrough.lean +-/ + +namespace Crabber +namespace Walkthrough + +open Test1Bar + +set_option linter.unusedSimpArgs false + +/-! ## Block `start` — `y := 0`, one successor `loop` + +**What we must show.** Crab claims nothing at `start` (⊤) and claims +`0 ≤ y ≤ 9` at `loop`. So: after running `y := 0` from *any* state, the result +must satisfy `0 ≤ y ≤ 9`. Since `y` is 0 afterwards, that is `0 ≤ 0 ≤ 9`. + +Each line below is annotated with the goal it *produces*. Follow along in the +InfoView. -/ +example : VC prog inv "start" := by + -- Goal: ⊢ VC prog inv "start" + -- + -- `VC` is a `def`, so `intro` sees through it without any unfolding step: + -- it is *definitionally* `∀ σ, ⟦inv "start"⟧ σ → wp … σ`. + -- The underscore in `_hpre` says "I know this is unused" — and it is: + -- Crab claims ⊤ at the entry, so the hypothesis carries no information. + intro σ _hpre + -- σ : State + -- _hpre : ⟦inv "start"⟧ σ + -- ⊢ wp (prog.body "start") (fun τ => ∀ B' ∈ prog.succ "start", ⟦inv B'⟧ τ) σ + + -- Look up the block in the CFG: what are its statements, and its successors? + simp only [prog, bodyOf, succOf] + -- ⊢ wp [Stmt.assign "y" { terms := [], const := 0 }] + -- (fun τ => ∀ B' ∈ ["loop"], ⟦inv B'⟧ τ) σ + + -- **The substitution step.** `wp` walks the body backwards. The assignment + -- becomes `σ.set "y" (…)`: no quantifier is introduced, the state is simply + -- rewritten. Forward reasoning would have needed `∃ y_old` here instead. + simp only [wp, wpStmt] + -- ⊢ ∀ B' ∈ ["loop"], ⟦inv B'⟧ (σ.set "y" ({ terms := [], const := 0 }.eval σ)) + + -- Discharge the successor quantifier. `simp only [List.mem_singleton]` turns + -- `B' ∈ ["loop"]` into `B' = "loop"`; `rintro B' rfl` then introduces `B'` + -- and *substitutes* it away using that equation. (`rfl` inside `rintro` means + -- "this hypothesis is an equation — use it to rewrite".) + -- + -- Do this BEFORE unfolding `inv`: while `B'` is still a variable, `inv B'` + -- cannot reduce, and unfolding it would dump the entire `match` into the goal. + simp only [List.mem_singleton] + rintro B' rfl + -- ⊢ ⟦inv "loop"⟧ (σ.set "y" ({ terms := [], const := 0 }.eval σ)) + + -- Now the label is a literal, so Crab's invariant for it can be looked up. + -- This is the exported data: `-1·y ≤ -0` and `1·y ≤ 9`. + simp only [inv, yGeq, yLeq] + -- ⊢ ⟦[[{op := le, terms := [(-1, "y")], const := -0}, + -- {op := le, terms := [(1, "y")], const := 9}]]⟧ (σ.set "y" …) + + -- `⟦·⟧` is ⋁⋀: "some disjunct, all of whose constraints hold". + simp only [Assn.holds, Conj.holds] + -- ⊢ ∃ k, k ∈ [[…, …]] ∧ ∀ c ∈ k, c.holds (σ.set "y" …) + + -- Give the atoms their arithmetic meaning: `LinCon.holds` matches on + -- the operator, `LinExp.eval` folds `Σ coef * σ(var) + const`. + simp only [Atom.holds, LinCon.holds, LinCon.lhs, LinExp.eval] + -- Same shape, but `c.holds` has become a `match c.op with | le => … ≤ …`. + + -- Finish: pick the single disjunct, evaluate the two folds, and fire + -- `State.set_same` to turn `(σ.set "y" 0).ints "y"` into `0`. What is left is + -- `0 ≤ 0 ∧ 0 ≤ 9`, which `simp` closes by computation — no `omega` needed. + simp + +/-! ## The same proof, instrumented with `trace_state` + +If the InfoView keeps showing "Goals accomplished!", your cursor is past the end +of the proof — it always reports the state *at the cursor*. This copy avoids +the problem entirely: `trace_state` **prints** the goal as a message, so all +eight states appear in the InfoView's *Messages* section (and in the Problems +panel) no matter where the cursor sits. + +Click anywhere in this example and read the messages top to bottom. Delete the +`trace_state` lines once cursor-stepping feels natural — it is the better tool +for real work, because it shows the state interactively rather than as a dump. -/ +example : VC prog inv "start" := by + trace_state -- ⊢ VC prog inv "start" + intro σ _hpre + trace_state -- the ∀σ and the hypothesis appear + simp only [prog, bodyOf, succOf] + trace_state -- the block's statements and successors + simp only [wp, wpStmt] + trace_state -- σ.set "y" … appears: substitution + simp only [List.mem_singleton] + rintro B' rfl + trace_state -- B' is now the literal "loop" + simp only [inv, yGeq, yLeq] + trace_state -- Crab's exported constraints, as data + simp only [Assn.holds, Conj.holds] + trace_state -- ⋁⋀ becomes ∃/∀ over lists + simp only [Atom.holds, LinCon.holds, LinCon.lhs, LinExp.eval] + trace_state -- and now it is arithmetic + simp + +/-! ## Block `loop` — `y := y + 1`, **two** successors + +The interesting one. This time we reduce the *hypothesis* first, so you can +read what Crab claims at the block entry before looking at the goal. + +The `rintro B' (rfl | rfl)` splits into **two goals**, one per successor. That +is the point of the VC: the body must establish every successor's invariant, +because which edge gets taken is not decided until the guard runs, inside the +edge block. -/ +example : VC prog inv "loop" := by + intro σ hpre + -- Reduce the precondition to arithmetic: `hpre : 0 ≤ σ.ints "y" ≤ 9`. + simp only [inv, yGeq, yLeq, Assn.holds, Conj.holds, Atom.holds, LinCon.holds, LinCon.lhs, + LinExp.eval] at hpre + simp at hpre + -- Now the goal, same recipe as `start`. + simp only [prog, bodyOf, succOf] + simp only [wp, wpStmt] + simp only [List.mem_cons, List.mem_singleton, List.not_mem_nil, or_false] + -- ⊢ ∀ B', (B' = "edge-loop-loop" ∨ B' = "edge-loop-out") → ⟦inv B'⟧ (σ.set "y" …) + rintro B' (rfl | rfl) + · -- successor `edge-loop-loop`: must establish `1 ≤ y ≤ 10` + simp only [inv, yGeq, yLeq, Assn.holds, Conj.holds, Atom.holds, LinCon.holds, + LinCon.lhs, LinExp.eval] + simp + -- hpre : 0 ≤ σ.ints "y" ∧ σ.ints "y" ≤ 9 + -- ⊢ 1 ≤ σ.ints "y" + 1 ∧ σ.ints "y" + 1 ≤ 10 + omega + · -- successor `edge-loop-out`: the same invariant, proved again + simp only [inv, yGeq, yLeq, Assn.holds, Conj.holds, Atom.holds, LinCon.holds, + LinCon.lhs, LinExp.eval] + simp + omega + +/-! ## Block `edge-loop-loop` — `assume(y ≤ 9)`, successor `loop` + +Here an **arrow** appears: `wp (assume c) Q = ⟦c⟧ → Q`, so the guard becomes the +antecedent of an implication and `intro hguard` assumes it. + +That arrow is the only one in the goal, and it comes from the `assume` in the +*program*. Nothing here comes from the transition relation — `wp_sound` +consumed all of that once, in `WP.lean`. -/ +example : VC prog inv "edge-loop-loop" := by + intro σ hpre + simp only [inv, yGeq, yLeq, Assn.holds, Conj.holds, Atom.holds, LinCon.holds, LinCon.lhs, + LinExp.eval] at hpre + simp at hpre + simp only [prog, bodyOf, succOf] + simp only [wp, wpStmt] + -- Give the guard its arithmetic meaning, then assume it. + simp only [yLeq, Atom.holds, LinCon.holds, LinCon.lhs, LinExp.eval] + simp only [List.foldr] + intro hguard + -- hguard : 1 * σ.ints "y" + 0 ≤ 9 + simp only [List.mem_singleton] + rintro B' rfl + simp only [inv, yGeq, yLeq, Assn.holds, Conj.holds, Atom.holds, LinCon.holds, + LinCon.lhs, LinExp.eval] + simp + omega + +/-! ## Block `edge-loop-out` — `assume(y ≥ 10)`, successor `out` + +The same shape with the negated guard. Watch how the loop exit is *proved*: +from `1 ≤ y ≤ 10` and `y ≥ 10` we get `y = 10`, which is exactly the invariant +Crab printed at `out`. This VC is why the assertion there can be discharged. -/ +example : VC prog inv "edge-loop-out" := by + intro σ hpre + simp only [inv, yGeq, yLeq, Assn.holds, Conj.holds, Atom.holds, LinCon.holds, LinCon.lhs, + LinExp.eval] at hpre + simp at hpre + simp only [prog, bodyOf, succOf] + simp only [wp, wpStmt] + simp only [yGeq, Atom.holds, LinCon.holds, LinCon.lhs, LinExp.eval] + simp only [List.foldr] + intro hguard + simp only [List.mem_singleton] + rintro B' rfl + simp only [inv, yGeq, yLeq, Assn.holds, Conj.holds, Atom.holds, LinCon.holds, + LinCon.lhs, LinExp.eval] + simp + omega + +/-! ## Block `out` — `assert(y = 10)`, **no** successors + +Two degenerate cases at once, both falling out with no special handling: + +* `succ "out" = []`, so the postcondition `∀ B' ∈ [], …` is vacuously `True`; +* an assert both obligates and filters, so `wp (assert c) Q = ⟦c⟧ ∧ Q` and an + `∧` appears rather than an arrow. + +`refine ⟨?_, ?_⟩` splits that conjunction into its two halves: the assert's own +obligation, and the (trivial) postcondition. Note the assert is **not** an +antecedent — an assert we cannot discharge is a failure, not a free pass. -/ +example : VC prog inv "out" := by + intro σ hpre + simp only [inv, yGeq, yLeq, Assn.holds, Conj.holds, Atom.holds, LinCon.holds, LinCon.lhs, + LinExp.eval] at hpre + simp at hpre + -- hpre : σ.ints "y" = 10 (from `10 ≤ y ≤ 10`) + simp only [prog, bodyOf, succOf] + simp only [wp, wpStmt] + refine ⟨?_, ?_⟩ + · -- the assert's obligation: `y = 10` + simp only [yEq10, Atom.holds, LinCon.holds, LinCon.lhs, LinExp.eval] + simp + omega + · -- the postcondition: `∀ B' ∈ [], …`, vacuous + simp + +/-! ## The entry obligation + +The other premise of `inductive_sound`. Crab claims ⊤ at `start`, so this is +immediate — but it is not vacuous in general: a domain that inferred something +at entry would have to justify it against `InitState`. -/ +example : ∀ σ : State, InitState prog σ → ⟦inv prog.entry⟧ σ := by + intro σ _ + simp only [prog, inv, Assn.top] + simp only [Assn.holds, Conj.holds] + -- ⊢ ∃ k ∈ [[]], ∀ c ∈ k, … + -- Supply the witness `[]`; the inner `∀` is then over the empty list. + exact ⟨[], by simp, by simp⟩ + +/-! ## The whole program, assembled + +`Test1Bar.lean` finishes in one line — `verified prog inv initiation vc_all` — +because `verified` chains the meta-theorems for you. Here that chain is +**pulled apart into named steps**: put the cursor after each `have` and read +what has been established so far. + +Read top to bottom as the whole argument: + + `vc_all` every block's VC holds ← arithmetic + `consecution_of_VC` therefore the annotation survives a step ← the adapter + `chk_of_VC` and every assert's obligation is inside it ← extraction + `inductive_sound` therefore it holds at every reachable state ← Park induction + `assert_safe` therefore no assert can fail ← the payoff + +Note that `vc_all` feeds **two** of these. An assert both filters and +obligates, so `wpStmt` puts its obligation into the block's own verification +condition; `consecution_of_VC` uses the VC for the invariant half, and +`chk_of_VC` pulls the obligation back out for the assertion half. That is why a +per-program file proves only two things, not three. + +Note also where the seam is: `hcons` is the first statement that mentions +`Step`. Everything above it is arithmetic; everything below is about the +transition system. That is the automation boundary of the design, visible as +one line. -/ +example : InvariantOf prog inv ∧ ¬ AssertFails prog := by + have hvc : ∀ B : Label, VC prog inv B := vc_all + have hcons : ∀ (L : Label) (σ : State) (L' : Label) (σ' : State), + ⟦inv L⟧ σ → Step prog (L, σ) (L', σ') → ⟦inv L'⟧ σ' := + consecution_of_VC prog inv hvc + have hinv : InvariantOf prog inv := + inductive_sound prog inv initiation hcons + have hchk := chk_of_VC prog inv hvc + have hsafe : ¬ AssertFails prog := + assert_safe prog inv hinv hchk + exact ⟨hinv, hsafe⟩ + +end Walkthrough +end Crabber diff --git a/lean/Crabber/Semantics.lean b/lean/Crabber/Semantics.lean new file mode 100644 index 0000000..1ee324d --- /dev/null +++ b/lean/Crabber/Semantics.lean @@ -0,0 +1,200 @@ +import Crabber.Assn +/- +# Crabber.Semantics — what a CrabIR program *does* + +**Trusted.** Nothing in this file is proved, because these definitions *are* our +claim about the meaning of CrabIR. If `Exec` is wrong, everything downstream is +proved about the wrong machine. The probe suite of small CrabIR programs run +against the real analyser is the mitigation: each measured fact there is +something this file must match. + +Two of those facts are visible in the code below: + + * **Integers are mathematical integers.** There is no wrapping anywhere; + `x:i8 := 127; x := x+1` gives 128, and truncating casts are the identity. + * **`assert` is check-then-assume.** `StmtExec.assert` requires the condition + to hold, so a failing assert has no successor state at all: execution simply + cannot continue past it. This is what makes Crab's downstream invariants + correct, and it means invariants describe only those executions in which + every assert so far has passed. +-/ + +namespace Crabber + +/-! ## One statement -/ + +/-- `StmtExec s σ σ'` — "statement `s` can take state σ to state σ'". + + A *relation*, not a function, because `havoc` is nondeterministic: from one + σ there are infinitely many σ'. Declaring it `inductive` means these four + constructors are the **only** ways a step can happen, which is what lets a + proof do case analysis on it. -/ +inductive StmtExec : Stmt → State → State → Prop where + -- Integer statements. + /-- Assignment overwrites `x` with the value of `e` in the *current* state. -/ + | assign {σ : State} {x : Var} {e : LinExp} : + StmtExec (.assign x e) σ (σ.set x (e.eval σ)) + /-- `havoc(x)` may write *any* integer. The constructor takes `v` as an + argument, so there is one step for each choice — this is where the + nondeterminism literally lives. -/ + | havoc {σ : State} {x : Var} (v : Int) : + StmtExec (.havoc x) σ (σ.set x v) + /-- `assume(c)` leaves the state alone, but only steps at all when `c` holds: + the hypothesis `c.holds σ` is a *premise* of the constructor. -/ + | assume {σ : State} {c : LinCon} (h : c.holds σ) : + StmtExec (.assume c) σ σ + /-- `assert(c)` behaves identically to `assume` *as a transition*. The + difference is not here but in the weakest-precondition calculus, which + additionally demands a proof of `c`. Filtering here is what makes the + invariants after an assert correct; obligating there is what makes the + assert mean something. -/ + | assert {σ : State} {c : LinCon} (h : c.holds σ) : + StmtExec (.assert c) σ σ + + -- Boolean statements. Nothing new happens here: each is an update, a filter, + -- or both, exactly as above, but against the boolean store. + /-- `x := c` evaluates the *integer* constraint and records the answer. + `LinCon.check` is the `Bool`-valued reading of `LinCon.holds`; that they + agree is `LinCon.check_eq_true`, and it is the only fact anything uses. -/ + | boolAssignCst {σ : State} {x : Var} {c : LinCon} : + StmtExec (.boolAssignCst x c) σ (σ.setBool x (c.check σ)) + /-- `x := y`, or `x := not y` when `negated`. `xor n` is the identity for + `n = false` and negation for `n = true`, which is exactly the flag's + meaning — so one clause covers both forms with no `if`. -/ + | boolAssignVar {σ : State} {x y : Var} {n : Bool} : + StmtExec (.boolAssignVar x y n) σ (σ.setBool x (n ^^ σ.bools y)) + /-- `x := y op z`. -/ + | boolBinop {σ : State} {x y z : Var} {op : BoolOp} : + StmtExec (.boolBinop x op y z) σ (σ.setBool x (op.apply (σ.bools y) (σ.bools z))) + /-- `assume(y)` / `assume(not y)`: the state is unchanged, and the step exists + only when the boolean holds — the premise is what does the filtering, just + as in the integer `assume`. -/ + | boolAssume {σ : State} {y : Var} {n : Bool} (h : (n ^^ σ.bools y) = true) : + StmtExec (.boolAssume y n) σ σ + /-- `assert(y)` — again identical to `assume` as a transition; the obligation + is added by the weakest-precondition calculus, not here. -/ + | boolAssert {σ : State} {y : Var} (h : σ.bools y = true) : + StmtExec (.boolAssert y) σ σ + /-- `x := if c then l else r`. -/ + | boolSelect {σ : State} {x c l r : Var} : + StmtExec (.boolSelect x c l r) σ + (σ.setBool x (if σ.bools c then σ.bools l else σ.bools r)) + +/-! ## A whole block body -/ + +/-- `Exec ss σ σ'` — "the statement list `ss` can take σ to σ'". + + The straight-line composition of `StmtExec`. A block body has no control + flow inside it — conditionals were compiled into separate edge blocks + carrying the guards — so a list is the whole story. -/ +inductive Exec : List Stmt → State → State → Prop where + /-- The empty body changes nothing. -/ + | nil {σ : State} : Exec [] σ σ + /-- Run the head, then the tail, through some intermediate state σ'. -/ + | cons {s : Stmt} {ss : List Stmt} {σ σ' σ'' : State} : + StmtExec s σ σ' → Exec ss σ' σ'' → Exec (s :: ss) σ σ'' + +/-! ## The transition system -/ + +/-- A configuration: which block we are at the top of, and the current state. -/ +abbrev Config := Label × State + +/-- `Step P c c'` — one move of the machine: run a whole block, then jump to one + of its successors. + + Kept as a plain `def` unfolding to a **conjunction**, so that the adapter + lemma in `VC.lean` can split it with `obtain ⟨_, _⟩`. That shape is + provisional: once procedure calls are added the machine gains a stack, + `Step` becomes an inductive, and that `obtain` becomes a `cases`. The + adapter lemma is the only place that would have to change. -/ +def Step (P : Cfg) (c c' : Config) : Prop := + c'.1 ∈ P.succ c.1 ∧ Exec (P.body c.1) c.2 c'.2 + +/-- Which states a program may start in. + + Crab assumes nothing about the values of variables on entry, so every state + is an initial state. This is a definition rather than a `Cfg` field because + it is a property of the analysis setup, not of the graph. Giving it a name + means that when input parameters with preconditions are added, only this + changes. -/ +def InitState (_P : Cfg) (_σ : State) : Prop := True + +/-- `Reachable P c` — the configurations the machine can actually get into. + + This is the **least fixed point** of the operator described by the two + constructors: `init` seeds it with the entry configurations, `step` closes it + under `Step`. In Lean, `inductive` *is* how you write a least fixed point — + the constructors say the set is closed under the rules, and the + automatically generated recursor (`Reachable.rec`) says it is the *smallest* + such set. That recursor is the induction principle used by `inductive_sound` + in `Soundness.lean`, and it is exactly the fixpoint-induction rule: the least + fixed point is contained in anything the operator maps into itself. + + Note what `Reachable` inherits from `Exec`: since a failing `assert` has no + `StmtExec` step, no configuration *past* a violated assert is reachable. + Invariants therefore describe assert-passing executions only, which is what + Crab computes. -/ +inductive Reachable (P : Cfg) : Config → Prop where + /-- Any state, at the entry block, is reachable. -/ + | init {σ : State} (h : InitState P σ) : Reachable P (P.entry, σ) + /-- Reachability is closed under `Step`. -/ + | step {c c' : Config} (hc : Reachable P c) (hs : Step P c c') : Reachable P c' + +/-! ## What it means for an assertion to fail -/ + +/-- `s.obligation σ` — what `s` demands of the state it is reached in. + + Every statement has one; for all but the two asserts it is `True`. Naming it + is what lets "an assertion fails" be stated once, over an arbitrary + statement, instead of once per kind of assert. + + That generalisation is forced rather than tidy. Written against + `Stmt.assert` alone, `AssertFails` would be *vacuously* unsatisfiable for a + program whose only assertions are boolean — the theorem would still read + "no assertion can fail" while quantifying over none of them. Every + assert-like construct still to come (division by zero, array bounds, + `select`'s guard) is one clause here and nothing else anywhere. + + `True` for the ordinary statements is not a placeholder: it is the claim + that they can be reached in any state whatsoever, which is exactly right. + + **Every constructor is listed, rather than a `_ => True` catch-all.** This + is a trusted definition, and a catch-all would silently give `True` to the + next statement added to `Stmt` — `select` with its division guard, or an + array load needing a bounds check. Those would then be *unobligated*, and + `¬ AssertFails` would quietly stop covering them while still reading as + though it did. Spelling the cases out turns that into a missing-cases error + at the one place where the question has to be answered. -/ +def Stmt.obligation : Stmt → State → Prop + | .assert c => fun σ => c.holds σ + | .boolAssert y => fun σ => σ.bools y = true + | .assign _ _ => fun _ => True + | .havoc _ => fun _ => True + | .assume _ => fun _ => True + | .boolAssignCst _ _ => fun _ => True + | .boolAssignVar _ _ _ => fun _ => True + | .boolBinop _ _ _ _ => fun _ => True + | .boolAssume _ _ => fun _ => True + | .boolSelect _ _ _ _ => fun _ => True + +/-- `AssertFails P` — some execution reaches a statement whose obligation is + false at that point. + + Spelled out concretely: there is a reachable configuration `(L, σ)`, the body + of `L` splits as `pre ++ s :: post`, running `pre` from σ can reach τ, and + `s`'s obligation fails at τ. + + `∃ L σ pre s post τ, …` chains six existentials; `∧` chains the four + conditions. `List.append` is written `++`. Quantifying over the way the body + splits is what makes "a statement occurring somewhere in the block" precise — + the append equation *is* its index. Positions holding an ordinary statement + contribute nothing, since `¬ True` is false. -/ +def AssertFails (P : Cfg) : Prop := + ∃ (L : Label) (σ : State) (pre : List Stmt) (s : Stmt) + (post : List Stmt) (τ : State), + Reachable P (L, σ) ∧ + P.body L = pre ++ s :: post ∧ + Exec pre σ τ ∧ + ¬ s.obligation τ + +end Crabber diff --git a/lean/Crabber/Soundness.lean b/lean/Crabber/Soundness.lean new file mode 100644 index 0000000..be5e298 --- /dev/null +++ b/lean/Crabber/Soundness.lean @@ -0,0 +1,123 @@ +import Crabber.VC +/- +# Crabber.Soundness — the two meta-theorems + +Proved once, program-independently. This is the heart of the project: +everything after it is plumbing and automation. +-/ + +namespace Crabber + +/-- `InvariantOf P I` — "`I` really is an invariant of `P`": every reachable + configuration satisfies the annotation at its own label. This is the property + `inductive_sound` delivers and `assert_safe` consumes. -/ +def InvariantOf (P : Cfg) (I : Label → Assn) : Prop := + ∀ c : Config, Reachable P c → ⟦I c.1⟧ c.2 + +/-- **`inductive_sound` — the inductive-assertion method.** + + In English: *if the annotation holds when the program starts, and no single + step can ever break it, then it holds at every state the program can ever + reach.* + + The two hypotheses are named arguments before the colon, so this theorem is a + **function**: hand it two proofs, get a proof back. + + What it is, structurally: `Reachable` is the least fixed point of the + operator its two constructors describe, and this theorem is the *leastness* + direction instantiated at the annotation. The two hypotheses together say + precisely that the set of states satisfying the annotation is closed under + that operator; the conclusion says `Reachable` is contained in it. That is + fixpoint induction, which is why the proof below is two lines: Lean *hands* + us the principle as `Reachable`'s recursor, and `induction … with` is sugar + over it. + + Note what it does **not** claim: nothing about the annotation being strongest + or precise, and nothing about termination — invariants are safety properties, + so a non-terminating program satisfies this vacuously. If Crab's output is + not inductive, the second hypothesis simply will not be provable. -/ +theorem inductive_sound (P : Cfg) (I : Label → Assn) + (initiation : ∀ σ : State, InitState P σ → ⟦I P.entry⟧ σ) + (consecution : ∀ (L : Label) (σ : State) (L' : Label) (σ' : State), + ⟦I L⟧ σ → Step P (L, σ) (L', σ') → ⟦I L'⟧ σ') : + InvariantOf P I := by + intro c h + -- Induct on the derivation of `Reachable P c`: exactly two cases, because + -- `Reachable` has exactly two constructors. They line up one-for-one with the + -- two hypotheses — that correspondence *is* the inductive-assertion method. + induction h with + | init hi => + -- The configuration is `(P.entry, σ)`; `initiation` is precisely this. + exact initiation _ hi + | step _hc hs ih => + -- `ih` is the induction hypothesis: the annotation held at the + -- predecessor. `hs` says we stepped from there. `consecution` closes it. + exact consecution _ _ _ _ ih hs + +/-- **`assert_safe` — the result users actually care about.** + + In English: *if the annotation is an invariant, and at every statement in + every block the invariant at that block's entry implies that statement's + obligation (after running the statements that precede it in the block), then + no execution of the program ever fails an assert.* + + The `chk` hypothesis quantifies over every way a block body splits as + `pre ++ s :: post` — the append equation is what makes "a statement occurring + somewhere in the block" precise. For a block whose assert is first, `pre` is + `[]` and `wp [] Q = Q`, so the obligation is just "the invariant implies the + condition"; for a statement that is not an assert the obligation is `True` + and there is nothing to show. + + Quantifying over an arbitrary statement, rather than over `Stmt.assert c`, is + what makes this cover the boolean asserts too — and every assert-like + construct still to come, each of which is a clause in `Stmt.obligation` and + nothing here. + + `chk` need not be supplied by hand: `chk_of_VC` derives it from the block + verification conditions, which is how `verified` below obtains it. It stays a + hypothesis so that this theorem remains true independently of that + derivation, which depends on how `wpStmt` treats an assert. -/ +theorem assert_safe (P : Cfg) (I : Label → Assn) + (hinv : InvariantOf P I) + (chk : ∀ (L : Label) (pre : List Stmt) (s : Stmt) (post : List Stmt), + P.body L = pre ++ s :: post → + ∀ σ : State, ⟦I L⟧ σ → wp pre (fun τ => s.obligation τ) σ) : + ¬ AssertFails P := by + -- `rintro` assumes `AssertFails P` and immediately destructs its six + -- existentials and four conjuncts into named pieces. + rintro ⟨L, σ, pre, s, post, τ, hreach, hbody, hexec, hfail⟩ + -- The invariant holds at the reachable configuration we landed on… + have hI : ⟦I L⟧ σ := hinv (L, σ) hreach + -- …so by `chk` the weakest precondition of the *prefix* for "s's obligation + -- holds" is true at σ… + have hwp := chk L pre s post hbody σ hI + -- …and `wp_sound`, given that the prefix really ran σ to τ, says the + -- obligation holds at τ. But `hfail` says it does not. Contradiction. + exact hfail (wp_sound hwp hexec) + +/-- **The bundle a per-program file proves.** + + In English: *given (i) the entry obligation and (ii) every block's + verification condition, the annotation is a genuine invariant and no + assertion can fail.* + + This is the single entry point for per-program files: it chains + `consecution_of_VC`, `chk_of_VC`, `inductive_sound` and `assert_safe` so that + such a file never mentions `Step`, `Reachable`, or `wp_sound`. + + **Two hypotheses, not three.** The assert obligations used to be a third + argument, generated per program. They are not, because `wpStmt` already puts + an assert's obligation inside its block's verification condition, and + `chk_of_VC` extracts it. A per-program file now supplies only what is + genuinely program-specific: the entry invariant is satisfied, and each block + preserves the annotation. -/ +theorem verified (P : Cfg) (I : Label → Assn) + (initiation : ∀ σ : State, InitState P σ → ⟦I P.entry⟧ σ) + (vcs : ∀ B : Label, VC P I B) : + InvariantOf P I ∧ ¬ AssertFails P := + -- `have` names the intermediate result so both halves can use it; the + -- anonymous constructor `⟨_, _⟩` builds the conjunction. + have hinv := inductive_sound P I initiation (consecution_of_VC P I vcs) + ⟨hinv, assert_safe P I hinv (chk_of_VC P I vcs)⟩ + +end Crabber diff --git a/lean/Crabber/State.lean b/lean/Crabber/State.lean new file mode 100644 index 0000000..2eb21ea --- /dev/null +++ b/lean/Crabber/State.lean @@ -0,0 +1,169 @@ +import Crabber.Syntax +/- +# Crabber.State — concrete states, and the meaning of expressions in one + +**Trusted.** Nothing here is proved, because these definitions *are* the claim +about what CrabIR means. A bug here would let us "prove" a false invariant. +-/ + +namespace Crabber + +/-- A concrete machine state. + + A record of *total* maps. Two consequences worth spelling out, because both + are load-bearing: + + * **Total, not partial.** There is no `Option`, so no case analysis for + "variable not yet assigned" ever appears in a proof. An unread variable + simply has some unknown value, which matches how Crab sees it: a variable + absent from the abstract domain is unconstrained. + * **`Var → Int`, a function.** Not a finite map. We never need to enumerate + the domain, and updating is just building a new function. + + **One map per type, all indexed by the same `Var`.** CrabIR's namespaces are + disjoint, so a name occurring in a boolean statement is a boolean variable and + `ints` is simply never asked about it. Booleans are `Bool`, not integers + confined to `{0,1}` — the argument is in `Syntax.lean`, and the consequence + visible here is that no well-formedness side condition relates the two maps. + They are independent, which is why writing one never disturbs the other. + + An array map is still absent, and will be the next field. -/ +structure State where + ints : Var → Int + bools : Var → Bool + +/-- `σ.set x v` is σ with the *integer* `x` remapped to `v`, everything else + untouched. + + Written out by hand rather than imported from a library. It is three lines, + it lets us state exactly the rewriting rules below — which is all the + automation ever uses — and it keeps this development free of any dependency + beyond Lean core. + + `{ σ with … }` is record-update notation: it copies every field not mentioned, + so the boolean store comes through unchanged. -/ +def State.set (σ : State) (x : Var) (v : Int) : State := + { σ with ints := fun y => if y = x then v else σ.ints y } + +/-- `σ.setBool x b` is σ with the *boolean* `x` remapped to `b`. -/ +def State.setBool (σ : State) (x : Var) (b : Bool) : State := + { σ with bools := fun y => if y = x then b else σ.bools y } + +/-- Reading back the variable you just wrote gives the written value. + + `@[simp]` registers this with the simplifier, so `simp` rewrites + `(σ.set "y" 0).ints "y"` to `0` automatically. Together with the three lemmas + below this is the entire interface to the update functions: no proof ever has + to unfold the `if`. -/ +@[simp] theorem State.set_same (σ : State) (x : Var) (v : Int) : + (σ.set x v).ints x = v := by + -- `simp [State.set]` unfolds the definition; the `if y = x` then has both + -- sides literally `x`, so the condition is `x = x`, which `simp` closes. + simp [State.set] + +/-- Reading a *different* variable is unaffected by the write. -/ +@[simp] theorem State.set_other (σ : State) (x y : Var) (v : Int) (h : y ≠ x) : + (σ.set x v).ints y = σ.ints y := by + simp [State.set, h] + +/-- The boolean counterpart of `set_same`. -/ +@[simp] theorem State.setBool_same (σ : State) (x : Var) (b : Bool) : + (σ.setBool x b).bools x = b := by + simp [State.setBool] + +/-- The boolean counterpart of `set_other`. -/ +@[simp] theorem State.setBool_other (σ : State) (x y : Var) (b : Bool) (h : y ≠ x) : + (σ.setBool x b).bools y = σ.bools y := by + simp [State.setBool, h] + +/-! ### The two stores do not interfere + +Both of these are true by `rfl` — `State.set` is a record update that does not +mention `bools`, so the projection reduces without any rewriting at all. They are +`@[simp]` lemmas anyway, and not because `simp` could not manage otherwise: they +are what lets an integer assignment be *skipped over* by a boolean goal without +first unfolding `State.set` and re-deriving a disequality on names. With them, +`(σ.set "y" 3).bools "b"` becomes `σ.bools "b"` in one step, whatever the names +are — and unlike `set_other` there is no side condition, because the +interference is impossible rather than merely absent. -/ + +@[simp] theorem State.set_bools (σ : State) (x : Var) (v : Int) (y : Var) : + (σ.set x v).bools y = σ.bools y := rfl + +@[simp] theorem State.setBool_ints (σ : State) (x : Var) (b : Bool) (y : Var) : + (σ.setBool x b).ints y = σ.ints y := rfl + +/-! ## Meaning of expressions and constraints + +These two functions are where syntax becomes arithmetic. `LinExp.eval` returns +an `Int` (a computation); `LinCon.holds` returns a `Prop` (a claim). -/ + +/-- The value of a linear expression in a state: `Σ coefᵢ * σ(varᵢ) + const`. + + `foldr f init` walks the list right-to-left; starting from `e.const` and + adding `coef * value` for each term gives exactly the sum above. -/ +def LinExp.eval (e : LinExp) (σ : State) : Int := + e.terms.foldr (fun t acc => t.1 * σ.ints t.2 + acc) e.const + +/-- The left-hand side of a constraint, evaluated: just the `Σ coefᵢ * varᵢ` + part, with no constant. -/ +def LinCon.lhs (c : LinCon) (σ : State) : Int := + ({ terms := c.terms, const := 0 } : LinExp).eval σ + +/-- What it means for a constraint to hold in a state. + + Note the return type is `Prop`, not `Bool`: this is a *proposition* about σ, + the thing `omega` will eventually be asked to prove. + + A `Bool`-valued version would be needed to *run* this check as compiled code + — for instance to ship an invariant checker to a browser — and that is a + genuinely different design, because a decidable version of implication + between assertions has to be written and proved sound by hand. This + development takes the other route: proofs are found at development time by + tactics, and the kernel checks them. -/ +def LinCon.holds (c : LinCon) (σ : State) : Prop := + match c.op with + | .le => c.lhs σ ≤ c.const + | .lt => c.lhs σ < c.const + | .eq => c.lhs σ = c.const + | .ne => c.lhs σ ≠ c.const + +/-! ### The one place a constraint must be a `Bool` + +`b := (x == 10)` writes a *value* into the boolean store, so it needs a `Bool`, +not the `Prop` above. The two are related by `check_eq_true` below, which is the +only bridge between them and the only lemma the automation uses. + +Written out rather than obtained as `decide (c.holds σ)` through a `Decidable` +instance. Both compute the same answer, but a derived instance is a term the +simplifier has to unfold through a `match` on the operator before anything can +happen, whereas the equation lemmas of this `def` fire directly. Since every +goal about a boolean assignment goes through it, predictability wins. -/ + +/-- Whether a constraint holds, as a `Bool`. -/ +def LinCon.check (c : LinCon) (σ : State) : Bool := + match c.op with + | .le => c.lhs σ ≤ c.const + | .lt => c.lhs σ < c.const + | .eq => c.lhs σ = c.const + | .ne => c.lhs σ ≠ c.const + +/-- The bridge: computing `true` and holding are the same thing. + + `@[simp]` in this direction — `check … = true` rewrites to `holds` — because + goals arrive with the `Bool` (it came out of the state) and `omega` wants the + `Prop`. -/ +@[simp] theorem LinCon.check_eq_true (c : LinCon) (σ : State) : + c.check σ = true ↔ c.holds σ := by + -- One case per operator; in each, `simp` reduces the decidable comparison + -- coerced to `Bool` back to the proposition it decides. + cases h : c.op <;> simp [LinCon.check, LinCon.holds, h] + +/-- The negative half. Needed as its own lemma, not derivable by `simp` from the + one above: `b = false` is not syntactically the negation of `b = true`, and + Crab exports `b0 = 0` as readily as `b0 = 1`. -/ +@[simp] theorem LinCon.check_eq_false (c : LinCon) (σ : State) : + c.check σ = false ↔ ¬ c.holds σ := by + cases h : c.op <;> simp [LinCon.check, LinCon.holds, h] + +end Crabber diff --git a/lean/Crabber/Syntax.lean b/lean/Crabber/Syntax.lean new file mode 100644 index 0000000..6d3c471 --- /dev/null +++ b/lean/Crabber/Syntax.lean @@ -0,0 +1,245 @@ +/- +# Crabber.Syntax — the deeply embedded CrabIR program + +"Deeply embedded" means a CrabIR program is *data* in Lean: an ordinary +inductive datatype we can pattern-match on, not a Lean program. That is what +lets the weakest-precondition calculus walk over a block body, and what lets a +frontend emit a program as a plain term. + +Everything here mirrors the JSON that `crabber --cfg-to-json` produces. +-/ + +namespace Crabber + +/-- A block name. + + Plain `String`, matching Crab's own labels. That includes the blocks Crab + synthesises rather than the ones you wrote: a conditional is compiled into + dedicated `edge--` blocks carrying the guard, and an artificial + `___exit` block may be added. We model the graph Crab *analysed*, so those + names have to be representable. + + Strings were chosen over a per-program enumeration so that one `Cfg` type + serves every program. The worry was that looking a label up would then be + expensive to reduce; in practice `simp` handles literal string matches + without difficulty. + + `abbrev` (rather than `def`) makes this a *reducible* alias: Lean unfolds it + silently, so a `Label` is interchangeable with a `String` everywhere. -/ +abbrev Label := String + +/-- A variable name. CrabIR is strongly typed with disjoint namespaces for + integers, booleans and arrays, so a name alone identifies a variable and no + sum type of values is needed. + + That disjointness is what lets `State` hold one map per type and index all of + them by the same `Var`: a name occurring in a boolean statement is a boolean + variable, and the integer map's answer for it is never consulted. -/ +abbrev Var := String + +/-! ## Linear expressions + +Crab's export gives every assignment right-hand side as a linear expression: +a list of (coefficient, variable) pairs plus a constant. So + + y := y + 1 is terms = [(1, "y")], const = 1 +-/ + +/-- A linear expression `Σ (coef * var) + const` over the integers. + + `structure` declares a record: one constructor (`LinExp.mk`) and one + projection per field (`e.terms`, `e.const`). `deriving Repr` asks Lean to + generate a printer, which is what makes `#eval` able to display one — handy + when debugging a transcription. -/ +structure LinExp where + terms : List (Int × Var) + const : Int + deriving Repr + +/-! ## Linear constraints + +Crab normalises every constraint to ` ` and tags it with the +type of its variables. We deliberately drop the bitwidth: measured against the +real analyser, Crab's integers behave as mathematical integers, not machine +words — `x:i8 := 127; x := x+1` yields `x == 128`, not `-128`, and a truncating +cast from `i32` to `i16` leaves the value unchanged. So the semantics here is +over unbounded `Int`, and a width would be recorded but never used. + +That is a genuine assumption about what CrabIR means, not a modelling +convenience. A wrapping semantics would be a separate development, under which +some of Crab's results would be expected to fail. -/ + +/-- The comparison operators Crab can emit: `<=`, `<`, `=`, `!=`. + + `inductive` declares a datatype by listing *all* the ways to build one. + These four constructors are the only `CmpOp`s that exist, which is what + makes a `match` over them exhaustive. -/ +inductive CmpOp where + | le | lt | eq | ne + deriving Repr, DecidableEq + +/-- A single linear constraint `Σ (coef * var) op const`. + + **Integer-typed, always.** The export tags every constraint with a type, and + a bool-tagged one is not one of these: it is a claim about a boolean + variable, and lives in the assertion language as its own atom (see + `Assn.lean`). Nothing in a `LinCon` ever reads the boolean store, which is + what keeps `LinCon.lhs` — and therefore every goal `omega` is handed — + purely integer arithmetic. -/ +structure LinCon where + op : CmpOp + terms : List (Int × Var) + const : Int + deriving Repr + +/-! ## Boolean operators + +The three Crab emits, under the names its export uses. `xor` rather than +"not-equal" because that is the operator's name in CrabIR; `not` is not here, +because Crab has no unary boolean statement — a negation is carried as the +`negated` flag on `bool_assign_var`, and `b := not(c)` in the surface syntax +compiles to exactly that. -/ + +/-- The boolean binary operators Crab can emit: `and`, `or`, `xor`. -/ +inductive BoolOp where + | and | or | xor + deriving Repr, DecidableEq + +/-- What a `BoolOp` computes. Kept next to the syntax rather than in `State` + because it involves no state: it is the meaning of the operator itself, and + `Bool`'s own connectives are that meaning. -/ +def BoolOp.apply : BoolOp → Bool → Bool → Bool + | .and => (· && ·) + | .or => (· || ·) + | .xor => (· ^^ ·) + +/-! ## Statements + +The numeric core, plus the boolean fragment. + +The four numeric constructors already exercise every interesting case of the +weakest-precondition calculus — substitution, quantifier introduction, +implication, and proof obligation. The six boolean ones add no new case to that +calculus: they are substitution, implication and obligation again, over the +boolean store instead of the integer one. + +### How the booleans are represented, and why + +Crab exports boolean *facts* as 0/1 linear constraints — an invariant contains +`b = 1`, tagged with type `bool` — so an invariant looks like one uniform linear +system. `State` deliberately does **not** follow suit. It carries a separate +`Var → Bool` map, and the assertion language gets a boolean atom of its own. + +Measured against the analyser, across `int`, `int-terms`, `int-set`, `zones`, +`oct-snf` and `pk`, a bool-tagged constraint is *always* `1·b = 0` or `1·b = 1`: +never relational, never a non-unit coefficient. Crab's booleans go through a flat +per-variable lattice, so there is no relational information to lose. The uniform +linear encoding therefore buys nothing here, and costs two things: + + * `b2 := b0 and b1` would have to be `min`, or a multiplication, and would drag + `if … then 1 else 0` terms into every arithmetic goal; + * nothing would confine a boolean to `{0, 1}`. A havoc'd or never-assigned + boolean would be an arbitrary integer, so `b or not b` would come out `7` and + Crab's (correct) `= 1` would be unprovable — unless `State` also carried a + type environment and `InitState` restricted it. + +The objection previously recorded against a separate map was that the meaning +function would then need each variable's type. It does — and the wire format +already supplies it, on every constraint, which is how the reader tells a boolean +atom from a linear one. + +Deferred, and named here so the omission is visible rather than silent: + + * `select`, `cast`, `unreachable`, and the non-linear binary operators. + Multiplication and division of variables are outside what `omega` decides, + and the exact rounding behaviour of Crab's four division operators — + signed and unsigned quotient and remainder are distinct in the export — has + not been pinned down. `cast` is the one that bites soonest: `samples/test-6` + reaches its booleans through `trunc`, so it stays out of scope even now. + * Procedure calls, which need a call rule and Crab's interprocedural + summaries; and the array statements, which need select/store reasoning in + the assertion language. +-/ + +/-- A CrabIR statement. -/ +inductive Stmt where + /-- `x := e` — assignment of a linear expression. -/ + | assign (x : Var) (e : LinExp) + /-- `havoc(x)` — `x` becomes an arbitrary integer. -/ + | havoc (x : Var) + /-- `assume(c)` — execution continues only if `c` holds. -/ + | assume (c : LinCon) + /-- `assert(c)` — a proof obligation *and* a filter on the state. Measured + against the real analyser, Crab treats an assert as check-then-assume: + after `havoc(x); assert(x >= 10)` the next block's invariant is + `x ∈ [10, +∞]`, even though the assert itself only produces a warning. -/ + | assert (c : LinCon) + /-- `x := c` — the boolean `x` records whether the *integer* constraint `c` + holds. This is the only statement that crosses between the two stores, and + it crosses one way: it reads the integer state and writes the boolean one. + + `c` is a `LinCon`, so integer-typed. The export permits a reference + constraint here too (`cst_kind` distinguishes them); references are not + modelled, and the reader refuses that form by name. -/ + | boolAssignCst (x : Var) (c : LinCon) + /-- `x := y` or `x := not y`, according to `negated`. Crab has no separate + negation statement: the surface `b := not(c)` compiles to this with the + flag set. -/ + | boolAssignVar (x : Var) (y : Var) (negated : Bool) + /-- `x := y op z` for `op` one of `and`, `or`, `xor`. -/ + | boolBinop (x : Var) (op : BoolOp) (y : Var) (z : Var) + /-- `assume(y)`, or `assume(not y)` when `negated`. Execution continues only + when the boolean holds. -/ + | boolAssume (y : Var) (negated : Bool) + /-- `assert(y)` — check-then-assume, exactly as the integer `assert`. There is + no `negated` flag: the export does not carry one for boolean asserts. -/ + | boolAssert (y : Var) + /-- `x := if c then l else r`, all four boolean. Crab's own parser cannot + produce this — it arrives from LLVM-style frontends — but the export can + contain it, so modelling it costs one clause and avoids an unmodelled + member of an otherwise complete group. -/ + | boolSelect (x : Var) (c : Var) (l : Var) (r : Var) + deriving Repr + +/-! ## Control-flow graphs -/ + +/-- Turn an association list into a **total** function, answering `dflt` for any + label the list does not mention. + + This is how a machine-generated program supplies its blocks: the frontend + splices in a list of (label, value) pairs, and this builds the total function + `Cfg` requires. Writing the function out as a chain of literal cases would do + just as well; a list keeps the generated term small and uniform. + + The comparison is `l = k`, propositional equality decided by `String.decEq`, + and that choice is load-bearing rather than incidental. The obvious + alternative is `List.lookup`, which compares with `BEq`. Both compute the + same answers, but proofs need the *other* direction too: showing that a label + naming no block gets the default, from hypotheses of the form `¬ B = "loop"`. + With `=` the simplifier rewrites the `if` with such a hypothesis directly; + with `==` it cannot, and the unknown-label case — which the bundling lemma + for every generated program depends on — does not go through. -/ +def table {α : Type} (dflt : α) : List (Label × α) → Label → α + | [], _ => dflt + | (k, v) :: rest, l => if l = k then v else table dflt rest l + +/-- A CFG: an entry label, and two *total* functions giving each label its + block body and its successors. + + Totality is a deliberate choice. The soundness argument needs "every block's + verification condition holds", quantified over every `String` — including + ones that name no block. Making `body` and `succ` total, defaulting to `[]`, + means that case is discharged once and for all by a single lemma rather than + needing a side condition at every use. It also matches the treatment of + states, whose variable maps are total for the same reason. + + Note the CFG we model is the one Crab *analysed*, not the source text: it + contains the synthesised edge blocks that carry compiled-away guards, and + may have been simplified further. A transcription of the source would not + line up with the labels the invariants are attached to. -/ +structure Cfg where + entry : Label + body : Label → List Stmt + succ : Label → List Label + +end Crabber diff --git a/lean/Crabber/Tactic.lean b/lean/Crabber/Tactic.lean new file mode 100644 index 0000000..15b9e46 --- /dev/null +++ b/lean/Crabber/Tactic.lean @@ -0,0 +1,80 @@ +import Crabber.Attr +import Crabber.VC +/- +# Crabber.Tactic — `crab_vc`, the per-block automation + +**Untrusted.** A tactic is a *metaprogram that runs in the elaborator and +constructs a proof term*; the term is what gets stored and checked by the +kernel. So `crab_vc` can be as unprincipled as convenient: the worst a bug can +do is fail to find a proof, or produce one the kernel rejects — a build error, +never a false theorem. That is why the tactic owes no correctness argument. +-/ + +namespace Crabber + +/-- **`crab_vc` — discharge one block's verification condition.** + + In English: *unfold everything until the goal is linear integer arithmetic, + then call `omega`.* + + The pipeline: + + 1. `intro σ hpre` — `VC` is a `def`, so it unfolds definitionally as `intro` + looks at the goal; no explicit unfolding step is needed. Take the state + arbitrary, assume the invariant at the block's entry. + 2. `simp` with the `crab` set — this does four things at once: + * unfolds the program and the annotation, so the block's concrete + statement list and successor list appear; + * unfolds the weakest-precondition calculus over that list, pushing the + postcondition backwards — assignments become state updates, `assume`s + become arrows; + * rewrites `(σ.set "y" v).ints "y"` to `v`, which is where substitution + actually happens. Boolean statements go the same way: `setBool_same` + substitutes, `LinCon.check_eq_true` turns a recorded comparison back + into the proposition it decided, and `Bool.and_eq_true` and friends + break the connectives apart, so a boolean assignment leaves *integer* + arithmetic behind and `omega` never sees a `Bool`; + * unfolds the meaning function on both the hypothesis and the goal, + turning invariant *data* into arithmetic, and collapses the bounded + quantifier over successors into a plain conjunction. + 3. `omega` on whatever is left — quantifier-free linear integer arithmetic. + 4. a `simp_all` pass, then `omega` again, for whatever step 3 could not + close. + + `all_goals omega` rather than `omega` so that a goal `simp` already closed + (for instance a block whose successors carry no constraints) is not an error. + + **Why step 4 exists, and why it is not step 2.** A boolean fact can have to + travel from the *hypothesis* to the goal — a loop carrying a boolean has + `b = true` in the invariant at both ends and no statement in between, so + nothing in the goal reduces it away. `simp … at hpre ⊢` cannot do that: it + simplifies the two independently. `simp_all` can, because it uses hypotheses + to rewrite the goal. + + So why not `simp_all` throughout? Because it is *not* a superset here: + replacing step 2 with it loses integer bounds that `omega` needs — `simp_all` + rewrites hypotheses with each other and can consume one that was carrying a + bound. Running the narrow pass first and `simp_all` only on the survivors + keeps every previously-provable goal provable and adds the boolean ones. + + **Where this will fail** — all of it out of scope for the modelled fragment, + and all of it producing "could not prove", never a wrong answer: + * non-linear statements (`x := y*z`, `y/z`): `omega` decides Presburger + arithmetic, and multiplication of variables is outside it. The rounding + behaviour of Crab's four division operators is not even fixed yet. + * disjunctive invariants from the powerset domains: `simp` turns them into + `∨` hypotheses, and the cost is (disjuncts in the precondition) × + (disjuncts in the postcondition) `omega` calls. + * programs over many variables, where the rewrite for *unrelated* writes + must discharge string disequalities to see through them. -/ +macro "crab_vc" : tactic => + `(tactic| ( + intro σ hpre + simp [crab, table, Assn.holds, Conj.holds, Atom.holds, LinCon.holds, + LinCon.lhs, LinExp.eval, BoolOp.apply, Assn.top, Assn.bot] at hpre ⊢ + all_goals (try omega) + all_goals (try simp_all [Atom.holds, LinCon.holds, LinCon.lhs, LinExp.eval, + BoolOp.apply]) + all_goals omega)) + +end Crabber diff --git a/lean/Crabber/VC.lean b/lean/Crabber/VC.lean new file mode 100644 index 0000000..715d318 --- /dev/null +++ b/lean/Crabber/VC.lean @@ -0,0 +1,170 @@ +import Crabber.WP +/- +# Crabber.VC — the per-block obligation, and the adapter to consecution + +This file is the seam of the whole development. Above it everything is about the +transition system; below it everything is arithmetic. Both theorems are proved +**once**, for every program and every annotation — no generated file ever redoes +this work. +-/ + +namespace Crabber + +/-- **`VC P I B` — the verification condition for block `B`.** + + In English: *assume the invariant Crab claims at `B`'s entry; then running + `B`'s straight-line body must land in a state satisfying the invariant Crab + claims at the entry of **every** successor of `B`.* + + Note this is a `def` returning `Prop`, not a `theorem`: it **asserts + nothing**. It is a statement *schema* indexed by a block — a function from + labels to statements. `VC prog inv "loop"` is a `Prop`; a separate `theorem` + supplies its proof. (`Monotone f` and `Function.Injective f` are the same + idiom.) + + Naming it earns three specific things: + 1. it can be **quantified over** — `consecution_of_VC` below takes + `∀ B, VC P I B` as a hypothesis, which is unsayable without a name; + 2. it gives the automation a single fixed **head symbol** to unfold; + 3. it lets `VC_of_unknown` prove a whole class of blocks at once. + + Two details of the postcondition: + * `∀ B' ∈ P.succ B, …` is a **bounded quantifier**, not a folded + conjunction over a list. Then "instantiate at the successor actually + taken" is plain function application in `consecution_of_VC`, and a block + with no successors degenerates to `True` for free. + * putting the successor quantifier *inside* the VC is what makes the + obligations **per-block** rather than per-edge: `n` blocks, `n` + obligations, whatever the edge count. + + Degenerate cases fall out with no special handling. A block Crab marked + unreachable gets `False` as its invariant, so its own obligation holds + vacuously and the burden shifts to its predecessors, which must then show it + cannot be entered — exactly the claim Crab is making there. -/ +def VC (P : Cfg) (I : Label → Assn) (B : Label) : Prop := + ∀ σ : State, ⟦I B⟧ σ → wp (P.body B) (fun τ => ∀ B' ∈ P.succ B, ⟦I B'⟧ τ) σ + +/-- **Labels naming no block are free.** + + `∀ B, VC P I B` ranges over *every* `String`, not just the block names of + `P`, because labels are strings. Since `Cfg.body` and `Cfg.succ` are total + functions defaulting to `[]`, all those labels have an empty body and no + successors, and their obligation is trivial: `wp [] Q = Q`, and the + postcondition is a vacuous bounded quantifier. + + Proving it here once is what keeps the per-program bundle finite. -/ +theorem VC_of_unknown (P : Cfg) (I : Label → Assn) (B : Label) + (hb : P.body B = []) (hs : P.succ B = []) : VC P I B := by + -- Take the state and discard the invariant hypothesis (`_` names it away). + intro σ _ + -- Rewriting with `hb` empties the body, so `wp` is the identity; rewriting + -- with `hs` empties the successor list, so the goal is `∀ B' ∈ [], …`. + simp [hb, hs] + +/-- A label absent from the table gets the default. + + The companion to `table`'s definition, and what makes the bundling lemma + below program-independent. -/ +theorem table_not_mem {α : Type} (dflt : α) (tbl : List (Label × α)) (B : Label) + (h : B ∉ tbl.map Prod.fst) : table dflt tbl B = dflt := by + induction tbl with + | nil => rfl + | cons p rest ih => + obtain ⟨k, v⟩ := p + -- `B` is neither this key nor any key in the rest. + simp only [List.map_cons, List.mem_cons, not_or] at h + simp [table, h.1, ih h.2] + +/-- **Bundling the per-block obligations into the one `consecution_of_VC` wants.** + + `∀ B, VC P I B` quantifies over every `String`, but a program has finitely + many blocks. This splits that quantifier once and for all: a label either + names a block, and is covered by the finitely many obligations proved for + the program, or it does not, and `VC_of_unknown` applies. + + Proving it here is what keeps a generated file free of the `by_cases` chain + over label literals that a hand-written one needs. The generated file + supplies its list of labels and one `crab_vc` per block; the case analysis + joining them is this lemma, written once. -/ +theorem vc_all_of_blocks (P : Cfg) (I : Label → Assn) (labels : List Label) + (hbody : ∀ B, B ∉ labels → P.body B = []) + (hsucc : ∀ B, B ∉ labels → P.succ B = []) + (h : ∀ B ∈ labels, VC P I B) : ∀ B, VC P I B := by + intro B + by_cases hm : B ∈ labels + · exact h B hm + · exact VC_of_unknown _ _ _ (hbody B hm) (hsucc B hm) + +/-- **`consecution_of_VC` — the adapter lemma.** + + In English: *if every block's verification condition holds, then the + annotation is preserved by every single step of the machine.* + + This is the bridge between two statement shapes that cannot be bent to meet + each other. The soundness meta-theorem needs a statement about `Step` — + right for induction over reachability, opaque to `omega`. What a frontend can + generate is `VC B` — block-local, quantifier-light arithmetic — right for + `omega`, useless to the meta-theorem. + + Isolating the bridge in one lemma means: + * it is **program-independent**, so no generated file re-derives `Step` + inversion or applies `wp_sound`; + * it is the **automation boundary**; + * it **localises the coupling to the semantics** — once procedure calls + turn `Step` into an inductive with a call stack, this proof is the only + thing that changes. -/ +theorem consecution_of_VC (P : Cfg) (I : Label → Assn) (hvc : ∀ B, VC P I B) : + ∀ (L : Label) (σ : State) (L' : Label) (σ' : State), + ⟦I L⟧ σ → Step P (L, σ) (L', σ') → ⟦I L'⟧ σ' := by + -- `∀` ⇒ take the labels and states arbitrary; `→` ⇒ assume the two premises. + intro L σ L' σ' h₁ h₂ + -- `Step` is definitionally a conjunction, so we can split it: + -- hsucc : L' ∈ P.succ L (L' really is a successor) + -- hexec : Exec (P.body L) σ σ' (the body really runs σ to σ') + obtain ⟨hsucc, hexec⟩ := h₂ + -- The block's own verification condition, fed the invariant at L. + -- This is a statement purely about the *pre*-state σ. + have hwp := hvc L σ h₁ + -- `wp_sound` trades it, together with the execution, for a statement about + -- the *post*-state σ'. This is where the `Exec` premise is consumed. + have hpost := wp_sound hwp hexec + -- `hpost : ∀ B' ∈ P.succ L, ⟦I B'⟧ σ'`. Applying it to `L'` and the proof + -- that `L'` is a successor is *literally function application* — the payoff + -- of using a bounded quantifier rather than a folded conjunction. + exact hpost L' hsucc + +/-- **`chk_of_VC` — the assertion obligations come free with the VCs.** + + In English: *if every block's verification condition holds, then at every + assert in every block the invariant at that block's entry already implies the + asserted condition.* + + This is the second hypothesis `assert_safe` wants, and it turns out not to be + a separate hypothesis at all. `wpStmt` puts an assert's obligation into the + precondition as a conjunct, so it is inside `VC` already; `wp_split` is the + lemma that pulls it back out. All that is left here is to rewrite the block's + body into the split the caller asked about. + + Proving it once, here, is what keeps it out of generated files. Before this + lemma, a per-program file carried a `chk` theorem of its own — a case split + over labels, then a statement-by-statement peel of `pre` for each one. That + script existed only to re-derive, per program, something true of every + program. + + **What it rests on.** The `∧` in `wpStmt`'s assert clause, and nothing else. + Under the assume-flavoured `→` reading weighed in `Samples/Test1Foo.lean` the + obligation would not be in the VC to extract, this lemma would be false, and + generated files would need their `chk` back. That is the price of the + simplification, and it is confined to this lemma and `verified`. -/ +theorem chk_of_VC (P : Cfg) (I : Label → Assn) (hvc : ∀ B, VC P I B) : + ∀ (L : Label) (pre : List Stmt) (s : Stmt) (post : List Stmt), + P.body L = pre ++ s :: post → + ∀ σ : State, ⟦I L⟧ σ → wp pre (fun τ => s.obligation τ) σ := by + intro L pre s post hsplit σ hI + -- The block's own verification condition, fed the invariant at L. + have hwp := hvc L σ hI + -- Replace the body by the split the caller named, so `wp_split` applies. + rw [hsplit] at hwp + exact wp_split pre s post _ σ hwp + +end Crabber diff --git a/lean/Crabber/WP.lean b/lean/Crabber/WP.lean new file mode 100644 index 0000000..50bb18c --- /dev/null +++ b/lean/Crabber/WP.lean @@ -0,0 +1,200 @@ +import Crabber.Semantics +/- +# Crabber.WP — the weakest-precondition calculus + +**Not trusted.** `wp` is an ordinary Lean function and `wp_sound` is an ordinary +theorem; a bug here cannot make a false invariant provable, only make a true one +unprovable. That freedom is why we may pick whichever calculus automates best. + +Three were available, and backward reasoning wins on goal shape: + + * **Relational** — `∀ σ σ', ⟦I B⟧ σ → Exec (body B) σ σ' → ⟦I B'⟧ σ'`. Needs no + calculus and no soundness lemma at all, but leaves an existentially + quantified intermediate state per statement, and the goal shape depends on + the order in which `Exec` is inverted. + * **Forward (strongest postcondition)** — matches the direction the analyser + itself runs, which would make a failed obligation easy to compare against + Crab's computed state. But assignment has to existentially quantify the + overwritten value, so goals accumulate quantifiers. + * **Backward (weakest precondition)** — assignment is substitution, which + introduces nothing; `assume` becomes an implication; only `havoc` introduces + a quantifier, and over an integer rather than over states. Goals come out as + quantifier-free linear integer arithmetic, which `omega` decides. + +The postcondition here is a Lean predicate (`State → Prop`) rather than a +formula in the assertion language. That spares us defining capture-avoiding +substitution and proving its lemmas. The cost is that `wp` cannot be *computed* +with — a `∀ v : Int` postcondition is a perfectly good proposition and +completely unevaluable — so this calculus cannot be compiled into a checker that +runs somewhere without a Lean elaborator. Doing that would need a second `wp` +mapping data to data, plus a decidable entailment test proved sound. +-/ + +namespace Crabber + +/-- `wpStmt s Q` — the weakest precondition of a single statement. + + Read each clause as: "for `Q` to hold *after* `s`, what must hold before?" + + * `assign` — `Q` must hold of the updated state. This is substitution: + nothing is quantified, the state is just rewritten. + * `havoc` — `Q` must hold *whatever* value lands in `x`, so a `∀`. The + adversary picks `v`; we must survive all of them. + * `assume` — we may assume `c`, so it becomes the *antecedent* of an + implication. Everything is easier if `c` is false. + * `assert` — check **and** assume. The `∧` is the proof obligation (we owe + `c`); it is *not* an antecedent, because an assert we cannot discharge is + a failure, not a free pass. + + The six boolean clauses introduce no new shape: `boolAssignCst`, + `boolAssignVar`, `boolBinop` and `boolSelect` are substitution into the + boolean store, `boolAssume` is an implication, `boolAssert` is a conjunction. + Every one of them mirrors its `StmtExec` constructor exactly, which is why + the soundness proof below stays one term per case. Note that no boolean + statement introduces a quantifier: `havoc` remains the only clause that does, + and it quantifies over an integer. + + `@[simp]` generates one equation lemma per clause, so `simp` unfolds this + automatically on a concrete statement. -/ +@[simp] def wpStmt (s : Stmt) (Q : State → Prop) : State → Prop := + match s with + | .assign x e => fun σ => Q (σ.set x (e.eval σ)) + | .havoc x => fun σ => ∀ v : Int, Q (σ.set x v) + | .assume c => fun σ => c.holds σ → Q σ + | .assert c => fun σ => c.holds σ ∧ Q σ + | .boolAssignCst x c => fun σ => Q (σ.setBool x (c.check σ)) + | .boolAssignVar x y n => fun σ => Q (σ.setBool x (n ^^ σ.bools y)) + | .boolBinop x op y z => fun σ => Q (σ.setBool x (op.apply (σ.bools y) (σ.bools z))) + | .boolAssume y n => fun σ => (n ^^ σ.bools y) = true → Q σ + | .boolAssert y => fun σ => σ.bools y = true ∧ Q σ + | .boolSelect x c l r => + fun σ => Q (σ.setBool x (if σ.bools c then σ.bools l else σ.bools r)) + +/-- `wp ss Q` — the weakest precondition of a statement *list*. + + Defined by structural recursion, threading the postcondition **backwards** + through the body: the last statement is processed first. `wp [] Q = Q` is the + base case — an empty body demands exactly what you wanted afterwards. -/ +@[simp] def wp : List Stmt → (State → Prop) → State → Prop + | [], Q => Q + | s :: ss, Q => wpStmt s (wp ss Q) + +/-- **Single-statement soundness.** If the weakest precondition of `s` for `Q` + holds before, and `s` really steps σ to σ', then `Q` holds after. + + The proof is one case per `StmtExec` constructor, and each case is a single + term — which is the point: `wpStmt` was *defined* to make these match. -/ +theorem wpStmt_sound {s : Stmt} {Q : State → Prop} {σ σ' : State} + (hwp : wpStmt s Q σ) (hex : StmtExec s σ σ') : Q σ' := by + -- `cases hex` splits on how the step was built. In each branch Lean also + -- rewrites `s` and `σ'` to the constructor's shape, so `hwp` refines too. + cases hex with + | assign => exact hwp -- hwp : Q (σ.set x (e.eval σ)); that *is* the goal + | havoc v => exact hwp v -- hwp : ∀ v, Q (σ.set x v); instantiate at the v chosen + | assume h => exact hwp h -- hwp : c.holds σ → Q σ; feed it the assume's premise + | assert h => exact hwp.2 -- hwp : c.holds σ ∧ Q σ; `.2` is the right conjunct + -- The boolean half, case for case the same three shapes. + | boolAssignCst => exact hwp + | boolAssignVar => exact hwp + | boolBinop => exact hwp + | boolSelect => exact hwp + | boolAssume h => exact hwp h + | boolAssert h => exact hwp.2 + +/-- **`wp_sound` — the soundness of the calculus.** The lemma that discharges the + `Exec` premise, once and for all. + + In English: if the weakest precondition of a block body for `Q` holds in σ, + and the body can execute from σ to σ', then `Q` holds in σ'. + + Everything about the transition relation is consumed *here*. After this + point, every arrow appearing in a verification condition comes from an + `assume` in the program, never from `Exec`. + + The argument order — weakest precondition first, execution second — is what + reads best at the one place that calls it, the adapter lemma in `VC.lean`. + The induction is on the `Exec` derivation either way. -/ +theorem wp_sound {ss : List Stmt} {Q : State → Prop} {σ σ' : State} + (hwp : wp ss Q σ) (hex : Exec ss σ σ') : Q σ' := by + -- Induct on the *derivation* of `Exec ss σ σ'`: one case per constructor. + induction hex with + | nil => + -- Body was empty, so σ' = σ and `wp [] Q = Q`: `hwp` is literally the goal. + exact hwp + | cons hstep _hrest ih => + -- Body was `s :: ss`. `hwp : wpStmt s (wp ss Q) σ`. + -- Push it through the first statement to get `wp ss Q` at the + -- intermediate state, then hand that to the induction hypothesis. + exact ih (wpStmt_sound hwp hstep) + +/-! ## Extracting the assertion obligations from a weakest precondition + +The three lemmas below exist for one purpose: to prove, once, that a block's +verification condition *already contains* the obligation of every assert in that +block. That makes the `chk` hypothesis of `assert_safe` a consequence of the VCs +rather than something a generated file has to prove for itself — see +`chk_of_VC` in `VC.lean`. + +The reason it works is the `∧` in `wpStmt`'s `assert` clause: the obligation sits +in the precondition unconditionally, so it survives being pushed leftwards +through the statements before it. Under the alternative `→` reading discussed in +`Samples/Test1Foo.lean`, `wp_split` would be false and the obligations would have +to be generated separately again. That is the one thing this depends on. -/ + +/-- **`wpStmt` is monotone in its postcondition.** Ask for less afterwards, and + you need less beforehand. + + One case per constructor, and each is a single term. The four shapes recur: + substitution applies `h` to the updated state, `havoc` under the `∀`, + `assume` under the `→`, `assert` inside the right conjunct. -/ +theorem wpStmt_mono {s : Stmt} {Q R : State → Prop} (h : ∀ σ, Q σ → R σ) : + ∀ σ : State, wpStmt s Q σ → wpStmt s R σ := by + intro σ hwp + cases s with + | assign => exact h _ hwp + | havoc => exact fun v => h _ (hwp v) + | assume => exact fun hc => h _ (hwp hc) + | assert => exact ⟨hwp.1, h _ hwp.2⟩ + | boolAssignCst => exact h _ hwp + | boolAssignVar => exact h _ hwp + | boolBinop => exact h _ hwp + | boolSelect => exact h _ hwp + | boolAssume => exact fun hc => h _ (hwp hc) + | boolAssert => exact ⟨hwp.1, h _ hwp.2⟩ + +/-- Monotonicity for a whole body, by induction over it. -/ +theorem wp_mono {ss : List Stmt} {Q R : State → Prop} (h : ∀ σ, Q σ → R σ) : + ∀ σ : State, wp ss Q σ → wp ss R σ := by + induction ss with + | nil => exact fun σ hwp => h σ hwp + | cons _ _ ih => exact fun σ hwp => wpStmt_mono ih σ hwp + +/-- **A weakest precondition entails the first statement's own obligation.** + + `first | exact hwp.1 | exact trivial` rather than a case list: for the two + asserts `wpStmt` is a conjunction whose left half *is* the obligation, and + for every other statement the obligation is `True`. The order matters — + `trivial` would not close an assert's goal, and `.1` does not elaborate + against the other clauses' shapes. -/ +theorem wpStmt_obligation {s : Stmt} {Q : State → Prop} {σ : State} + (hwp : wpStmt s Q σ) : s.obligation σ := by + cases s <;> first | exact hwp.1 | exact trivial + +/-- **The extraction lemma.** If a body split as `pre ++ s :: post` has a + weakest precondition, then running just `pre` establishes `s`'s obligation. + + In other words: whatever the block was ultimately asked to achieve, getting + there entails discharging every assert on the way. Induction on `pre`, with + monotonicity doing the work of pushing the weakened postcondition back + through each preceding statement. -/ +theorem wp_split (pre : List Stmt) (s : Stmt) (post : List Stmt) + (Q : State → Prop) : + ∀ σ : State, wp (pre ++ s :: post) Q σ → wp pre (fun τ => s.obligation τ) σ := by + induction pre with + -- `pre` empty: the split's head *is* `s`, so this is `wpStmt_obligation`. + | nil => exact fun σ hwp => wpStmt_obligation hwp + -- `pre = p :: pre'`: both sides start with `wpStmt p`, and the induction + -- hypothesis is exactly the implication `wpStmt_mono` needs between them. + | cons _ _ ih => exact fun σ hwp => wpStmt_mono ih σ hwp + +end Crabber diff --git a/lean/CrabberJson.lean b/lean/CrabberJson.lean new file mode 100644 index 0000000..7f943a4 --- /dev/null +++ b/lean/CrabberJson.lean @@ -0,0 +1,25 @@ +/- +# CrabberJson — the frontend: crabber's JSON export, read into Lean + +Kept in a library of its own, imported by neither `Crabber` nor anything it +imports. Two reasons, both deliberate: + + * the proof library has a dependency footprint of zero and is built from core + datatypes only. Reading JSON needs `Lean` itself as a library, which is a + heavy import; confining it here keeps the trusted development untouched by + it; + * the split matches the trust boundary. `Crabber` says what CrabIR means and + proves things about it. `CrabberJson` only transcribes — and its output is + checked against its input rather than believed. + + Schema — the wire types, the JSON instances, and the conversion to Cfg/Assn + RoundTrip — reading a document back out and comparing, so a mistranslation is + visible rather than silent + Elab — `crab_program`, which loads an export while a file is elaborated + Samples/* — one file per analysed program: the loader line, then the proofs +-/ +import CrabberJson.Schema +import CrabberJson.RoundTrip +import CrabberJson.Elab +import CrabberJson.Samples.Test1Bar +import CrabberJson.Samples.TestBool1 diff --git a/lean/CrabberJson/Elab.lean b/lean/CrabberJson/Elab.lean new file mode 100644 index 0000000..39bae02 --- /dev/null +++ b/lean/CrabberJson/Elab.lean @@ -0,0 +1,247 @@ +import CrabberJson.RoundTrip +import Crabber +/- +# CrabberJson.Elab — `crab_program`, loading an export at elaboration time + + namespace MyProgram + crab_program "exports/test-1.json" cfg "bar" + +That one line reads the JSON while the file is being elaborated, converts it, +and adds the definitions a proof needs — `bodyTable`, `succTable`, `invTable`, +`labels`, `prog`, `inv` — as if they had been written out by hand. + +## Why a command rather than generated source text + +The alternative is a script that writes a `.lean` file. Both put the same term +in front of the kernel, but a generator adds a *printer* to the trusted path: +the JSON becomes Lean source, and nothing checks that the source says what the +JSON said. Here the data never becomes text. It is read, checked against the +document it came from (`CrabberJson.RoundTrip`), and handed to the elaborator +as a term. What stays trusted is the reader, and the reader has an inverse. + +## What is trusted here, and what is not + +The definitions this command adds are **data**, and data is trusted: if the +table said something other than what Crab analysed, the theorems below it would +be about the wrong program. That is the exposure the round-trip check addresses. + +The *proofs* in a file using this command are not trusted at all. `crab_vc` may +be as unprincipled as convenient — the kernel checks what it produces. + +## One practical caveat + +Lean does not track a file read during elaboration as a build dependency, so +editing the JSON will not by itself trigger a rebuild of the module that loads +it. Re-export and rebuild from clean when the analysed program changes. +-/ + +namespace CrabberJson + +open Lean Elab Command Term + +/-! The program AST has to be convertible into a Lean term. `deriving instance` +works from outside a type's own module, which is what keeps `Lean` out of the +trusted core's imports: `Crabber.Syntax` never mentions any of this. -/ + +deriving instance ToExpr for Crabber.CmpOp +deriving instance ToExpr for Crabber.BoolOp +deriving instance ToExpr for Crabber.LinExp +deriving instance ToExpr for Crabber.LinCon +deriving instance ToExpr for Crabber.Atom +deriving instance ToExpr for Crabber.Stmt + +/-- Add a definition holding a spliced value. + + Built as an `Expr` and installed with `addDecl` rather than by rendering a + term and re-parsing it. `ToExpr` supplies both the value and its type, so + there is no place for a printer to disagree with what was read. -/ +private def addValueDef {α : Type} [ToExpr α] (name : Name) (v : α) + (simpSet : Bool) : CommandElabM Unit := do + let full := (← getCurrNamespace) ++ name + -- `.regular 0`, not `.abbrev`: an abbreviation is unfolded eagerly, which + -- would inline an entire block table into every definition mentioning it. + -- `simp` unfolds these through the `crab` attribute's equation lemma instead, + -- which does not depend on the reducibility hint. + liftCoreM do + addDecl (.defnDecl + { name := full, levelParams := [], type := toTypeExpr α, value := toExpr v, + hints := .regular 0, safety := .safe }) + -- A declaration added this way has no equation lemmas until realizations are + -- switched on for it. Without this the definition exists but `simp` cannot + -- unfold it, which is the whole reason it is here. + enableRealizationsForConst full + -- The tables must be in the set `crab_vc` unfolds; `labels` must not be, or + -- it would be unfolded in goals that are about the label list itself. + if simpSet then + elabCommand (← `(command| attribute [crab] $(mkIdent name))) + +/-- **`crab_program "file.json" cfg "name"`** — load one analysed cfg. + + The path is relative to the directory `lake` was invoked from. The named cfg + must exist in the document; a document holds every cfg of the analysed file, + so `samples/test-1.crabir` offers both `foo` and `bar`. + + Fails, with the reason, if the document cannot be read, if reading it is not + faithful to the input, or if the program uses constructs outside the + modelled fragment — procedure calls, casts, arithmetic binops and arrays are + all rejected by name. Booleans are *not*: the six boolean statements are + modelled, and `samples/test-bool-1.crabir` is the sample that exercises + them. -/ +syntax (name := crabProgram) "crab_program " str " cfg " str : command + +@[command_elab crabProgram] +def elabCrabProgram : CommandElab := fun stx => do + match stx with + | `(command| crab_program $pathStx:str cfg $cfgStx:str) => do + let path := pathStx.getString + let text ← + try IO.FS.readFile path + catch e => throwErrorAt pathStx m!"cannot read '{path}': {e.toMessageData}" + match programOfString text cfgStx.getString with + | .error e => throwErrorAt stx e + | .ok p => + -- Tabulated over the block list, so the tables and `labels` cannot + -- describe different sets of blocks. + addValueDef `bodyTable (p.labels.map fun l => (l, p.cfg.body l)) true + addValueDef `succTable (p.labels.map fun l => (l, p.cfg.succ l)) true + addValueDef `invTable (p.labels.map fun l => (l, p.inv l)) true + addValueDef `labels p.labels false + -- `prog` and `inv` are not data: they turn the tables into the total + -- functions `Cfg` requires, via the library's `table`. + -- + -- Every name here goes through `mkIdent`. An identifier written literally + -- inside a quotation carries macro scopes — Lean's hygiene, which stops a + -- macro from capturing names at the use site — and would therefore not + -- refer to the plainly-named declarations added just above, nor be + -- referable by the proofs that follow. `mkIdent` builds a scope-free name, + -- which is what is wanted precisely because these *are* meant to be + -- visible to the surrounding file. + let progId := mkIdent `prog + let invId := mkIdent `inv + let bodyId := mkIdent `bodyTable + let succId := mkIdent `succTable + let invTId := mkIdent `invTable + -- `noncomputable` because these exist only to be reasoned about. A `Cfg` + -- stores its blocks as *functions* of the label, and asking the code + -- generator to build one from the tables is both pointless — no proof ever + -- runs it — and, on this toolchain, enough to crash it. The tables + -- themselves stay computable, which is what a future reflective checker + -- would need. + elabCommand (← `(command| + @[crab] noncomputable def $progId : Crabber.Cfg := + { entry := $(quote p.entry) + body := Crabber.table [] $bodyId + succ := Crabber.table [] $succId })) + elabCommand (← `(command| + @[crab] noncomputable def $invId : Crabber.Label → Crabber.Assn := + Crabber.table Crabber.Assn.bot $invTId)) + | _ => throwUnsupportedSyntax + +/-! ## `crab_verify` — the proofs, for a program `crab_program` has loaded + + crab_program "exports/test-1.json" cfg "bar" + crab_verify + +Adds `body_keys`, `succ_keys`, `vc_all`, `initiation` and the theorem that +bundles them. It is a second command rather than part of `crab_program` so +that a file can load a program and then reason about it by hand — which is what +the worked example under `Samples/` does. + +**Why the proofs are generated here rather than written as reusable tactics.** +Nothing in these scripts depends on the program: none of them counts blocks, and +the case analysis over labels is `repeat'` over however many alternatives `simp` +produced, so three blocks and thirty take the same script. They could therefore +be tactics in the library — except that they must mention `prog`, `inv`, +`labels` and the tables, which live in the *generated file's* namespace and are +invisible to a macro defined elsewhere. Passing seven identifiers to every +tactic call is the alternative, and it is worse to read. Here the elaborator has +already built each name with `mkIdent`, so it can splice them directly. + +**These proofs are not trusted.** A tactic that goes wrong fails to find a proof, +or produces one the kernel rejects; it cannot produce a false theorem. What is +trusted is the data `crab_program` installed above. + +**When it fails.** The invariants may genuinely not be inductive; the arithmetic +may be beyond `omega`; the entry invariant may not be ⊤; or the program may have +an assertion that really can fail, which under the current reading of `assert` +makes a block's verification condition false rather than merely hard. A failure +here is never by itself evidence that Crab is wrong. -/ +syntax (name := crabVerify) "crab_verify" : command + +@[command_elab crabVerify] +def elabCrabVerify : CommandElab := fun _ => do + -- Same `mkIdent` discipline as above: these have to name the declarations the + -- surrounding file can see, so they must carry no macro scopes. + let progId := mkIdent `prog + let invId := mkIdent `inv + let labelsId := mkIdent `labels + let bodyId := mkIdent `bodyTable + let succId := mkIdent `succTable + let invTId := mkIdent `invTable + let bodyKeysId := mkIdent `body_keys + let succKeysId := mkIdent `succ_keys + let vcAllId := mkIdent `vc_all + let initId := mkIdent `initiation + let resultId := mkIdent `verified_program + + -- The tables and `labels` are built from one list, so these hold by + -- computation: both sides are literals. + elabCommand (← `(command| + theorem $bodyKeysId : List.map Prod.fst $bodyId = $labelsId := rfl)) + elabCommand (← `(command| + theorem $succKeysId : List.map Prod.fst $succId = $labelsId := rfl)) + + -- Every label's obligation: the blocks that exist, then every other string. + elabCommand (← `(command| + theorem $vcAllId : ∀ B : Crabber.Label, Crabber.VC $progId $invId B := by + refine Crabber.vc_all_of_blocks $progId $invId $labelsId ?_ ?_ ?_ + · intro B h + show Crabber.table [] $bodyId B = [] + exact Crabber.table_not_mem [] $bodyId B ($bodyKeysId ▸ h) + · intro B h + show Crabber.table [] $succId B = [] + exact Crabber.table_not_mem [] $succId B ($succKeysId ▸ h) + · intro B hB + simp only [$labelsId:ident, List.mem_cons, List.not_mem_nil, or_false] at hB + repeat' (rcases hB with rfl | hB) + -- `rfl` written inside a quotation carries macro scopes, so `rcases` + -- reads it as a fresh name rather than as the substitution pattern: the + -- equation lands in the context instead of being applied. `subst_vars` + -- applies whatever equations ended up there, which is what was meant. + all_goals (try subst_vars) + all_goals crab_vc)) + + -- The entry obligation. `InitState` constrains nothing, so this goes through + -- exactly when Crab claimed ⊤ at the entry block. + elabCommand (← `(command| + theorem $initId : ∀ σ : Crabber.State, Crabber.InitState $progId σ → + Crabber.Assn.holds ($invId ($progId).entry) σ := by + intro σ _ + simp only [$progId:ident, $invId:ident, $invTId:ident, Crabber.table, if_pos] + first + | exact Crabber.Assn.holds_top σ + -- `all_goals omega`, not `omega`: an entry invariant that is trivially + -- true without being literally ⊤ -- `[[0 ≤ 0]]`, which the octagon + -- domain exports where the interval domain exports an empty conjunction + -- -- is closed by `simp` alone, and `omega` would then fail for want of + -- a goal. + | (simp [Crabber.Assn.holds, Crabber.Conj.holds, Crabber.LinCon.holds, + Crabber.LinCon.lhs, Crabber.LinExp.eval] + all_goals omega))) + + -- The assertion obligations are *not* generated. `wpStmt` puts an assert's + -- obligation inside its block's verification condition, so `Crabber.chk_of_VC` + -- extracts it from `vc_all` for every program at once. What used to stand here + -- was a per-program case split over labels followed by a statement-by-statement + -- peel of the prefix — a script that re-derived, once per program, something + -- true of all of them. See `chk_of_VC` for the one assumption it rests on. + + -- The result. `verified` chains the adapter lemma, the extraction lemma, the + -- inductive-assertion meta-theorem and assertion safety, so nothing above + -- mentions `Step`, `Reachable` or `wp_sound`. + elabCommand (← `(command| + theorem $resultId : + Crabber.InvariantOf $progId $invId ∧ ¬ Crabber.AssertFails $progId := + Crabber.verified $progId $invId $initId $vcAllId)) + +end CrabberJson diff --git a/lean/CrabberJson/RoundTrip.lean b/lean/CrabberJson/RoundTrip.lean new file mode 100644 index 0000000..25e816f --- /dev/null +++ b/lean/CrabberJson/RoundTrip.lean @@ -0,0 +1,102 @@ +import CrabberJson.Schema +/- +# CrabberJson.RoundTrip — reading the export back out again + +The reader in `Schema.lean` is trusted: nothing proves that the `Cfg` it +produces is the graph Crab analysed. This module supplies the check that makes +a mistranslation visible instead of silent. + +The idea is only that a faithful reader has an inverse. Read the document into +the wire types, write those back out, and compare against what was read. A +reader that dropped a statement, misparsed a coefficient, or ignored a key +cannot reproduce the input, because the information needed to do so is no longer +there. The comparison is on `Json` values rather than on text, so key ordering +and whitespace are irrelevant. + +What this does **not** check: that the wire types mean what the conversion to +`Cfg`/`Assn` says they mean. Dropping the bitwidth, reading `1·b = 1` as a claim +about the boolean store, discarding an assertion's source location — those are +choices argued for where they are made, and no round trip can validate them. +What it covers is the mechanical half, which is the half where a silent slip is +plausible. + +Nor does it apply to documents this library refuses outright. A program using +statements outside the modelled fragment fails at the reading step, loudly; +there is nothing to round-trip. That is the intended behaviour, not a gap. +-/ + +namespace CrabberJson + +open Lean (Json toJson fromJson?) + +/-- Where two JSON documents first diverge, with a little context from each. + + Both sides are printed in Lean's canonical compressed form — object keys + sorted, no whitespace — so the offset is a genuine locator rather than an + artifact of formatting. -/ +def firstDifference (a b : Json) : String := + let sa := a.compress + let sb := b.compress + let la := sa.toList + let lb := sb.toList + let rec go (xs ys : List Char) (n : Nat) : Nat := + match xs, ys with + | x :: xs', y :: ys' => if x == y then go xs' ys' (n + 1) else n + | _, _ => n + let n := go la lb 0 + let window (s : String) : String := + let start := if n < 30 then 0 else n - 30 + String.ofList ((s.toList.drop start).take 90) + s!"first difference at offset {n}\n read : …{window sb}…\n input: …{window sa}…" + +/-- Read a document and confirm the reader is faithful to it. + + Returns the document on success, so a caller that wants both the check and + the data does not parse twice. -/ +def readChecked (raw : Json) : Except String WDoc := do + let d ← docOfJson raw + let back := toJson d + if back == raw then + return d + else + throw s!"the JSON reader is not faithful to this document: writing the parsed \ + form back out does not reproduce the input. Something was dropped or \ + misread.\n{firstDifference raw back}" + +/-- Parse one CFG and confirm the parse reproduces the JSON it came from. + + This is where the round trip earns its keep. `readChecked` above covers the + document's header, but the header is small and mostly carried verbatim; the + statements, the successors and the invariants are what a mistranslation + would silently corrupt, and they all live here. + + Doing it per CFG rather than for the whole array is what stops one CFG the + library cannot model from condemning its neighbours. Only the CFG actually + being verified has to parse. -/ +def cfgChecked (raw : Json) : Except String WCfg := do + let c : WCfg ← fromJson? raw + let back := toJson c + if back == raw then + return c + else + throw s!"the JSON reader is not faithful to this cfg: writing the parsed \ + form back out does not reproduce the input. Something was dropped \ + or misread.\n{firstDifference raw back}" + +/-- Read one named cfg from a document's text, checking both round trips on the + way. This is the entry point a generated file should use: it is the only + path that both produces a `Program` and validates the reading of it. -/ +def programOfString (text : String) (cfgName : String) : Except String Program := do + let raw ← Json.parse text + let d ← readChecked raw + let cfgRaw ← d.rawCfg cfgName + let c ← cfgChecked cfgRaw + c.toProgram + +/-- The names of every cfg in a document, without parsing any of them. -/ +def cfgNamesOfString (text : String) : Except String (List String) := do + let raw ← Json.parse text + let d ← readChecked raw + return d.cfgNames + +end CrabberJson diff --git a/lean/CrabberJson/Samples/Test1Bar.lean b/lean/CrabberJson/Samples/Test1Bar.lean new file mode 100644 index 0000000..e078277 --- /dev/null +++ b/lean/CrabberJson/Samples/Test1Bar.lean @@ -0,0 +1,115 @@ +import CrabberJson.Elab +/- +# `samples/test-1.crabir`, cfg `bar`, proved from the JSON export + +The same result as the hand-transcribed `Crabber.Samples.Test1Bar`, with the +program and the invariants **read from Crab's export** instead of typed in. + + build/crabber samples/test-1.crabir -d int --print-invariants-to-json \ + lean/CrabberJson/Samples/test-1.json + +The source program is a counting loop: + + start: y := 0 goto loop + loop: y := y + 1 if (y <= 9) goto loop else goto out + out: assert(y == 10) + +The CFG below is the one Crab **analysed**, not the source text: the conditional +has been compiled into the two `edge-loop-*` blocks carrying the guards, which is +why the export walks the analyser's final graph. + +Everything specific to this program is the one `crab_program` line. What follows +is the same for every program of this shape, which is the point: the per-program +artifact is data, and the proofs below are a fixed recipe. +-/ + +namespace CrabberJson +namespace Test1Bar + +open Crabber + +/-! ## The program and the invariants + +Reads `CrabberJson/Samples/test-1.json` while this file is elaborated, checks that reading +it is faithful to the document, and defines `bodyTable`, `succTable`, +`invTable`, `labels`, `prog` and `inv`. Nothing became source text on the way. -/ + +crab_program "CrabberJson/Samples/test-1.json" cfg "bar" + +/-! ## The per-block obligations + +`vc_all_of_blocks` reduces "every label's obligation holds" to "every label *in +the block list*", which is a finite check. Its two side conditions say the +tables and `labels` agree about which blocks exist — true by construction, since +the loader builds all three from the same list, and provable by `rfl` because +both sides are literals. -/ + +theorem body_keys : bodyTable.map Prod.fst = labels := rfl +theorem succ_keys : succTable.map Prod.fst = labels := rfl + +/-- Every label's verification condition. + + The five blocks are discharged by `crab_vc` — unfold to arithmetic, call + `omega` — and every other string by `table_not_mem`, which says a label the + tables do not mention gets the empty body and no successors. -/ +theorem vc_all : ∀ B : Label, VC prog inv B := by + refine vc_all_of_blocks prog inv labels ?_ ?_ ?_ + -- `prog.body` *is* `table [] bodyTable`, but `show` is needed to make the + -- projection through the structure literal explicit before applying the lemma. + · intro B h + show table [] bodyTable B = [] + exact table_not_mem [] bodyTable B (body_keys ▸ h) + · intro B h + show table [] succTable B = [] + exact table_not_mem [] succTable B (succ_keys ▸ h) + · intro B hB + simp only [labels, List.mem_cons, List.not_mem_nil, or_false] at hB + rcases hB with rfl | rfl | rfl | rfl | rfl <;> crab_vc + +/-! ## The entry obligation -/ + +/-- Every initial state satisfies the invariant at the entry block. Crab claims + ⊤ at `start`, so this is immediate — though not vacuous in general. -/ +theorem initiation : ∀ σ : State, InitState prog σ → ⟦inv prog.entry⟧ σ := by + intro σ _ + simp only [prog, inv, invTable, table, if_pos] + exact Assn.holds_top σ + +/-! ## The assertion obligation + +At every statement in every block, the invariant at that block's entry must imply +that statement's obligation after the statements preceding it. Where the +statement is not an assert the obligation is `True`. + +This used to be the longest proof in the file: a case split over the five +blocks, then an attempt to refute the split `pre ++ s :: post` in each of the +four that contain no assert. All of it was redundant. `wpStmt` puts an assert's +obligation into the precondition as a conjunct, so it is already inside the +verification conditions `vc_all` proved above, and `chk_of_VC` is the general +lemma that takes it back out. + +The generated form of this file (`crab_verify`) no longer emits anything here at +all, for the same reason. -/ + +theorem chk : ∀ (L : Label) (pre : List Stmt) (s : Stmt) (post : List Stmt), + prog.body L = pre ++ s :: post → + ∀ σ : State, ⟦inv L⟧ σ → wp pre (fun τ => s.obligation τ) σ := + chk_of_VC prog inv vc_all + +/-! ## The result -/ + +/-- **The theorem.** + + *The invariants Crab inferred for cfg `bar` of `samples/test-1.crabir` under + `-d int` are genuine invariants of the program, and the program's assertion + can never fail* — with the program and the invariants taken from Crab's own + JSON export rather than transcribed by hand. + + Trusted for this claim: the Lean semantics of CrabIR, Crab's exporter, and + the JSON reader — whose faithfulness to the document was checked when this + file was elaborated. Not trusted, because proved: everything else. -/ +theorem bar_verified : InvariantOf prog inv ∧ ¬ AssertFails prog := + verified prog inv initiation vc_all + +end Test1Bar +end CrabberJson diff --git a/lean/CrabberJson/Samples/TestBool1.lean b/lean/CrabberJson/Samples/TestBool1.lean new file mode 100644 index 0000000..ae2f5cc --- /dev/null +++ b/lean/CrabberJson/Samples/TestBool1.lean @@ -0,0 +1,128 @@ +import CrabberJson.Elab +/- +# `samples/test-bool-1.crabir`, proved from the JSON export + +The boolean fragment, end to end. Both cfgs of the sample are loaded from Crab's +own export: + + build/crabber samples/test-bool-1.crabir -d int --print-invariants-to-json \ + lean/CrabberJson/Samples/test-bool-1.json + +`safe` is the one that verifies. `unsafe` is its companion with the assertion +negated, and its failing block's verification condition is *refuted* below rather +than merely left unproved — the boolean counterpart of `test-1`'s `foo`/`bar` +pair, and the check that this fragment is not vacuous. + +## Why this sample rather than `test-6` + +`samples/test-6.crabir` also uses booleans, and cannot be checked: it reaches +them through `trunc`, and integer casts are not modelled. `test-bool-1` avoids +casts deliberately, so every statement in it is one the semantics interprets. + +## What `safe` exercises + +Every boolean statement Crab's parser can emit: + + * `bool_assign_cst` — `b0 := (x == 10)`, the one statement that reads the + integer store and writes the boolean one; + * `bool_binop` — all three of `and`, `or`, `xor`; + * `bool_assign_var` — both polarities, since `b3 := not(b2)` compiles to the + plain form with `negated` set rather than to a statement of its own; + * `bool_assume` — a whole block whose only content is `assume(b2)`; + * `bool_assert` — four of them, in the final block. + +`bool_select` is the one member of the group with no coverage here, because +crabber's parser cannot produce one; it arrives only from LLVM-style frontends. + +Two of the assertions are worth noting. `b4 := b0 or not(b0 and b1)` is a +tautology, and `b5 := b0 xor not(b0 and b1)` is one too given `b1`; Crab gets +both right, and the proofs go through as ordinary boolean reasoning rather than +through any 0/1 arithmetic — booleans never enter `omega`'s goals at all. +-/ + +namespace CrabberJson +namespace TestBool1 + +open Crabber + +/-! ## `safe` — the cfg that verifies + +Reads the export while this file is elaborated, checks that reading it is +faithful to the document, and defines `bodyTable`, `succTable`, `invTable`, +`labels`, `prog` and `inv`. `crab_verify` then proves the entry obligation and +every block's verification condition, and bundles them. + +Nothing here is specific to booleans: the same two lines serve any program in +the modelled fragment. That is the point of the exercise. -/ + +namespace Safe + +crab_program "CrabberJson/Samples/test-bool-1.json" cfg "safe" +crab_verify + +/-- **The theorem**, restated under a name that says what it is. + + *The invariants Crab inferred for cfg `safe` are genuine invariants, and none + of its four boolean assertions can fail.* + + `verified_program` is what `crab_verify` generated; this is an alias, so that + the claim is greppable and so that a reader arriving at the bottom of the + file does not have to know the generated name. -/ +theorem safe_verified : InvariantOf prog inv ∧ ¬ AssertFails prog := + verified_program + +end Safe + +/-! ## `unsafe` — the cfg whose assertion is false + +Same program, asserting `not(y == 10)` where `y` is 10. Crab reports the +assertion as an error, and the source marks it `EXPECT_EQ(false, …)`. + +Only `crab_program` is used here: `crab_verify` would fail, because block `end`'s +verification condition is false and no tactic can prove it. Instead the negation +is proved outright, which is a stronger and much more informative statement than +"the tactic did not succeed". + +Note what this separates. Crab's *invariants* for `unsafe` are perfectly sound — +it correctly infers `c1 = false` at `end`. It is the *assertion* that fails, and +because `wpStmt` carries an assert's obligation inside its block's verification +condition, that one false assertion is what makes the block's VC unprovable. The +same coupling is discussed at length in `Crabber.Samples.Test1Foo`; this is its +boolean instance. -/ + +namespace Unsafe + +crab_program "CrabberJson/Samples/test-bool-1.json" cfg "unsafe" + +/-- A state matching what Crab inferred at `end`: `y = 10`, `c0` true, and every + other boolean — `c1` among them — false. + + `fun v => v == "c0"` is the boolean store as a predicate on names; `==` is + `String`'s decidable equality returning `Bool`, which is exactly the type the + field wants. The integer store is the constant 10, since only `y` is read. -/ +def sigmaBad : State := ⟨fun _ => 10, fun v => v == "c0"⟩ + +/-- **Block `end`'s verification condition is false.** + + In English: *there is a state satisfying the invariant Crab printed at `end` + in which the asserted boolean `c1` is false* — so no proof of + `VC prog inv "end"` exists. + + This is not a limitation of `omega` or of `crab_vc`. The invariant Crab + printed at `end` literally contains `c1 = false`, and the block literally + asserts `c1`. Crab reports the assertion as an error; Lean agrees. -/ +theorem vc_end_false : ¬ VC prog inv "end" := by + -- Assume the VC held, and instantiate it at the offending state. + intro h + have hpre : ⟦inv "end"⟧ sigmaBad := by + simp [crab, table, sigmaBad, Assn.holds, Conj.holds, Atom.holds, + LinCon.holds, LinCon.lhs, LinExp.eval] + -- `h sigmaBad hpre` unfolds to `sigmaBad.bools "c1" = true ∧ True`, and the + -- left conjunct is `("c1" == "c0") = true`, which reduces to `False`. + have hbad := h sigmaBad hpre + simp [crab, table, sigmaBad] at hbad + +end Unsafe + +end TestBool1 +end CrabberJson diff --git a/lean/CrabberJson/Samples/test-1.json b/lean/CrabberJson/Samples/test-1.json new file mode 100644 index 0000000..50151ea --- /dev/null +++ b/lean/CrabberJson/Samples/test-1.json @@ -0,0 +1,399 @@ +{ + "schema": 1, + "kind": "invariants", + "source": {"name": "/Users/jorge/Repos/crabber/samples/test-1.crabir"}, + "options": {"simplify_cfg": false}, + "analysis": { + "domain": "int", + "widening_delay": 2, + "descending_iters": 1, + "thresholds": 0, + "checker": true + }, + "cfgs": [ + { + "name": "foo", + "declaration": { + "inputs": [], + "outputs": [] + }, + "entry": "start", + "exit": "out", + "blocks": [ + { + "label": "edge-loop-loop", + "stmts": [ + { + "stmt": "assume", + "cond": { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "x"] + ], + "const": "9" + } + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "x"] + ], + "const": "-1" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "x"] + ], + "const": "10" + } + ] + ] + }, + "succs": ["loop"] + }, + { + "label": "edge-loop-out", + "stmts": [ + { + "stmt": "assume", + "cond": { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "x"] + ], + "const": "-10" + } + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "x"] + ], + "const": "-1" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "x"] + ], + "const": "10" + } + ] + ] + }, + "succs": ["out"] + }, + { + "label": "loop", + "stmts": [ + { + "stmt": "assign", + "rhs": { + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "x"] + ], + "const": "1" + }, + "lhs": {"name": "x", "type": {"kind": "int", "bitwidth": 32}} + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "x"] + ], + "const": "0" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "x"] + ], + "const": "9" + } + ] + ] + }, + "succs": ["edge-loop-loop", "edge-loop-out"] + }, + { + "label": "out", + "stmts": [ + { + "stmt": "assert", + "cond": { + "op": "!=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "x"] + ], + "const": "10" + }, + "loc": {"file": "no-filename", "line": 17, "col": 0, "id": 0} + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "x"] + ], + "const": "-10" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "x"] + ], + "const": "10" + } + ] + ] + }, + "succs": [] + }, + { + "label": "start", + "stmts": [ + { + "stmt": "assign", + "rhs": { + "type": null, + "terms": [], + "const": "0" + }, + "lhs": {"name": "x", "type": {"kind": "int", "bitwidth": 32}} + } + ], + "invariant": { + "kind": "true" + }, + "succs": ["loop"] + } + ] + }, + { + "name": "bar", + "declaration": { + "inputs": [], + "outputs": [] + }, + "entry": "start", + "exit": "out", + "blocks": [ + { + "label": "edge-loop-loop", + "stmts": [ + { + "stmt": "assume", + "cond": { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "y"] + ], + "const": "9" + } + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "y"] + ], + "const": "-1" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "y"] + ], + "const": "10" + } + ] + ] + }, + "succs": ["loop"] + }, + { + "label": "edge-loop-out", + "stmts": [ + { + "stmt": "assume", + "cond": { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "y"] + ], + "const": "-10" + } + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "y"] + ], + "const": "-1" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "y"] + ], + "const": "10" + } + ] + ] + }, + "succs": ["out"] + }, + { + "label": "loop", + "stmts": [ + { + "stmt": "assign", + "rhs": { + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "y"] + ], + "const": "1" + }, + "lhs": {"name": "y", "type": {"kind": "int", "bitwidth": 32}} + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "y"] + ], + "const": "0" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "y"] + ], + "const": "9" + } + ] + ] + }, + "succs": ["edge-loop-loop", "edge-loop-out"] + }, + { + "label": "out", + "stmts": [ + { + "stmt": "assert", + "cond": { + "op": "=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "y"] + ], + "const": "10" + }, + "loc": {"file": "no-filename", "line": 27, "col": 0, "id": 1} + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "y"] + ], + "const": "-10" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "y"] + ], + "const": "10" + } + ] + ] + }, + "succs": [] + }, + { + "label": "start", + "stmts": [ + { + "stmt": "assign", + "rhs": { + "type": null, + "terms": [], + "const": "0" + }, + "lhs": {"name": "y", "type": {"kind": "int", "bitwidth": 32}} + } + ], + "invariant": { + "kind": "true" + }, + "succs": ["loop"] + } + ] + } + ], + "checks": [ + {"file": "no-filename", "line": 17, "col": 0, "id": 0, "result": "warning"}, + {"file": "no-filename", "line": 27, "col": 0, "id": 1, "result": "safe"} + ] +} diff --git a/lean/CrabberJson/Samples/test-bool-1.json b/lean/CrabberJson/Samples/test-bool-1.json new file mode 100644 index 0000000..fc12301 --- /dev/null +++ b/lean/CrabberJson/Samples/test-bool-1.json @@ -0,0 +1,701 @@ +{ + "schema": 1, + "kind": "invariants", + "source": {"name": "samples/test-bool-1.crabir"}, + "options": {"simplify_cfg": false}, + "analysis": { + "domain": "int", + "widening_delay": 2, + "descending_iters": 1, + "thresholds": 0, + "checker": true + }, + "cfgs": [ + { + "name": "safe", + "declaration": { + "inputs": [], + "outputs": [] + }, + "entry": "start", + "exit": "end", + "blocks": [ + { + "label": "edge-loop-loop", + "stmts": [ + { + "stmt": "assume", + "cond": { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "x"] + ], + "const": "9" + } + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "x"] + ], + "const": "-1" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "x"] + ], + "const": "10" + } + ] + ] + }, + "succs": ["loop"] + }, + { + "label": "edge-loop-post", + "stmts": [ + { + "stmt": "assume", + "cond": { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "x"] + ], + "const": "-10" + } + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "x"] + ], + "const": "-1" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "x"] + ], + "const": "10" + } + ] + ] + }, + "succs": ["post"] + }, + { + "label": "end", + "stmts": [ + { + "stmt": "bool_assert", + "cond": {"name": "b2", "type": {"kind": "bool"}}, + "loc": {"file": "no-filename", "line": 39, "col": 0, "id": 0} + }, + { + "stmt": "bool_assert", + "cond": {"name": "b4", "type": {"kind": "bool"}}, + "loc": {"file": "no-filename", "line": 40, "col": 0, "id": 1} + }, + { + "stmt": "bool_assert", + "cond": {"name": "b5", "type": {"kind": "bool"}}, + "loc": {"file": "no-filename", "line": 41, "col": 0, "id": 2} + }, + { + "stmt": "bool_assert", + "cond": {"name": "b6", "type": {"kind": "bool"}}, + "loc": {"file": "no-filename", "line": 42, "col": 0, "id": 3} + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "x"] + ], + "const": "-10" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "x"] + ], + "const": "10" + }, + { + "op": "=", + "type": {"kind": "bool"}, + "terms": [ + ["1", "b0"] + ], + "const": "1" + }, + { + "op": "=", + "type": {"kind": "bool"}, + "terms": [ + ["1", "b1"] + ], + "const": "1" + }, + { + "op": "=", + "type": {"kind": "bool"}, + "terms": [ + ["1", "b2"] + ], + "const": "1" + }, + { + "op": "=", + "type": {"kind": "bool"}, + "terms": [ + ["1", "b3"] + ], + "const": "0" + }, + { + "op": "=", + "type": {"kind": "bool"}, + "terms": [ + ["1", "b4"] + ], + "const": "1" + }, + { + "op": "=", + "type": {"kind": "bool"}, + "terms": [ + ["1", "b5"] + ], + "const": "1" + }, + { + "op": "=", + "type": {"kind": "bool"}, + "terms": [ + ["1", "b6"] + ], + "const": "1" + } + ] + ] + }, + "succs": [] + }, + { + "label": "guard", + "stmts": [ + { + "stmt": "bool_assume", + "cond": {"name": "b2", "type": {"kind": "bool"}}, + "negated": false + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "x"] + ], + "const": "-10" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "x"] + ], + "const": "10" + }, + { + "op": "=", + "type": {"kind": "bool"}, + "terms": [ + ["1", "b0"] + ], + "const": "1" + }, + { + "op": "=", + "type": {"kind": "bool"}, + "terms": [ + ["1", "b1"] + ], + "const": "1" + }, + { + "op": "=", + "type": {"kind": "bool"}, + "terms": [ + ["1", "b2"] + ], + "const": "1" + }, + { + "op": "=", + "type": {"kind": "bool"}, + "terms": [ + ["1", "b3"] + ], + "const": "0" + }, + { + "op": "=", + "type": {"kind": "bool"}, + "terms": [ + ["1", "b4"] + ], + "const": "1" + }, + { + "op": "=", + "type": {"kind": "bool"}, + "terms": [ + ["1", "b5"] + ], + "const": "1" + }, + { + "op": "=", + "type": {"kind": "bool"}, + "terms": [ + ["1", "b6"] + ], + "const": "1" + } + ] + ] + }, + "succs": ["end"] + }, + { + "label": "loop", + "stmts": [ + { + "stmt": "assign", + "rhs": { + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "x"] + ], + "const": "1" + }, + "lhs": {"name": "x", "type": {"kind": "int", "bitwidth": 32}} + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "x"] + ], + "const": "0" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "x"] + ], + "const": "9" + } + ] + ] + }, + "succs": ["edge-loop-loop", "edge-loop-post"] + }, + { + "label": "post", + "stmts": [ + { + "stmt": "bool_assign_cst", + "cst_kind": "linear", + "rhs": { + "op": "=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "x"] + ], + "const": "10" + }, + "lhs": {"name": "b0", "type": {"kind": "bool"}} + }, + { + "stmt": "bool_assign_cst", + "cst_kind": "linear", + "rhs": { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "x"] + ], + "const": "0" + }, + "lhs": {"name": "b1", "type": {"kind": "bool"}} + }, + { + "stmt": "bool_binop", + "op": "and", + "left": {"name": "b0", "type": {"kind": "bool"}}, + "right": {"name": "b1", "type": {"kind": "bool"}}, + "lhs": {"name": "b2", "type": {"kind": "bool"}} + }, + { + "stmt": "bool_assign_var", + "rhs": {"name": "b2", "type": {"kind": "bool"}}, + "negated": true, + "lhs": {"name": "b3", "type": {"kind": "bool"}} + }, + { + "stmt": "bool_binop", + "op": "or", + "left": {"name": "b0", "type": {"kind": "bool"}}, + "right": {"name": "b3", "type": {"kind": "bool"}}, + "lhs": {"name": "b4", "type": {"kind": "bool"}} + }, + { + "stmt": "bool_binop", + "op": "xor", + "left": {"name": "b0", "type": {"kind": "bool"}}, + "right": {"name": "b3", "type": {"kind": "bool"}}, + "lhs": {"name": "b5", "type": {"kind": "bool"}} + }, + { + "stmt": "bool_assign_var", + "rhs": {"name": "b2", "type": {"kind": "bool"}}, + "negated": false, + "lhs": {"name": "b6", "type": {"kind": "bool"}} + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "x"] + ], + "const": "-10" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "x"] + ], + "const": "10" + } + ] + ] + }, + "succs": ["guard"] + }, + { + "label": "start", + "stmts": [ + { + "stmt": "assign", + "rhs": { + "type": null, + "terms": [], + "const": "0" + }, + "lhs": {"name": "x", "type": {"kind": "int", "bitwidth": 32}} + } + ], + "invariant": { + "kind": "true" + }, + "succs": ["loop"] + } + ] + }, + { + "name": "unsafe", + "declaration": { + "inputs": [], + "outputs": [] + }, + "entry": "start", + "exit": "end", + "blocks": [ + { + "label": "edge-loop-loop", + "stmts": [ + { + "stmt": "assume", + "cond": { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "y"] + ], + "const": "9" + } + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "y"] + ], + "const": "-1" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "y"] + ], + "const": "10" + } + ] + ] + }, + "succs": ["loop"] + }, + { + "label": "edge-loop-post", + "stmts": [ + { + "stmt": "assume", + "cond": { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "y"] + ], + "const": "-10" + } + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "y"] + ], + "const": "-1" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "y"] + ], + "const": "10" + } + ] + ] + }, + "succs": ["post"] + }, + { + "label": "end", + "stmts": [ + { + "stmt": "bool_assert", + "cond": {"name": "c1", "type": {"kind": "bool"}}, + "loc": {"file": "no-filename", "line": 59, "col": 0, "id": 4} + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "y"] + ], + "const": "-10" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "y"] + ], + "const": "10" + }, + { + "op": "=", + "type": {"kind": "bool"}, + "terms": [ + ["1", "c0"] + ], + "const": "1" + }, + { + "op": "=", + "type": {"kind": "bool"}, + "terms": [ + ["1", "c1"] + ], + "const": "0" + } + ] + ] + }, + "succs": [] + }, + { + "label": "loop", + "stmts": [ + { + "stmt": "assign", + "rhs": { + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "y"] + ], + "const": "1" + }, + "lhs": {"name": "y", "type": {"kind": "int", "bitwidth": 32}} + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "y"] + ], + "const": "0" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "y"] + ], + "const": "9" + } + ] + ] + }, + "succs": ["edge-loop-loop", "edge-loop-post"] + }, + { + "label": "post", + "stmts": [ + { + "stmt": "bool_assign_cst", + "cst_kind": "linear", + "rhs": { + "op": "=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "y"] + ], + "const": "10" + }, + "lhs": {"name": "c0", "type": {"kind": "bool"}} + }, + { + "stmt": "bool_assign_var", + "rhs": {"name": "c0", "type": {"kind": "bool"}}, + "negated": true, + "lhs": {"name": "c1", "type": {"kind": "bool"}} + } + ], + "invariant": { + "kind": "disj", + "disjuncts": [ + [ + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["-1", "y"] + ], + "const": "-10" + }, + { + "op": "<=", + "type": {"kind": "int", "bitwidth": 32}, + "terms": [ + ["1", "y"] + ], + "const": "10" + } + ] + ] + }, + "succs": ["end"] + }, + { + "label": "start", + "stmts": [ + { + "stmt": "assign", + "rhs": { + "type": null, + "terms": [], + "const": "0" + }, + "lhs": {"name": "y", "type": {"kind": "int", "bitwidth": 32}} + } + ], + "invariant": { + "kind": "true" + }, + "succs": ["loop"] + } + ] + } + ], + "checks": [ + {"file": "no-filename", "line": 39, "col": 0, "id": 0, "result": "safe"}, + {"file": "no-filename", "line": 40, "col": 0, "id": 1, "result": "safe"}, + {"file": "no-filename", "line": 41, "col": 0, "id": 2, "result": "safe"}, + {"file": "no-filename", "line": 42, "col": 0, "id": 3, "result": "safe"}, + {"file": "no-filename", "line": 59, "col": 0, "id": 4, "result": "warning"} + ] +} diff --git a/lean/CrabberJson/Schema.lean b/lean/CrabberJson/Schema.lean new file mode 100644 index 0000000..6147aa6 --- /dev/null +++ b/lean/CrabberJson/Schema.lean @@ -0,0 +1,641 @@ +import Lean +import Crabber.Syntax +import Crabber.Assn +/- +# CrabberJson.Schema — reading crabber's JSON export + +`crabber --print-invariants-to-json out.json` emits one self-contained document +holding, for every block, its statements, its successors *and* the invariant +Crab inferred for it. This module turns that document into the data the proof +library consumes: a `Cfg` and a `Label → Assn`. + +## Why this is two layers rather than one + +The types below (`W…`, for "wire") mirror the JSON **exactly** — same fields, +same names, same nesting, including information the proof library has no use +for, such as bitwidths and source locations. Only afterwards does a separate +conversion drop what is unused and build `Cfg`/`Assn`. + +The extra layer buys a check. Because the wire types are faithful, they can be +written *back* to JSON and compared against the document that was read. A +mapping that silently drops a statement, or misreads a coefficient, produces a +document that differs from the input, and the comparison catches it. Converting +straight to `Cfg` would make that impossible: `Cfg` has function fields and has +already discarded the bitwidths, so there would be nothing to compare. + +Most of the mapping is not written by hand at all. Lean's derived JSON encoding +for a *structure* is a flat object of its fields, which is precisely the shape +crabber emits, so `deriving FromJson, ToJson` is exact for every record here. +Only the two tagged unions — statements, keyed by `"stmt"`, and invariants, +keyed by `"kind"` — use a discriminator convention of their own and need +instances written out. + +## Trust + +This module is **trusted**: nothing here is proved, and a bug that mistranslated +the program or the invariant would let the library prove a theorem about +something other than what Crab analysed. That is what the round-trip comparison +in `CrabberJson.RoundTrip` is for. The conversion is deliberately total and +fail-loud — every unsupported construct raises an error naming itself, and +nothing is ever skipped. +-/ + +namespace CrabberJson + +open Lean (Json FromJson ToJson fromJson? toJson) +open Crabber + +/-! ## Wire types + +One per JSON object in the export. Field names are the JSON keys verbatim; do +not rename them, as the derived instances are what make the names load-bearing. +-/ + +/-- Raw JSON has no `Repr`, and the records below carry some verbatim. Showing + it as its own compact text beats a constructor tree, so this is what `#eval` + on a wire record prints for the parts nothing interprets. -/ +instance : Repr Json := ⟨fun j _ => Std.Format.text j.compress⟩ + +/-- A CrabIR type: `{"kind": "int", "bitwidth": 32}`. + + `bitwidth` is carried only by `int`; `bool` and `int_array` omit the key + entirely, so it is optional here. Note the export distinguishes *omitted* + from *null*, and uses both — a missing bitwidth is an absent key, whereas an + untyped expression is an explicit `null` (see `WExp`). The instances below + have to preserve that difference for the round trip to mean anything. -/ +structure WTy where + kind : String + bitwidth : Option Nat := none + deriving FromJson, Repr, BEq + +/-- One object field, present only when the value is. + + Needed because the export distinguishes an omitted key from a null one, and + Lean's derived encoding does not: it writes `none` as an explicit `null`. + Using the derived instance where crabber omits the key produces a document + that differs from the input — which the round-trip check reports, and which + is how this was found rather than reasoned about. -/ +private def optField [ToJson α] (k : String) : Option α → List (String × Json) + | some x => [(k, toJson x)] + | none => [] + +instance : ToJson WTy where + toJson t := Json.mkObj (("kind", toJson t.kind) :: optField "bitwidth" t.bitwidth) + +/-- A variable occurrence: `{"name": "x", "type": {...}}`. -/ +structure WVar where + name : String + type : WTy + deriving FromJson, ToJson, Repr, BEq + +/-! ### Parts the proof never looks at + +Several pieces of the export exist for provenance or for other consumers, and +nothing in the proof depends on them: where an assertion was written, the +function signature, which file was analysed, which domain ran, and Crab's own +verdict on each assertion. + +They are held as raw `Lean.Json` rather than modelled with a record apiece. +Deleting them instead would be the obvious move, but it would quietly gut the +round-trip check: an unmodelled key is dropped on read and missing on write, so +every document would fail to reproduce. Carrying them opaquely keeps the check +over the *whole* document — `Json`'s own JSON instances are the identity, so a +value read into one of these fields is written back byte for byte — while +costing no types and no maintenance when a field is added to one of them. + +The one to revisit is `checks`. Crab's per-assertion verdicts are exactly what a +finished `chk` should be compared against — Crab says "safe", Lean either proves +it or does not, and a disagreement is the interesting signal. When that +comparison is built, `checks` earns a real type. -/ + +/-- A linear expression: `{"type", "terms": [["1","y"]], "const": "9"}`. + + Coefficients and constants are **decimal strings**, not JSON numbers: Crab's + numbers are arbitrary precision, and most JSON consumers would round them + through a double. They are parsed to `Int` during conversion, not here. + + `type` is `null` when the expression is a bare constant — `x := 0` has no + variable for Crab to take a type from. So an absent type is not missing + information; it says the expression mentions no variables, which the + conversion below checks rather than assumes. -/ +structure WExp where + type : Option WTy + terms : Array (Array String) + const : String + deriving Repr, BEq + +/-- A linear constraint. + + Usually a comparison — a `WExp` plus an operator — but a domain may also + export the two *nullary* constraints, written `{"op": "true"}` and + `{"op": "false"}` with no other keys. The octagon domain emits `true` for a + block it knows nothing about, where the interval domain emits an empty + conjunction instead, so which of these appears depends on the domain rather + than on the program. -/ +inductive WCon where + /-- `{"op": "true"}` — a constraint that constrains nothing. -/ + | tt + /-- `{"op": "false"}` — an unsatisfiable constraint. -/ + | ff + /-- A comparison. `type` is optional for the same reason as in `WExp`. -/ + | cmp (op : String) (type : Option WTy) (terms : Array (Array String)) + (const : String) + deriving Repr, BEq + +/-- A statement, tagged by the `"stmt"` key. + + The four of the numeric core and the six boolean ones. The remaining kinds + crabber can emit — `binop`, `select`, `cast`, `unreachable`, the four array + ones, `callsite` and the reference/region family — are rejected by name when + read, rather than given a constructor here that the semantics could not + interpret. -/ +inductive WStmt where + | assign (lhs : WVar) (rhs : WExp) + | assume (cond : WCon) + | assert (cond : WCon) (loc : Json) + | havoc (lhs : WVar) + /-- `bool_assign_cst`. The right-hand side is either a linear constraint or a + *reference* constraint, and the export says which in a sibling `cst_kind` + key rather than by the shape of `rhs`. + + `rhs` is kept as raw `Json` for exactly that reason: its schema depends on + another field, and only one of the two schemas is modelled. References are + not, so parsing `rhs` is deferred to the conversion below, which reads it + as a `WCon` when `cst_kind` is `"linear"` and refuses it by name otherwise. + Holding it opaquely also keeps the round trip exact either way — `Json`'s + own JSON instances are the identity — so a document containing a reference + constraint is still reported against the construct, not against the + reader. -/ + | boolAssignCst (cstKind : String) (rhs : Json) (lhs : WVar) + /-- `bool_assign_var`. `negated` carries `b := not(c)`; Crab has no separate + unary boolean statement. -/ + | boolAssignVar (rhs : WVar) (negated : Bool) (lhs : WVar) + /-- `bool_binop`, with `op` one of `"and"`, `"or"`, `"xor"`. -/ + | boolBinop (op : String) (left : WVar) (right : WVar) (lhs : WVar) + /-- `bool_assume`, with the same `negated` flag. -/ + | boolAssume (cond : WVar) (negated : Bool) + /-- `bool_assert`. No `negated` key — the export does not write one here. -/ + | boolAssert (cond : WVar) (loc : Json) + /-- `bool_select`. Crab's own parser cannot produce one; the export can. -/ + | boolSelect (cond : WVar) (left : WVar) (right : WVar) (lhs : WVar) + deriving Repr, BEq + +/-- An invariant, tagged by the `"kind"` key: `"true"`, `"false"`, or a + `"disj"` of conjunctions. Top and bottom are explicit in the export because + an empty list of disjuncts would be ambiguous on the wire. -/ +inductive WInv where + | top + | bot + | disj (disjuncts : Array (Array WCon)) + deriving Repr, BEq + +/-- A block: everything Crab knows about it, in one object. This is the shape + that makes a separate CFG document unnecessary — statements, successors and + the inferred invariant cannot disagree about which block they describe. -/ +structure WBlock where + label : String + stmts : Array WStmt + invariant : WInv + succs : Array String + deriving Repr, BEq + +/-- One analysed CFG. A document holds several — `samples/test-1.crabir` has + `foo` and `bar` — so a caller must say which one it means. + + `declaration` (the signature) and `exit` (the final block, `null` for two of + the samples) are carried verbatim. Neither reaches a proof: the obligation + for a block with no successors is discharged by the empty conjunction, not by + knowing which block is final. -/ +structure WCfg where + name : String + declaration : Json + entry : String + exit : Json + blocks : Array WBlock + deriving Repr, BEq + +/-- The whole document. + + `schema` and `kind` are checked; the rest of the header — which file was + analysed, how the CFG was built, which domain ran, and Crab's own verdict on + each assertion — passes through untouched. + + **`cfgs` is deliberately left unparsed.** A document holds every CFG of the + analysed file, and they are independent: one may use a construct this + library does not model while another is perfectly ordinary. Parsing the + array eagerly would make a single unsupported CFG condemn all of them — + `samples/test-call-1.crabir` has a `main` that calls, and an `inc` that + contains nothing but an assignment, and there is no reason the second should + be unreadable because of the first. + + So a CFG is parsed only when it is asked for, and only that one has to + succeed. The round-trip check moves with it: it is applied to the selected + CFG against the JSON it came from, which is where it was doing the work + anyway. -/ +structure WDoc where + schema : Nat + kind : String + source : Json + options : Json + analysis : Json + cfgs : Array Json + checks : Json + deriving Repr, BEq + +/-! ## The two hand-written instances + +Everything above is a record, and Lean's derived encoding for a record is a flat +object of its fields — exactly crabber's shape. The two tagged unions are the +exception: Lean would encode `WStmt.assume c` as `{"assume": …}`, whereas the +export writes `{"stmt": "assume", "cond": …}`. So these four instances are the +only place where the correspondence between Lean and the schema is asserted by +hand, and the only place a typo could go unnoticed by the compiler. -/ + +/-! The three records carrying an *explicitly null* field are written out too. +Lean's derived encoding omits a `none`, whereas crabber writes `null`, and the +round trip only means something if that distinction survives it. (Contrast +`WTy.bitwidth`, where crabber omits the key and the derived behaviour is +therefore already right.) -/ + +instance : FromJson WExp where + fromJson? j := do + return { type := ← j.getObjValAs? (Option WTy) "type" + terms := ← j.getObjValAs? (Array (Array String)) "terms" + const := ← j.getObjValAs? String "const" } + +instance : ToJson WExp where + toJson e := Json.mkObj + [("type", toJson e.type), ("terms", toJson e.terms), ("const", toJson e.const)] + +instance : FromJson WCon where + fromJson? j := do + match ← j.getObjValAs? String "op" with + -- The nullary forms carry no other keys, so they must be recognised before + -- anything tries to read a term list that is not there. + | "true" => return .tt + | "false" => return .ff + | op => + return .cmp op (← j.getObjValAs? (Option WTy) "type") + (← j.getObjValAs? (Array (Array String)) "terms") + (← j.getObjValAs? String "const") + +instance : ToJson WCon where + toJson + | .tt => Json.mkObj [("op", "true")] + | .ff => Json.mkObj [("op", "false")] + | .cmp op type terms const => Json.mkObj + [("op", toJson op), ("type", toJson type), + ("terms", toJson terms), ("const", toJson const)] + +instance : FromJson WStmt where + fromJson? j := do + match ← j.getObjValAs? String "stmt" with + | "assign" => return .assign (← j.getObjValAs? WVar "lhs") (← j.getObjValAs? WExp "rhs") + | "assume" => return .assume (← j.getObjValAs? WCon "cond") + | "assert" => return .assert (← j.getObjValAs? WCon "cond") (← j.getObjValAs? Json "loc") + | "havoc" => return .havoc (← j.getObjValAs? WVar "lhs") + | "bool_assign_cst" => + return .boolAssignCst (← j.getObjValAs? String "cst_kind") + (← j.getObjValAs? Json "rhs") + (← j.getObjValAs? WVar "lhs") + | "bool_assign_var" => + return .boolAssignVar (← j.getObjValAs? WVar "rhs") + (← j.getObjValAs? Bool "negated") + (← j.getObjValAs? WVar "lhs") + | "bool_binop" => + return .boolBinop (← j.getObjValAs? String "op") + (← j.getObjValAs? WVar "left") + (← j.getObjValAs? WVar "right") + (← j.getObjValAs? WVar "lhs") + | "bool_assume" => + return .boolAssume (← j.getObjValAs? WVar "cond") + (← j.getObjValAs? Bool "negated") + | "bool_assert" => + return .boolAssert (← j.getObjValAs? WVar "cond") (← j.getObjValAs? Json "loc") + | "bool_select" => + return .boolSelect (← j.getObjValAs? WVar "cond") + (← j.getObjValAs? WVar "left") + (← j.getObjValAs? WVar "right") + (← j.getObjValAs? WVar "lhs") + | other => + throw s!"statement kind '{other}' is outside the fragment this library \ + models (assign, assume, assert, havoc, and the six boolean \ + statements). It is rejected rather than skipped: dropping a \ + statement would weaken every proof obligation in its block." + +instance : ToJson WStmt where + toJson + | .assign lhs rhs => Json.mkObj + [("stmt", "assign"), ("lhs", toJson lhs), ("rhs", toJson rhs)] + | .assume c => Json.mkObj [("stmt", "assume"), ("cond", toJson c)] + | .assert c loc => Json.mkObj + [("stmt", "assert"), ("cond", toJson c), ("loc", toJson loc)] + | .havoc lhs => Json.mkObj [("stmt", "havoc"), ("lhs", toJson lhs)] + | .boolAssignCst k rhs lhs => Json.mkObj + [("stmt", "bool_assign_cst"), ("cst_kind", toJson k), ("rhs", rhs), + ("lhs", toJson lhs)] + | .boolAssignVar rhs n lhs => Json.mkObj + [("stmt", "bool_assign_var"), ("rhs", toJson rhs), ("negated", toJson n), + ("lhs", toJson lhs)] + | .boolBinop op l r lhs => Json.mkObj + [("stmt", "bool_binop"), ("op", toJson op), ("left", toJson l), + ("right", toJson r), ("lhs", toJson lhs)] + | .boolAssume c n => Json.mkObj + [("stmt", "bool_assume"), ("cond", toJson c), ("negated", toJson n)] + | .boolAssert c loc => Json.mkObj + [("stmt", "bool_assert"), ("cond", toJson c), ("loc", toJson loc)] + | .boolSelect c l r lhs => Json.mkObj + [("stmt", "bool_select"), ("cond", toJson c), ("left", toJson l), + ("right", toJson r), ("lhs", toJson lhs)] + +instance : FromJson WInv where + fromJson? j := do + match ← j.getObjValAs? String "kind" with + | "true" => return .top + | "false" => return .bot + | "disj" => return .disj (← j.getObjValAs? (Array (Array WCon)) "disjuncts") + | other => throw s!"unknown invariant kind '{other}' (expected true, false or disj)" + +instance : ToJson WInv where + toJson + | .top => Json.mkObj [("kind", "true")] + | .bot => Json.mkObj [("kind", "false")] + | .disj ds => Json.mkObj [("kind", "disj"), ("disjuncts", toJson ds)] + +-- Derived, but only here: each of these contains the one above it, so the +-- instances have to be introduced outermost-last. +deriving instance FromJson, ToJson for WBlock +deriving instance FromJson, ToJson for WCfg +deriving instance FromJson, ToJson for WDoc + +/-! ## Conversion to the proof library's types + +Everything below can fail, and says why when it does. The failures are not +defensive padding: the unmodelled statement kinds occur throughout `samples/` — +`test-6` reaches its booleans through a `cast` and is refused for that reason +alone — so these paths are exercised. -/ + +/-- Parse one of the export's decimal strings. -/ +def parseInt (s : String) : Except String Int := + match s.toInt? with + | some n => .ok n + | none => .error s!"'{s}' is not a decimal integer" + +/-- Reject anything that is not an integer type. + + The types that reach this are `bool`, `int_array` and the reference/region + family. Booleans are the case that matters, and the reason it is still an + error rather than a widening: an integer *expression* or *constraint* over a + boolean variable would mean Crab had put a boolean into arithmetic, which the + state's two-store representation says is not what CrabIR does. Boolean facts + reach the assertion language through `WCon.toAtom` below, which is the only + path that accepts a bool-typed constraint, and it accepts only the shapes + Crab actually writes. + + The bitwidth is deliberately ignored rather than rejected. Measured against + the analyser, Crab's integers behave as mathematical integers — `x:i8 := 127; + x := x+1` yields 128, and a truncating cast does not truncate — so the + semantics is over unbounded `Int` and a width would be recorded but never + consulted. -/ +def WTy.expectInt (t : WTy) (ctx : String) : Except String Unit := + if t.kind == "int" then .ok () else + .error s!"{ctx} has type '{t.kind}', which is outside the fragment this \ + library models. An integer type is required here: boolean \ + variables live in their own store, and only an invariant's \ + conjuncts may be bool-typed." + +/-- Reject anything that is not a boolean type. Used for the operands and + targets of the boolean statements, all of which the export types `bool`. -/ +def WTy.expectBool (t : WTy) (ctx : String) : Except String Unit := + if t.kind == "bool" then .ok () else + .error s!"{ctx} has type '{t.kind}', but a boolean statement's operands must \ + be boolean" + +def opOfString : String → Except String Crabber.CmpOp + | "<=" => .ok .le + | "<" => .ok .lt + | "=" => .ok .eq + | "!=" => .ok .ne + | s => .error s!"unknown comparison operator '{s}'" + +def boolOpOfString : String → Except String Crabber.BoolOp + | "and" => .ok .and + | "or" => .ok .or + | "xor" => .ok .xor + | s => .error s!"unknown boolean operator '{s}' (expected and, or or xor)" + +/-- `[["1","y"], ["-2","x"]]` becomes `[(1, "y"), (-2, "x")]`. -/ +def termsToList (ts : Array (Array String)) : Except String (List (Int × Crabber.Var)) := + ts.toList.mapM fun t => + match t.toList with + | [coef, var] => do return (← parseInt coef, var) + | _ => .error s!"a term must be a [coefficient, variable] pair, got {t.size} elements" + +/-- Check the type of an expression or constraint, which may be absent. + + Absence is not "type unknown": Crab writes `null` exactly when there is no + variable to take a type from, i.e. for a bare constant such as the right-hand + side of `x := 0`. So the untyped case is accepted, but only after confirming + that it really does mention no variables — an untyped expression *with* terms + would mean the export had lost information, and guessing `int` there is + precisely the silent assumption worth refusing to make. -/ +def expectIntType (t : Option WTy) (terms : Array (Array String)) + (ctx : String) : Except String Unit := + match t with + | some ty => ty.expectInt ctx + | none => + if terms.isEmpty then .ok () else + .error s!"{ctx} carries no type, which the export uses to mean 'a bare \ + constant', yet it mentions {terms.size} variable(s)" + +def WExp.toLinExp (e : WExp) : Except String Crabber.LinExp := do + expectIntType e.type e.terms "a right-hand side" + return { terms := ← termsToList e.terms, const := ← parseInt e.const } + +/-- The two nullary constraints have exact counterparts in the assertion + language, so neither needs a special case downstream. + + `LinCon.lhs` of an empty term list is `0`, so `0 ≤ 0` is satisfied by every + state and `0 ≤ -1` by none — which is what `true` and `false` mean. Encoding + them this way rather than extending `LinCon` keeps the proof library's + syntax unchanged and its meaning function untouched. -/ +def WCon.toLinCon : WCon → Except String Crabber.LinCon + | .tt => .ok { op := .le, terms := [], const := 0 } + | .ff => .ok { op := .le, terms := [], const := -1 } + | .cmp op type terms const => do + expectIntType type terms "a constraint" + return { op := ← opOfString op, terms := ← termsToList terms, + const := ← parseInt const } + +/-- A bool-typed constraint, read as a claim about the boolean store. + + **Only `1·b = 0` and `1·b = 1` are accepted.** That is not a simplification: + measured across `int`, `int-terms`, `int-set`, `zones`, `oct-snf` and `pk`, + it is the only bool-tagged shape Crab emits, because its booleans go through + a flat per-variable lattice with no relational information to export. + + Anything else — a comparison other than `=`, a coefficient other than 1, more + than one term, a constant other than 0 or 1 — is refused, naming what was + seen. The alternative would be to read such a constraint as arithmetic over a + 0/1 encoding, which is precisely the representation the state does not use; + it would be quietly meaningless. If a future domain does export a relational + boolean fact, this error is where it will surface, and the assertion language + will need an atom for it rather than a silent misreading. -/ +def WCon.toBoolAtom (op : String) (terms : Array (Array String)) + (const : String) : Except String Crabber.Atom := do + let ts ← termsToList terms + match op, ts, const with + | "=", [(1, b)], "0" => .ok (.bool b false) + | "=", [(1, b)], "1" => .ok (.bool b true) + | _, _, _ => + .error s!"a bool-typed constraint here is '{op}' over {terms.size} term(s) \ + against '{const}', which is outside the fragment this library \ + models. Only '1·b = 0' and '1·b = 1' are understood, and measured \ + against every domain crabber offers that is the only shape Crab \ + exports for a boolean. Reading anything else would mean treating \ + a boolean as a 0/1 integer, which is not how the state \ + represents one." + +/-- One conjunct of an invariant, dispatched on the type the export tagged it + with. This is the only place a bool-typed constraint is accepted. -/ +def WCon.toAtom : WCon → Except String Crabber.Atom + | .cmp op (some ty) terms const => + if ty.kind == "bool" then WCon.toBoolAtom op terms const + else do return .lin (← WCon.toLinCon (.cmp op (some ty) terms const)) + | c => do return .lin (← c.toLinCon) + +/-- Drops the source location: the asserts carry only their condition, since the + proof obligation does not depend on where the assertion was written. -/ +def WStmt.toStmt : WStmt → Except String Crabber.Stmt + | .assign lhs rhs => do + lhs.type.expectInt s!"the assignment target '{lhs.name}'" + return .assign lhs.name (← rhs.toLinExp) + | .assume c => return .assume (← c.toLinCon) + | .assert c _ => return .assert (← c.toLinCon) + | .havoc lhs => do + lhs.type.expectInt s!"the havoc target '{lhs.name}'" + return .havoc lhs.name + -- `rhs` was held as raw JSON because its schema depends on `cst_kind`; this is + -- where that is resolved. A reference constraint is refused by name — the + -- reference and region statements are unmodelled as a group, and accepting + -- their constraints alone would be meaningless. + | .boolAssignCst kind rhs lhs => do + lhs.type.expectBool s!"the boolean assignment target '{lhs.name}'" + if kind != "linear" then + throw s!"a bool_assign_cst whose right-hand side is a '{kind}' \ + constraint. References are outside the fragment this library \ + models; only a linear constraint is understood here." + let c : WCon ← fromJson? rhs + return .boolAssignCst lhs.name (← c.toLinCon) + | .boolAssignVar rhs neg lhs => do + lhs.type.expectBool s!"the boolean assignment target '{lhs.name}'" + rhs.type.expectBool s!"the boolean assignment source '{rhs.name}'" + return .boolAssignVar lhs.name rhs.name neg + | .boolBinop op l r lhs => do + lhs.type.expectBool s!"the boolean operation target '{lhs.name}'" + l.type.expectBool s!"the left operand '{l.name}'" + r.type.expectBool s!"the right operand '{r.name}'" + return .boolBinop lhs.name (← boolOpOfString op) l.name r.name + | .boolAssume c neg => do + c.type.expectBool s!"the assumed boolean '{c.name}'" + return .boolAssume c.name neg + | .boolAssert c _ => do + c.type.expectBool s!"the asserted boolean '{c.name}'" + return .boolAssert c.name + | .boolSelect c l r lhs => do + lhs.type.expectBool s!"the boolean select target '{lhs.name}'" + c.type.expectBool s!"the select condition '{c.name}'" + l.type.expectBool s!"the left operand '{l.name}'" + r.type.expectBool s!"the right operand '{r.name}'" + return .boolSelect lhs.name c.name l.name r.name + +def WInv.toAssn : WInv → Except String Crabber.Assn + | .top => .ok Crabber.Assn.top + | .bot => .ok Crabber.Assn.bot + | .disj ds => ds.toList.mapM fun d => d.toList.mapM WCon.toAtom + +/-! ## Building the CFG + +`Cfg.body` and `Cfg.succ` are *total* functions: every label, including strings +naming no block, must have an answer. The export gives an association list, so +the total function is a lookup defaulting to the empty list — which is exactly +the convention the library's "unknown label" lemma expects. The invariant map +defaults to bottom for the same reason: a label that names no block is not +reachable, and bottom is the claim that says so. -/ + +/-- One analysed program, in the form the proof library wants. + + `labels` is kept because the bundling step needs to case-split over exactly + the blocks that exist, and because it is the list a generated file prints. -/ +structure Program where + name : String + entry : Crabber.Label + labels : List Crabber.Label + cfg : Crabber.Cfg + inv : Crabber.Label → Crabber.Assn + +/-- A block after conversion, before the maps are assembled. -/ +private structure BlockData where + label : Crabber.Label + body : List Crabber.Stmt + succs : List Crabber.Label + inv : Crabber.Assn + +private def WBlock.toData (b : WBlock) : Except String BlockData := do + return { label := b.label + body := ← b.stmts.toList.mapM WStmt.toStmt + succs := b.succs.toList + inv := ← b.invariant.toAssn } + +def WCfg.toProgram (c : WCfg) : Except String Program := do + let bs ← c.blocks.toList.mapM WBlock.toData + let bodyTbl := bs.map fun b => (b.label, b.body) + let succTbl := bs.map fun b => (b.label, b.succs) + let invTbl := bs.map fun b => (b.label, b.inv) + -- Duplicate labels would make the lookups below silently prefer the first, + -- so the two documents could agree while describing different graphs. + let labels := bs.map (·.label) + if labels.eraseDups.length != labels.length then + throw s!"cfg '{c.name}' lists a block label twice" + return { name := c.name + entry := c.entry + labels := labels + cfg := { entry := c.entry + body := fun l => (bodyTbl.lookup l).getD [] + succ := fun l => (succTbl.lookup l).getD [] } + inv := fun l => (invTbl.lookup l).getD Crabber.Assn.bot } + +/-! ## Entry points -/ + +/-- Read a document, checking it is the combined invariants export rather than + the CFG-only one — the latter has no `invariant` on its blocks, and silently + accepting it would produce a program annotated entirely with bottom. -/ +def docOfJson (j : Json) : Except String WDoc := do + let d : WDoc ← fromJson? j + if d.schema != 1 then + throw s!"unsupported schema version {d.schema} (this reader knows version 1)" + if d.kind != "invariants" then + throw s!"document kind is '{d.kind}'; expected 'invariants', the export that \ + carries the CFG and the inferred invariants together" + return d + +/-- The name of an unparsed CFG, read straight out of its JSON. + + Enough to find the one that was asked for without committing to parsing any + of the others. -/ +def cfgNameOf (j : Json) : Option String := + (j.getObjValAs? String "name").toOption + +/-- Every CFG the document mentions, named but not parsed. -/ +def WDoc.cfgNames (d : WDoc) : List String := + d.cfgs.toList.filterMap cfgNameOf + +/-- The JSON of one named CFG, still unparsed. -/ +def WDoc.rawCfg (d : WDoc) (cfgName : String) : Except String Json := + match d.cfgs.find? (fun j => cfgNameOf j == some cfgName) with + | some j => .ok j + | none => + let available := String.intercalate ", " d.cfgNames + .error s!"no cfg named '{cfgName}' in this document (it has: {available})" + +end CrabberJson diff --git a/lean/lake-manifest.json b/lean/lake-manifest.json new file mode 100644 index 0000000..8356e7e --- /dev/null +++ b/lean/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "crabber", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lean/lakefile.toml b/lean/lakefile.toml new file mode 100644 index 0000000..d55e0f0 --- /dev/null +++ b/lean/lakefile.toml @@ -0,0 +1,26 @@ +name = "crabber" +defaultTargets = ["Crabber", "CrabberJson"] + +# No dependencies, deliberately. `omega` — the decision procedure that closes +# every per-block proof obligation — is part of Lean core, and the library is +# built from core datatypes only. State updates are written out by hand rather +# than taken from Mathlib, which is three lines and avoids pulling in a large +# dependency for them. Builds stay fast and the trusted development has a +# dependency footprint of zero. +# +# Revisit only if non-linear arithmetic becomes necessary: `omega` decides +# Presburger arithmetic, so multiplication or division of variables would need +# `nlinarith` or similar, which does require Mathlib. + +[[lean_lib]] +name = "Crabber" + +# The frontend, kept out of `Crabber`'s import graph on purpose. Reading JSON +# needs `Lean` as a library; the trusted proof development stays free of it. +[[lean_lib]] +name = "CrabberJson" + +# Exercises the reader over exported documents: lake exe checkjson out.json … +[[lean_exe]] +name = "checkjson" +root = "CheckJson" diff --git a/lean/lean-toolchain b/lean/lean-toolchain new file mode 100644 index 0000000..025e595 --- /dev/null +++ b/lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.33.0 diff --git a/samples/test-1.crabir b/samples/test-1.crabir index 981edf9..ccda9d1 100644 --- a/samples/test-1.crabir +++ b/samples/test-1.crabir @@ -1,3 +1,6 @@ +# How to run: +# crabber test-1.crabir -d int + # this is a comment # newline is used to delimit a new instruction, new block or new cfg # A cfg must have a name diff --git a/samples/test-10.crabir b/samples/test-10.crabir index 81314e6..5d69be2 100644 --- a/samples/test-10.crabir +++ b/samples/test-10.crabir @@ -1,3 +1,6 @@ +# How to run: +# crabber test-10.crabir -d int-terms + cfg("terms") start: havoc(x:i32) diff --git a/samples/test-11.crabir b/samples/test-11.crabir index 4fe937a..453ca51 100644 --- a/samples/test-11.crabir +++ b/samples/test-11.crabir @@ -1,3 +1,9 @@ +# How to run: +# crabber test-11.crabir -d int --print-invariants +# +# Deeply nested loops: a fixpoint stress test. It has no EXPECT_EQ, so nothing +# is checked. Not registered as a test in CMakeLists.txt. + cfg("nested-loops-2") start: i:i64 := 0 diff --git a/samples/test-2.crabir b/samples/test-2.crabir index abeecca..ccea2e3 100644 --- a/samples/test-2.crabir +++ b/samples/test-2.crabir @@ -1,3 +1,9 @@ +# How to run: +# crabber test-2.crabir -d int --print-invariants +# +# A parsing showcase: it has no EXPECT_EQ, so nothing is checked. Not +# registered as a test in CMakeLists.txt. + # Parsing example cfg("parsing-example") diff --git a/samples/test-3.crabir b/samples/test-3.crabir index f62a49f..67abe04 100644 --- a/samples/test-3.crabir +++ b/samples/test-3.crabir @@ -1,3 +1,6 @@ +# How to run: +# crabber test-3.crabir -d int + cfg("nested-loops") start: i:i32 := 0 diff --git a/samples/test-4.crabir b/samples/test-4.crabir index 4a6ad93..d6f7ee5 100644 --- a/samples/test-4.crabir +++ b/samples/test-4.crabir @@ -1,3 +1,6 @@ +# How to run: +# crabber test-4.crabir -d oct-snf + cfg("octagons") start: diff --git a/samples/test-5.crabir b/samples/test-5.crabir index 6e34340..b70566a 100644 --- a/samples/test-5.crabir +++ b/samples/test-5.crabir @@ -1,3 +1,10 @@ +# How to run: +# crabber test-5.crabir -d int --widening-thresholds 10 --print-invariants +# +# This sample checks an inferred invariant rather than an assertion: with +# widening thresholds the output must contain +# b1: ({}, {n -> [0, 60]}) + cfg("thresholds") start: n:i32 := 0 diff --git a/samples/test-6.crabir b/samples/test-6.crabir index 2b5cedd..8876d28 100644 --- a/samples/test-6.crabir +++ b/samples/test-6.crabir @@ -1,3 +1,7 @@ +# How to run: +# crabber test-6.crabir -d int +# + # this is a comment # newline is used to delimit a new instruction, new block or new cfg # A cfg must have a name diff --git a/samples/test-7.crabir b/samples/test-7.crabir index 21e669f..821d7ca 100644 --- a/samples/test-7.crabir +++ b/samples/test-7.crabir @@ -1,3 +1,11 @@ +# How to run (one invocation per partitioning/disjunctive domain): +# crabber test-7.crabir -d int-set --widening-delay 10 +# crabber test-7.crabir -d int-val-part --widening-delay 10 +# crabber test-7.crabir -d zones-val-part --widening-delay 10 +# crabber test-7.crabir -d boxes --widening-delay 10 +# +# The boxes run needs Crab built with -DCRAB_USE_LDD=ON. + cfg("loop-partitioning") start: x:i32 := 0 diff --git a/samples/test-8.crabir b/samples/test-8.crabir index 413ac9a..2c56ac3 100644 --- a/samples/test-8.crabir +++ b/samples/test-8.crabir @@ -1,3 +1,6 @@ +# How to run: +# crabber test-8.crabir -d zones + cfg("arrays") start: x_addr:i64 := 1024 diff --git a/samples/test-9.crabir b/samples/test-9.crabir index 3092490..38ad24e 100644 --- a/samples/test-9.crabir +++ b/samples/test-9.crabir @@ -1,3 +1,6 @@ +# How to run: +# crabber test-9.crabir -d tvpi-dbm --coefficients "4,8" + cfg("non-unit-coefficients") start: havoc(N:i32) diff --git a/samples/test-bool-1.crabir b/samples/test-bool-1.crabir new file mode 100644 index 0000000..2de8a00 --- /dev/null +++ b/samples/test-bool-1.crabir @@ -0,0 +1,59 @@ +# How to run: +# crabber test-bool-1.crabir -d int +# crabber test-bool-1.crabir -d int --verify-with-lean +# +# The boolean fragment, exercised deliberately: every boolean statement Crab's +# parser can produce appears here, and the two cfgs differ only in whether the +# asserted boolean is the one the analysis actually knows. +# +# Note test-6.crabir also uses booleans, but reaches them through trunc, which +# the Lean semantics does not model. This file avoids casts on purpose, so it is +# the one that can be checked end to end. + +# `safe`: the four assertions all hold, and Crab proves them. +cfg("safe") + start: + x:i32 := 0 + goto loop + loop: + x:i32 := x + 1 + if (x <= 9):i32 goto loop else goto post + post: + # bool_assign_cst: record whether an integer constraint holds + b0 := (x == 10):i32 + b1 := (x >= 0):i32 + # bool_binop: and / or / xor + b2 := b0 and b1 + # bool_assign_var, negated (the surface `not` compiles to the flag) + b3 := not(b2) + b4 := b0 or b3 # b0 ∨ ¬(b0 ∧ b1): true whatever b0 and b1 are + b5 := b0 xor b3 # b0 ⊕ ¬(b0 ∧ b1) + # bool_assign_var, plain + b6:i1 := b2 + goto guard + guard: + # bool_assume: everything after this may take b2 for granted + assume(b2) + goto end + end: + EXPECT_EQ(true, assert(b2)) + EXPECT_EQ(true, assert(b4)) + EXPECT_EQ(true, assert(b5)) + EXPECT_EQ(true, assert(b6)) + +# `unsafe`: the same program asserting the negation. Crab reports an error, and +# Lean refutes the block's verification condition rather than merely failing to +# prove it -- the boolean counterpart of test-1's foo/bar pair. +cfg("unsafe") + start: + y:i32 := 0 + goto loop + loop: + y:i32 := y + 1 + if (y <= 9):i32 goto loop else goto post + post: + c0 := (y == 10):i32 + c1 := not(c0) + goto end + end: + EXPECT_EQ(false, assert(c1)) diff --git a/samples/test-call-1.crabir b/samples/test-call-1.crabir index 3b3f643..a9a3b79 100644 --- a/samples/test-call-1.crabir +++ b/samples/test-call-1.crabir @@ -1,3 +1,7 @@ +# How to run: +# crabber test-call-1.crabir -d zones +# + # Function calls: a cfg with one input and one output parameter. # # A cfg parameter list is written after the cfg name as a comma-separated diff --git a/samples/test-call-2.crabir b/samples/test-call-2.crabir index 242b9dd..37b3e6d 100644 --- a/samples/test-call-2.crabir +++ b/samples/test-call-2.crabir @@ -1,3 +1,7 @@ +# How to run: +# crabber test-call-2.crabir -d zones +# + # Function calls: multiple inputs and multiple outputs. # # When a call has more than one output, the outputs are written as a diff --git a/samples/test-call-3.crabir b/samples/test-call-3.crabir index e78dc17..9f7dd8d 100644 --- a/samples/test-call-3.crabir +++ b/samples/test-call-3.crabir @@ -1,3 +1,7 @@ +# How to run: +# crabber test-call-3.crabir -d zones +# + # Function calls: a call with no outputs (void call) and an input-only cfg. # # When a callee has no output parameters, the call is written without a diff --git a/samples/test-call-4.crabir b/samples/test-call-4.crabir index 5fbeedc..e11b1c7 100644 --- a/samples/test-call-4.crabir +++ b/samples/test-call-4.crabir @@ -1,3 +1,7 @@ +# How to run: +# crabber test-call-4.crabir -d zones +# + # Function calls: the same callee is invoked from several call sites and the # callee itself has non-trivial control flow (a loop). diff --git a/samples/test-call-fail-1.crabir b/samples/test-call-fail-1.crabir index 0d84a9b..81b982c 100644 --- a/samples/test-call-fail-1.crabir +++ b/samples/test-call-fail-1.crabir @@ -1,3 +1,9 @@ +# How to run: +# crabber test-call-fail-1.crabir -d int +# +# Any domain will do: the program is rejected before the analysis runs. +# + # NEGATIVE TEST: this program must FAIL to compile. # # A cfg's input and output parameters must be disjoint: the same variable diff --git a/samples/test-call-fail-2.crabir b/samples/test-call-fail-2.crabir index 226bc80..3b1a757 100644 --- a/samples/test-call-fail-2.crabir +++ b/samples/test-call-fail-2.crabir @@ -1,3 +1,9 @@ +# How to run: +# crabber test-call-fail-2.crabir -d int +# +# Any domain will do: the program is rejected before the analysis runs. +# + # NEGATIVE TEST: this program must FAIL to compile. # # A call instruction is written as "call callee(args)". Here the argument diff --git a/src/crabber.cpp b/src/crabber.cpp index 209526b..2fa4464 100644 --- a/src/crabber.cpp +++ b/src/crabber.cpp @@ -2,17 +2,21 @@ #include #include +#include #include #include +#include #include #include #include +#include using namespace std; namespace crabber { TestResult run_program(std::istream &is, const CrabIrBuilderOpts &irOpts, - const CrabIrAnalyzerOpts &anaOpts) { + const CrabIrAnalyzerOpts &anaOpts, + const LeanVerifyOpts &leanOpts) { CrabIrBuilder crabIR(is, irOpts); CrabIrAnalyzer crabAnalyzer(crabIR, anaOpts); crabAnalyzer.analyze(); @@ -42,6 +46,45 @@ TestResult run_program(std::istream &is, const CrabIrBuilderOpts &irOpts, }); } + // The document just written is the whole interface to the Lean side: it is + // read back by Lean, not passed along in memory, so what gets proved is + // exactly what was exported. + if (leanOpts.enabled) { + crab::outs() << "\n### LEAN VERIFICATION ###\n"; + // Announced before the results, since every CFG below was checked against + // this one document. + if (leanOpts.keep_temp) { + crab::outs() << " invariants : " << anaOpts.print_invariants_to_json + << "\n"; + } + auto results = + verifyWithLean(anaOpts.print_invariants_to_json, crabIR, leanOpts); + for (auto const &r : results) { + crab::outs() << describe(r) << "\n"; + // Where the arithmetic ran out, in the program's own variables. It is an + // assignment the proof could not rule out, not necessarily a reachable + // one -- but it is the fastest way to see what fact is missing. + if (!r.counterexample.empty()) { + crab::outs() << " cannot rule out : " << r.counterexample << "\n"; + } + // Everything needed to take a failure apart by hand: the file Lean was + // given, and the command that runs it again. + if (!r.lean_file.empty()) { + crab::outs() << " lean file : " << r.lean_file << "\n" + << " reproduce : " << leanReproduceCommand(r.lean_file) + << "\n"; + } + if (leanOpts.show_output && r.verdict != LeanVerdict::Proved && + !r.output.empty()) { + crab::outs() << r.output; + } + } + // Said once, rather than implied by each line: a negative result here is + // about this proof attempt, never about the analysis. + crab::outs() << "(\"could not verify\" means Lean found no proof; it is not " + "a claim that the invariants are wrong)\n"; + } + unsigned expected_ok = 0; unsigned unexpected_ok = 0; unsigned expected_failure = 0; @@ -165,6 +208,28 @@ int main(int argc, char **argv) { app.add_option("--print-invariants-to-json", print_invariants_to_json, "Write invariants and analyzed CFG to FILE in JSON format") ->type_name("FILE"); + + // Registered whether or not this build can act on it, so that a user on an + // unconfigured build is told a build flag exists instead of being given + // CLI11's bare "unknown option". + bool verify_with_lean = false; + app.add_flag("--verify-with-lean", verify_with_lean, + "After the analysis, ask Lean to prove the inferred invariants " + "sound (implies --print-invariants-to-json)"); + + unsigned lean_heartbeats = 400000; + app.add_option("--lean-heartbeats", lean_heartbeats, + "Elaboration budget per CFG for --verify-with-lean " + "(default 400000)"); + + bool lean_keep_temp = false; + app.add_flag("--lean-keep-temp", lean_keep_temp, + "Keep the exported JSON and the generated Lean files, and print " + "where they are and how to re-run them"); + + bool lean_show_output = false; + app.add_flag("--lean-show-output", lean_show_output, + "Print Lean's full output for a CFG that was not proved"); /// Options for debugging/logging in crab @@ -204,6 +269,35 @@ int main(int argc, char **argv) { CRAB_ERROR("Cannot open file ", filename); } + LeanVerifyOpts leanOpts; + leanOpts.enabled = verify_with_lean; + leanOpts.heartbeats = lean_heartbeats; + leanOpts.keep_temp = lean_keep_temp; + leanOpts.show_output = lean_show_output; + + // Written here rather than left to a temporary that outlives this scope: the + // path has to stay valid until run_program has both exported to it and had + // Lean read it back. + string lean_scratch_json; + if (leanOpts.enabled) { + if (!leanAvailable()) { + CRAB_ERROR("--verify-with-lean is not available: ", + leanUnavailableReason()); + } + // The check reads whatever document the export produced, so if the user did + // not ask for one, produce one for it alone. + if (print_invariants_to_json.empty()) { + const char *tmp = getenv("TMPDIR"); + string dir = tmp ? string(tmp) : string("/tmp"); + if (!dir.empty() && dir.back() == '/') { + dir.pop_back(); + } + lean_scratch_json = + dir + "/crabber-" + std::to_string(getpid()) + ".json"; + print_invariants_to_json = lean_scratch_json; + } + } + CrabIrBuilderOpts irOpts; irOpts.simplify_cfg = simplify; irOpts.cfg_to_dot = cfg_to_dot; @@ -255,7 +349,13 @@ int main(int argc, char **argv) { anaOpts.widening_delay = widening_delay; anaOpts.descending_iters = descending_iters; anaOpts.thresholds_size = thresholds_size; - TestResult res = run_program(ifs, irOpts, anaOpts); + TestResult res = run_program(ifs, irOpts, anaOpts, leanOpts); + + // Only if we made it ourselves; a path the user asked for is theirs to keep, + // and --lean-keep-temp keeps ours too so the failure can be reproduced. + if (!lean_scratch_json.empty() && !leanOpts.keep_temp) { + std::remove(lean_scratch_json.c_str()); + } cout << "\n### TESTS RESULTS ###\n"; cout << "Expected OK : " << res.expected_ok << "\n"; diff --git a/src/lean_verify.cpp b/src/lean_verify.cpp new file mode 100644 index 0000000..99876a3 --- /dev/null +++ b/src/lean_verify.cpp @@ -0,0 +1,445 @@ +#include + +#include + +#include + +#include +#include +#include +#include +#include +#include +#include + +#ifdef CRABBER_WITH_LEAN +#include +#include +#endif + +namespace crabber { + +bool leanAvailable() { +#ifdef CRABBER_WITH_LEAN + return true; +#else + return false; +#endif +} + +std::string leanProjectDir() { +#ifdef CRABBER_WITH_LEAN + return CRABBER_LEAN_PROJECT; +#else + return ""; +#endif +} + +std::string leanReproduceCommand(const std::string &leanFile) { + return "cd " + leanProjectDir() + " && lake env lean " + leanFile; +} + +std::string leanUnavailableReason() { + return "this build was configured without Lean support; reconfigure with " + "-DLAKE_EXECUTABLE=$(which lake)"; +} + +std::string describe(const LeanResult &r) { + std::ostringstream os; + switch (r.verdict) { + case LeanVerdict::Proved: + os << "proved " << r.cfg_name + << " : invariants sound, all assertions proved"; + break; + case LeanVerdict::OutOfScope: + os << "not attempted " << r.cfg_name << " : " << r.detail; + break; + case LeanVerdict::Exhausted: + os << "gave up " << r.cfg_name + << " : elaboration budget exhausted (raise --lean-heartbeats)"; + break; + case LeanVerdict::Skipped: + os << "not checked " << r.cfg_name + << " : called by another CFG; its invariants hold relative to its " + "callers, which this check does not model"; + break; + case LeanVerdict::Unproved: + // Deliberately not "Crab is wrong". A failure here may only mean the proof + // search was too weak, so it must not read as a claim about the analysis. + os << "could not verify " << r.cfg_name << " : " << r.detail; + break; + } + return os.str(); +} + +#ifdef CRABBER_WITH_LEAN + +namespace { + +/** Quote for /bin/sh: wrap in '...', closing and reopening around any quote. */ +std::string shellQuote(const std::string &s) { + std::string out = "'"; + for (char c : s) { + if (c == '\'') { + out += "'\\''"; + } else { + out += c; + } + } + out += "'"; + return out; +} + +/** Escape for a Lean string literal. */ +std::string leanString(const std::string &s) { + std::string out = "\""; + for (char c : s) { + if (c == '"' || c == '\\') { + out += '\\'; + } + out += c; + } + out += "\""; + return out; +} + +/** + * Absolute form of `path`. + * + * Load-bearing rather than tidiness: Lean runs with its working directory set + * to the Lean project, not to wherever crabber was invoked, so a relative path + * in the generated file would resolve somewhere else or not at all. + */ +std::string absolutePath(const std::string &path) { + char buf[PATH_MAX]; + if (realpath(path.c_str(), buf) != nullptr) { + return std::string(buf); + } + return path; +} + +std::string tempDir() { + if (const char *t = getenv("TMPDIR")) { + std::string d(t); + if (!d.empty() && d.back() == '/') { + d.pop_back(); + } + return d; + } + return "/tmp"; +} + +/** The Lean file for one CFG. Everything program-specific is the two strings. */ +void writeProofFile(const std::string &path, const std::string &jsonAbs, + const std::string &cfgName, unsigned heartbeats) { + std::ofstream ofs(path); + ofs << "import CrabberJson.Elab\n" + << "set_option maxHeartbeats " << heartbeats << "\n" + << "namespace CrabberJson.Generated\n" + << "crab_program " << leanString(jsonAbs) << " cfg " + << leanString(cfgName) << "\n" + << "crab_verify\n" + << "end CrabberJson.Generated\n"; +} + +struct RunOutput { + int exit_code; + std::string text; +}; + +/** + * Run `lake env lean ` with the Lean project as working directory. + * + * `lake env` supplies LEAN_PATH for that project without adding the file to its + * build graph, so nothing is written into the source tree and the file need not + * live there. Lean writes diagnostics to stdout and lake may write its own + * noise to stderr, so both are merged and read together. + */ +RunOutput runLean(const std::string &leanFile) { + const std::string cmd = "cd " + shellQuote(CRABBER_LEAN_PROJECT) + " && " + + shellQuote(CRABBER_LAKE) + " env lean " + + shellQuote(leanFile) + " 2>&1"; + + FILE *pipe = popen(cmd.c_str(), "r"); + if (!pipe) { + CRAB_ERROR("could not execute ", CRABBER_LAKE); + } + std::string text; + char buf[4096]; + while (std::fgets(buf, sizeof(buf), pipe) != nullptr) { + text += buf; + } + const int status = pclose(pipe); + const int code = WIFEXITED(status) ? WEXITSTATUS(status) : -1; + return {code, text}; +} + +/** First line of Lean's output, trimmed of its file:line:col prefix. */ +std::string firstMessage(const std::string &text) { + std::istringstream is(text); + std::string line; + while (std::getline(is, line)) { + if (line.empty()) { + continue; + } + // Lean prefixes diagnostics with "::: error: ". + const std::string marker = "error: "; + const size_t at = line.find(marker); + std::string msg = (at != std::string::npos) ? line.substr(at + marker.size()) + : line; + // Lean's message ends in a colon introducing the detail below it. Whether + // that detail is printed depends on there being a counterexample, so the + // colon would otherwise dangle. + if (!msg.empty() && msg.back() == ':') { + msg.pop_back(); + } + return msg; + } + return "no output"; +} + +LeanVerdict classify(const RunOutput &out) { + if (out.exit_code == 0) { + return LeanVerdict::Proved; + } + // The reader names the construct it refuses, which is what lets an + // unsupported program be reported as out of scope rather than as a failure. + // + // This phrase is a contract with the Lean side: every refusal there that means + // "this program is outside what the semantics models", as opposed to "the + // document is malformed", spells it out verbatim. Grep for it in + // lean/CrabberJson/Schema.lean before changing either end. + if (out.text.find("outside the fragment this library models") != + std::string::npos) { + return LeanVerdict::OutOfScope; + } + if (out.text.find("maximum number of heartbeats") != std::string::npos) { + return LeanVerdict::Exhausted; + } + return LeanVerdict::Unproved; +} + +/** Replace whole-word occurrences of `from` with `to`. */ +std::string replaceWord(std::string s, const std::string &from, + const std::string &to) { + const auto isWordChar = [](char c) { + return std::isalnum(static_cast(c)) || c == '_'; + }; + size_t at = 0; + while ((at = s.find(from, at)) != std::string::npos) { + const bool leftOk = (at == 0) || !isWordChar(s[at - 1]); + const size_t after = at + from.size(); + const bool rightOk = (after >= s.size()) || !isWordChar(s[after]); + if (leftOk && rightOk) { + s.replace(at, from.size(), to); + at += to.size(); + } else { + at = after; + } + } + return s; +} + +std::string trim(const std::string &s) { + size_t b = s.find_first_not_of(" \t"); + if (b == std::string::npos) { + return ""; + } + size_t e = s.find_last_not_of(" \t"); + return s.substr(b, e - b + 1); +} + +/** + * The counterexample `omega` reports, restated in the program's variables. + * + * Lean prints it against placeholder names with the bindings below: + * + * a possible counterexample may satisfy the constraints + * 101 <= a <= 200 + * where + * a := sigma.ints "y" + * + * which is unreadable next to a CrabIR program. Substituting the bindings turns + * that into `101 <= y <= 200` -- a statement about the program, which is what + * makes it worth printing at all. + * + * Only the first block is taken. A failing CFG may produce several, and the rest + * are available through --lean-show-output. + */ +std::string extractCounterexample(const std::string &text) { + const std::string marker = "a possible counterexample may satisfy the constraints"; + const size_t at = text.find(marker); + if (at == std::string::npos) { + return ""; + } + std::istringstream is(text.substr(at + marker.size())); + std::string line; + + std::vector constraints; + while (std::getline(is, line)) { + const std::string t = trim(line); + if (t.empty()) { + continue; + } + if (t == "where") { + break; + } + // A new diagnostic means the block ended without any bindings. + if (t.find(": error: ") != std::string::npos) { + return ""; + } + constraints.push_back(t); + } + + // ` a := "x"` -- the quoted name is the program variable. + while (std::getline(is, line)) { + const std::string t = trim(line); + if (t.empty() || t.find(": error: ") != std::string::npos) { + break; + } + const size_t assign = t.find(":="); + const size_t open = t.find('"', assign == std::string::npos ? 0 : assign); + if (assign == std::string::npos || open == std::string::npos) { + break; + } + const size_t close = t.find('"', open + 1); + if (close == std::string::npos) { + break; + } + const std::string placeholder = trim(t.substr(0, assign)); + const std::string variable = t.substr(open + 1, close - open - 1); + for (auto &c : constraints) { + c = replaceWord(c, placeholder, variable); + } + } + + std::string out; + for (auto const &c : constraints) { + if (!out.empty()) { + out += ", "; + } + out += c; + } + return out; +} + +/** + * The construct the reader refused, pulled out of its (deliberately long) + * explanation so the report stays one line per CFG. + */ +std::string refusedConstruct(const std::string &text) { + const std::string marker = "statement kind '"; + const size_t at = text.find(marker); + if (at == std::string::npos) { + return "uses a construct the Lean semantics does not model"; + } + const size_t start = at + marker.size(); + const size_t end = text.find('\'', start); + if (end == std::string::npos) { + return "uses a construct the Lean semantics does not model"; + } + return "uses " + text.substr(start, end - start) + + ", which the Lean semantics does not model"; +} + +} // namespace + +std::vector verifyWithLean(const std::string &jsonPath, + const CrabIrBuilder &crabIR, + const LeanVerifyOpts &opts) { + std::vector results; + const std::string jsonAbs = absolutePath(jsonPath); + const std::string dir = tempDir(); + const long pid = static_cast(getpid()); + + auto &cg = const_cast(crabIR).getCallGraph(); + + // Only the roots of the call graph -- the CFGs nothing calls. + // + // A callee's invariants are *conditional on its callers*: Crab's top-down + // inter-procedural analysis derives them from the call sites, so `inc`'s entry + // invariant may be `a >= 5` purely because `main` happens to call it that way. + // The theorem Lean proves quantifies over every initial state, which is a + // strictly stronger claim than Crab made, so a callee checked in isolation + // fails for a reason that says nothing about the analysis. Verifying roots + // keeps the question asked the same as the question answered. + auto entries = cg.entries(); + if (entries.empty()) { + // Every CFG has a caller, so the call graph is one or more cycles with no + // way in. Crab's own analyzer treats all nodes as entries in that case; + // matching it keeps the two sides describing the same runs. + auto p = cg.nodes(); + entries.insert(entries.end(), p.first, p.second); + } + + unsigned index = 0; + for (auto n : entries) { + auto cfg_ref = n.get_cfg(); + if (!cfg_ref.has_func_decl()) { + continue; + } + const std::string name = cfg_ref.get_func_decl().get_func_name(); + + std::ostringstream fileName; + fileName << dir << "/crabber-lean-" << pid << "-" << index++ << ".lean"; + const std::string leanFile = fileName.str(); + + writeProofFile(leanFile, jsonAbs, name, opts.heartbeats); + const RunOutput out = runLean(leanFile); + + LeanResult r; + r.cfg_name = name; + r.verdict = classify(out); + r.output = out.text; + if (r.verdict == LeanVerdict::OutOfScope) { + r.detail = refusedConstruct(out.text); + } else if (r.verdict != LeanVerdict::Proved) { + r.detail = firstMessage(out.text); + r.counterexample = extractCounterexample(out.text); + } + + // Reporting belongs to the caller, which knows about the JSON as well; all + // this decides is whether the file survives. + if (opts.keep_temp) { + r.lean_file = leanFile; + } else { + std::remove(leanFile.c_str()); + } + results.push_back(r); + } + + // Anything the analysis covered but this check did not, named so the gap is + // visible in the report rather than inferred from an absence. + for (auto n : boost::make_iterator_range(cg.nodes())) { + auto cfg_ref = n.get_cfg(); + if (!cfg_ref.has_func_decl()) { + continue; + } + const std::string name = cfg_ref.get_func_decl().get_func_name(); + bool checked = false; + for (auto const &r : results) { + if (r.cfg_name == name) { + checked = true; + break; + } + } + if (!checked) { + LeanResult r; + r.cfg_name = name; + r.verdict = LeanVerdict::Skipped; + results.push_back(r); + } + } + return results; +} + +#else // !CRABBER_WITH_LEAN + +std::vector verifyWithLean(const std::string &, const CrabIrBuilder &, + const LeanVerifyOpts &) { + return {}; +} + +#endif + +} // namespace crabber