Does `mvcgen` support recursive functions?

Stream: Program verification

[Alexander Bentkamp]

It seems recursion is not yet supported?

import Std.Tactic.Do

open Std.Do

def loop (i : Nat) : Except String Nat := do
  match i with
  | 0 => pure 0
  | (n + 1) => loop n

@[spec]
theorem spec (x : Nat):
    ⦃ ⌜ True ⌝ ⦄
    loop x
    ⦃ ⇓ r => ⌜ True ⌝ ⦄ := by
  mvcgen [loop]


-- unsolved goals
-- case vc1
-- x : Nat
-- ⊢ (wp⟦loop x⟧ (PostCond.noThrow fun r => ⌜True⌝)).down

[Sebastian Graf]

This is slightly hacky, but it seems to work?

import Std.Tactic.Do

open Std.Do

def loop (i : Nat) : Except String Nat := do
  match i with
  | 0 => pure 0
  | (n + 1) => loop n

@[spec]
theorem spec (x : Nat):
    ⦃ ⌜ True ⌝ ⦄
    loop x
    ⦃ ⇓ r => ⌜ True ⌝ ⦄ := by
  unfold loop
  mvcgen [spec]

[Alexander Bentkamp]

Ah, of course! That's great, thank you!