Talos · verification report
← all projects

rust_array_tests verified

rust: rust/rust_array_tests · lean: lean/Project/RustArrayTests · repo @ ee45cadd9455 · leanprover/lean4:v4.32.0
4 / 4 exports have a proven spec
Exports
4
Specs
8
Verifications
8
Diagnostics
8

Formal specs

Project.RustArrayTests.Spec.LenPlusOneSpec lean/Project/RustArrayTests/Spec.lean:35
1 proof

Informal spec

No informal description provided.

Formal statement

LenPlusOneSpec : Prop := ∀ (ptr len : UInt32),

Proofs

↗ Project.RustArrayTests.Spec.len_plus_one_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-internal rust_array_tests::len_plus_one
Project.RustArrayTests.Spec.LenPlusArgSpec lean/Project/RustArrayTests/Spec.lean:60
1 proof

Informal spec

No informal description provided.

Formal statement

LenPlusArgSpec : Prop := ∀ (ptr len n : UInt32),

Proofs

↗ Project.RustArrayTests.Spec.len_plus_arg_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-internal rust_array_tests::len_plus_arg
Project.RustArrayTests.Spec.EmptyPlusThreeSpec lean/Project/RustArrayTests/Spec.lean:85
1 proof

Informal spec

No informal description provided.

Formal statement

EmptyPlusThreeSpec : Prop := ∀ (ptr len : UInt32),

Proofs

↗ Project.RustArrayTests.Spec.empty_plus_three_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-internal rust_array_tests::empty_plus_three
Project.RustArrayTests.Spec.EmptyXorFlagSpec lean/Project/RustArrayTests/Spec.lean:141
1 proof

Informal spec

No informal description provided.

Formal statement

EmptyXorFlagSpec : Prop := ∀ (ptr len flag : UInt32),

Proofs

↗ Project.RustArrayTests.Spec.empty_xor_flag_correct

Rust binding

No @[spec_of "rust-exported" …] reference. Cannot link to a Rust export.

References

  • rust-internal rust_array_tests::empty_xor_flag
Project.RustArrayTests.Spec.LenPlusArgExportSpec lean/Project/RustArrayTests/Spec.lean:259
1 proof

Informal spec

No informal description provided.

Formal statement

LenPlusArgExportSpec : Prop :=

Proofs

↗ Project.RustArrayTests.Spec.len_plus_arg_export_correct

Rust binding

↗len_plus_arg 
fn len_plus_arg(xs: &[u8], n: usize) -> usize

References

  • rust-exported rust_array_tests::len_plus_arg

Exported functions

len_plus_one rust/rust_array_tests/src/exports.rs:11 
fn len_plus_one(xs: &[u8]) -> usize
len_plus_arg rust/rust_array_tests/src/exports.rs:16 
fn len_plus_arg(xs: &[u8], n: usize) -> usize
empty_plus_three rust/rust_array_tests/src/exports.rs:21 
fn empty_plus_three(xs: &[u8]) -> u32
empty_xor_flag rust/rust_array_tests/src/exports.rs:26 
fn empty_xor_flag(xs: &[u8], flag: u32) -> u32

Program (Lean)

Project.RustArrayTests.module lean/Project/RustArrayTests/Program.lean:136 
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 := []
}

Diagnostics

missing_docstring info
lean/Project/RustArrayTests/Spec.lean:35
spec `Project.RustArrayTests.Spec.LenPlusOneSpec` has no `/-- … -/` docstring
missing_docstring info
lean/Project/RustArrayTests/Spec.lean:60
spec `Project.RustArrayTests.Spec.LenPlusArgSpec` has no `/-- … -/` docstring
missing_docstring info
lean/Project/RustArrayTests/Spec.lean:85
spec `Project.RustArrayTests.Spec.EmptyPlusThreeSpec` has no `/-- … -/` docstring
missing_docstring info
lean/Project/RustArrayTests/Spec.lean:141
spec `Project.RustArrayTests.Spec.EmptyXorFlagSpec` has no `/-- … -/` docstring
missing_docstring info
lean/Project/RustArrayTests/Spec.lean:207
spec `Project.RustArrayTests.Spec.LenPlusOneExportSpec` has no `/-- … -/` docstring
missing_docstring info
lean/Project/RustArrayTests/Spec.lean:259
spec `Project.RustArrayTests.Spec.LenPlusArgExportSpec` has no `/-- … -/` docstring
missing_docstring info
lean/Project/RustArrayTests/Spec.lean:313
spec `Project.RustArrayTests.Spec.EmptyPlusThreeExportSpec` has no `/-- … -/` docstring
missing_docstring info
lean/Project/RustArrayTests/Spec.lean:395
spec `Project.RustArrayTests.Spec.EmptyXorFlagExportSpec` has no `/-- … -/` docstring

