rust_array_tests verified

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

import CodeLib

set_option maxRecDepth 1048576

namespace Project.RustArrayTests

open Wasm

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

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

def func1 : Wasm.Program :=
  [
  .localGet 1,
  .const (1 : UInt32),
  .add,
  .ret
]

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

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

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

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

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

def func4 : Wasm.Program :=
  [
  .localGet 0,
  .localGet 1,
  .call 3,
  .const (1 : UInt32),
  .and,
  .const (3 : UInt32),
  .add,
  .ret
]

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

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

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

/-- export: empty_xor_flag -/
def func6 : Wasm.Program :=
  [
  .localGet 0,
  .load32 (0 : UInt32),
  .localGet 0,
  .load32 (4 : UInt32),
  .localGet 1,
  .call 2,
  .ret
]

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

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

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

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

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

def «module» : Wasm.Module :=
{
  imports := [],
  funcs := [
    func0Def,
    func1Def,
    func2Def,
    func3Def,
    func4Def,
    func5Def,
    func6Def,
    func7Def,
    func8Def
  ],
  exports := [
    { name := "empty_plus_three", funcIdx := 5 },
    { name := "empty_xor_flag", funcIdx := 6 },
    { name := "len_plus_arg", funcIdx := 7 },
    { name := "len_plus_one", funcIdx := 8 }
  ],
  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, .i32], results := [.i32] },
    { params := [.i32, .i32], results := [.i32] },
    { params := [.i32], results := [.i32] }
  ],
  tables := [
    { min := 1, max := some 1, elemType := .funcref }
  ],
  elements := []
}

end Project.RustArrayTests

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

/-!
# Reuse tests for the `CodeLib/RustStd/Array` corpus
-/

namespace Project.RustArrayTests.Spec

open Wasm Wasm.RustStd Wasm.RustStd.Array

-- The export proofs below unfold the 9-function module deep enough to need a
-- raised recursion limit; set it once for the file.
set_option maxRecDepth 4096

/-! ## Shared call bridges

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

private theorem isEmpty_call {env : HostEnv Unit} (st : Store Unit)
    (ptr len : UInt32) (rest : List Value) :
    TerminatesWith env «module» 3 st (.i32 len :: .i32 ptr :: rest)
      (fun st' vs => vs = .i32 (isEmptyValue len) :: rest ∧ framePost st st') :=
  isEmptyBodyTerminates st ptr len rest rfl rfl rfl rfl

private theorem lenPlusOne_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 (len + 1) :: rest) := by
  apply TerminatesWith.of_wp_entry_for (f := func1Def) rfl
  unfold func1Def func1
  wp_run
  simp [UInt32.add_comm 1 len]

private theorem lenPlusArg_call {env : HostEnv Unit} (st : Store Unit)
    (dataPtr len n : UInt32) (rest : List Value) :
    TerminatesWith env «module» 0 st (.i32 n :: .i32 len :: .i32 dataPtr :: rest)
      (fun _ vs => vs = .i32 (len + n) :: rest) := by
  apply TerminatesWith.of_wp_entry_for (f := func0Def) rfl
  unfold func0Def func0
  wp_run
  simp [UInt32.add_comm n len]

private theorem emptyPlusThree_call {env : HostEnv Unit} (st : Store Unit)
    (dataPtr len : UInt32) (rest : List Value) :
    TerminatesWith env «module» 4 st (.i32 len :: .i32 dataPtr :: rest)
      (fun _ vs => vs = .i32 (isEmptyValue len + 3) :: rest) := by
  apply TerminatesWith.of_wp_entry_for (f := func4Def) rfl
  unfold func4Def func4
  wp_run
  apply wp_call_tw (isEmpty_call st dataPtr len [])
  intro st1 vs1 h1
  obtain ⟨hvs1, _, _⟩ := h1
  subst hvs1
  wp_run
  rw [isEmptyValue_and_one]
  rw [UInt32.add_comm 3 (isEmptyValue len)]
  simp

private theorem emptyXorFlag_call {env : HostEnv Unit} (st : Store Unit)
    (dataPtr len flag : UInt32) (rest : List Value) :
    TerminatesWith env «module» 2 st (.i32 flag :: .i32 len :: .i32 dataPtr :: rest)
      (fun _ vs => vs = .i32 (isEmptyValue len ^^^ flag) :: rest) := by
  apply TerminatesWith.of_wp_entry_for (f := func2Def) rfl
  unfold func2Def func2
  wp_run
  apply wp_call_tw (isEmpty_call st dataPtr len [])
  intro st1 vs1 h1
  obtain ⟨hvs1, _, _⟩ := h1
  subst hvs1
  wp_run
  rw [isEmptyValue_and_one]
  simp

/-! ## Internal impl-body specs

Each is the matching call bridge at `«module».initialStore` with an empty trailing
stack. -/

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

@[proves Project.RustArrayTests.Spec.LenPlusOneSpec]
theorem len_plus_one_correct : LenPlusOneSpec := by
  intro env ptr len
  exact lenPlusOne_call «module».initialStore ptr len []

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

@[proves Project.RustArrayTests.Spec.LenPlusArgSpec]
theorem len_plus_arg_correct : LenPlusArgSpec := by
  intro env ptr len n
  exact lenPlusArg_call «module».initialStore ptr len n []

@[spec_of "rust-internal" "rust_array_tests::empty_plus_three"]
def EmptyPlusThreeSpec : Prop := ∀ (env : HostEnv Unit) (ptr len : UInt32),
  TerminatesWith env «module» 4 «module».initialStore [.i32 len, .i32 ptr]
    (fun _ rs => rs = [.i32 (isEmptyValue len + 3)])

@[proves Project.RustArrayTests.Spec.EmptyPlusThreeSpec]
theorem empty_plus_three_correct : EmptyPlusThreeSpec := by
  intro env ptr len
  exact emptyPlusThree_call «module».initialStore ptr len []

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

@[proves Project.RustArrayTests.Spec.EmptyXorFlagSpec]
theorem empty_xor_flag_correct : EmptyXorFlagSpec := by
  intro env ptr len flag
  exact emptyXorFlag_call «module».initialStore ptr len flag []

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

The internal specs above verify the inlined-reuse impl bodies. The wasm exports
(`func5`–`func8`) receive the slice as a fat pointer in linear memory: each loads
`(dataPtr, len)` back with `fatPtrLoadWp` and calls the impl body above. So, like
the `rust_u64_tests` crate, the actual exported functions are verified — but
unlike that scalar crate, here end-to-end through the memory marshalling,
conditional on the shared `FatPtrAt` ABI contract, reusing the same call
bridges. -/

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

@[proves Project.RustArrayTests.Spec.LenPlusOneExportSpec]
theorem len_plus_one_export_correct : LenPlusOneExportSpec := by
  intro env st p dataPtr len hfat
  open_slice_export func8Def, func8 at p, dataPtr, len using hfat
  apply wp_call_tw (lenPlusOne_call st dataPtr len [])
  intro st1 vs1 h1
  subst h1
  wp_run
  simp

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

@[proves Project.RustArrayTests.Spec.LenPlusArgExportSpec]
theorem len_plus_arg_export_correct : LenPlusArgExportSpec := by
  intro env st p dataPtr len n hfat
  open_slice_export func7Def, func7 at p, dataPtr, len using hfat
  wp_run
  apply wp_call_tw (lenPlusArg_call st dataPtr len n [])
  intro st1 vs1 h1
  subst h1
  wp_run
  simp

@[spec_of "rust-exported" "rust_array_tests::empty_plus_three"]
def EmptyPlusThreeExportSpec : 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 + 3)])

@[proves Project.RustArrayTests.Spec.EmptyPlusThreeExportSpec]
theorem empty_plus_three_export_correct : EmptyPlusThreeExportSpec := by
  intro env st p dataPtr len hfat
  open_slice_export func5Def, func5 at p, dataPtr, len using hfat
  apply wp_call_tw (emptyPlusThree_call st dataPtr len [])
  intro st1 vs1 h1
  subst h1
  wp_run
  simp

@[spec_of "rust-exported" "rust_array_tests::empty_xor_flag"]
def EmptyXorFlagExportSpec : Prop :=
  ∀ (env : HostEnv Unit) (st : Store Unit) (p dataPtr len flag : UInt32),
    FatPtrAt st p dataPtr len →
    TerminatesWith env «module» 6 st [.i32 flag, .i32 p]
      (fun _ rs => rs = [.i32 (isEmptyValue len ^^^ flag)])

@[proves Project.RustArrayTests.Spec.EmptyXorFlagExportSpec]
theorem empty_xor_flag_export_correct : EmptyXorFlagExportSpec := by
  intro env st p dataPtr len flag hfat
  open_slice_export func6Def, func6 at p, dataPtr, len using hfat
  wp_run
  apply wp_call_tw (emptyXorFlag_call st dataPtr len flag [])
  intro st1 vs1 h1
  subst h1
  wp_run
  simp

end Project.RustArrayTests.Spec

//! Reuse tests for the `CodeLib/RustStd/Array` corpus.
//!
//! Each primitive gets two structurally-distinct users. At opt-0 `len` inlines to
//! a length read while `is_empty` lowers to a `call`, so the two shapes the chunk
//! corpus targets are both exercised: the inlined-`len` read is stepped directly
//! by `wp_run` (`wp_localGet_cons`/`wp_add_cons`), while the `is_empty` `call`
//! reuses the CodeLib `isEmptyBodyTerminates` leaf bridge. The source helpers are generic
//! over `T`; these wrappers only choose a concrete monomorphization so Rust emits
//! wasm.

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

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

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

#[unsafe(no_mangle)]
pub extern "C" fn empty_xor_flag(xs: &[u8], flag: u32) -> u32 {
    crate::empty_xor_flag(xs, flag)
}

#![allow(improper_ctypes_definitions)]

mod exports;

/// Inline `len` use followed by arithmetic.
pub fn len_plus_one<T>(xs: &[T]) -> usize {
    xs.len() + 1
}

/// Inline `len` use combined with an independent argument.
pub fn len_plus_arg<T>(xs: &[T], n: usize) -> usize {
    xs.len() + n
}

/// `is_empty` use (lowered to a `call` at opt-0) followed by arithmetic.
pub fn empty_plus_three<T>(xs: &[T]) -> u32 {
    xs.is_empty() as u32 + 3
}

/// `is_empty` use (lowered to a `call` at opt-0) combined with an independent flag.
pub fn empty_xor_flag<T>(xs: &[T], flag: u32) -> u32 {
    (xs.is_empty() as u32) ^ flag
}

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

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

[dependencies]