RustRuntime.lean🔗

Rust Runtime Panic Hooks

Models Rust panic = abort entry points by wrapping a Program hook table (Rust.withPanics) so calls to core::panicking::*, unwrap/expect failure paths, slice bounds checks, and allocation error handlers transition s.status to .Panicked.

@[expose] public section

namespace Arm64.Rust

def isPanicSymbolL26–40 ↗#

Demangled names of functions that start a panic. Everything in core::panicking panics; the others are the out-of-line panic paths of unwrap/expect, slice indexing, and allocation failure.

def isPanicSymbol (name : String) : Bool :=
  name.startsWith "core::panicking::" ||
  [ "core::result::unwrap_failed",
    "core::option::unwrap_failed",
    "core::option::expect_failed",
    "core::slice::index::slice_start_index_len_fail",
    "core::slice::index::slice_end_index_len_fail",
    "core::slice::index::slice_index_order_fail",
    "core::slice::index::slice_index_fail",
    "alloc::raw_vec::handle_error",
    "alloc::raw_vec::capacity_overflow",
    "alloc::alloc::handle_alloc_error" ].contains name

def panickedL42–44 ↗#

The effect of entering a panic.

def panicked (s : State) : State :=
  { s with status := .Panicked }

1 declaration not shown (lines 46–49): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Rust.withPanics

end Arm64.Rust