total_variation verified

/-
  AUTO-GENERATED by `verifier emit`. Do not edit by hand.
-/

import CodeLib

set_option maxRecDepth 1048576

namespace Project.TotalVariation

open Wasm

def func0 : Wasm.Program :=
  [
  .globalGet 0,
  .const (16 : UInt32),
  .sub,
  .localSet 2,
  .block 0 0 [
    .block 0 0 [
      .localGet 0,
      .localGet 1,
      .ltUI64,
      .const (1 : UInt32),
      .and,
      .br_if 0,
      .localGet 2,
      .localGet 0,
      .localGet 1,
      .subI64,
      .store64 (8 : UInt32),
      .br 1
    ],
    .localGet 2,
    .localGet 1,
    .localGet 0,
    .subI64,
    .store64 (8 : UInt32)
  ],
  .localGet 2,
  .load64 (8 : UInt32),
  .ret
]

def func0Def : Wasm.Function :=
  { params := [.i64, .i64], locals := [.i32], body := func0, results := [.i64] }

/-- export: total_variation -/
def func1 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .call 0,
  .localGet 1,
  .localGet 2,
  .call 0,
  .addI64,
  .ret
]

def func1Def : Wasm.Function :=
  { params := [.i64, .i64, .i64], locals := [], body := func1, results := [.i64] }

def «module» : Wasm.Module :=
{
  imports := [],
  funcs := [
    func0Def,
    func1Def
  ],
  exports := [
    { name := "total_variation", funcIdx := 1 }
  ],
  memory := some { pagesMin := (16 : UInt32), pagesMax := none, data := [] },
  globals := [
    { init := .i32 (1048576 : UInt32) },
    { init := .i32 (1048576 : UInt32) },
    { init := .i32 (1048576 : UInt32) }
  ],
  types := [
    { params := [.i64, .i64], results := [.i64] },
    { params := [.i64, .i64, .i64], results := [.i64] }
  ],
  tables := [
    { min := 1, max := some 1, elemType := .funcref }
  ],
  elements := []
}

end Project.TotalVariation

import Project.TotalVariation.Program

/-!
# `total_variation a b c = |a-b| + |b-c|`

The proof uses iris-lean's WP over the small-step machine. Both generated
calls reuse the contextual `absDiff_smallStep_wp_to_return` body rule.
-/

namespace Project.TotalVariation.Spec

open Wasm Wasm.RustStd.U64
open Iris Iris.ProgramLogic Language.Notation Std
open Wasm.SepLogic Wasm.SmallStep

def totalVariationConfig (a b c : UInt64) : Config Unit :=
  let initial := «module».initialStore
  { expr := .running
      ⟨⟨[.i64 a, .i64 b, .i64 c], [], []⟩,
        func1, 1, [], [], []⟩
    store :=
      { runtime := { module := «module», host := {} }
        wasm := { initial with mem := initial.mem.write64 1048568 0 } } }

@[spec_of "rust-exported" "total_variation::total_variation"]
def TotalVariationSpec : Prop :=
  ∀ (a b c : UInt64),
    PartiallyMeets (totalVariationConfig a b c)
      (fun rs _ => rs =
        [.i64 ((if a < b then b - a else a - b)
             + (if b < c then c - b else b - c))])

set_option maxHeartbeats 8000000 in
@[proves Project.TotalVariation.Spec.TotalVariationSpec]
theorem total_variation_correct : TotalVariationSpec := by
  intro a b c
  apply wasm_smallStep_heap_globals_runtime_partiallyMeets.{0}
      (α := Unit)
      (σ := absDiffHeap 0)
      (globalσ := absDiffGlobals)
      (φ := fun rs => rs =
        [.i64 ((if a < b then b - a else a - b)
             + (if b < c then c - b else b - c))])
  · simpa [totalVariationConfig, absDiffBodyConfig] using
      absDiffBodyHeap_agrees «module» «module».initialStore a b 0
  · apply absDiffBodyHeap_inBounds «module» «module».initialStore a b 0
    decide
  · simpa [totalVariationConfig, absDiffBodyConfig] using
      absDiffBodyGlobals_agree «module» «module».initialStore a b 0 rfl
  · intro gs
    iintro ⟨Hbytes, Hglobals, Hruntime⟩
    ihave Hscratch := absDiffHeap_pointsTo 0 $$ Hbytes
    ihave Hglobal := absDiffGlobals_pointsTo $$ Hglobals
    simp only [totalVariationConfig, func1]
    iapply wp_localGet rfl
    inext
    iapply wp_localGet rfl
    inext
    iapply wp_call «module» 0 func0Def (by simp [«module»]) (by simp [«module»]) $$
      Hruntime
    inext
    iintro Hruntime
    simp [func0Def, Function.toLocals, Function.numParams, ValueType.zero]
    rw [show func0 = absDiffBody by rfl]
    iapply absDiff_smallStep_wp_to_return
      (runtimeModuleOwn «module») _ 1048576 a b 0 (by decide) (by decide)
    · iintro ⟨Hruntime, Hglobal, Hscratch⟩
      iapply wp_returnFromCallExplicit
      inext
      iapply wp_localGet rfl
      inext
      iapply wp_localGet rfl
      inext
      simp only [List.take, UInt32.reduceSub, UInt32.reduceAdd]
      iapply wp_call «module» 0 func0Def (by simp [«module»]) (by simp [«module»]) $$
        Hruntime
      inext
      iintro Hruntime
      simp [func0Def, Function.toLocals, Function.numParams, ValueType.zero]
      rw [show func0 = absDiffBody by rfl]
      iapply absDiff_smallStep_wp_to_return
        (runtimeModuleOwn «module») _ 1048576 b c
        (if a < b then b - a else a - b) (by decide) (by decide)
      · iintro ⟨Hruntime, Hglobal, Hscratch⟩
        iapply wp_returnFromCallExplicit
        inext
        simp only [List.take, List.singleton_append]
        iapply wp_addI64
        inext
        iapply wp_returnFromFunction
        inext
        iapply wp_value'
        ipureintro
        rfl
      · simp only [UInt32.reduceSub, UInt32.reduceAdd]
        iframe
    · simp only [UInt32.reduceSub, UInt32.reduceAdd]
      iframe

end Project.TotalVariation.Spec

#[unsafe(no_mangle)]
pub extern "C" fn total_variation(a: u64, b: u64, c: u64) -> u64 {
    a.abs_diff(b).wrapping_add(b.abs_diff(c))
}

mod exports;

[package]
name = "total_variation"
version = "0.1.0"
edition = "2024"

[lib]
crate-type = ["cdylib", "rlib"]

[dependencies]