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

vcgen: no spec found for a call through a structure projection `ops.op x` with `ops` a concrete instance

Open
  • Is something wrong?
#15,731 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
30/100
Issue type
Bug
Clarity
Clearly specified
Activity status
Active
Domain
devtools

Research direction

Start from the standalone reproducer: prog calls ops.op x, and opImpl_spec is stated about opImpl x. Find where vcgen looks up a spec by the program's head symbol and why it does not unfold the structure projection of the concrete ops instance. Compare with the working spec_proj case. Done when the first example, sym => vcgen [prog, ops, opImpl_spec] <;> finish, closes without the "No spec found" error.

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 looks a spec up by the program's head symbol as written: a call
through a record of operations, (ops).op x with ops a concrete
structure instance, is not matched by a spec stated about the field's
body (opImpl x), although the projection of the instance reduces to it.

Expected: vcgen [opImpl_spec] (or vcgen [ops, opImpl_spec]) handles
(ops).op x, the projection reducing to opImpl x.
Observed (v4.35.0 and nightly-2026-10-15): "No spec found for program (ops).op x"
(con-leche: (sharedOpsC mode fe).isDefEq env d a b vs a triple about
opB mode fe d a b).
Workaround: state the callee spec at the projection form (spec_proj).

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 Ops where
  op : Nat → M Nat

def opImpl (x : Nat) : M Nat := modifyGet fun s => (x, s + 1)

def ops : Ops := ⟨opImpl⟩

def prog (x : Nat) : M Nat := do
  let a ← ops.op x
  pure (a + 1)

theorem opImpl_spec (x : Nat) {s₀ : Nat} :
    ⦃fun s => s = s₀⦄ opImpl x ⦃fun v s' => v = x ∧ s' = s₀ + 1; ⊤⦄ := by
  sorry

/-- fails: "No spec found for program ops.op x" -/
example (x : Nat) {s₀ : Nat} :
    ⦃fun s => s = s₀⦄ prog x ⦃fun v _ => v = x + 1; ⊤⦄ := by
  sym => vcgen [prog, ops, opImpl_spec] <;> finish

theorem spec_proj (x : Nat) {s₀ : Nat} :
    ⦃fun s => s = s₀⦄ ops.op x ⦃fun v s' => v = x ∧ s' = s₀ + 1; ⊤⦄ := opImpl_spec x

/-- works -/
example (x : Nat) {s₀ : Nat} :
    ⦃fun s => s = s₀⦄ prog x ⦃fun v _ => v = x + 1; ⊤⦄ := by
  sym => vcgen [prog, spec_proj] <;> finish
Dominant language
Lean
Stars
9.6k
Forks
1.1k
Avg merge
1d 17m
Merged PRs (30d)
296

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.