[codex] add guarded ReadersWriters reference app#219
Merged
rita-aga merged 2 commits intoMay 15, 2026
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds a Temper ReadersWriters reference app that faithfully mirrors the Quint transition relation through a small WASM transition module and guarded IOA callbacks.
What changed
reference-apps/readers-writerswith the IOA spec, CSDL model, Cedar policy, pure Rust transition logic, trace tests, validation tests, and WASM step module.wasm_in_flightguard to serialize public protocol actions while a WASM callback chain is open, preventing stale overlapping proposals from drifting detailed queue fields from projected counters.Impact
The reference app demonstrates ReadersWriters behavior under Temper verification: multiple readers can share the resource, writers wait for readers, readers wait for writers, and no reader/writer overlap is admitted. Concurrent public calls now get visible backpressure through the guard instead of racing detailed WASM-managed fields.
No HTML report files are included in this PR.
Validation
cargo fmt --all --checkcargo test -p readers-writers-referencecargo test -p temper-sandboxcargo build -p temper-cli