qedgen v2.7.1 F5 followup fixture for QEDGen/solana-skills#12 — axiom → Prop can't satisfy Decidable in requires

README.md

qedgen v2.7.1 F5-followup fixture bundle

Accompanies QEDGen/solana-skills#12.

Single-finding followup on v2.7.1 F5 (axiom emission for uninterpreted helpers in Expr::App position). The axioms now land — but they emit as → Prop and requires position needs a computable, Decidable guard, so lake build rejects the transition function.

Files

File	Role
repro-f5-axiom-decidability.qedspec	13-line minimal repro. Handler with requires foo(state.c) else E and a non-empty effect.
Spec.generated.lean	Full generated Lean from the repro — shows axiom foo : Nat → Prop at line 15 and the if-guard at line 27 that can't resolve Decidable.
lake-build-error.txt	Full lake build output for copy-paste reference.

Reproducing

QEDGEN="$HOME/.agents/skills/qedgen/tools/qedgen"
mkdir repro && cd repro && git init -q
cp ../repro-f5-axiom-decidability.qedspec spec.qedspec
"$QEDGEN" init --name ReproF5 --spec spec.qedspec --output-dir .
"$QEDGEN" codegen --lean --lean-output Spec.lean
rm -rf programs
lake build

Expected output (excerpt):

error: Spec.lean:27:2: failed to synthesize instance of type class
  Decidable (s.status = Status.Active ∧ foo s.c)

Root cause

lean_gen.rs emits uninterpreted helpers as:

axiom foo : Nat → Prop

requires clauses lower to the transition's if-guard:

def hTransition (s : State) (signer : Pubkey) : Option State :=
  if s.status = Status.Active ∧ foo s.c then     -- ← needs Decidable
    some { s with c := 1 }
  else none

axiom … → Prop is opaque and has no Decidable instance, so Lean rejects the if-expression. open Classical + Classical.propDecidable moves past that but makes the definition noncomputable, which applyOp / applyOps pattern-matching downstream doesn't accept.

Fix options (full discussion in issue #12)

1. Emit as → Bool instead of → Prop — auto-decidable, if-guards work naturally. Shortest diff. My recommendation.
2. Pair each axiom with a Decidable instance — typechecks via Classical.propDecidable but noncomputable; breaks downstream applyOp use. Not viable.
3. Emit both a Prop axiom (for proofs) and a Bool companion (for lowering) with a reflection axiom tying them together. Richer but heavier scaffolding.

Environment

• qedgen v2.7.1 (release binary, sha256-verified)
• Lean 4.15.0 / Lake 5.0.0-1165156

lake-build-error.txt

✖ [7/8] Building Spec (654ms)
trace: .> LEAN_PATH=/tmp/repro-f5/lean_solana/.lake/build/lib/lean:/tmp/repro-f5/.lake/build/lib/lean /home/lars/.elan/toolchains/leanprover--lean4---v4.30.0-rc2/bin/lean /tmp/repro-f5/Spec.lean -o /tmp/repro-f5/.lake/build/lib/lean/Spec.olean -i /tmp/repro-f5/.lake/build/lib/lean/Spec.ilean -c /tmp/repro-f5/.lake/build/ir/Spec.c --setup /tmp/repro-f5/.lake/build/ir/Spec.setup.json --json
error: Spec.lean:27:2: failed to synthesize instance of type class
  Decidable (s.status = Status.Active ∧ foo s.c)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
warning: Spec.lean:42:8: declaration uses `sorry`
warning: Spec.lean:43:5: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
error: Lean exited with code 1
Some required targets logged failures:
- Spec

repro-f5-axiom-decidability.qedspec

spec ReproF5
program_id "11111111111111111111111111111111"

type State
  | Active of { c : U8 }

type Error | E

handler h : State.Active -> State.Active {
  permissionless
  requires foo(state.c) else E
  effect { c := 1 }
}

Spec.generated.lean

import QEDGen.Solana.Account
import QEDGen.Solana.Cpi
import QEDGen.Solana.State
import QEDGen.Solana.Valid

namespace ReproF5

open QEDGen.Solana

-- Uninterpreted helpers: declared axiomatically so generated
-- proofs typecheck even though the DSL doesn't model their
-- semantics. Treat each as an abstract property; strengthen
-- into a concrete definition in your support module if you
-- want to discharge it (rather than trust it).
axiom foo : Nat → Prop

inductive Status where
  | Active
  deriving Repr, DecidableEq, BEq

structure State where
  c : Nat
  status : Status
  deriving Repr, DecidableEq, BEq

def hTransition (s : State) (signer : Pubkey) : Option State :=
  if s.status = .Active ∧ (foo (s.c)) then
    some { s with c := 1, status := .Active }
  else none

inductive Operation where
  | h
  deriving Repr, DecidableEq, BEq

def applyOp (s : State) (signer : Pubkey) : Operation → Option State
  | .h => hTransition s signer

-- ============================================================================
-- Abort conditions — operations must reject under specified conditions
-- ============================================================================

theorem h_aborts_if_E (s : State) (signer : Pubkey)
    (h : ¬((foo (s.c)))) : hTransition s signer = none := by
  unfold hTransition
  rw [if_neg (fun hg => h hg.2)]

end ReproF5