Source files (appendix)

Lean (2)

lean/Project/RustArrayTests/Program.lean lean · 174 lines 
/-
  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
lean/Project/RustArrayTests/Spec.lean lean · 479 lines 
import Project.RustArrayTests.Program

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

namespace Project.RustArrayTests.Spec

open Wasm Wasm.RustStd Wasm.RustStd.Array
open Iris Iris.ProgramLogic Language.Notation
open Wasm.SepLogic

-- 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

/-! ## Internal impl-body specs

Each is proved directly over its generated small-step body. -/

private def bodyConfig (body : Program) (params : List Value) :
    SmallStep.Config Unit :=
  { expr := .running ⟨⟨params, [], []⟩, body, 1, [], [], []⟩
    store :=
      { runtime := { module := «module», host := {} }
        wasm := «module».initialStore } }

private def exportConfig (env : HostEnv Unit) (st : Store Unit)
    (body : Program) (params : List Value) : SmallStep.Config Unit :=
  { expr := .running ⟨⟨params, [], []⟩, body, 1, [], [], []⟩
    store :=
      { runtime := { module := «module», host := env }
        wasm := st } }

@[spec_of "rust-internal" "rust_array_tests::len_plus_one"]
def LenPlusOneSpec : Prop := ∀ (ptr len : UInt32),
  SmallStep.PartiallyMeets
    (bodyConfig func1 [.i32 ptr, .i32 len])
    (fun rs _store => rs = [.i32 (len + 1)])

@[proves Project.RustArrayTests.Spec.LenPlusOneSpec]
theorem len_plus_one_correct : LenPlusOneSpec := by
  intro ptr len
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [bodyConfig, func1]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_const
  inext
  iapply SmallStep.wp_add
  inext
  rw [UInt32.add_comm 1 len]
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

@[spec_of "rust-internal" "rust_array_tests::len_plus_arg"]
def LenPlusArgSpec : Prop := ∀ (ptr len n : UInt32),
  SmallStep.PartiallyMeets
    (bodyConfig func0 [.i32 ptr, .i32 len, .i32 n])
    (fun rs _store => rs = [.i32 (len + n)])

@[proves Project.RustArrayTests.Spec.LenPlusArgSpec]
theorem len_plus_arg_correct : LenPlusArgSpec := by
  intro ptr len n
  apply SmallStep.wasm_smallStep_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [bodyConfig, func0]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_add
  inext
  rw [UInt32.add_comm n len]
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

@[spec_of "rust-internal" "rust_array_tests::empty_plus_three"]
def EmptyPlusThreeSpec : Prop := ∀ (ptr len : UInt32),
  SmallStep.PartiallyMeets
    (bodyConfig func4 [.i32 ptr, .i32 len])
    (fun rs _store => rs = [.i32 (isEmptyValue len + 3)])

@[proves Project.RustArrayTests.Spec.EmptyPlusThreeSpec]
theorem empty_plus_three_correct : EmptyPlusThreeSpec := by
  intro ptr len
  apply SmallStep.wasm_smallStep_runtime_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [bodyConfig, func4]
  iintro Hruntime
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_call «module» 3 func3Def
    (by simp [«module»]) (by simp [«module»]) $$ Hruntime
  inext
  iintro Hruntime
  simp [func3Def, Function.toLocals, Function.numParams, func3]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_const
  inext
  iapply SmallStep.wp_eq (result := isEmptyValue len) (by rfl)
  inext
  iapply SmallStep.wp_const
  inext
  iapply SmallStep.wp_and
  inext
  rw [show isEmptyValue len &&& 1 = isEmptyValue len by
    unfold isEmptyValue
    by_cases h : len = 0 <;> simp [h]]
  iapply SmallStep.wp_returnFromCallExplicit
  inext
  simp only [List.take, List.singleton_append]
  iapply SmallStep.wp_const
  inext
  iapply SmallStep.wp_and
  inext
  rw [show isEmptyValue len &&& 1 = isEmptyValue len by
    unfold isEmptyValue
    by_cases h : len = 0 <;> simp [h]]
  iapply SmallStep.wp_const
  inext
  iapply SmallStep.wp_add
  inext
  rw [UInt32.add_comm 3 (isEmptyValue len)]
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

@[spec_of "rust-internal" "rust_array_tests::empty_xor_flag"]
def EmptyXorFlagSpec : Prop := ∀ (ptr len flag : UInt32),
  SmallStep.PartiallyMeets
    (bodyConfig func2 [.i32 ptr, .i32 len, .i32 flag])
    (fun rs _store => rs = [.i32 (isEmptyValue len ^^^ flag)])

@[proves Project.RustArrayTests.Spec.EmptyXorFlagSpec]
theorem empty_xor_flag_correct : EmptyXorFlagSpec := by
  intro ptr len flag
  apply SmallStep.wasm_smallStep_runtime_partiallyMeets.{0} (α := Unit)
  intro gs
  simp only [bodyConfig, func2]
  iintro Hruntime
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_call «module» 3 func3Def
    (by simp [«module»]) (by simp [«module»]) $$ Hruntime
  inext
  iintro Hruntime
  simp [func3Def, Function.toLocals, Function.numParams, func3]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_const
  inext
  iapply SmallStep.wp_eq (result := isEmptyValue len) (by rfl)
  inext
  iapply SmallStep.wp_const
  inext
  iapply SmallStep.wp_and
  inext
  rw [show isEmptyValue len &&& 1 = isEmptyValue len by
    unfold isEmptyValue
    by_cases h : len = 0 <;> simp [h]]
  iapply SmallStep.wp_returnFromCallExplicit
  inext
  simp only [List.take, List.singleton_append]
  iapply SmallStep.wp_const
  inext
  iapply SmallStep.wp_and
  inext
  rw [show isEmptyValue len &&& 1 = isEmptyValue len by
    unfold isEmptyValue
    by_cases h : len = 0 <;> simp [h]]
  iapply SmallStep.wp_localGet rfl
  inext
  iapply SmallStep.wp_xor
  inext
  iapply SmallStep.wp_returnFromFunction
  inext
  iapply wp_value'
  ipureintro
  rfl

/-! ## 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)` through the authoritative iris-lean fat-pointer loader 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 →
    SmallStep.PartiallyMeets
      (exportConfig env st func8 [.i32 p])
      (fun rs _store => rs = [.i32 (len + 1)])

@[proves Project.RustArrayTests.Spec.LenPlusOneExportSpec]
theorem len_plus_one_export_correct : LenPlusOneExportSpec := by
  intro env st p dataPtr len hfat
  apply SmallStep.wasm_smallStep_heap_runtime_partiallyMeets.{0} (α := Unit)
      (σ := fatPtrHeap p dataPtr len)
      (φ := fun rs => rs = [.i32 (len + 1)])
  · exact fatPtrHeap_agrees hfat
  · exact fatPtrHeap_inBounds hfat
  · intro gs
    iintro ⟨Hbytes, Hruntime⟩
    ihave Hfat := fatPtrHeap_pointsTo p dataPtr len hfat.noWrap $$ Hbytes
    icases Hfat with ⟨Hdata, Hlen⟩
    simp only [exportConfig, func8]
    ihave HdataLater : ▷ pointsTo_u32 p dataPtr $$ [Hdata]
    · inext
      iexact Hdata
    ihave HlenLater : ▷ pointsTo_u32 (p + 4) len $$ [Hlen]
    · inext
      iexact Hlen
    iapply wp_loadFatPtr 0 p dataPtr len rfl hfat.noWrap $$
      HdataLater HlenLater
    inext
    iapply SmallStep.wp_call «module» 1 func1Def
      (by simp [«module»]) (by simp [«module»]) $$ Hruntime
    inext
    iintro Hruntime
    simp [func1Def, Function.toLocals, Function.numParams, func1]
    iapply SmallStep.wp_localGet rfl
    inext
    iapply SmallStep.wp_const
    inext
    iapply SmallStep.wp_add
    inext
    rw [UInt32.add_comm 1 len]
    iapply SmallStep.wp_returnFromCallExplicit
    inext
    simp only [List.take, List.singleton_append]
    iapply SmallStep.wp_returnFromFunction
    inext
    iapply wp_value'
    iclear Hruntime
    ipureintro
    rfl

@[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 →
    SmallStep.PartiallyMeets
      (exportConfig env st func7 [.i32 p, .i32 n])
      (fun rs _store => 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
  apply SmallStep.wasm_smallStep_heap_runtime_partiallyMeets.{0} (α := Unit)
      (σ := fatPtrHeap p dataPtr len)
      (φ := fun rs => rs = [.i32 (len + n)])
  · exact fatPtrHeap_agrees hfat
  · exact fatPtrHeap_inBounds hfat
  · intro gs
    iintro ⟨Hbytes, Hruntime⟩
    ihave Hfat := fatPtrHeap_pointsTo p dataPtr len hfat.noWrap $$ Hbytes
    icases Hfat with ⟨Hdata, Hlen⟩
    simp only [exportConfig, func7]
    ihave HdataLater : ▷ pointsTo_u32 p dataPtr $$ [Hdata]
    · inext
      iexact Hdata
    ihave HlenLater : ▷ pointsTo_u32 (p + 4) len $$ [Hlen]
    · inext
      iexact Hlen
    iapply wp_loadFatPtr 0 p dataPtr len rfl hfat.noWrap $$
      HdataLater HlenLater
    inext
    iapply SmallStep.wp_localGet rfl
    inext
    iapply SmallStep.wp_call «module» 0 func0Def
      (by simp [«module»]) (by simp [«module»]) $$ Hruntime
    inext
    iintro Hruntime
    simp [func0Def, Function.toLocals, Function.numParams, func0]
    iapply SmallStep.wp_localGet rfl
    inext
    iapply SmallStep.wp_localGet rfl
    inext
    iapply SmallStep.wp_add
    inext
    rw [UInt32.add_comm n len]
    iapply SmallStep.wp_returnFromCallExplicit
    inext
    simp only [List.take, List.singleton_append]
    iapply SmallStep.wp_returnFromFunction
    inext
    iapply wp_value'
    iclear Hruntime
    ipureintro
    rfl

@[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 →
    SmallStep.PartiallyMeets
      (exportConfig env st func5 [.i32 p])
      (fun rs _store => 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
  apply SmallStep.wasm_smallStep_heap_runtime_partiallyMeets.{0} (α := Unit)
      (σ := fatPtrHeap p dataPtr len)
      (φ := fun rs => rs = [.i32 (isEmptyValue len + 3)])
  · exact fatPtrHeap_agrees hfat
  · exact fatPtrHeap_inBounds hfat
  · intro gs
    iintro ⟨Hbytes, Hruntime⟩
    ihave Hfat := fatPtrHeap_pointsTo p dataPtr len hfat.noWrap $$ Hbytes
    icases Hfat with ⟨Hdata, Hlen⟩
    simp only [exportConfig, func5]
    ihave HdataLater : ▷ pointsTo_u32 p dataPtr $$ [Hdata]
    · inext
      iexact Hdata
    ihave HlenLater : ▷ pointsTo_u32 (p + 4) len $$ [Hlen]
    · inext
      iexact Hlen
    iapply wp_loadFatPtr 0 p dataPtr len rfl hfat.noWrap $$
      HdataLater HlenLater
    inext
    iapply SmallStep.wp_call «module» 4 func4Def
      (by simp [«module»]) (by simp [«module»]) $$ Hruntime
    inext
    iintro Hruntime
    simp [func4Def, Function.toLocals, Function.numParams, func4]
    iapply SmallStep.wp_localGet rfl
    inext
    iapply SmallStep.wp_localGet rfl
    inext
    iapply SmallStep.wp_call «module» 3 func3Def
      (by simp [«module»]) (by simp [«module»]) $$ Hruntime
    inext
    iintro Hruntime
    simp [func3Def, Function.toLocals, Function.numParams, func3]
    iapply SmallStep.wp_localGet rfl
    inext
    iapply SmallStep.wp_const
    inext
    iapply SmallStep.wp_eq (result := isEmptyValue len) (by rfl)
    inext
    iapply SmallStep.wp_const
    inext
    iapply SmallStep.wp_and
    inext
    rw [show isEmptyValue len &&& 1 = isEmptyValue len by
      unfold isEmptyValue
      by_cases h : len = 0 <;> simp [h]]
    iapply SmallStep.wp_returnFromCallExplicit
    inext
    simp only [List.take, List.singleton_append]
    iapply SmallStep.wp_const
    inext
    iapply SmallStep.wp_and
    inext
    rw [show isEmptyValue len &&& 1 = isEmptyValue len by
      unfold isEmptyValue
      by_cases h : len = 0 <;> simp [h]]
    iapply SmallStep.wp_const
    inext
    iapply SmallStep.wp_add
    inext
    rw [UInt32.add_comm 3 (isEmptyValue len)]
    iapply SmallStep.wp_returnFromCallExplicit
    inext
    simp only [List.take, List.singleton_append]
    iapply SmallStep.wp_returnFromFunction
    inext
    iapply wp_value'
    iclear Hruntime
    ipureintro
    rfl

@[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 →
    SmallStep.PartiallyMeets
      (exportConfig env st func6 [.i32 p, .i32 flag])
      (fun rs _store => 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
  apply SmallStep.wasm_smallStep_heap_runtime_partiallyMeets.{0} (α := Unit)
      (σ := fatPtrHeap p dataPtr len)
      (φ := fun rs => rs = [.i32 (isEmptyValue len ^^^ flag)])
  · exact fatPtrHeap_agrees hfat
  · exact fatPtrHeap_inBounds hfat
  · intro gs
    iintro ⟨Hbytes, Hruntime⟩
    ihave Hfat := fatPtrHeap_pointsTo p dataPtr len hfat.noWrap $$ Hbytes
    icases Hfat with ⟨Hdata, Hlen⟩
    simp only [exportConfig, func6]
    ihave HdataLater : ▷ pointsTo_u32 p dataPtr $$ [Hdata]
    · inext
      iexact Hdata
    ihave HlenLater : ▷ pointsTo_u32 (p + 4) len $$ [Hlen]
    · inext
      iexact Hlen
    iapply wp_loadFatPtr 0 p dataPtr len rfl hfat.noWrap $$
      HdataLater HlenLater
    inext
    iapply SmallStep.wp_localGet rfl
    inext
    iapply SmallStep.wp_call «module» 2 func2Def
      (by simp [«module»]) (by simp [«module»]) $$ Hruntime
    inext
    iintro Hruntime
    simp [func2Def, Function.toLocals, Function.numParams, func2]
    iapply SmallStep.wp_localGet rfl
    inext
    iapply SmallStep.wp_localGet rfl
    inext
    iapply SmallStep.wp_call «module» 3 func3Def
      (by simp [«module»]) (by simp [«module»]) $$ Hruntime
    inext
    iintro Hruntime
    simp [func3Def, Function.toLocals, Function.numParams, func3]
    iapply SmallStep.wp_localGet rfl
    inext
    iapply SmallStep.wp_const
    inext
    iapply SmallStep.wp_eq (result := isEmptyValue len) (by rfl)
    inext
    iapply SmallStep.wp_const
    inext
    iapply SmallStep.wp_and
    inext
    rw [show isEmptyValue len &&& 1 = isEmptyValue len by
      unfold isEmptyValue
      by_cases h : len = 0 <;> simp [h]]
    iapply SmallStep.wp_returnFromCallExplicit
    inext
    simp only [List.take, List.singleton_append]
    iapply SmallStep.wp_const
    inext
    iapply SmallStep.wp_and
    inext
    rw [show isEmptyValue len &&& 1 = isEmptyValue len by
      unfold isEmptyValue
      by_cases h : len = 0 <;> simp [h]]
    iapply SmallStep.wp_localGet rfl
    inext
    iapply SmallStep.wp_xor
    inext
    iapply SmallStep.wp_returnFromCallExplicit
    inext
    simp only [List.take, List.singleton_append]
    iapply SmallStep.wp_returnFromFunction
    inext
    iapply wp_value'
    iclear Hruntime
    ipureintro
    rfl

end Project.RustArrayTests.Spec

Rust (2)

rust/rust_array_tests/src/exports.rs rust · 30 lines 
//! 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)
}
rust/rust_array_tests/src/lib.rs rust · 24 lines 
#![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
}

Other (1)

rust/rust_array_tests/Cargo.toml toml · 10 lines 
[package]
name = "rust_array_tests"
version = "0.1.0"
edition = "2024"

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

[dependencies]