diff --git a/verified_libs/vstd_extra/src/lib.rs b/verified_libs/vstd_extra/src/lib.rs index 68cf8e5ae..b295f6728 100644 --- a/verified_libs/vstd_extra/src/lib.rs +++ b/verified_libs/vstd_extra/src/lib.rs @@ -5,6 +5,7 @@ #![feature(nonzero_internals)] #![feature(sized_hierarchy)] #![feature(proc_macro_hygiene)] +#![feature(ptr_metadata)] #![cfg_attr(verus_keep_ghost, feature(allocator_api))] #![allow(non_snake_case)] #![allow(unused_parens)] @@ -39,3 +40,4 @@ pub mod spec_operators; pub mod state_machine; pub mod sum; pub mod temporal_logic; +pub mod typing; diff --git a/verified_libs/vstd_extra/src/typing/any_of.rs b/verified_libs/vstd_extra/src/typing/any_of.rs new file mode 100644 index 000000000..1a30b33d3 --- /dev/null +++ b/verified_libs/vstd_extra/src/typing/any_of.rs @@ -0,0 +1,132 @@ +//! The [`AnyOf`] macro: build a closed world of types from a list. +//! +//! Writing an aggregate by hand means writing, per member, a [`TypeSet`] impl and a +//! [`HasId`] impl, then one `DisjointFrom` witness per nesting node, then the +//! nested type itself. All of it is mechanical, and all of it is the part a person +//! gets wrong — a reused id is a soundness bug that no single declaration looks +//! wrong in isolation. +//! +//! [`TypeSet`]: super::types::TypeSet +//! [`HasId`]: super::types::HasId +//! +//! # Why it emits `verus!` blocks +//! +//! The macro must be invoked *outside* a `verus!` block, and expands to `verus!` +//! blocks of its own. This is forced: `verus!` is a proc macro that consumes its +//! token stream directly, so a `macro_rules!` call appearing inside one is never +//! expanded — Verus would see the literal tokens `AnyOf!(..)` and reject them. The +//! tree recursion therefore emits one small `verus!` block per step rather than +//! accumulating everything into a single one. +//! +//! # Nesting direction +//! +//! The tree is built *left*-nested — `ConsType, LeafType>, +//! LeafType>` — for a mechanical reason rather than a semantic one. Both +//! directions are equivalent (`possible_types` and `valid` are unions, and union +//! is associative), but a +//! `macro_rules!` accumulator can only grow outward, and right-nesting would need +//! it to grow into a hole in the middle of an already-built type. +//! +//! # Collisions fail verification, they are not merely undetected +//! +//! The macro does not check that the ids differ, and does not need to. A duplicate +//! id makes one of the generated `DisjointFrom` proofs unprovable, so the build +//! fails at the node that joins the colliding members. That is the property the +//! whole design exists for: uniqueness is enforced per node, at compile time, +//! instead of by a global registry someone has to remember to audit. +//! +//! # A type belongs to exactly one world +//! +//! Ids live in the member's own `TypeSet` impl, so a type cannot appear in two +//! `AnyOf!` invocations — the second expansion collides with `E0119 conflicting +//! implementations`. This is the right constraint rather than a limitation, and it +//! matches `core::any::TypeId`, which is likewise global to the type: an id +//! meaning different things in different aggregates would make the ids useless as +//! identity. Two worlds sharing members means one world with the union of them. +//! +//! # What it does not generate +//! +//! Nothing about representation. `LeafType` is a [`Member`] only when `M` is +//! [`ByteRepr`], and a byte layout is a fact about the type that cannot be +//! derived — so each member still needs its own `ByteSized`/`ByteRepr` impls. +//! The split is deliberate: this macro settles *identity*, which is what can be +//! mechanised. +//! +//! [`Member`]: super::types::Member +//! [`ByteRepr`]: super::types::ByteRepr +//! +//! # Example +//! +//! ```ignore +//! AnyOf!(World = [MetaA = 1, MetaB = 2, MetaC = 3]); +//! ``` +//! +//! expands to `TypeSet`/`HasId` for each of the three, two `DisjointFrom` +//! witnesses, and `pub type World = ConsType, +//! LeafType>, LeafType>`. +/// Defines a closed world of types as a nested `EitherType` tree. +/// +/// See the [module docs](self) for the shape of the expansion, why ids are given +/// explicitly, and what is deliberately left out. +#[macro_export] +macro_rules! AnyOf { + // ---- entry: a name for the world, then the members and their ids ---- + ($world:ident = [$t0:ty = $id0:literal $(, $t:ty = $id:literal)* $(,)?]) => { + $crate::AnyOf!(@ids $t0 = $id0 $(, $t = $id)*); + $crate::AnyOf!(@tree $world; $crate::typing::types::LeafType<$t0> $(; $t)*); + }; + + // ---- per-member identity ---- + // + // `wf` is `true` because a type owning exactly one id carries its identity in + // its type: there is no tag that could disagree with anything. + (@ids $($t:ty = $id:literal),+) => { + ::vstd::prelude::verus!{ + $( + impl $crate::typing::types::TypeSet for $t { + open spec fn possible_types() -> ::vstd::set::Set { + ::vstd::set::Set::empty().insert($id as nat) + } + } + + impl $crate::typing::types::HasId for $t { + open spec fn id_of(&self) -> nat { + $id as nat + } + + open spec fn wf(&self) -> bool { + true + } + + proof fn id_of_in_possible_types(&self) { + } + } + )+ + } +}; + + // ---- tree: no members left, name the accumulated type ---- + (@tree $world:ident; $acc:ty) => { + ::vstd::prelude::verus!{ + pub type $world = $acc; + } +}; + + // ---- tree: join one more member, discharging its node's obligation ---- + // + // This impl is where a duplicate id is caught: its body is empty, so the + // proof succeeds only if the two sides really are disjoint. + (@tree $world:ident; $acc:ty ; $next:ty $(; $rest:ty)*) => { + ::vstd::prelude::verus!{ + impl $crate::typing::types::DisjointFrom<$crate::typing::types::LeafType<$next>> for $acc { + proof fn disjoint(type_id: nat) { + } + } + } +$crate::AnyOf!( + @tree $world; + $crate::typing::types::ConsType<$acc, $crate::typing::types::LeafType<$next>> + $(; $rest)* + ); + }; +} diff --git a/verified_libs/vstd_extra/src/typing/example.rs b/verified_libs/vstd_extra/src/typing/example.rs new file mode 100644 index 000000000..11bf6d9fa --- /dev/null +++ b/verified_libs/vstd_extra/src/typing/example.rs @@ -0,0 +1,757 @@ +//! A worked three-member aggregate, `L1 | (L2 | L3)`, to exercise the laws. +//! +//! The point is to check that uniqueness *composes*: the outer node must show +//! `L1` is disjoint from `L2 | L3`, and the inner node that `L2` is disjoint +//! from `L3`. Neither obligation mentions the other, and no global registry is +//! consulted — which is the property that a flat tag scheme cannot offer. +//! +//! Three members is the smallest size that actually tests nesting, and it is the +//! case the binary-tag design could not express at all. + +use core::marker::PhantomData; + +use vstd::prelude::*; +use vstd::std_specs::convert::{IntoSpec, IntoSpecImpl, TryFromSpec, TryFromSpecImpl}; + +use super::types::*; + +verus! { + +/// Byte width used throughout this example. +pub const EX_SIZE: usize = 8; + +/// Sized to `EX_SIZE`, not a unit struct. +/// +/// A ZST would make [`ByteSized`] *false* — `size_of::() == 0`, not 8 — +/// and axiomatizing `size_correct` for it would have been assuming +/// something untrue, which is worse than leaving it unproved. +#[repr(transparent)] +pub struct L1(pub u64); + +/// Sized to `EX_SIZE`, not a unit struct. +/// +/// A ZST would make [`ByteSized`] *false* — `size_of::() == 0`, not 8 — +/// and axiomatizing `size_correct` for it would have been assuming +/// something untrue, which is worse than leaving it unproved. +#[repr(transparent)] +pub struct L2(pub u64); + +/// Sized to `EX_SIZE`, not a unit struct. +/// +/// A ZST would make [`ByteSized`] *false* — `size_of::() == 0`, not 8 — +/// and axiomatizing `size_correct` for it would have been assuming +/// something untrue, which is worse than leaving it unproved. +#[repr(transparent)] +pub struct L3(pub u64); + +// Leaves each own a single id. +impl TypeSet for L1 { + open spec fn possible_types() -> Set { + Set::empty().insert(1nat) + } +} + +impl HasId for L1 { + open spec fn id_of(&self) -> nat { + 1 + } + + /// A type owning exactly one id carries its identity in its type, so + /// there is no tag that could disagree with anything. + open spec fn wf(&self) -> bool { + true + } + + proof fn id_of_in_possible_types(&self) { + } +} + +impl TypeSet for L2 { + open spec fn possible_types() -> Set { + Set::empty().insert(2nat) + } +} + +impl HasId for L2 { + open spec fn id_of(&self) -> nat { + 2 + } + + /// A type owning exactly one id carries its identity in its type, so + /// there is no tag that could disagree with anything. + open spec fn wf(&self) -> bool { + true + } + + proof fn id_of_in_possible_types(&self) { + } +} + +impl TypeSet for L3 { + open spec fn possible_types() -> Set { + Set::empty().insert(3nat) + } +} + +impl HasId for L3 { + open spec fn id_of(&self) -> nat { + 3 + } + + /// A type owning exactly one id carries its identity in its type, so + /// there is no tag that could disagree with anything. + open spec fn wf(&self) -> bool { + true + } + + proof fn id_of_in_possible_types(&self) { + } +} + + +/// Encoding of [`L1`], left uninterpreted. +/// +/// A concrete byte layout is a fact about the type's representation, not +/// about the aggregate machinery. Naming it without defining it is what +/// lets the round-trip law below be the *only* thing consumers may assume. +pub uninterp spec fn l1_encode(v: L1) -> [u8; EX_SIZE]; + +/// Decoding of [`L1`], left uninterpreted. +/// +/// Note it is total and may return `Ok` for bytes that never came from an +/// `L1`. Nothing here rules that out, and nothing should: rejecting foreign +/// byte patterns is not how members are told apart — see [`DisjointFrom`]. +pub uninterp spec fn l1_decode(b: [u8; EX_SIZE]) -> Result; + +/// Decoding recovers what encoding produced. +/// +/// Axiomatized: this is the representation obligation a real member would +/// discharge from its layout, and the single fact the aggregate needs. +#[verifier::external_body] +pub broadcast proof fn axiom_l1_round_trip(v: L1) + ensures + #[trigger] l1_decode(l1_encode(v)) == Ok(v), +{ +} + +/// A valid byte pattern is the encoding of what it decodes to. +/// +/// The second representation obligation, independent of the round trip above and +/// equally a layout fact. It is what makes the encoding canonical: no two byte +/// patterns decode to the same `L1`. A real member discharges this from its +/// layout, by having no padding and no redundant encodings. +#[verifier::external_body] +pub broadcast proof fn axiom_l1_canonical(b: [u8; EX_SIZE]) + requires + l1_decode(b) is Ok, + ensures + #[trigger] l1_encode(l1_decode(b)->Ok_0) == b, +{ +} + +impl TryFrom<[u8; EX_SIZE]> for L1 { + type Error = (); + + #[verifier::external_body] + fn try_from(b: [u8; EX_SIZE]) -> Result { + unimplemented!() + } +} + +impl TryFromSpecImpl<[u8; EX_SIZE]> for L1 { + open spec fn obeys_try_from_spec() -> bool { + true + } + + open spec fn try_from_spec(b: [u8; EX_SIZE]) -> Result { + l1_decode(b) + } +} + +#[allow(clippy::from_over_into)] +impl Into<[u8; EX_SIZE]> for L1 { + #[verifier::external_body] + fn into(self) -> [u8; EX_SIZE] { + unimplemented!() + } +} + +impl IntoSpecImpl<[u8; EX_SIZE]> for L1 { + open spec fn obeys_into_spec() -> bool { + true + } + + open spec fn into_spec(self) -> [u8; EX_SIZE] { + l1_encode(self) + } +} + +impl ByteSized<{ EX_SIZE }> for L1 { + /// Axiomatized: `#[repr(transparent)]` over a `u64` is 8 bytes, which is + /// a layout fact Verus does not derive for user structs. + #[verifier::external_body] + proof fn size_correct() { + } +} + +impl ByteRepr<{ EX_SIZE }> for L1 { + proof fn round_trip(self) { + broadcast use axiom_l1_round_trip; + } + + proof fn canonical(data: [u8; EX_SIZE]) { + broadcast use axiom_l1_canonical; + } +} + +/// Encoding of [`L2`], left uninterpreted. +/// +/// A concrete byte layout is a fact about the type's representation, not +/// about the aggregate machinery. Naming it without defining it is what +/// lets the round-trip law below be the *only* thing consumers may assume. +pub uninterp spec fn l2_encode(v: L2) -> [u8; EX_SIZE]; + +/// Decoding of [`L2`], left uninterpreted. +/// +/// Note it is total and may return `Ok` for bytes that never came from an +/// `L2`. Nothing here rules that out, and nothing should: rejecting foreign +/// byte patterns is not how members are told apart — see [`DisjointFrom`]. +pub uninterp spec fn l2_decode(b: [u8; EX_SIZE]) -> Result; + +/// Decoding recovers what encoding produced. +/// +/// Axiomatized: this is the representation obligation a real member would +/// discharge from its layout, and the single fact the aggregate needs. +#[verifier::external_body] +pub broadcast proof fn axiom_l2_round_trip(v: L2) + ensures + #[trigger] l2_decode(l2_encode(v)) == Ok(v), +{ +} + +/// A valid byte pattern is the encoding of what it decodes to. +/// +/// The second representation obligation, independent of the round trip above and +/// equally a layout fact. It is what makes the encoding canonical: no two byte +/// patterns decode to the same `L2`. A real member discharges this from its +/// layout, by having no padding and no redundant encodings. +#[verifier::external_body] +pub broadcast proof fn axiom_l2_canonical(b: [u8; EX_SIZE]) + requires + l2_decode(b) is Ok, + ensures + #[trigger] l2_encode(l2_decode(b)->Ok_0) == b, +{ +} + +impl TryFrom<[u8; EX_SIZE]> for L2 { + type Error = (); + + #[verifier::external_body] + fn try_from(b: [u8; EX_SIZE]) -> Result { + unimplemented!() + } +} + +impl TryFromSpecImpl<[u8; EX_SIZE]> for L2 { + open spec fn obeys_try_from_spec() -> bool { + true + } + + open spec fn try_from_spec(b: [u8; EX_SIZE]) -> Result { + l2_decode(b) + } +} + +#[allow(clippy::from_over_into)] +impl Into<[u8; EX_SIZE]> for L2 { + #[verifier::external_body] + fn into(self) -> [u8; EX_SIZE] { + unimplemented!() + } +} + +impl IntoSpecImpl<[u8; EX_SIZE]> for L2 { + open spec fn obeys_into_spec() -> bool { + true + } + + open spec fn into_spec(self) -> [u8; EX_SIZE] { + l2_encode(self) + } +} + +impl ByteSized<{ EX_SIZE }> for L2 { + /// Axiomatized: `#[repr(transparent)]` over a `u64` is 8 bytes, which is + /// a layout fact Verus does not derive for user structs. + #[verifier::external_body] + proof fn size_correct() { + } +} + +impl ByteRepr<{ EX_SIZE }> for L2 { + proof fn round_trip(self) { + broadcast use axiom_l2_round_trip; + } + + proof fn canonical(data: [u8; EX_SIZE]) { + broadcast use axiom_l2_canonical; + } +} + +/// Encoding of [`L3`], left uninterpreted. +/// +/// A concrete byte layout is a fact about the type's representation, not +/// about the aggregate machinery. Naming it without defining it is what +/// lets the round-trip law below be the *only* thing consumers may assume. +pub uninterp spec fn l3_encode(v: L3) -> [u8; EX_SIZE]; + +/// Decoding of [`L3`], left uninterpreted. +/// +/// Note it is total and may return `Ok` for bytes that never came from an +/// `L3`. Nothing here rules that out, and nothing should: rejecting foreign +/// byte patterns is not how members are told apart — see [`DisjointFrom`]. +pub uninterp spec fn l3_decode(b: [u8; EX_SIZE]) -> Result; + +/// Decoding recovers what encoding produced. +/// +/// Axiomatized: this is the representation obligation a real member would +/// discharge from its layout, and the single fact the aggregate needs. +#[verifier::external_body] +pub broadcast proof fn axiom_l3_round_trip(v: L3) + ensures + #[trigger] l3_decode(l3_encode(v)) == Ok(v), +{ +} + +/// A valid byte pattern is the encoding of what it decodes to. +/// +/// The second representation obligation, independent of the round trip above and +/// equally a layout fact. It is what makes the encoding canonical: no two byte +/// patterns decode to the same `L3`. A real member discharges this from its +/// layout, by having no padding and no redundant encodings. +#[verifier::external_body] +pub broadcast proof fn axiom_l3_canonical(b: [u8; EX_SIZE]) + requires + l3_decode(b) is Ok, + ensures + #[trigger] l3_encode(l3_decode(b)->Ok_0) == b, +{ +} + +impl TryFrom<[u8; EX_SIZE]> for L3 { + type Error = (); + + #[verifier::external_body] + fn try_from(b: [u8; EX_SIZE]) -> Result { + unimplemented!() + } +} + +impl TryFromSpecImpl<[u8; EX_SIZE]> for L3 { + open spec fn obeys_try_from_spec() -> bool { + true + } + + open spec fn try_from_spec(b: [u8; EX_SIZE]) -> Result { + l3_decode(b) + } +} + +#[allow(clippy::from_over_into)] +impl Into<[u8; EX_SIZE]> for L3 { + #[verifier::external_body] + fn into(self) -> [u8; EX_SIZE] { + unimplemented!() + } +} + +impl IntoSpecImpl<[u8; EX_SIZE]> for L3 { + open spec fn obeys_into_spec() -> bool { + true + } + + open spec fn into_spec(self) -> [u8; EX_SIZE] { + l3_encode(self) + } +} + +impl ByteSized<{ EX_SIZE }> for L3 { + /// Axiomatized: `#[repr(transparent)]` over a `u64` is 8 bytes, which is + /// a layout fact Verus does not derive for user structs. + #[verifier::external_body] + proof fn size_correct() { + } +} + +impl ByteRepr<{ EX_SIZE }> for L3 { + proof fn round_trip(self) { + broadcast use axiom_l3_round_trip; + } + + proof fn canonical(data: [u8; EX_SIZE]) { + broadcast use axiom_l3_canonical; + } +} + +// The aggregate tree. Each leaf wraps a representable type; nodes join them. +/// `L1` as a one-member aggregate. +pub type M1 = LeafType; + +/// `L2` as a one-member aggregate. +pub type M2 = LeafType; + +/// `L3` as a one-member aggregate. +pub type M3 = LeafType; + +/// The inner node, `L2 | L3`. +pub type Inner = ConsType; + +/// The whole aggregate, `L1 | (L2 | L3)`. +pub type Outer = ConsType; + +/// Bytes tagged with which of the three members they hold. +/// +/// One tag for a three-deep tree — the point of moving from `LEFT`/`RIGHT` to +/// a member id. Under the old design this type could not be written at all. +pub type Store = GhostTaggedArray<{ EX_SIZE }, Outer>; + +// Disjointness witnesses, discharged by computation on the leaf ids. Note +// these are stated on the *aggregates*, since that is what `EitherType` joins. +impl DisjointFrom for M2 { + proof fn disjoint(type_id: nat) { + } +} + +impl DisjointFrom for M1 { + proof fn disjoint(type_id: nat) { + } +} + +/// Storing an `L2` yields a well-formed `Store` reporting `L2`'s id. +/// +/// The payoff: `wf` is established by construction, two levels down, with no +/// axiom and nothing to remember at the call site. +pub exec fn store_l2(v: L2) -> (r: Store) + ensures + r.wf(), + r.id_of() == 2, + r.data == >::into_spec(v), +{ + proof { + lemma_leaf_valid::<{ EX_SIZE }, L2>(v); + } + let data: [u8; EX_SIZE] = v.into(); + Store { id: Ghost(2nat), data, _t: PhantomData } +} + +/// A well-formed `Store` holding `L2`'s id satisfies the `EitherType` law at the +/// outer node: the id belongs to the `L2 | L3` side and not to `L1`. +pub proof fn stored_is_one_side(tracked r: &Store) + requires + r.wf(), + r.id_of() == 2, + ensures + Inner::possible_types().contains(r.id_of()) && !M1::possible_types().contains(r.id_of()), +{ + r.type_id_laws(); +} + +/// Disjointness at the inner node: `L2` and `L3` share no id. +pub proof fn inner_disjoint(t: nat) + ensures + !(M2::possible_types().contains(t) && M3::possible_types().contains(t)), +{ +} + +/// Disjointness at the outer node: `L1` shares no id with `L2 | L3`. +/// +/// Note this is discharged *without* reference to the inner node's own +/// obligation. That independence is the composition property being checked: +/// adding a member changes only the node that admits it. +pub proof fn outer_disjoint(t: nat) + ensures + !(M1::possible_types().contains(t) && Inner::possible_types().contains(t)), +{ +} + +/// A member of the aggregate lands in exactly one leaf. +/// +/// This is the shape a downcast consumes: given an id known to inhabit the +/// aggregate, exactly one leaf claims it, so testing against a leaf cannot +/// succeed for the wrong one. +pub proof fn exactly_one_leaf(t: nat) + requires + Outer::possible_types().contains(t), + ensures + ({ + &&& L1::possible_types().contains(t) ==> !L2::possible_types().contains(t) && !L3::possible_types().contains(t) + &&& L2::possible_types().contains(t) ==> !L1::possible_types().contains(t) && !L3::possible_types().contains(t) + &&& L3::possible_types().contains(t) ==> !L1::possible_types().contains(t) && !L2::possible_types().contains(t) + }), +{ +} + +// ------------------------------------------------------------------ +// The three behaviors. +// ------------------------------------------------------------------ + +/// **Upcast.** A stored member, viewed as an erased aggregate. +/// +/// Two erasures compose here: the concrete `L2` becomes bytes-plus-ghost-id +/// ([`store_l2`]), and that becomes `&dyn EitherType` (`as_dyn`). The id +/// survives both, which is what makes the result useful rather than opaque. +pub fn upcast_l2(s: &Store) -> (r: &dyn EitherType) + requires + s.wf(), + s.id_of() == 2, + ensures + r.dyn_id() == 2, + r.dyn_wf(), +{ + proof { + lemma_dyn_agrees::<{ EX_SIZE }, M1, Inner>(s); + } + s.as_dyn() +} + +/// **Dispatch, at the aggregate.** Get the uniqueness law through an erased +/// reference, without knowing which member is live. +/// +/// This is proof-mode dynamic dispatch: `type_id_laws` is resolved through the +/// vtable of whatever concrete type was erased. +pub proof fn dispatch_erased(tracked r: &dyn EitherType) + requires + r.dyn_wf(), + ensures + ({ + ||| M1::possible_types().contains(r.dyn_id()) && !Inner::possible_types().contains(r.dyn_id()) + ||| Inner::possible_types().contains(r.dyn_id()) && !M1::possible_types().contains(r.dyn_id()) + }), +{ + r.type_id_laws(); +} + +/// **Downcast.** Recover the concrete `L2` from the aggregate. +/// +/// The `id` parameter is not redundant with the ghost tag: the tag is *ghost*, +/// so no executable code may branch on it. A runtime witness has to come from +/// somewhere, and the precondition is what ties it to the ghost tag — exactly +/// the pairing the frame layer maintains between a stored word and its ghost +/// twin, except stated as a precondition instead of assumed by an axiom. +/// +/// The postcondition is an `<==>`, so this records both halves: the downcast +/// *succeeds* for the right member and *fails* for every other one. The second +/// half is the soundness property, and it is where `DisjointFrom` is spent. +/// +/// This discriminates rather than verifying vacuously. Probed by substituting +/// `L3::try_from` for `L2::try_from` with everything else unchanged: the +/// unreachability of the `Err` branch stops being provable, because a tag of +/// `2` says nothing about whether the bytes decode as an `L3`. +pub fn downcast_l2(s: &Store, id: usize) -> (r: Option) + requires + s.wf(), + id as nat == s.id_of(), + ensures + (r is Some) <==> s.id_of() == 2, +{ + if id == 2 { + assert(>::valid(2, s.data)) by { + assert(!>::valid(2, s.data)); + assert(!>::valid(2, s.data)); + } + match L2::try_from(s.data) { + Ok(v) => Some(v), + Err(_) => { + assert(false); + None + }, + } + } else { + None + } +} + +/// The downcast cannot succeed for a member other than the one stored. +/// +/// Stated separately because it is the property worth having in isolation: +/// given only that some id belongs to the aggregate, at most one leaf claims it. +pub proof fn downcast_rejects_others(s: &Store) + requires + s.wf(), + s.id_of() == 2, + ensures + !M1::possible_types().contains(s.id_of()), + !M3::possible_types().contains(s.id_of()), + M2::possible_types().contains(s.id_of()), +{ +} + +/// **Dispatch, at the member.** A real three-way vtable call. +/// +/// Separate from the aggregate's erased view, and necessarily so: the +/// aggregate's tag is ghost, so nothing executable can branch on it. Runtime +/// dispatch has to come from a real vtable, which means erasing the *member* +/// types rather than the storage. The two erasures answer different questions — +/// `EitherType` says which member it is, `Payload` runs its code. +/// +/// Note `Payload` has no supertrait. Giving it [`HasId`] would drag in +/// [`TypeSet`], which `dyn` does not satisfy, so it re-declares the id itself. +pub trait Payload { + spec fn word_spec(&self) -> u64; + + spec fn payload_id(&self) -> nat; + + fn word(&self) -> (r: u64) + ensures + r == self.word_spec(), + ; +} + +impl Payload for L1 { + open spec fn word_spec(&self) -> u64 { + self.0 + } + + open spec fn payload_id(&self) -> nat { + 1 + } + + fn word(&self) -> (r: u64) { + self.0 + } +} + +impl Payload for L2 { + open spec fn word_spec(&self) -> u64 { + self.0 + } + + open spec fn payload_id(&self) -> nat { + 2 + } + + fn word(&self) -> (r: u64) { + self.0 + } +} + +impl Payload for L3 { + open spec fn word_spec(&self) -> u64 { + self.0 + } + + open spec fn payload_id(&self) -> nat { + 3 + } + + fn word(&self) -> (r: u64) { + self.0 + } +} + +/// Dispatch through an erased member: three impls, one call site. +pub fn dispatch_payload(d: &dyn Payload) -> (r: u64) + ensures + r == d.word_spec(), +{ + d.word() +} + +/// Upcast a member and dispatch to it, with the id carried across. +/// +/// The `assert`s are the point: after erasure Verus still knows *which* impl +/// was erased, so both the id and the dispatched value are pinned down. +pub fn upcast_and_dispatch_l2(v: L2) -> (r: u64) + ensures + r == v.0, +{ + let d: &dyn Payload = &v; + assert(d.payload_id() == 2); + assert(d.word_spec() == v.0); + dispatch_payload(d) +} + + +/// The word carried by the member that `data` encodes at `id`. +/// +/// Needed because [`dispatch_store`] promising only the id would make dispatch +/// useless: a caller could tell *which* member is live but learn nothing from +/// running its code. This is the closed-world match at the spec level, and it is +/// what lets the value survive erasure. +pub open spec fn word_at(id: nat, data: [u8; EX_SIZE]) -> u64 { + if id == 1 { + >::try_from_spec(data)->Ok_0.0 + } else if id == 2 { + >::try_from_spec(data)->Ok_0.0 + } else { + >::try_from_spec(data)->Ok_0.0 + } +} + +/// **The bridge.** Stored bytes to a dispatchable reference to the shared trait. +/// +/// This is what `dispatch_meta` does in the frame layer, and it is the piece that +/// makes an aggregate useful rather than merely identifiable: the caller gets to +/// *run the member's code* without knowing which member it is. +/// +/// The `tag` argument is the ghost id's runtime witness, as in [`downcast_l2`] — +/// exec code cannot branch on ghost state, and vtable selection is exec. Upstream +/// that word is the vtable pointer already living in the slot, so carrying it +/// costs nothing that was not already being paid. +/// +/// Two things are worth noting about the proof. The match is *exhaustive over the +/// aggregate*, not over `usize`: the default arm is dead because `wf` forces the +/// id to inhabit `Outer`, i.e. to be one of `1`, `2`, `3`. And the postcondition +/// holds because each arm's `&Ln -> &dyn Payload` coercion is one Verus tracks — +/// it knows which impl was erased, so it knows the erased `payload_id`. +/// +/// So the only assumed step in the whole path is [`borrow_as`]. +/// +/// This discriminates. Probed by swapping one arm's member while leaving its +/// guard alone: both postconditions fail *and* `borrow_as`'s precondition fails, +/// since a tag of `2` neither makes the bytes an `L1` nor gives `L1`'s id. +pub fn dispatch_store(s: &Store, tag: usize) -> (r: &dyn Payload) + requires + s.wf(), + tag as nat == s.id_of(), + ensures + r.payload_id() == s.id_of(), + r.word_spec() == word_at(s.id_of(), s.data), +{ + proof { + // `wf` says some member admits these bytes; that pins the id to a leaf. + >::valid_in_possible_types(s.id_of(), s.data); + } + if tag == 1 { + assert(>::valid(1, s.data)); + borrow_as::<{ EX_SIZE }, L1>(&s.data) + } else if tag == 2 { + assert(>::valid(2, s.data)); + borrow_as::<{ EX_SIZE }, L2>(&s.data) + } else { + assert(tag == 3); + assert(>::valid(3, s.data)); + borrow_as::<{ EX_SIZE }, L3>(&s.data) + } +} + +/// End to end: store a member, then run its code through the erased reference. +/// +/// Neither `dispatch_store` nor `dispatch_payload` is told which member is live, +/// yet the returned word is pinned to the one that was stored. +pub fn store_then_dispatch(v: L2) -> (r: u64) + ensures + r == v.0, +{ + let s = store_l2(v); + let d = dispatch_store(&s, 2); + proof { + // The bytes decode back to `v`, so the erased word is `v`'s. + v.round_trip(); + } + assert(d.payload_id() == 2); + dispatch_payload(d) +} + +} // verus! diff --git a/verified_libs/vstd_extra/src/typing/example_any_of.rs b/verified_libs/vstd_extra/src/typing/example_any_of.rs new file mode 100644 index 000000000..000bf53b9 --- /dev/null +++ b/verified_libs/vstd_extra/src/typing/example_any_of.rs @@ -0,0 +1,78 @@ +//! [`AnyOf`](crate::AnyOf) applied to a three-member world. +//! +//! The same aggregate [`super::example`] builds by hand, to check that the +//! generated impls are the ones the laws need. Note the macro call sits outside +//! any `verus!` block — see the [macro docs](super::any_of) for why it must. +use vstd::prelude::*; + +use super::types::*; + +verus! { + +/// Three members with no shared behavior, only ids. +pub struct W1(pub u64); + +/// Second member. +pub struct W2(pub u64); + +/// Third member. +pub struct W3(pub u64); + +} // verus! +AnyOf!(World = [W1 = 1, W2 = 2, W3 = 3]); + +verus! { + +/// A one-member world, to exercise the recursion's base case. +pub struct S1(pub u64); + +/// A two-member world's members. Fresh types, not reused from `World`: a type +/// belongs to exactly one world, since its id lives in its own `TypeSet` impl. +/// Reusing `W1` here fails with `E0119 conflicting implementations`. +pub struct P1(pub u64); + +/// Second member of the pair. +pub struct P2(pub u64); + +} // verus! +AnyOf!(Single = [S1 = 7]); + +AnyOf!(Pair = [P1 = 8, P2 = 9]); + +verus! { + +/// The generated tree admits exactly the three ids. +pub proof fn world_admits_three(t: nat) + ensures + World::possible_types().contains(t) <==> (t == 1 || t == 2 || t == 3), +{ +} + +/// A member of the world lands in exactly one leaf. +/// +/// This is the property the hand-written example proves as `exactly_one_leaf`; it +/// holds here with no hand-written disjointness at all. +pub proof fn world_exactly_one(t: nat) + requires + World::possible_types().contains(t), + ensures + ({ + &&& W1::possible_types().contains(t) ==> !W2::possible_types().contains(t) + && !W3::possible_types().contains(t) + &&& W2::possible_types().contains(t) ==> !W1::possible_types().contains(t) + && !W3::possible_types().contains(t) + &&& W3::possible_types().contains(t) ==> !W1::possible_types().contains(t) + && !W2::possible_types().contains(t) + }), +{ +} + +/// The generated `HasId` satisfies its law. +pub proof fn world_id_of_in_possible_types(v: W2) + ensures + W2::possible_types().contains(v.id_of()), +{ + v.id_of_in_possible_types(); +} + +} // verus! diff --git a/verified_libs/vstd_extra/src/typing/example_meta.rs b/verified_libs/vstd_extra/src/typing/example_meta.rs new file mode 100644 index 000000000..1645910ac --- /dev/null +++ b/verified_libs/vstd_extra/src/typing/example_meta.rs @@ -0,0 +1,456 @@ +//! A syntax-faithful mimic of the frame layer's `dyn` casts. +//! +//! Every item here matches `ostd/src/mm/frame/meta.rs` and +//! `ostd/src/mm/frame/mod.rs` as closely as the types allow — same field shapes, +//! same casts, same call syntax — with the metadata impls reduced to dummies. The +//! purpose is to locate precisely where Verus stops accepting the real code. +//! +//! The four casts, in the order the frame layer performs them: +//! +//! 1. `&metadata as &dyn AnyFrameMeta` then `core::ptr::metadata(..)`, capturing a +//! vtable pointer at write time — `MetaSlot::write_meta`. +//! 2. `core::ptr::from_raw_parts_mut(storage_ptr, vtable_ptr)` to rebuild a +//! `*mut dyn AnyFrameMeta`, then dispatch `on_drop` through it and +//! `drop_in_place` it — `MetaSlot::drop_meta_in_place`. +//! 3. `transmute::, Frame>` — `Frame::into_dyn`. +//! 4. `(meta as &dyn core::any::Any).is::()` then the reverse transmute — +//! `TryFrom> for Frame`. +//! +//! # Result +//! +//! Casts 1–3 are accepted as written. The wide-pointer construction, the dispatch +//! through a rebuilt `*mut dyn`, and the transmutes all typecheck, needing +//! `external_body` only because `core::ptr::metadata`, `from_raw_parts_mut`, +//! `drop_in_place` and `transmute` have no Verus specifications. Nothing about +//! `dyn` itself obstructs them. +//! +//! Three registrations are needed first, none of them hard: +//! +//! - `UnsafeCell` has no `vstd` specification, so upstream's `MetaSlot` fields +//! cannot be written until it is registered — and the registration Verus's own +//! diagnostic suggests is incomplete, needing `external_body` as well because +//! `UnsafeCell`'s field is private. This is what our `PCell`/`PPtr` fields avoid. +//! - `DynMetadata` registers cleanly, but its parameter must be bounded by +//! `PointeeSized`, not `?Sized`: under `feature(sized_hierarchy)` a `?Sized` +//! proxy still carries a `MetaSized` predicate the external type does not have, +//! and the bounds must match exactly. +//! - `write_meta` needs an explicit `M: 'static`. Upstream gets it free from +//! `AnyFrameMeta: Any`, since `Any: 'static`; without `Any` the coercion inside +//! `core::ptr::metadata` fails with `E0310`. +//! +//! Cast 4 is **impossible in Verus today**, and not for want of a proof. It needs +//! `AnyFrameMeta: Any`, and: +//! +//! - Declaring that bound makes Verus panic rather than report an error: +//! `thread 'rustc' panicked at vir/src/traits.rs:1610: compute_dyn_compatibility: +//! missing trait Path(core, ["any" :: "Any"])`. The panic fires because +//! `compute_dyn_compatibility` looks every supertrait up in its map of +//! Verus-known traits, and `core::any::Any` is registered nowhere in `vstd`. +//! - Registering it is then blocked by two checks that contradict each other. +//! `type ExternalTraitSpecificationFor: Any;` fails with *external_trait_ +//! specification trait bound mismatch*, the diagnostic naming the missing bound +//! as `'static`. Adding it — `: Any + 'static` — fails with *unexpected bound in +//! ExternalTraitSpecificationFor*. Since `Any: 'static` is part of `Any`'s own +//! definition and the bounds must match exactly, no spelling satisfies both. +//! - Without the bound, the cast is rejected by *rustc*, before Verus sees it: +//! `E0605: non-primitive cast: &dyn AnyMeta as &(dyn core::any::Any + 'static)`. +//! +//! # `EitherType` cannot stand in for `Any` either +//! +//! The natural repair is to notice that `x as &dyn Any` is a dyn-to-dyn *upcast*, +//! and to put [`super::types::EitherType`] in that slot: make it a supertrait of +//! `AnyMeta`, upcast to `&dyn EitherType`, and read the id from there. It would +//! be a one-to-one syntactic match, and it would recover the id through the +//! upcast rather than through `AnyMeta`. +//! +//! It does not work, for a reason more basic than anything about `Any`: +//! +//! > `the trait bound Dyn<2, ()>: T196_Either is not satisfied` +//! +//! **Verus's dyn type does not implement the erased trait's Verus supertraits.** +//! Probed with a parameter-free supertrait carrying a single spec fn, which fails +//! identically (`Dyn<3, ()>: T198_Marker`), so this is not about `EitherType`'s +//! generics. Only marker and auto traits (`Send`, `Sync`) survive in supertrait +//! position. The same root cause explains two earlier observations: `dyn HasId` +//! does not typecheck because `HasId: TypeSet`, and a spec fn inherited from a +//! supertrait is not preserved across the `&T -> &dyn Trait` coercion. Verus +//! simply does not model the supertrait relation for dyn types. +//! +//! Verus does have an escape hatch — its `unsized_blanketed_traits` set makes a +//! supertrait usable if it has an unbounded `impl`. That cannot help +//! here: a blanket impl gives every type the *same* id, and an identity trait +//! whose answer does not depend on the type is no identity trait. +//! +//! So a `dyn` trait in Verus must be self-contained: everything an erased value +//! needs to report has to be declared on that one trait. [`try_from_tagged`] is +//! therefore not a workaround for a missing feature — it is the only shape +//! available, and [`AnyMeta::type_id`] must live where it does. +//! +//! So `/*Any +*/` in our `AnyFrameMeta`, and the commented-out `TryFrom`, are +//! forced rather than chosen. Verus needs either a `vstd` registration of `Any` or +//! `'static` support in `external_trait_specification` before a downcast built on +//! `Any` can be verified. +//! +//! [`try_from_tagged`] is the replacement, mirroring cast 4 with the one +//! substitution that makes it expressible: `Any::is::()` becomes a comparison of +//! a dyn-dispatched tag against a statically known one. That test is *verified*, +//! and the `Result` shape, the unchanged-on-failure `Err`, and the transmute are +//! all preserved. +//! +//! Note the field types below are upstream Asterinas's, not the ones in our +//! `MetaSlot` — ours carries `vtable_ptr: PPtr` under a comment reading +//! "VERUS LIMITATION: Currently we do not verify this because of the dependency on +//! the `dyn Trait` pattern". Casts 1–3 are evidence that field can be restored to +//! `UnsafeCell>`. +use core::cell::UnsafeCell; +use core::marker::PhantomData; +use core::mem::MaybeUninit; +use core::ptr::DynMetadata; + +use vstd::prelude::*; + +verus! { + +/// Registers `UnsafeCell` with Verus. +/// +/// Needed because upstream's `MetaSlot` fields are `UnsafeCell`, and Verus has no +/// specification for it — our tree sidesteps this with `PCell`/`PPtr`. The +/// declaration is the one Verus's own diagnostic suggests. +#[verifier::reject_recursive_types(T)] +#[verifier::external_type_specification] +#[verifier::external_body] +pub struct ExUnsafeCell(UnsafeCell) where T: core::marker::MetaSized + ?Sized; + +/// Registers `DynMetadata` with Verus. +/// +/// The vtable-pointer type itself. Unlike `core::any::Any` this registers without +/// trouble — it carries no `'static` bound, which is the thing that made `Any` +/// unregisterable. +#[verifier::reject_recursive_types(T)] +#[verifier::external_type_specification] +#[verifier::external_body] +pub struct ExDynMetadata(DynMetadata); + +/// Mimics `FRAME_METADATA_MAX_SIZE`. +pub const META_MAX_SIZE: usize = 8; + +/// Mimics `MetaSlotStorage`. +/// +/// Upstream this is a raw `[u8; FRAME_METADATA_MAX_SIZE]`; ours is an exec-tagged +/// union. Kept as bytes here because the casts under test do not care which. +pub struct MetaSlotStorage { + pub bytes: [u8; META_MAX_SIZE], +} + +/// Mimics `AnyFrameMeta`. +/// +/// Same shape as the real trait: `unsafe`, `Send + Sync`, an `open spec fn` +/// per-impl precondition, and an exec `on_drop` on `&mut self` whose `requires` +/// calls that precondition. The real one also threads a `VmReader` and two +/// `Tracked` owner arguments; those are dropped as orthogonal to dispatch. +/// +/// `Any` is absent from the supertraits, exactly as in our tree. See the module +/// docs — the bound cannot be written, so [`Self::type_id`] takes its place. +pub unsafe trait AnyMeta: Send + Sync { + /// The id of *this value's* type, readable through an erased reference. + /// + /// Declared here rather than inherited from a supertrait, and not + /// `where Self: Sized`, because both are needed for it to survive the + /// `&M -> &dyn AnyMeta` coercion. This is the stand-in for `Any::type_id`. + spec fn type_id(&self) -> usize; + + /// The executable form, dispatched through the vtable. + fn type_id_val(&self) -> (r: usize) + ensures + r == self.type_id(), + ; + + /// Per-impl precondition for [`Self::on_drop`]. Default is `true`. + open spec fn on_drop_pre(&self) -> bool { + true + } + + fn on_drop(&mut self) + requires + old(self).on_drop_pre(), + ; +} + +/// The static half of the identity test. +/// +/// Separate from [`AnyMeta`] because it is deliberately *not* dyn-dispatched: a +/// downcast needs `M`'s id without having an `M` to ask, which is what +/// `TypeId::of::()` supplies upstream. An associated const would be the natural +/// spelling and is what forces the split — associated consts are not +/// dyn-compatible, so putting one on `AnyMeta` would make `dyn AnyMeta` illegal. +pub trait MetaTag { + spec fn tag_spec() -> usize; + + fn tag() -> (r: usize) + ensures + r == Self::tag_spec(), + ; + + /// A value's dispatched id agrees with its type's static id. + /// + /// This is the fact `Any` provides for free and the one thing that has to be + /// supplied by hand. Without it the two halves of the test are unrelated and a + /// successful comparison would say nothing. + proof fn tag_coherent(&self) where Self: core::marker::Sized + AnyMeta + ensures + self.type_id() == Self::tag_spec(), + ; +} + +/// Mimics `FrameMetaVtablePtr`. +pub type MetaVtablePtr = DynMetadata; + +/// Mimics `MetaSlot`, with the fields upstream actually uses. +pub struct MetaSlot { + pub storage: UnsafeCell, + pub vtable_ptr: UnsafeCell>, +} + +/// A dummy metadata type, standing in for e.g. `MetaPageMeta`. +pub struct MetaA { + pub val: u64, +} + +/// A second dummy, so dispatch and downcasting have something to choose between. +/// With one impl a vtable-shaped call would verify vacuously. +pub struct MetaB { + pub val: u64, +} + +#[verifier::external] +unsafe impl Send for MetaA { + +} + +#[verifier::external] +unsafe impl Sync for MetaA { + +} + +#[verifier::external] +unsafe impl Send for MetaB { + +} + +#[verifier::external] +unsafe impl Sync for MetaB { + +} + +unsafe impl AnyMeta for MetaA { + open spec fn type_id(&self) -> usize { + 1 + } + + fn type_id_val(&self) -> (r: usize) { + 1 + } + + #[verifier::external_body] + fn on_drop(&mut self) { + } +} + +impl MetaTag for MetaA { + open spec fn tag_spec() -> usize { + 1 + } + + fn tag() -> (r: usize) { + 1 + } + + proof fn tag_coherent(&self) { + } +} + +unsafe impl AnyMeta for MetaB { + open spec fn type_id(&self) -> usize { + 2 + } + + fn type_id_val(&self) -> (r: usize) { + 2 + } + + #[verifier::external_body] + fn on_drop(&mut self) { + } +} + +impl MetaTag for MetaB { + open spec fn tag_spec() -> usize { + 2 + } + + fn tag() -> (r: usize) { + 2 + } + + proof fn tag_coherent(&self) { + } +} + +impl MetaSlot { + /// Cast 1 — upcast at write time. Mimics `MetaSlot::write_meta`. + /// + /// The body is the line that is *commented out* in our tree. It typechecks; + /// `external_body` is needed only because `core::ptr::metadata` has no spec. + /// Note the explicit `'static`. Upstream it is implied by `AnyFrameMeta: Any`, + /// since `Any: 'static`; with `Any` unavailable the bound has to be written by + /// hand, or `core::ptr::metadata` rejects the coercion with `E0310`. + #[verifier::external_body] + pub unsafe fn write_meta(&self, metadata: M) { + // SAFETY: Caller ensures that the access to the fields are exclusive. + let vtable_ptr = unsafe { &mut *self.vtable_ptr.get() }; + vtable_ptr.write(core::ptr::metadata(&metadata as &dyn AnyMeta)); + } + + /// Cast 2 — rebuild a wide pointer and dispatch through it. + /// Mimics `MetaSlot::drop_meta_in_place`. + /// + /// This is the shape our tree currently keeps alive only as a type-check. It + /// is accepted as written. + #[verifier::external_body] + pub unsafe fn drop_meta_in_place(&self) { + // SAFETY: We have exclusive access to the frame metadata. + let vtable_ptr = unsafe { &mut *self.vtable_ptr.get() }; + // SAFETY: The frame metadata is initialized and valid. + let vtable_ptr = unsafe { vtable_ptr.assume_init_read() }; + + let storage_ptr: *mut () = self.storage.get() as *mut (); + let meta_ptr: *mut dyn AnyMeta = core::ptr::from_raw_parts_mut(storage_ptr, vtable_ptr); + + // SAFETY: `ptr` points to the metadata storage which is valid to be + // mutably borrowed under `vtable_ptr` because the metadata is valid, + // the vtable is correct, and we have exclusive access. + unsafe { + // Invoke the custom `on_drop` handler. + (*meta_ptr).on_drop(); + // Drop the frame metadata. + core::ptr::drop_in_place(meta_ptr); + } + } + + /// Mimics `MetaSlot::dyn_meta_ptr`, the shared-reference form. + #[verifier::external_body] + pub unsafe fn dyn_meta_ptr(&self) -> *mut dyn AnyMeta { + // SAFETY: The page metadata is valid to be borrowed immutably, since it + // will never be borrowed mutably after initialization. + let vtable_ptr = unsafe { &*self.vtable_ptr.get() }; + + // SAFETY: The page metadata is initialized and valid. + let vtable_ptr = *unsafe { vtable_ptr.assume_init_ref() }; + + core::ptr::from_raw_parts_mut(self as *const MetaSlot as *mut MetaSlot, vtable_ptr) + } +} + +/// Mimics `Frame`. +/// +/// `#[repr(transparent)]` over a pointer plus a ZST phantom, as upstream, which is +/// what makes the transmutes in casts 3 and 4 layout-valid. +#[repr(transparent)] +pub struct Frame { + pub ptr: *const MetaSlot, + pub _marker: PhantomData, +} + +impl Frame { + /// Cast 3 — erase the static metadata type. Mimics `Frame::into_dyn`. + #[verifier::external_body] + pub fn into_dyn(self) -> Frame { + // SAFETY: `Frame` is `#[repr(transparent)]` over a thin pointer plus a + // zero-size `PhantomData`. `Frame` has the same runtime + // layout (thin pointer + ZST phantom). + unsafe { core::mem::transmute(self) } + } +} + +impl Frame { + /// The id of the metadata this frame points at. + /// + /// Uninterpreted here because the dummy slot carries no ghost state; in the + /// frame layer this is the region's view of the slot. + pub uninterp spec fn meta_id(&self) -> usize; + + /// Mimics `Frame::::dyn_meta`. + /// + /// The `ensures` is what makes the erased reference usable: without tying the + /// dispatched id back to the frame, a caller could compare tags and conclude + /// nothing about *this* frame. + #[verifier::external_body] + pub fn dyn_meta(&self) -> (r: &dyn AnyMeta) + ensures + r.type_id() == self.meta_id(), + { + // SAFETY: The metadata is initialized and valid. + unsafe { &*(*self.ptr).dyn_meta_ptr() } + } +} + +/// Cast 4, with the one substitution that makes it expressible. +/// +/// Mirrors `TryFrom> for Frame`, except that +/// +/// ```text +/// if (dyn_frame.dyn_meta() as &dyn core::any::Any).is::() { +/// ``` +/// +/// becomes +/// +/// ```text +/// if dyn_frame.dyn_meta().type_id_val() == M::tag() { +/// ``` +/// +/// Both compare an id read through the vtable against one known statically. The +/// difference is only where the ids come from: the compiler's `TypeId`, which +/// Verus cannot see, versus [`MetaTag`], which it can. +/// +/// A free function rather than a `TryFrom` impl, to keep the tag plumbing visible; +/// the `Result` shape and the unchanged-on-failure `Err` are preserved. +/// +/// The transmute stays `external_body`, as upstream. What is *gained* is that the +/// test guarding it is verified: the postcondition records that `Ok` happens +/// exactly when the frame's metadata has `M`'s id. +pub fn try_from_tagged(dyn_frame: Frame) -> (res: + Result, Frame>) + ensures + (res is Ok) == (dyn_frame.meta_id() == M::tag_spec()), +{ + if dyn_frame.dyn_meta().type_id_val() == M::tag() { + // SAFETY: The metadata is coerceable and the struct is transmutable. + Ok(transmute_to_typed::(dyn_frame)) + } else { + Err(dyn_frame) + } +} + +/// The transmute half of cast 4, split out so the test above stays verified. +#[verifier::external_body] +pub fn transmute_to_typed(dyn_frame: Frame) -> Frame { + // SAFETY: The metadata is coerceable and the struct is transmutable. + unsafe { core::mem::transmute::, Frame>(dyn_frame) } +} + +/// The downcast admits the right type and rejects the other. +/// +/// Both directions matter and neither is vacuous: `Ok` needs the tags to agree, +/// and `Err` is what stops a `MetaB` frame from being read as a `MetaA`. +pub fn downcast_discriminates(a: Frame, b: Frame) + requires + a.meta_id() == 1, + b.meta_id() == 2, +{ + let ra = try_from_tagged::(a); + assert(ra is Ok); + let rb = try_from_tagged::(b); + assert(rb is Err); +} + +} // verus! diff --git a/verified_libs/vstd_extra/src/typing/mod.rs b/verified_libs/vstd_extra/src/typing/mod.rs new file mode 100644 index 000000000..7b160e8ad --- /dev/null +++ b/verified_libs/vstd_extra/src/typing/mod.rs @@ -0,0 +1,21 @@ +//! A closed-world model of runtime type identity. +//! +//! Verus does not expose `TypeId`, so a value that has been erased has no way to +//! say what it is. This module builds the missing piece out of ordinary traits: +//! members are given ids, aggregates are built by nesting, and uniqueness of ids +//! is discharged *per nesting node* rather than by a global registry — so adding +//! a member changes only the node that admits it. +//! +//! [`types`] has the machinery; [`example`] exercises it on a three-member +//! aggregate, including the three behaviors that motivate the whole thing: +//! upcast, downcast, and dispatch. +#[macro_use] +pub mod any_of; + +pub mod types; + +pub mod example; + +pub mod example_meta; + +pub mod example_any_of; diff --git a/verified_libs/vstd_extra/src/typing/types.rs b/verified_libs/vstd_extra/src/typing/types.rs new file mode 100644 index 000000000..014193db9 --- /dev/null +++ b/verified_libs/vstd_extra/src/typing/types.rs @@ -0,0 +1,365 @@ +use vstd::prelude::*; + +use vstd::std_specs::convert::{IntoSpec, TryFromSpec}; + +use core::marker::PhantomData; + +verus! { + +pub trait ByteSized: Sized { + proof fn size_correct() + ensures + size_of::() == SIZE, + ; +} + +pub trait ByteRepr: ByteSized + TryFromSpec<[u8; SIZE]> + + IntoSpec<[u8; SIZE]> { + proof fn round_trip(self) + ensures + Self::try_from_spec(self.into_spec()) == Ok(self), + ; + + proof fn canonical(data: [u8; SIZE]) + requires + Self::try_from_spec(data) is Ok, + ensures + Self::try_from_spec(data)->Ok_0.into_spec() == data, + ; +} + +pub trait TypeSet { + spec fn possible_types() -> Set where Self: Sized; +} + +pub trait HasId: TypeSet { + /// The id of *this value*. + spec fn id_of(&self) -> nat; + + /// This value's id and its contents agree. + spec fn wf(&self) -> bool; + + proof fn id_of_in_possible_types(&self) + where Self: Sized + requires + self.wf(), + ensures + Self::possible_types().contains(self.id_of()), + ; +} + +/// A witness that two members' id sets do not overlap. +pub trait DisjointFrom: TypeSet + Sized { + proof fn disjoint(type_id: nat) + ensures + !(Self::possible_types().contains(type_id) + && B::possible_types().contains(type_id)), + ; +} + +/// The erased view of an aggregate value. +/// +/// # Why this declares its own `id_of`/`wf` +/// +/// A spec fn survives the `&T -> &dyn Trait` coercion only if `Trait` itself +/// declares it. Inheriting it from a supertrait is not enough: Verus propagates +/// the *declaring* trait's functions across the coercion, so a postcondition +/// stated with a supertrait's spec fn is unprovable at the coercion site even +/// though the same postcondition using an own function goes through. Probed both +/// ways, generically and at a concrete type. +/// +/// Hence [`Self::dyn_id`] and [`Self::dyn_wf`], which mirror [`HasId::id_of`] and +/// [`HasId::wf`]. The duplication is not free, but the alternative is an erased +/// object about which nothing can be concluded, which defeats the purpose. +/// +/// [`HasId`] is deliberately *not* a supertrait, for a second reason: it extends +/// [`TypeSet`], and Verus's dyn type does not satisfy that bound, so `dyn HasId` +/// does not even typecheck. Aggregates implement both traits independently — +/// `HasId` for use at the concrete type, `EitherType` for use through an erased +/// one — and [`lemma_dyn_agrees`] moves between them. +/// +/// Note the sides are bounded by [`TypeSet`], not [`HasId`]: the law below names +/// only `A::possible_types` and `B::possible_types`. That matters for nesting — the right +/// side of a nest is a *phantom* describing an id set, with no values of its own, +/// so demanding `HasId` of it would mean inventing an `id_of` for a type that +/// never has one. +pub trait EitherType { + /// This value's id, readable through an erased reference. + spec fn dyn_id(&self) -> nat; + + /// This value's well-formedness, readable through an erased reference. + spec fn dyn_wf(&self) -> bool; + + /// Every well-formed value belongs to exactly one side. + /// + /// This is where uniqueness comes from, and it is worth being precise about + /// how: the obligation is discharged *per nesting node*, so a collision + /// between two members fails a proof at the node that joins them. Nothing + /// global has to be maintained, and nothing has to be remembered when a + /// member is added — which is the advantage over a flat tag registry with a + /// hand-kept range discipline. + /// + /// This is also the aggregate's *dispatch*: callable on `&dyn EitherType`, + /// it yields the disjunction without the caller knowing which member is live. + proof fn type_id_laws(tracked &self) + requires + self.dyn_wf(), + ensures + { + ||| A::possible_types().contains(self.dyn_id()) + && !B::possible_types().contains(self.dyn_id()) + ||| B::possible_types().contains(self.dyn_id()) + && !A::possible_types().contains(self.dyn_id()) + }, + ; + +} + +/// A description of what byte patterns encode which members. +/// +pub trait Member: TypeSet + Sized { + /// `data` is a valid encoding of the member of this aggregate named by `id`. + spec fn valid(id: nat, data: [u8; SIZE]) -> bool; + + /// Only ids this aggregate admits can be held by it. + /// + /// Proved rather than assumed at every impl below, which is what keeps + /// `GhostTaggedArray`'s `id_of_in_possible_types` axiom-free. + proof fn valid_in_possible_types(id: nat, data: [u8; SIZE]) + requires + Self::valid(id, data), + ensures + Self::possible_types().contains(id), + ; +} + +/// A single-member aggregate wrapping a concrete representable type. +pub struct LeafType(pub PhantomData); + +impl TypeSet for LeafType { + open spec fn possible_types() -> Set { + M::possible_types() + } +} + +impl> Member for LeafType { + /// The bytes decode as `M`, and `id` is one of `M`'s ids. + /// + /// Note it does not say the decoded value's `id_of` *equals* `id`. It cannot + /// without knowing that value is well-formed, and it need not: for a member + /// owning a single id the two coincide, and for one owning several, which of + /// them is live is not something the aggregate arbitrates. + open spec fn valid(id: nat, data: [u8; SIZE]) -> bool { + &&& M::try_from_spec(data) is Ok + &&& M::possible_types().contains(id) + } + + proof fn valid_in_possible_types(id: nat, data: [u8; SIZE]) { + } +} + +/// Two aggregates joined: ids and valid encodings are the union of the sides'. +/// +/// Stating `possible_types` as the union is what makes +/// `Self::possible_types().contains(self.id_of())` derivable rather than an extra +/// obligation: given [`EitherType`]'s disjunction, membership in one side gives +/// membership in the union. +pub struct ConsType(pub PhantomData<(A, B)>); + +impl TypeSet for ConsType { + open spec fn possible_types() -> Set { + A::possible_types().union(B::possible_types()) + } +} + +impl, B: Member> Member for ConsType { + open spec fn valid(id: nat, data: [u8; SIZE]) -> bool { + A::valid(id, data) || B::valid(id, data) + } + + proof fn valid_in_possible_types(id: nat, data: [u8; SIZE]) { + if A::valid(id, data) { + A::valid_in_possible_types(id, data); + } else { + B::valid_in_possible_types(id, data); + } + } +} + +/// Bytes plus a ghost id saying which member of `T` they hold. +/// +/// The id is held *directly* rather than recovered by decoding, and it is a +/// member id rather than a per-level `LEFT`/`RIGHT`. Both changes are what make +/// this nest: `T` may be an arbitrarily deep [`ConsType`] tree, and no matter how +/// deep the matching member sits, there is exactly one tag and it is stored +/// exactly once — in ghost state, so the runtime footprint is still just the +/// bytes, as upstream. +/// +/// The cost is that tag and bytes can disagree, since nothing about the struct +/// forces them to. That is what [`HasId::wf`] is for: constructors carry it as a +/// postcondition and consumers as a precondition, so it is checked rather than +/// trusted. Elsewhere in this tree the same pairing — a stored word plus a ghost +/// type tag — had to be propped up by an axiom and an unenforced "always write +/// both together" convention. +pub struct GhostTaggedArray> { + /// The member id, as ghost state. + pub id: Ghost, + pub data: [u8; SIZE], + pub _t: PhantomData, +} + +impl> TypeSet for GhostTaggedArray { + open spec fn possible_types() -> Set { + T::possible_types() + } +} + +impl> HasId for GhostTaggedArray { + open spec fn id_of(&self) -> nat { + self.id@ + } + + open spec fn wf(&self) -> bool { + T::valid(self.id@, self.data) + } + + proof fn id_of_in_possible_types(&self) { + T::valid_in_possible_types(self.id@, self.data); + } +} + +impl + DisjointFrom, B: Member> EitherType< + A, + B, +> for GhostTaggedArray> { + open spec fn dyn_id(&self) -> nat { + self.id@ + } + + open spec fn dyn_wf(&self) -> bool { + ConsType::::valid(self.id@, self.data) + } + + proof fn type_id_laws(tracked &self) { + // "not both" from the disjointness witness ... + A::disjoint(self.dyn_id()); + // ... and "at least one" from whichever side admits the bytes. + if A::valid(self.id@, self.data) { + A::valid_in_possible_types(self.id@, self.data); + } else { + B::valid_in_possible_types(self.id@, self.data); + } + } +} + +impl + DisjointFrom, B: Member> GhostTaggedArray< + SIZE, + ConsType, +> { + /// Upcast: view the stored bytes as an erased member of the `A | B` aggregate. + /// + /// Borrows rather than boxing: a metadata slot has no allocator, and the + /// caller only needs to dispatch through the value, not own it. This is the + /// same shape as `dispatch_meta` in the frame layer. + /// + /// Note the `DisjointFrom` bound, which is not incidental: erasure is only + /// available once the two sides are *known* not to collide. A design that + /// let you erase first and check uniqueness later would have to check it + /// globally, which is the thing this is meant to avoid. + /// + /// The postconditions are what make the erased value usable. Both `id_of` + /// and `wf` survive because neither is `where Self: Sized`, so both are in + /// the vtable — without them the result would be an opaque object nothing + /// could be concluded about, which is what an `external_body` version of + /// this promising nothing would have amounted to. + pub exec fn as_dyn(&self) -> (r: &dyn EitherType) + ensures + r.dyn_id() == self.dyn_id(), + r.dyn_wf() == self.dyn_wf(), + { + self + } +} + +/// The concrete and erased views of an aggregate agree. +/// +/// Both sides are `open`, so this is definitional — it exists to be cited rather +/// than to be proved, and it is the seam between constructors (which establish +/// [`HasId::wf`]) and consumers (which see [`EitherType::dyn_wf`]). +pub proof fn lemma_dyn_agrees + DisjointFrom, B: Member>( + s: &GhostTaggedArray>, +) + ensures + s.dyn_id() == s.id_of(), + s.dyn_wf() == s.wf(), +{ +} + +/// Storing a well-formed member establishes [`Member::valid`] at its own id. +/// +/// This is the constructor side of `wf`, and the one place [`ByteRepr`]'s +/// round-trip law is consumed: it is what says the bytes just written decode +/// again, while `id_of_in_possible_types` says the id recorded beside them is one this +/// leaf admits. +pub proof fn lemma_leaf_valid>(m: M) + requires + m.wf(), + ensures + as Member>::valid(m.id_of(), m.into_spec()), +{ + m.round_trip(); + m.id_of_in_possible_types(); +} + + +/// Reinterpret stored bytes as a reference to the member they encode. +/// +/// # The one axiom +/// +/// This is the only assumed fact in the module that is not a per-type layout +/// obligation, and it is what makes a stored member *dispatchable*: with a `&M` +/// in hand, an ordinary `&M -> &dyn Tr` coercion produces an erased reference to +/// whatever trait the members share, and Verus already tracks which impl was +/// erased across that coercion. So no `Any`-style downcast axiom is needed — +/// reinterpretation is the whole of the gap. +/// +/// It cannot be proved. Verus has no model of the pointer cast involved, and the +/// fact being asserted is that a byte pattern satisfying `M`'s decode really may +/// be *read as* an `M` in place, rather than decoded into a fresh value. That is +/// a statement about layout, which is why the precondition is exactly the decode +/// and nothing weaker: bytes that do not decode may not be borrowed at all. +/// +/// The frame layer's `borrow_meta_mut` is the same axiom for the mutable case. +#[verifier::external_body] +pub exec fn borrow_as<'a, const SIZE: usize, M: ByteRepr>(data: &'a [u8; SIZE]) -> (r: &'a M) + requires + M::try_from_spec(*data) is Ok, + ensures + *r == M::try_from_spec(*data)->Ok_0, +{ + unimplemented!() +} + +/// Distinct valid byte patterns decode to distinct values. +/// +/// The content of [`ByteRepr::canonical`], stated the way it is usually wanted: +/// decoding is injective on valid patterns. Together with +/// [`ByteRepr::round_trip`] — which makes it surjective onto values — this is the +/// bijection, and it is what a storage abstraction needs in order to promise that +/// reading a value out and writing it back leaves the bytes alone. +pub proof fn lemma_decode_injective>( + a: [u8; SIZE], + b: [u8; SIZE], +) + requires + M::try_from_spec(a) is Ok, + M::try_from_spec(b) is Ok, + M::try_from_spec(a) == M::try_from_spec(b), + ensures + a == b, +{ + M::canonical(a); + M::canonical(b); +} + +} // verus!