Skip to content

Commit

Permalink
Do not store second branch condition. (#2397)
Browse files Browse the repository at this point in the history
  • Loading branch information
chriseth authored Jan 28, 2025
1 parent 3a42332 commit 8d89d80
Show file tree
Hide file tree
Showing 3 changed files with 22 additions and 17 deletions.
17 changes: 10 additions & 7 deletions executor/src/witgen/jit/compiler.rs
Original file line number Diff line number Diff line change
Expand Up @@ -409,9 +409,14 @@ fn format_expression<T: FieldElement>(e: &SymbolicExpression<T, Variable>) -> St
}
}

fn format_condition<T: FieldElement>(condition: &BranchCondition<T, Variable>) -> String {
let var = format!("IntType::from({})", variable_to_string(&condition.variable));
let (min, max) = condition.first_branch.range();
fn format_condition<T: FieldElement>(
BranchCondition {
variable,
condition,
}: &BranchCondition<T, Variable>,
) -> String {
let var = format!("IntType::from({})", variable_to_string(variable));
let (min, max) = condition.range();
match min.cmp(&max) {
Ordering::Equal => format!("{var} == {min}",),
Ordering::Less => format!("{min} <= {var} && {var} <= {max}"),
Expand Down Expand Up @@ -950,8 +955,7 @@ extern \"C\" fn witgen(
let effects = vec![Effect::Branch(
BranchCondition {
variable: x.clone(),
first_branch: RangeConstraint::from_range(7.into(), 20.into()),
second_branch: RangeConstraint::from_range(21.into(), 6.into()),
condition: RangeConstraint::from_range(7.into(), 20.into()),
},
vec![assignment(&y, symbol(&x) + number(1))],
vec![assignment(&y, symbol(&x) + number(2))],
Expand Down Expand Up @@ -997,8 +1001,7 @@ extern \"C\" fn witgen(
let branch_effect = Effect::Branch(
BranchCondition {
variable: x.clone(),
first_branch: RangeConstraint::from_range(7.into(), 20.into()),
second_branch: RangeConstraint::from_range(21.into(), 6.into()),
condition: RangeConstraint::from_range(7.into(), 20.into()),
},
vec![assignment(&y, symbol(&x) + number(1))],
vec![assignment(&y, symbol(&x) + number(2))],
Expand Down
19 changes: 11 additions & 8 deletions executor/src/witgen/jit/effect.rs
Original file line number Diff line number Diff line change
Expand Up @@ -109,8 +109,7 @@ impl<T: FieldElement, V> Assertion<T, V> {
#[derive(Clone, PartialEq, Eq)]
pub struct BranchCondition<T: FieldElement, V> {
pub variable: V,
pub first_branch: RangeConstraint<T>,
pub second_branch: RangeConstraint<T>,
pub condition: RangeConstraint<T>,
}

/// Helper function to render a list of effects. Used for informational purposes only.
Expand Down Expand Up @@ -156,12 +155,16 @@ pub fn format_code<T: FieldElement>(effects: &[Effect<T, Variable>]) -> String {
.join("\n")
}

fn format_condition<T: FieldElement>(condition: &BranchCondition<T, Variable>) -> String {
let var = &condition.variable;
let (min, max) = condition.first_branch.range();
fn format_condition<T: FieldElement>(
BranchCondition {
variable,
condition,
}: &BranchCondition<T, Variable>,
) -> String {
let (min, max) = condition.range();
match min.cmp(&max) {
Ordering::Equal => format!("{var} == {min}"),
Ordering::Less => format!("{min} <= {var} && {var} <= {max}"),
Ordering::Greater => format!("{var} <= {min} || {var} >= {max}"),
Ordering::Equal => format!("{variable} == {min}"),
Ordering::Less => format!("{min} <= {variable} && {variable} <= {max}"),
Ordering::Greater => format!("{variable} <= {min} || {variable} >= {max}"),
}
}
3 changes: 1 addition & 2 deletions executor/src/witgen/jit/witgen_inference.rs
Original file line number Diff line number Diff line change
Expand Up @@ -156,8 +156,7 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
common_code,
condition: BranchCondition {
variable: variable.clone(),
first_branch: high_condition,
second_branch: low_condition,
condition: high_condition,
},
branches: [self, low_branch],
}
Expand Down

0 comments on commit 8d89d80

Please sign in to comment.