Move assumption/assertion generation to its own pass #496
Conversation
This file contains 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
|
@rachitnigam There is some finicky stuff here caused by the fact that |
rachitnigam
reviewed
Mar 20, 2025
| pub type PortInfo = | ||
| (/*lens=*/ Vec<usize>, /*gen_ports=*/ Vec<PortIdx>); | ||
| /// A mapping from a bundle with a list of dimensions to the list of generated ports. | ||
| type PortInfo = (/*lens=*/ Vec<usize>, /*gen_ports=*/ Vec<PortIdx>); |
There was a problem hiding this comment.
If we're extracting these into separate types, might as well give the fields real names?
rachitnigam
reviewed
Mar 20, 2025
| @@ -4,9 +4,9 @@ use fil_ir::{self as ir, AddCtx, Ctx, ExprIdx, PropIdx}; | |||
|
|
|||
| /// Generates default assumptions to the Filament program for assumptions using custom functions | |||
| #[derive(Default)] | |||
| pub struct Assume; | |||
| pub struct FunAssumptions; | |||
There was a problem hiding this comment.
Nit: I don't love the name. Can we use something like InferAssumes which implies some relationship between existing assumptions and created ones?
rachitnigam
reviewed
Mar 20, 2025
| Time, TimeIdx, TimeSub, | ||
| }; | ||
|
|
||
| impl<C> Foreign<Expr, C> |
There was a problem hiding this comment.
What is this exactly used for and can we give this a better name/trait wrapper?
rachitnigam
approved these changes
Mar 20, 2025
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.
This PR divests core assumption/assertion generation (about event constraints, param constraints, and range constraints) from astconv. This cleans up astconv a bit and also adds the important ability for the IR to generate its own assertions necessary for discharging. This will be useful in scheduling and is also necessary if we want to be able to discharge after monomorphization properly.