Hacktoberfest 2026: the issues maintainers tagged for October, open and beginner-friendly. Browse Hacktoberfest issues

vcgen: spec not applicable when a program argument is a projection `(mk e).env` that reduces to the spec's argument

Open
  • Is something wrong?
#15,732 0 comments 0 reactions 0 assignees View on GitHub

Maintainers usually reply within 1 day

Nobody has claimed this yet.

Assessment

Difficulty
4/5
Estimated time
3-5 days
Newbie friendliness
35/100
Issue type
Bug
Clarity
Clearly specified
Activity status
Active
Domain
devtools

Research direction

Start from the standalone reproducer in the issue: prog_spec runs sym only [] => vcgen [prog, callee_spec] <;> finish and fails with 'No spec applicable' when the argument is (mk e).env. Find where vcgen matches program arguments against a spec's stated arguments, and check why (mk e).env is not reduced to e there, even though it is rfl-equal. Done when prog_spec compiles without restating callee_spec at the projection form.

Written by the indexing model from the issue text.

Description

This issue was written by Claude (an AI assistant) on behalf of @nomeata.

Found while moving con-leche's cached-to-pure simulation proofs (a few thousand lines) to vcgen + grind (sym … => vcgen … <;> finish). Each case has a workaround in con-leche; the reproducer below is standalone.

vcgen instantiates a callee spec against the program's arguments up to
reducible unfolding only: an argument (mk e).env — the field of a
structure built by a plain def — is not matched against a spec stated
at e when e is already fixed by another argument, although
(mk e).env reduces to e by rfl.

Expected: vcgen [callee_spec] handles callee (mk e) (mk e).env.
Observed (v4.35.0 and nightly-2026-10-15): "No spec applicable to program callee (mk e) (mk e).env …
Candidates were [SpecProof.global callee_spec]" (con-leche's instance of
it reports "No spec found for program …").
(con-leche: certifyNatEqs (sharedOpsC mode fe) fe.env … in checkDeclC
at fe := mkFEnv env, against certifyNatEqsS_spec stated at env.)
Workaround: restate the callee spec at the argument form the program
has (certifyNatOpEqsS_spec, ConLeche/Verify/Cached/BridgeC.lean).

import Std.WP
import Std.Tactic.Do
open Std.WP
open scoped Lean.Order
set_option experimental.vcgen true

abbrev M := StateT Nat (Except String)

structure Box where
  env : Nat

def mk (e : Nat) : Box := ⟨e⟩

def callee (b : Box) (e : Nat) : M Nat := pure (b.env + e)

theorem callee_spec (e : Nat) :
    ⦃fun _ => True⦄ callee (mk e) e ⦃fun v _ => v = e + e; ⊤⦄ := by
  sym only [mk] => vcgen [callee] <;> finish

def prog (e : Nat) : M Nat := callee (mk e) (mk e).env

-- fails: No spec applicable to program callee (mk e) (mk e).env
theorem prog_spec (e : Nat) :
    ⦃fun _ => True⦄ prog e ⦃fun v _ => v = e + e; ⊤⦄ := by
  sym only [] => vcgen [prog, callee_spec] <;> finish
Dominant language
Lean
Stars
9.6k
Forks
1.1k
Avg merge
1d 1h
Merged PRs (30d)
279

Getting set up

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from leanprover/lean4

All issues in leanprover/lean4

Similar issues

More DevTools issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.