refactor: Allow op and model initialisation to fail, and promises - #246
refactor: Allow op and model initialisation to fail, and promises#246tperami wants to merge 1 commit into
Conversation
| ((∃ tid, Error s ∈ PState.run_tid isem prom tid finPs) | ||
| ∨ | ||
| (∃ tid ev, | ||
| PState.allowed_promises_tid isem prom certified finPs |
There was a problem hiding this comment.
I think we should consider the case where emit_promise returns Error "invalid promise". In certified mode, this branch still requires allowed_promises_tid, which requires the same promise call to return Ok. Therefore, it cannot return an Error here, and promise-emission failures can never be reported by the certified model. Could we handle the Error case before checking certification?
There was a problem hiding this comment.
This is a very good catch and quite a deep edge-case. Great work! I don't think we have a good way of handling this right now, this fundamentally ties in the fact that Promising is not good enough to properly handle error in presence of load-buffering. Happy to talk about it tomorrow.
3606975 to
fccc2c3
Compare
OpModel allows initialisation to fail GenPromise allows initialisation and promise emission to fail
fccc2c3 to
a29afe6
Compare
2 participants
OpModel allows initialisation to fail
GenPromise allows initialisation and promise emission to fail
This PR is part of a stack containing 3 PRs:
main