Conversation
abentkamp
force-pushed
the
specs
branch
2 times, most recently
from
2ee2b9c to
86790d0
Compare
abentkamp
changed the title
abentkamp
changed the title
clementblaudeau
left a comment
clementblaudeau
left a comment
There was a problem hiding this comment.
Looks good overall. A couple of comments below. To me, the main question is : where should the specs go, and where should the spec attributes go ? Inheriting from step is not enough I assume ? By putting them directly with the definitions we run the risk of upstreaming, and by putting them separately we run the risk of desync/missing annotations.
| theorem triple_of_result_eq {α : Type} {x : Result α} {v : α} : | ||
| ⦃ ⌜ True ⌝ ⦄ x ⦃ ⇓ r => ⌜ r = v ⌝ ⦄ ↔ x = .ok v := by | ||
| cases x <;> simp_all [Triple, WP.wp, PredTrans.apply] |
There was a problem hiding this comment.
Out of curiosity, what is the use of that theorem ?
There was a problem hiding this comment.
I've renamed it to triple_post_eq_iff_eq now. It's used a few lemmas further down.
| (inv : α → Prop) | ||
| (rel : γ → γ → Prop) | ||
| (termination : α → γ) | ||
| (hwf : WellFounded rel) |
There was a problem hiding this comment.
Should this be a typeclass argument ? or implicit ?
There was a problem hiding this comment.
I don't think so. There is a type class WellFoundedRelation that attaches one canonical well-founded relation to a type. But here, we don't necessarily want the canonical one. So I think we need to keep it explicit.
There was a problem hiding this comment.
Oh, wait, did you mean making inv implicit? Yeah, we could do that.
|
In Aeneas, I have already extended the |
|
To be clear: I think the |
|
The |
2 participants
This PR adds specs for some tricky functions in Aeneas and in core.
Open question: Should I put the non-core specs into the Aeneas repo? Where though?
All specs are annotated with a global
@[spec]. I think that is the right thing to do because otherwise users will need to figure out how to turn on specs before being able to use them. Although specs can't be deactivated globally, it's fairly easy to override them with a higher-prio spec or deactivate them locally usingmvcgen [-my_spec].Another problem is that slicing is defined wrong in Aeneas when start and end are equal. I left a TODO comment in the two places where that pops up here.