Skip to content

Quantifier free randomness mapping - #360

Draft
tornado80 wants to merge 4 commits into
mainfrom
amir/quantifier-free-randomness-mapping
Draft

Quantifier free randomness mapping #360
tornado80 wants to merge 4 commits into
mainfrom
amir/quantifier-free-randomness-mapping

Conversation

@tornado80

Copy link
Copy Markdown
Contributor

Closes #206 and #67

@tornado80
tornado80 requested a review from siccegge July 15, 2026 14:18
pub count: usize,
pub positions: Vec<Position>,
// maximum offset of each sampling operation for each exported oracle
pub max_offset: Option<HashMap<Export, HashMap<Position, usize>>>,

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

shouldn't this be HashMap<Export, usize> as we are already looking at a concrete sample position?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we have one SampleInfo for each game instance and not for each position. So the max_offset also computes the maximum possible counter for each sample position reachable from each exported oracle.

Comment thread src/transforms/samplify.rs
.unwrap_or_else(|ResolutionError(failed_oracle_stmts)| {
panic!("error resolving oracles: {failed_oracle_stmts:?}")
});
max_offset_extractor::Transformation(&comp, &mut samplinginfo).transform();

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

would it make more sense to fold this into samplify?

then you also can get rid of the Option

@tornado80 tornado80 Jul 21, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One issue is that max_offset_extractor needs to find all reachable sampling positions from an exported oracle so it needs oracle resolution. Samplify can be moved after oracle resolution. However, samplify and max_offset_extractor have different AST traversal order. Samplify linearly updates the code of oracles of all packages while max_offset_extractor DFS into each exported oracle. I think keeping them separate helps readability but we could move max_offset out of SampleInfo.

@siccegge

siccegge commented Jul 25, 2026

Copy link
Copy Markdown
Contributor

Ah one thing: it would be nice if we could keep the sample-infos in the order in which they appear in that export call. Then we can re-use the information also for a order-based randomness mapping!

I.e. instead of accumulating into a HashMap, collect into a Vec -- given that the number of entries is going to be small this might even be more efficient 🙃

@tornado80

Copy link
Copy Markdown
Contributor Author

Excellent point 👍

@tornado80

Copy link
Copy Markdown
Contributor Author
  • Group by types!
  • Assert equality of samplings instead of using rand-is-eq

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Define randomness mappings without quantifiers?

2 participants