RFC: "Safe" monadic assertions for use with `mvcgen`

Proposal

While experimenting with the new Std.do library, I have noticed that, in certain cases, proofs that would normally have to be inlined within a program can in fact be deferred to an extrinsic specification proof without changing the functionality of the code. For instance, consider the following example:

noncomputable def setZero : StateM (Array Nat) Unit := do
  let mut i := 0
  let len := (← get).size
  for _ in [0:len] do
    let ns ← get
    let h : i < ns.size := sorry -- need proof that `i < ns.size`
    modify fun _ => ns.set i 0 h
    i := i + 1

Here, the Array.set function requires an array access validity proof, which we provide via h. Proving h, however, is not possible here (without tacking on invariant properties to the mutated loop variable). To have a sorry-free implementation, one thing you can do is to use an extraneous dite guard conditions, which we know will always evaluate to true:

noncomputable def setZero : StateM (Array Nat) Unit := do
  let mut i := 0
  let len := (← get).size
  for _ in [0:len] do
    let ns ← get
    if h : i < ns.size then
      modify fun _ => ns.set i 0 h
      i := i + 1

Now, rather than having to show h in the program itself, we can instead show it in the correctness proof, where mvcgen creates a VC for the else case that we can show by contradiction:

theorem setZero_spec :
   ⦃⌜True⌝⦄
   setZero
   ⦃⇓ _ => ⌜1 < 2⌝⦄ := by
  unfold setZero
  mvcgen

  case inv =>
    exact ⇓ (i, sp) =>
      ⌜(#gns).size = len⌝ ∧
      ⌜i = sp.rpref.length⌝ ∧
      ⌜i ≤ (#gns).size⌝

  . mintro t
    rename_i h
    mvcgen
    mleave
    simp only [SPred.and_cons, SVal.curry_cons, SVal.curry_nil,
      SVal.uncurry_cons, SVal.uncurry_nil, SPred.and_nil] at h -- see #9363
    grind

  . mleave
    rename_i h
    simp only [SPred.and_cons, SVal.curry_cons, SVal.curry_nil,
      SVal.uncurry_cons, SVal.uncurry_nil, SPred.and_nil] at h
    rename_i _ _ h'
    false_or_by_contra
    apply h'

    -- FIXME `mvcgen` should leave us here
    rename_i hsp _ _
    have : (rpref.reverse ++ x :: suff).length = len := by
      rw [← hsp]
      simp
    rw [List.length_append, List.length_reverse, List.length_cons] at this
    omega

  . mleave
    rename_i h
    simp
    rfl

Using this strategy, we will sometimes also need to provide the else case:

def foo (ns : Array Nat) : StateM Unit Nat := do
  let ns' := ns ++ #[1, 2, 3]
  if h : ns'.size > ns.size then
    pure (ns'[ns.size]'h)
  else
    pure default -- never happens

theorem foo_spec (ns : Array Nat) :
   ⦃⌜True⌝⦄
   foo ns
   ⦃⇓ r => ⌜r = 1⌝⦄ := by
  mvcgen [foo]

  . mleave
    simp

  . mleave
    rename_i h
    false_or_by_contra
    apply h

    -- FIXME `mvcgen` should leave us here
    simp

Ideally, we would have automation to make this easier, so we don't have to explicitly write out any if/else branches. We would like our program to look something like this instead:

def foo : StateM Unit Nat := do
  let ns := #[1, 2, 3]
  pure $ ns[0]'?

Where the ? signals to the elaborator to nest the rest of the code block in an dependent if/else block with a condition hypothesis h, which is substituted in for ?.

However, if we were to do this, there's the question of what to put in the else branch. That's easy if the return type is inhabited, since we can just use pure default as above. If it isn't, however, we might want to have a special exception type, which we could throw in the else case when using a compatible monad:

structure AssertException where

abbrev AStateT := fun σ m => ExceptT AssertException (StateT σ m)
abbrev AStateM := fun σ => AStateT σ Id

structure SNat where
  n : Nat

-- This definition:
--
-- def foo (ns : Array Nat) : AStateM Unit SNat := do
--   let ns' := ns ++ #[1, 2, 3]
--   pure (.mk (ns'[ns.size]'?))
--
-- Elaborates to:
def foo (ns : Array Nat) : AStateM Unit SNat := do
  let ns' := ns ++ #[1, 2, 3]
  if h : ns'.size > ns.size then
    pure (.mk (ns'[ns.size]'h))
  else
    throw .mk

theorem foo_spec (ns : Array Nat) :
   ⦃⌜True⌝⦄
   foo ns
   ⦃⇓ r => ⌜r = .mk 1⌝⦄ := by
  mvcgen [foo]

  . mleave
    simp

  . mleave
    rename_i h
    false_or_by_contra
    apply h

    -- FIXME `mvcgen` should leave us here
    simp

Though perhaps that's not the only way about it.

The functionality being requested here is similar to what we already have with the assert! [cond] command. But rather than panicking when the assertion condition is violated, we branch off into a provably unreachable part of the code. Another similar piece of syntax sugar is unless [cond] do ..., which we could adapt in our case as unless [cond] do pure default/unless [cond] do throw .mk, but this doesn't quite get use there since unless doesn't allow you to bind a proof of the condition for you to use (unless h : [cond] do throw .mk is a syntax error). But unless seems to be the closest existing thing to what we want here.

Community Feedback

Briefly discussed in DMs with @sgraf812

Start with the proposal's examples using Std.do, mvcgen, assert!, and unless, then trace how dependent-if elaboration and exception behavior would interact. Done means an agreed design for safe monadic assertions, including proof binding and handling the unreachable else branch.