Support statements in ITE in hint functions

[katat]

In order to support the following calculation:

// 1 if true, 0 if false
function long_gt(n, k, a, b) {
    for (var i = k - 1; i >= 0; i--) {
        if (a[i] > b[i]) {
            return 1;
        }
        if (a[i] < b[i]) {
            return 0;
        }
    }
    return 0;
}

The compiler should support statements and early returns in the ITE block, otherwise it is too tricky to implement the logic like this. Perhaps at least we should enhance this feature in the hint functions.

[mimoo]

agree that in the hint functions we should allow anything (early return, early break, large if-then-else statements, etc.)

in the rest IMO we should not for now, as it would be hard to support other backends than r1cs

[0xnullifier]

@katat I see the pr that you raised was closed for some reason. Is this something not desired anymore? or is it just too difficult to implement atm? imho it will be a great feature and would love to work on this

[katat]

It can be tricky to support this on different arithmetic backends. Also there will be issues when calling builtin functions like assert(), which is not compatible with this kind of statement support.

However, it should be feasible to enhance the ITE in hint functions, which doesn't involve constraints.

[0xnullifier]

Got it so we can do this for hint functions atm. Can I take up this with #211 as they are kind of similar and make a single PR for both or maybe first do #211 and then come back to this?

[katat]

Yeah, cool! Let's ignore #211 for now, just focus on enhancing the ITE in hint functions.

[0xnullifier]

@katat a question
For only allowing if else in hint functions I would have to know when parsing the statement that whether it was in an hint function or not. So for example this is the sig of Stmt::parse

 pub fn parse(ctx: &mut ParserCtx, tokens: &mut Tokens) -> Result<Self> 

so do we change this to

pub fn parse(ctx: &mut ParserCtx, tokens: &mut Tokens, from_hint: bool) -> Result<Self>

or is there any way for me to get the context of body is from which function that I am parsing? I cannot reverse iterate over tokens as the iterator is already moved forward.
So do we add a field in ParserCtx indicating that if it was a hint function or not? or otherwise add a boolean field to FunctionDef::parse_fn_body , Stmt::parse

[0xnullifier]

Also there is a thing with returning early from the ite statements. I think we have to also drill down the function's return_type into parse_fn_body so that we can pass it into type_checker .

So what I was doing was something like this:

  StmtKind::Ite {
        condition,
        then_branch,
        else_branch,
       // add a  return_type  Option<Ty> here
  } => {
      //enter a new scope
      typed_fn_env.nest();
      let cond_type = self.compute_type(condition, typed_fn_env)?.unwrap();
      if !is_bool(&cond_type.typ) {
          return Err(self.error(
              ErrorKind::IfElseInvalidConditionType(cond_type.typ),
              condition.span,
          ));
      }

      typed_fn_env.start_ite();
      // check block and pass the expected return which should the return type of the hint function
      self.check_block(typed_fn_env, then_branch, expected_return, new_scope) // pass it down here
  }

or is there any other way for me to get the function scope that I am in and extract that function's return type

[katat]

or is there any way for me to get the context of body is from which function that I am parsing?

In parser phase, it would need to assume the ITE branches support statements.

When it comes to type check phase, it will know whether it is a hint function or not when computing the expression types. ITE can be checked and statements should be only allowed in hint functions.

About the idea of adding StmtKind::Ite

I think it makes sense to create a new statement kind for the ITE like that, as it would to type check the branch blocks in a way similar to function block.

After the parser phase, the FunctionDef will have is_hint to indicate whether it is a hint function or not. Indeed we need to figure out how to propagate this property in a way that can help differentiate the type checking rules among hint or constraint functions for ITE statement.

[0xnullifier]

In parser phase, it would need to assume the ITE branches support statements.

So we would parse ITE anyway and throw error at the type checker level

After the parser phase, the FunctionDef will have is_hint to indicate whether it is a hint function or not. Indeed we need to figure out how to propagate this property in a way that can help differentiate the type checking rules among hint or constraint functions for ITE statement.

Can we add this to the ParserCtx struct? cause to me that makes the most sense that the parser should have context of the function it is parsing. Like if we do something like

struct ParserCtx {
..
// bool indicates whether it is a hint function or not
pub fn_sig: Option<(FnSig,bool)> // stores the Fn signature for which the parser was called from this allows us to type check the ite 
// statement and see if the return type in the ite statements match the return type of fn_sig from the parser
}

or is there anything else we can do?
I think adding this to the ParserCtx will be useful when we are adding early return for other block type statement like for loops.

So here is what the flow is:

1. Whenever we call FunctionDef::parsewe mutate the context to add the fn_sig field. something like

