--verdict rejects a reused proof after reconstructing a constructor with a function field #1623

What you did

From Bend source commit 234cb9b950800f20b15feafcb4ce2f43e76e7fae, run:

bun bend2/main.ts proof_reuse.bend --check-only
bun bend2/main.ts proof_reuse.bend --verdict
bun bend2/main.ts proof_reuse.bend -o proof_reuse.bendtt

The verdict run uses the unchanged BendTT kernel built with Lean 4.34.0.
The same failure occurs with the constructor expected-type fix in #1620.
I tested a checkout whose safe.ts is byte-identical to that PR's version
at 9144e4e95a69ae9ed325628b84fd79ba7a92ea16.

What happened

Source checking exits 0:

ALL PROOFS CHECK
Use --verdict for mathematical validity.

--verdict exits 1 and reports:

SOME PROOFS FAIL
In use:
expected: {(.Box, (x0, ())) == (.Box, (x0, ())) : Box}
observed: {(.Box, (λx1 => (x0 x1), ())) == (.Box, (λx1 => (x0 x1), ())) : Box}

The usual TypeScript/BendTT mismatch message follows. Export exits 0, emits
the complete theorem, and gives no out-of-scope diagnostic. Running the
unchanged kernel directly on that export gives the same rejection.

The file

Save this as proof_reuse.bend:

type Box is Type:
  Box{value: Type -> Type}

def reflexive(-x: Box) -> {x == x : Box}:
  {==}

def use(h: Box) -> {h == h : Box}:
  match h:
    case Box{f}:
      reflexive(Box{f})

This file has no imports, generic type parameters, templates, recursion,
unsafe code, or open laws.

Controls and expected behavior

Both of these replacements for use pass source checking and --verdict:

# Pass the original value to the same proof.
def use(h: Box) -> {h == h : Box}:
  reflexive(h)

# Prove the same branch goal directly.
def use(h: Box) -> {h == h : Box}:
  match h:
    case Box{f}:
      {==}

As a negative control, a proof of Box{f} == Box{g} from only
reflexive(Box{f}), with unrelated f and g, fails source checking.
These results are the same on main and with the #1620 fix.

The reused reflexivity proof should verify as the direct proof does.
The current behavior prevents this helper from being reused after matching
and reconstructing a value that contains a function.

Where the comparison differs

In safe.ts, ctr_term knows the field type Type -> Type. Its call to
arg_term expands f to x => f(x). The emitted branch calls:

(reflexive -(.Box, (λx1 => (x0 x1), ())))

The helper's result type is {x == x : Box}. Application substitutes the
expanded constructor into that result type. The branch's expected type
still contains the matched field x0, as the diagnostic shows.

Bend source conversion accepts this η equation. BendTT conversion does not
identify the neutral function x0 with λx1 => (x0 x1). Thus a source
proof that works directly fails when the same goal is obtained through a
helper's dependent result type.

This is distinct from #1619/#1620: the field type is declared directly,
and no generic parameter or expected constructor type is missing. It is
also distinct from the lambda-quantity conversion change in #1224. The
comparison here is between a function variable and its η expansion.

Experimental solution

I have an experimental extension of BendTT conversion that accepts this same
emitted proof. It includes Lean proofs of the revised checker's safety
properties. The complete development still exceeds the kernel's file
limit, so it is not ready for an upstream PR. These proofs do not establish
safe.ts translation correctness.

Environment

• Bend: source commit 234cb9b950800f20b15feafcb4ce2f43e76e7fae.
• Additional run: the identical constructor fix from fix(verdict): a bare constructor in a type goes to the kernel at its goal (#1619) #1620; unchanged kernel.
• Bun: 1.3.14.
• Lean: 4.34.0.
• uname -sm: Darwin arm64.
• Clang: Apple clang version 21.0.0 (clang-2100.1.1.101); not used by these checks.