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.

Sign up for GitHub

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

Jump to bottom

GarageDoor does not compile with latest bedrock2 (Leakage traces) #2007

Closed
andres-erbsen opened this issue Jan 24, 2025 · 2 comments · Fixed by mit-plv/bedrock2#445 · May be fixed by #2009
Closed

GarageDoor does not compile with latest bedrock2 (Leakage traces) #2007

andres-erbsen opened this issue Jan 24, 2025 · 2 comments · Fixed by mit-plv/bedrock2#445 · May be fixed by #2009

Comments

@andres-erbsen
Copy link
Contributor

GarageDoor.v calls memequal. memequal has a proof in LeakageSemantics. Garagedoor uses Semantics. It should be changed to use LeakageSemantics or MetricLeakageSemantics, but

  • I couldn't find a weakening lemma to prove a degenerate LeakageSemantics call using Semantics
  • I couldn't find programlogic & etc for MetricLeakageSemantics

The first one is probably easier to fix. Do you agree, @OwenConoly ? Do you then know which semantics we'd want to call the compiler-correctness theorem with?

As for who would do this work: I was thinking I'd do it when I merged the bedrock2 PR but now I have questions for you (and I am at a conference anyway) so if you want to give it a stab it would be very welcome.

(As a last-resort fallback, e.g. if this ends up blocking a coq-compat PR, we could also duplicate memequal.)
@OwenConoly
Copy link
Collaborator

There is no MetricLeakageProgramLogic etc since, given the lack of test cases, I figured MetricLeakageProgramLogic would be about worthless and filled with bugs. (I spent a lot of time fixing problems with LeakageProgramLogic.)

There are no Semantics -> LeakageSemantics, Semantics -> MetricSemantics, MetricSemantics -> LeakageSemantics, MetricSemantics -> Semantics, or MetricLeakageSemantics -> LeakageSemantics lemmas because I did not realize they'd be useful. But it would be very easy to add any or all of these. I agree that this would be the easiest route.

Do you then know which semantics we'd want to call the compiler-correctness theorem with?

I believe the only compiler theorem we have is in terms of MetricLeakageSemantics.

I'd probably be able to fix this by next Wednesday or Thursday. If that is soon enough then I'd be happy to take care of it.

@andres-erbsen
Copy link
Contributor Author

Next week sounds fine. Thank you.

This was referenced Jan 31, 2025
Merged
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
2 participants
@andres-erbsen @OwenConoly