rust_array verified

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

import CodeLib

set_option maxRecDepth 1048576

namespace Project.RustArray

open Wasm

def func0 : Wasm.Program :=
  [
  .localGet 1,
  .ret
]

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

def func1 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .call 2,
  .const (1 : UInt32),
  .and,
  .ret
]

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

def func2 : Wasm.Program :=
  [
  .localGet 1,
  .const (0 : UInt32),
  .eq,
  .const (1 : UInt32),
  .and,
  .ret
]

def func2Def : Wasm.Function :=
  { params := [.i32, .i32], locals := [], body := func2, results := [.i32] }

/-- export: entrypoint -/
def func3 : Wasm.Program :=
  [
  .globalGet 0,
  .const (16 : UInt32),
  .sub,
  .localSet 1,
  .localGet 1,
  .globalSet 0,
  .localGet 0,
  .load32 (0 : UInt32),
  .localSet 2,
  .localGet 0,
  .load32 (4 : UInt32),
  .localSet 3,
  .localGet 1,
  .localGet 2,
  .store32 (0 : UInt32),
  .localGet 1,
  .localGet 3,
  .store32 (4 : UInt32),
  .localGet 1,
  .call 4,
  .drop,
  .localGet 0,
  .load32 (0 : UInt32),
  .localSet 4,
  .localGet 0,
  .load32 (4 : UInt32),
  .localSet 5,
  .localGet 1,
  .localGet 4,
  .store32 (8 : UInt32),
  .localGet 1,
  .localGet 5,
  .store32 (12 : UInt32),
  .localGet 1,
  .const (8 : UInt32),
  .add,
  .call 5,
  .drop,
  .localGet 1,
  .const (16 : UInt32),
  .add,
  .globalSet 0,
  .ret
]

def func3Def : Wasm.Function :=
  { params := [.i32], locals := [.i32, .i32, .i32, .i32, .i32], body := func3, results := [] }

/-- export: len -/
def func4 : Wasm.Program :=
  [
  .localGet 0,
  .load32 (0 : UInt32),
  .localGet 0,
  .load32 (4 : UInt32),
  .call 0,
  .ret
]

def func4Def : Wasm.Function :=
  { params := [.i32], locals := [], body := func4, results := [.i32] }

/-- export: is_empty -/
def func5 : Wasm.Program :=
  [
  .localGet 0,
  .load32 (0 : UInt32),
  .localGet 0,
  .load32 (4 : UInt32),
  .call 1,
  .const (1 : UInt32),
  .and,
  .ret
]

def func5Def : Wasm.Function :=
  { params := [.i32], locals := [], body := func5, results := [.i32] }

def «module» : Wasm.Module :=
{
  imports := [],
  funcs := [
    func0Def,
    func1Def,
    func2Def,
    func3Def,
    func4Def,
    func5Def
  ],
  exports := [
    { name := "entrypoint", funcIdx := 3 },
    { name := "len", funcIdx := 4 },
    { name := "is_empty", funcIdx := 5 }
  ],
  memory := some { pagesMin := (16 : UInt32), pagesMax := none, data := [] },
  globals := [
    { init := .i32 (1048576 : UInt32) },
    { init := .i32 (1048576 : UInt32) },
    { init := .i32 (1048576 : UInt32) }
  ],
  types := [
    { params := [.i32, .i32], results := [.i32] },
    { params := [.i32], results := [] },
    { params := [.i32], results := [.i32] }
  ],
  tables := [
    { min := 1, max := some 1, elemType := .funcref }
  ],
  elements := []
}

end Project.RustArray

import Project.RustArray.Program
import Interpreter.Wasm.Wp.Call

/-!
# Specs for the `rust_array` slice primitive corpus

Two layers, both discharged by reusing the `CodeLib/RustStd/Array` chunks:

* the internal raw `(ptr, len)` bodies (`func0` = `len`, `func2` = `is_empty`),
  reusing the CodeLib leaf bridges `lenBodyTerminates` / `isEmptyBodyTerminates`
  (both instances of the trunk's `unSliceBodyTerminates`); and
* the exported ABI wrappers (`func4` = `len`, `func5` = `is_empty`), which receive
  the slice as a fat pointer in linear memory: they `load32` the `(dataPtr, len)`
  fields back with `fatPtrLoadWp` and then `call` the bodies above (`is_empty`
  through the `crate::is_empty` re-mask wrapper `func1`). The export specs are
  therefore conditional on the caller having laid a fat pointer in memory at the
  argument pointer `p` — the shared `FatPtrAt` contract (`dataPtr` at `p+0`, `len`
  at `p+4`, in bounds). They are *conditional total correctness*: given that
  contract the call terminates with the right value; the out-of-bounds case
  (where the `load32` traps) is outside the contract and deliberately not
  asserted.
-/

namespace Project.RustArray.Spec

open Wasm Wasm.RustStd Wasm.RustStd.Array

/-! ## Call bridges

Each bridge is the callee's behaviour at an *arbitrary* store (these bodies touch
no memory), reusing the CodeLib `Array` chunks. They serve both layers: the
internal specs below are each the matching bridge at `«module».initialStore`, and
the exported wrappers `call` the same body after marshalling the fat pointer back
from memory. -/

/-- `func0` (`len` body) as a callee: returns the length argument, via the CodeLib
leaf bridge `lenBodyTerminates`. -/
private theorem len_call {env : HostEnv Unit} (st : Store Unit)
    (dataPtr len : UInt32) (rest : List Value) :
    TerminatesWith env «module» 0 st (.i32 len :: .i32 dataPtr :: rest)
      (fun st' vs => vs = .i32 len :: rest ∧ framePost st st') :=
  lenBodyTerminates st dataPtr len rest rfl rfl rfl rfl

