Conversation
`any.rs` was orphaned: the module was never declared, so the two `assume_specification`s for `TypeId::of` and `TypeId::eq` were not compiled and the whole type-identity feature was inert. The declaration is present on `typeid-counter-ids`; it was lost squashing onto upstream, which had added `pub mod array;` at the same alphabetical slot.
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Hi! This PR is motivated by an attempt to verify code that uses
Anyto identify which concrete type is currently carried by adynobject. Specifically, ifAnyFoo: Any, andfoo: dyn AnyFoo, we would like to be able to check iffoois some specificAnyFoo,F, with:(foo as &dyn core::any::Any).is::<F>()I've written a minimal example of how we're approaching this at: https://github.com/certikproject/typeid-example-pub
We can handle most of the reasoning by creating our own axiomatization of
Any. The missing ingredient is the existence of a type identifier that is guaranteed to be distinct across different types. This PR introduces that type as a primitiveTypeTag(sinceTypeIdis already taken) that lowers into AIR as a curried application of uninterpreted functions. This could be the basis for eventualAnysupport within Verus, and in the meantime it is enough to support our needs while hopefully not being intrusive.Built-in types and type decorations are assigned unique, negative integer values. User-defined types are assigned positive values by hashing their paths. (I played around with a version that just counted all types in the context, but found reasoning about it a bit harder. E.g., what if something perturbs the order? But it's also a reasonable approach if you prefer.)
Since this is likely to be a pretty niche feature, I set it up to only emit axioms if the AST actually contains a type tag, to keep it from destabilizing the solver context for people who aren't using it.This wasn't having much impact relative to the complexity, so I've dropped it.That's the broad overview. Happy to answer questions and make changes if needed. Thanks for your time!
Assisted by: Claude Code:Opus 5
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.