Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

docs: locality names have Top_ prefix #20

Open
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

cfm
Copy link
Contributor

@cfm cfm commented Feb 13, 2024

The extraction I see from docs/encrypted_key_basic.owl as of a4108a6 includes the Top_ prefix both in the arguments expected by main() and in the names of the configuration files generated by cargo run -- config.

@pratapsingh1729
Copy link
Collaborator

Hi! Thanks for checking out Owl :)

We are currently working on a rewrite of the extraction mechanism. The current extraction mechanism produces unverified plain Rust implementations. When the rewrite is complete, extraction will generate formally verified Rust implementations that are proved to have the same input-output behavior as the Owl source program, using Verus, a deductive program verifier for Rust. The issue about locality naming has been fixed in that branch, but we didn’t backport it into the old Rust extraction mechanism. We hope to have a version of the new extraction mechanism merged soon.

@cfm
Copy link
Contributor Author

cfm commented Feb 14, 2024

That's exciting news, @pratapsingh1729. I've assumed there are implementation changes forthcoming, but I at least needed to understand the delta between the documented and actual paths in order to try out the current implementation on main. That delta is all this patch tries to resolve in the documentation. :-)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants