[SwayamInSync]

A Lean goal was one disjunction: the negation of every assumption before what it must show. A proof found its way to the conclusion by counting disjuncts, and nothing said which disjunct was the precondition, which a callee's postcondition, which the value of a variable:

def cppverify_twice_edf933_postcondition_28de726e : Prop :=
  ∀ … ,
    ¬(… x_0 …) ∨ ¬(…) ∨ (…) ∨ ¬((…) ∧ __local_call_1_1 = x_0 + (BitVec.ofInt 32 (1))) ∨ ¬(a_1 = __local_call_1_1) ∨ … ∨ …

Each goal now also has a readable form, with a bridge to the goal that the kernel checks:

def cppverify_twice_edf933_postcondition_28de726e.readable : Prop :=
  ∀ … (x_0 : BitVec 32),
    (h_pre_1 : (cppBvSle (BitVec.ofInt 32 (0)) x_0) ∧ (cppBvSlt x_0 (BitVec.ofInt 32 (50)))) →
    (h_null_1 : (heapSelectInt __heap_alloc_0 (0 : Int)) = (0 : Int)) →
    (h_null_2 : ¬(heapSelectBool __heap_live_0 (0 : Int))) →
    (h_call_next_1 : (…) ∧ __local_call_1_1 = x_0 + (BitVec.ofInt 32 (1))) →
    (h_a_1 : a_1 = __local_call_1_1) →
    (h_call_next_2 : (…) ∧ __local_call_2_1 = a_1 + (BitVec.ofInt 32 (1))) →
    (h_b_1 : b_1 = __local_call_2_1) →
    (h_result_1 : __result_1 = b_1) →
    (…) ∧ __result_1 = x_0 + (BitVec.ofInt 32 (2))

theorem cppverify_twice_edf933_postcondition_28de726e.of_readable (h : ….readable) : cppverify_twice_edf933_postcondition_28de726e :=
  fun … x_0 =>
  cppverify_imp_or fun h_pre_1 =>
  …
  h … x_0 h_pre_1 h_null_1 h_null_2 h_call_next_1 h_a_1 h_call_next_2 h_b_1 h_result_1

A new proof file starts from it, with every name introduced, and a proof can use the hypotheses by name:

theorem cppverify_twice_edf933_postcondition_28de726e_proof : cppverify_twice_edf933_postcondition_28de726e := by
  apply cppverify_twice_edf933_postcondition_28de726e.of_readable
  intro __heap_alloc_0 __heap_live_0 __local_call_1_1 __local_call_2_1 __result_1 a_1 b_1 x_0 h_pre_1 h_null_1 h_null_2 h_call_next_1 h_a_1 h_call_next_2 h_b_1 h_result_1
  obtain ⟨_, first⟩ := h_call_next_1
  obtain ⟨_, second⟩ := h_call_next_2
  subst h_result_1 h_b_1 second h_a_1 first
  …

Design

Decision 6 of the Lean plan: the canonical goal stays the anchor, which certification checks and identity hashes, and the readable form is a checked consequence. Frama-C's WP labels each step of a sequent by kind (Type:, Have:, When:) and with the property it comes from; Vermilion gives its hypotheses names from its VC generator, with an ordinal for each callee. This takes both, and adds the bridge neither has: Vermilion prints only the sequent, so a printer bug there is a wrong theorem.

• Where each assumption comes from. The passivizer records an origin with every assumption, from a current origin that each statement kind sets and its parts refine:

  • def (a definition), call:f (a callee's postcondition), inv, cond, and exit (a loop), keep (the value a path that skips an assignment keeps), exact (a machine operation's exact value), check, spec:f (a proved spec fact), reads:f, and choose;
  • at entry, pre for a written precondition, entry for a generated one, null, and object.

  makeGoal marks each Or it builds with the origin (LogicExpr::Premise). Like trigger patterns, the mark is outside the term's meaning, hash, and archive; the clones and the in-place simplifier keep it. A goal built elsewhere (spec checks) marks its assumptions fact.

