Sanjit Bhat
Sanjit Bhat
@celinval did you get a chance to look at this PR?
Not currently, but I think it's fairly close to being ready to go. @celinval how close do you think it is? I can take a look at the comments tomorrow,...
Update: will only be able to get to this over the upcoming weekend.
Concretely, in Perennial, I think we should be able to (faultily) prove this, whereas in Golang, this assertion fails. ``` func test() { slEmpt := make([]byte, 0) machine.Assert((slEmpt == nil)...
Ran into this as well. Came up with the following slightly reduced examples: ```go func oneRet(b []byte) []byte { return b } func twoRet(b []byte) (uint64, []byte) { return 0,...
I'd imagine having some sort of named-based pattern matching in `selpat` would be fairly convenient. Would it be useful to use regex for this? E.g., that could allow specifying which...
aside: i always found it a bit un-intuitive that `f ::= v` is the goose notation for a pair. that looks a lot more like some sort of assignment operation.
note: it'd be nice if rocq had a tool that generates an export ordering graph for a project. it'd help us get actual data on the various modules and their...