zksecurity / noname

Noname: a programming language to write zkapps
https://zksecurity.github.io/noname/
188 stars 48 forks source link

make assert_eq generic, without introducing generics :o) #31

Open mimoo opened 6 months ago

mimoo commented 6 months ago

Right now the builtins are defined as embedded noname code. Here's assert_eq:

const ASSERT_EQ_FN: &str = "assert_eq(lhs: Field, rhs: Field)";

The string gets parsed by a fake mini-compiler that only does the lexer and parses the code expecting a function signature.

Then the implementation is given by some Rust code. The two are associated in some array:

pub const BUILTIN_FNS_DEFS: [(&str, FnHandle); 2] =
    [(ASSERT_EQ_FN, assert_eq), (ASSERT_FN, assert)];

fn assert_eq(compiler: &mut CircuitWriter, vars: &[VarInfo], span: Span) -> Result<Option<Var>> {
   // ...

I think the builtin code should be refactored to allow assert_eq(T, T) (as long as the types match, they should work! The Rust implementation of assert_eq can be made generic very easily, so there's probably not too much that's blocking us here.

I do not want to introduce generics in the noname language atm. So the builtins would have to be able to handle that instead.

mimoo commented 2 months ago

I think it'd be cool if any such builtin function would implement a trait, that would split the type checking from the circuit building phase (this would allow type checking to easily be generic!). It could look like this:

impl BuiltinFn for AssertEq {
  const SIGNATURE: Option<&str> = None; // the signatures don't allow us to do generic type checking yet, so we pass None
  fn type_check(args: &[VarInfo], span: Span) -> Result<()>;
  fn synthesize(compiler: &mut CircuitWriter, vars: &[VarInfo], span: Span) -> Result<Option<Var>>;
}