• The readable form peels the marked chain: each hypothesis is the operand its Or negates, or ¬B where simplification folded ¬¬B to B. It is named h_<origin>_<n>, the ordinal counted within the goal so that a line shift renames nothing; a definition is named by what it defines (h_x_1). No name is ever a binder's (h_x_1_1 beside a variable h_x_1). Its lets are the large subterms of the hypotheses and the conclusion. An unmarked disjunction, such as a postcondition !p || q, stays in the conclusion.

• The bridge G.of_readable : G.readable → G is a term with one prelude lemma per hypothesis: cppverify_imp_or : (a → b) → ¬a ∨ b, or cppverify_not_imp_or : (¬a → b) → a ∨ b for a folded one. It builds with Generated.lean, so certification checks every bridge, and a readable form that says less than its goal fails the build.

• Stubs apply the bridge and introduce every name, lets included. A proof of G itself, as earlier projects wrote, still checks, since Check.lean still checks G_proof : G.

Tests

• New suite/lean_readable.cpp:
  • the readable form of each kind of assumption: preconditions, two calls of one callee, a definition, the return value, a loop's invariant, condition, exact value, kept value, and exit, a check proved before, a spec's postcondition at two applications, an extent and an object at entry, a name that a variable already has, and a postcondition's own disjunction kept as the conclusion;
  • the bridge, and the stub with its names;
  • a goal large enough to get lets, whose stub introduces them;
  • every stub of the project builds;
  • proofs that use the hypotheses by name certify;
  • a readable form changed to say less than its goal fails at its bridge: Application type mismatch: The argument h_b_1 has type b_1 = __local_call_2_1 but is expected to have type b_1 = x_0 + BitVec.ofInt 32 2.
• Updated: lean_certify.cpp proves its True goals with trivial, since after the stub's apply the goal is the readable form.
• Lean differential: every suite export (375 files) built as Lean projects, against LM1's results: the same exports, and the same 351 projects build, every bridge included.

Mutants of LeanBackend.cpp, Obligation.cpp, ObligationSimplify.cpp, Passivize.cpp, and Verifier.cpp, each rebuilt and run against the Lean tests: 17 of 19 killed.

• the bridge's two lemmas swapped; a hypothesis always printed as the negated operand; no readable forms;

• assumptions not marked; callee postconditions, statements, invariants, exact values, kept values, or spec postconditions left unnamed; written preconditions taken as generated;

• a hypothesis allowed a variable's name; definitions not named by what they define;

• the parts of a large goal, or the variables, not introduced; stubs without their names; stubs with names taken for proofs.

  The two survivors drop the mark in the generic clones of a goal. No path from makeGoal to the Lean exporter copies a marked Or today (the simplifier rewrites goals in place), so they are equivalent there. The copies stay, so the mark survives a copy as a source location does.

Docs

• tooling.rst: readable forms, the bridge, and stubs in the --lean-project row.
• Book, ch17: "Goals as hypotheses": a goal's readable form, what each kind of name means, the bridge, the stub, a proof by the names, and its certification, all with exact output.
• Release notes: "Lean goals as hypotheses".
• ARCHITECTURE.md: "Readable goals" under the project goals. DESIGN.md: the readable form and the bridge.

Checked

Builds on #58 (stable proof identity) and #56, whose commits come first here until they merge.

• Verify lit suite, release build: 437 passed and 1 unsupported, since this records an origin for every assumption the passivizer makes. The origins are metadata that no solver reads, and the semantic hash and archive are unchanged. VerifyTests: 62 passed, 1 skipped (EncodingParityTest, which needs archives). The assertions build is left to CI.
• Lean differential: above.
• On main, the new test fails from its first check of a readable form.
• Docs: the site builds with -W; docs_coverage.test and docs_examples.test pass, and the book's outputs are from this build. clang-format: clean.