use bare assumed bool conditionals in XMSS aggregation and recursion programs

Author: morganthomas

crates/lean_compiler/src/grammar.pest

@@ -42,7 +42,7 @@ if_statement = { "if" ~ condition ~ "{" ~ statement* ~ "}" ~ else_clause? }
 
 condition = { expression | assumed_bool_expr }
 
-assumed_bool_expr = { "!assume_bool" ~ "(" ~ expression ~ ")" }
+assumed_bool_expr = { "!!assume_bool" ~ "(" ~ expression ~ ")" }
 
 else_clause = { "else" ~ "{" ~ statement* ~ "}" }
 

crates/lean_compiler/src/parser/parsers/statement.rs

@@ -129,15 +129,16 @@ pub struct ConditionParser;
 
 impl Parse<Condition> for ConditionParser {
     fn parse(pair: ParsePair<'_>, ctx: &mut ParseContext) -> ParseResult<Condition> {
-        if pair.as_rule() == Rule::assumed_bool_expr {
+        let mut inner_pair = next_inner_pair(&mut pair.into_inner(), "inner expression")?;
+        if inner_pair.as_rule() == Rule::assumed_bool_expr {
             ExpressionParser::parse(
-                next_inner_pair(&mut pair.into_inner(), "inner expression")?,
+                next_inner_pair(&mut inner_pair.into_inner(), "inner expression")?,
                 ctx,
             )
             .map(|e| Condition::Expression(e, AssumeBoolean::AssumeBoolean))
         } else {
             let expr_result = ExpressionParser::parse(
-                next_inner_pair(&mut pair.into_inner(), "inner expression")?,
+                inner_pair,
                 ctx,
             );
             match expr_result {

crates/rec_aggregation/recursion_program.lean_lang

@@ -293,7 +293,7 @@ fn sample_stir_indexes_and_fold(fs_state, num_queries, merkle_leaves_in_basefiel
     fs_states_b[0] = fs_state_9;
 
     // the number of chunk of 8 field elements per merkle leaf opened
-    if merkle_leaves_in_basefield == 1 {
+    if !!assume_bool(merkle_leaves_in_basefield) {
         n_chuncks_per_answer = two_pow_folding_factor / 8; // "/ 8" because initial merkle leaves are in the basefield
     } else {
         n_chuncks_per_answer = two_pow_folding_factor * DIM / 8;
@@ -350,7 +350,7 @@ fn sample_stir_indexes_and_fold(fs_state, num_queries, merkle_leaves_in_basefiel
     fs_state_11 = fs_states_c[num_queries];
 
     folds = malloc(num_queries * DIM);
-    if merkle_leaves_in_basefield == 1 {
+    if !!assume_bool(merkle_leaves_in_basefield) {
         folding_randomness_alligned = malloc_vec(1, log2_ceil(DIM * FOLDING_FACTOR_0));
         folding_randomness_alligned_ptr = folding_randomness_alligned * (2 ** log2_ceil(DIM * FOLDING_FACTOR_0));
         for i in 0..FOLDING_FACTOR_0 unroll {

crates/rec_aggregation/src/xmss_aggregate.rs

@@ -43,7 +43,7 @@ pub fn run_xmss_benchmark(n_xmss: usize) -> XmssBenchStats {
         bitield = public_input_start + (2 + N_PUBLIC_KEYS) * 8;
         signatures_start = private_input_start / 8;
         for i in 0..N_PUBLIC_KEYS {
-            if bitield[i] == 1 {
+            if !!assume_bool(bitield[i]) {
                 xmss_public_key = all_public_keys + i;
 
                 sig_index = counter_hint();