/-- `func2` (`is_empty` leaf body) as a callee: returns `isEmptyValue len`,
reusing the CodeLib leaf bridge `isEmptyBodyTerminates`. -/
private theorem isEmptyLeaf_call {env : HostEnv Unit} (st : Store Unit)
    (dataPtr len : UInt32) (rest : List Value) :
    TerminatesWith env «module» 2 st (.i32 len :: .i32 dataPtr :: rest)
      (fun st' vs => vs = .i32 (isEmptyValue len) :: rest ∧ framePost st st') :=
  isEmptyBodyTerminates st dataPtr len rest rfl rfl rfl rfl

/-- `func1` (`crate::is_empty`) as a callee: calls the leaf `is_empty` and
re-masks the bool with `& 1`, which `isEmptyValue_and_one` collapses. -/
private theorem crateIsEmpty_call {env : HostEnv Unit} (st : Store Unit)
    (dataPtr len : UInt32) (rest : List Value) :
    TerminatesWith env «module» 1 st (.i32 len :: .i32 dataPtr :: rest)
      (fun _ vs => vs = .i32 (isEmptyValue len) :: rest) := by
  apply TerminatesWith.of_wp_entry_for (f := func1Def) rfl
  unfold func1Def func1
  wp_run
  apply wp_call_tw (isEmptyLeaf_call st dataPtr len [])
  intro st1 vs1 h1
  obtain ⟨hvs1, _⟩ := h1
  subst hvs1
  wp_run
  rw [isEmptyValue_and_one]
  simp

/-! ## Internal `(ptr, len)` body specs

Each is the matching call bridge at `«module».initialStore` with an empty trailing
stack (`.mono` drops the `framePost` frame the caller-facing spec doesn't need). -/

@[spec_of "rust-internal" "rust_array::len"]
def LenSpec : Prop := ∀ (env : HostEnv Unit) (ptr len : UInt32),
  TerminatesWith env «module» 0 «module».initialStore [.i32 len, .i32 ptr]
    (fun _ rs => rs = [.i32 len])

@[proves Project.RustArray.Spec.LenSpec]
theorem len_correct : LenSpec := by
  intro env ptr len
  exact (len_call «module».initialStore ptr len []).mono (fun _ _ h => h.1)

@[spec_of "rust-internal" "rust_array::is_empty"]
def IsEmptySpec : Prop := ∀ (env : HostEnv Unit) (ptr len : UInt32),
  TerminatesWith env «module» 2 «module».initialStore [.i32 len, .i32 ptr]
    (fun _ rs => rs = [.i32 (isEmptyValue len)])

@[proves Project.RustArray.Spec.IsEmptySpec]
theorem is_empty_correct : IsEmptySpec := by
  intro env ptr len
  exact (isEmptyLeaf_call «module».initialStore ptr len []).mono (fun _ _ h => h.1)

/-! ## Exported ABI wrappers (fat pointer in memory) -/

@[spec_of "rust-exported" "rust_array::len"]
def LenExportSpec : Prop := ∀ (env : HostEnv Unit) (st : Store Unit) (p dataPtr len : UInt32),
  FatPtrAt st p dataPtr len →
  TerminatesWith env «module» 4 st [.i32 p]
    (fun _ rs => rs = [.i32 len])

@[proves Project.RustArray.Spec.LenExportSpec]
theorem len_export_correct : LenExportSpec := by
  intro env st p dataPtr len hfat
  open_slice_export func4Def, func4 at p, dataPtr, len using hfat
  apply wp_call_tw (len_call st dataPtr len [])
  intro st1 vs1 h1
  obtain ⟨hvs1, _⟩ := h1
  subst hvs1
  wp_run
  simp

@[spec_of "rust-exported" "rust_array::is_empty"]
def IsEmptyExportSpec : Prop := ∀ (env : HostEnv Unit) (st : Store Unit) (p dataPtr len : UInt32),
  FatPtrAt st p dataPtr len →
  TerminatesWith env «module» 5 st [.i32 p]
    (fun _ rs => rs = [.i32 (isEmptyValue len)])

@[proves Project.RustArray.Spec.IsEmptyExportSpec]
theorem is_empty_export_correct : IsEmptyExportSpec := by
  intro env st p dataPtr len hfat
  open_slice_export func5Def, func5 at p, dataPtr, len using hfat
  apply wp_call_tw (crateIsEmpty_call st dataPtr len [])
  intro st1 vs1 h1
  subst h1
  wp_run
  rw [isEmptyValue_and_one]
  simp

end Project.RustArray.Spec

//! Slice primitive corpus. The primitive helpers are generic over `T`; these
//! wrappers pick one concrete monomorphization so the verifier has wasm to lift.
//! The emitted `len`/`is_empty` bodies only inspect the slice length, so the
//! codelib theorems are about the `&[T]` fat-pointer shape, not this element type.

#[unsafe(no_mangle)]
pub extern "C" fn len(xs: &[u8]) -> usize {
    crate::len(xs)
}

#[unsafe(no_mangle)]
pub extern "C" fn is_empty(xs: &[u8]) -> bool {
    crate::is_empty(xs)
}

#[unsafe(no_mangle)]
pub extern "C" fn entrypoint(xs: &[u8]) {
    let _ = len(xs);
    let _ = is_empty(xs);
}

#![allow(improper_ctypes_definitions)]

mod exports;

/// Primitive slice length operation for `&[T]`.
pub fn len<T>(xs: &[T]) -> usize {
    xs.len()
}

/// Primitive slice emptiness operation for `&[T]`.
pub fn is_empty<T>(xs: &[T]) -> bool {
    xs.is_empty()
}

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

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

[dependencies]