PCC: add basic "memory types".#7219
Merged
Merged
Conversation
fitzgen
approved these changes
Oct 11, 2023
Member
fitzgen
left a comment
There was a problem hiding this comment.
r=me with nitpick-y suggestions that you can take or leave but also a more important point about a git submodule that should definitely be addressed before landing
Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>
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
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.
This PR adds a notion of "memory types" to the PCC (proof-carrying code) framework. To borrow a doc-comment:
A memory type is a struct-like definition -- fields with offsets, each field having a type and possibly an attached fact -- that we can use in proof-carrying code to validate accesses to structs and propagate facts onto the loaded values as well.
Memory types are meant to be rich enough to describe the layout of values in memory, but do not necessarily need to embody higher-level features such as subtyping directly. Rather, they should encode an implementation of a type or object system.
Note also that it is a non-goal for now for this type system to be "complete" or fully orthogonal: we have some restrictions now (e.g., struct fields are only primitives) because this is all we need for existing PCC applications, and it keeps the implementation simpler.
While developing this, we originally sketched out a more complete type-system that had arrays, allowed struct fields to be memory types themselves, and was in general more flexible. However, the possibility of cycles, non-statically-sized types, etc., was getting overly complex and I decided to YAGNI-simplify a bit for now. The Doc-comment on the module does sketch out what other types will be needed, and I think those plus a GV-bounded
maxfact will be enough to express PCC facts for all static and dynamic memories and table accesses in Wasmtime. (A partial further development of the more complete system, with some more validator checks for cycles, etc., is on this WIP branch.)Part of this change was
Co-authored-by: Nick Fitzgerald fitzgen@gmail.com