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