Module exec_spec

This module provides runtime utilities for the compiled executable code of [builtin_macros::exec_spec].

Macros

exec_spec

Automatically compiles spec items to exec items, with proofs of functional correctness.

Traits

DeepViewClone

Cloned objects have the same deep view

ExecSpecEq

Spec for the executable version of equality.

ExecSpecIndex

Spec for executable version of Seq indexing.

ExecSpecLen

Spec for executable version of Seq::len.

ExecSpecType

Any spec types used in exec_spec macro must implement this trait to indicate the corresponding exec type (owned and borrowed versions).

ToOwned

ToRef

ToRef and ToOwned are almost the same trait but separated to avoid type inference ambiguities.

Type Aliases

SpecString

We use this special alias to tell the exec_spec macro to compile Seq<char> to String instead of Vec<char>.