const fn_sig = FnSig::parse(ctx,tokens)?;  // code in function def
ctx.fn_sig = Some((fn_sig,false) // from FunctionDef::parse 

ctx.fn_sig = Some((fn_sig,true)) // from FunctionDef::parse_hint

2. Now whenever we parse ITE statments we just get the fn_sig from the context and do the assertion of and then we change the Stmt::Ite to something like:

pub enum Stmt {
Ite {
  return_ty: Option<Ty> // if the put this in the stmt so we can type check at the checker
}

3. and with check_block function we pass the expected output type to return_ty from the ite.

[katat]

I am not sure I follow the idea of adding ParserCtx.

We already have the is_hint parsed and saved in FunctionDef. Can we just propagate this flag using the TypedFnEnv and use it to differentiate type check rules?

Or are there benefits of having ParserCtx instead of relying on TypedFnEnv to achieve that?

[0xnullifier]

We already have the is_hint parsed and saved in FunctionDef. Can we just propagate this flag using the TypedFnEnv and use it to differentiate type check rules?

Got it will move this logic to TypedFnEnv I also need to parse the return type of the function I am in for the early case of early return. So what I need in TypedFnEnv would be something like this:

struct TypedFnEnv {
..
return_and_is_hint: (Option<Ty> , bool)
}

Should I make two fields in the struct or one tuple?

Does this makes more sense now I agree that this better than mutating the parser ctx. Just set this value in the analyse function before calling the self.check_block

[0xnullifier]

hey @katat I have been stuck on how to do this at the IR level. The crate circify/circ that is used for ir I could not find support for ITE branches maybe it does not have one?

One thing I though was to convert the if-else blocks into if-else expression internally i.e turn the If-Else statements into term![Op::Ite; cond , inside_then_val , outside_then_val]? Can you give me a direction here? highly appreciated

[katat]

One thing I though was to convert the if-else blocks into if-else expression internally i.e turn the If-Else statements into term![Op::Ite; cond , inside_then_val , outside_then_val]?

I think you are going in the right direction.

Indeed the circ IR doesn't have the "term" to support branches directly. Instead we will need to compose the expressions in branches into two terms, one for the then branch and another for the else branch.

As we have already supported converting expressions or statements to the circ IR, I think what would be needed for enhancing the ITE statement is plugging its parsed branches AST into the existing compute_expr in the IR writer.

Let me know if this answers your question.

[0xnullifier]

As we have already supported converting expressions or statements to the circ IR, I think what would be needed for enhancing the ITE statement is plugging its parsed branches AST into the existing compute_expr in the IR writer

So should this be done at the parser/type checker level itself? Like converting if-else branches into if-else inline statments.
Say for this case:

hint fn ite(xx: Field , arr: [Field;LEN]) -> Field {
    let mut var = 0;
    if xx == 10 {
        var = xx;
        for idx in 0..LEN {
            var = var + arr[idx];
        }
        var = xx * var;
    } else {
        var = xx * xx;
    }
    return var;
}

How do handle loops, function calls etc?

[katat]

The ITE branches in hint function can support statements like a function blocks.

In the IR writer, it already supports converting the function block to an IR term or a list of IR terms. For example, when it tries to execute a hint function, it basically converts the MAST of that hint function into IR terms before computing its values.

So once the ITE branches are parsed as blocks, which may be comprised of statements, then converting the these branch blocks to the IR terms should be the same as the existing conversion logic in the existing IR writer.

I think these ITE branch blocks should be parsed in the parser phase, similar to how a for loop statement is parsed.

Currently the ITE is seen as an expression. We might need to change it to be a statement, which can contain branch blocks and get processed similar to for loop statement:

noname/src/circuit_writer/ir.rs

Lines 396 to 400 in bb87a88

	StmtKind::ForLoop {
	var,
	argument,
	body,
	} => {

[0xnullifier]

The ITE branches in hint function can support statements like a function blocks.

@katat This part is done and in the ir have somthing like:

StmtKind::Ite {
                condition,
                then_branch,
                else_branch,
            } => {
                fn_env.nest();
                let cond_var = self.compute_expr(fn_env, condition)?;
                let ret = self.compile_block(fn_env, then_branch)?;
                match else_branch {
                    Some(stmts) => {
                        //start another block
                        fn_env.nest();
                        self.compile_block(fn_env, stmts)?;
                        fn_env.pop();
                    }
                    None => (),
                }
                let var = ret.map(|var| VarOrRef::Var(var));
                return Ok(var);
            }

The code above is obvisouly wrong as there is no branching logic. Now what I am asking is how do I add this branching logic. As circify does not have logic of branching what can I do here?

[katat]

Here is the example on how to create circ term for branching:

noname/src/circuit_writer/ir.rs

Line 818 in bb87a88

let ite_ir = term![Op::Ite; cond, then_, else_];

The results of the compile_block, which the are the computed circ terms based on the statements and expressions, can be passed as _then and _else.

[0xnullifier]

Here is the example on how to create circ term for branching:

Yup but this support only if the if-else blocks have return not the general branching right? like how would I handle this case

let mut var = 0;
if xx == 10 {
var += xx * xx;
}  else {
var += xx
}

cause return of compile_block is None in this case

[katat]

Mmm, the term example I pointed to actually also support general branching. Each circ term can represent either a single field or a block of statements.

…

On Sat, Jan 25, 2025 at 5:23 PM Utkarsh Sharma ***@***.***> wrote: Here is the example on how to create circ term for branching: Yup but this support only if the if-else blocks have return not the general branching right? like how would I handle this case let mut var = 0;if xx == 10 { var += xx * xx;} else { var += xx} — Reply to this email directly, view it on GitHub <#248 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAMDRGHLHXLYKT7VPS5MMEL2MNJZTAVCNFSM6AAAAABUL3WNN6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDMMJTHA2TSNJYGE> . You are receiving this because you were mentioned.Message ID: ***@***.***>