Add a new cell benchmark: MutableTree

[samuelchassot]

No description provided.

[vkuncak]

This benchmark did not work for me due to inv check failing.

Maybe we can add this one and turn off termination checking.

import stainless.annotation.*
import stainless.lang.StaticChecks.*
import stainless.lang.*

object MutableTreeWithCell:
  sealed trait Tree
  case class Node(l: Cell[Tree], r: Cell[Tree]) extends Tree
  case class Leaf(x: BigInt) extends Tree

  def mirror(t: Tree): Unit =
    t match
      case Node(l, r) =>
        mirror(l.v)
        mirror(r.v)
        swap(l, r)
      case Leaf(_) => ()
  
  def l(x:BigInt) = Leaf(x)
  def n(l:Tree, r: Tree) = Node(Cell(l), Cell(r))

  def main(): Unit = 
    val t = n(n(l(4), l(3)), n(l(2),l(1)))
    mirror(t)

[samuelchassot]

This benchmark did not work for me due to inv check failing.

Maybe we can add this one and turn off termination checking.

import stainless.annotation.*
import stainless.lang.StaticChecks.*
import stainless.lang.*

object MutableTreeWithCell:
  sealed trait Tree
  case class Node(l: Cell[Tree], r: Cell[Tree]) extends Tree
  case class Leaf(x: BigInt) extends Tree

  def mirror(t: Tree): Unit =
    t match
      case Node(l, r) =>
        mirror(l.v)
        mirror(r.v)
        swap(l, r)
      case Leaf(_) => ()
  
  def l(x:BigInt) = Leaf(x)
  def n(l:Tree, r: Tree) = Node(Cell(l), Cell(r))

  def main(): Unit = 
    val t = n(n(l(4), l(3)), n(l(2),l(1)))
    mirror(t)

Yeah, I know I was trying to make it work but the inv is indeed invalid during the swap operation, so it cannot work with the current implementation. We can indeed turn off termination and keep the first version I had on this PR, without sizes.