zkas
zkas is a compiler for the Halo2 zkVM language used in DarkFi.
The current implementation found in the DarkFi repository inside
src/zkas
is the reference compiler and language implementation. It is a
toolchain consisting of a lexer, parser, static and semantic analyzers,
and a binary code compiler.
The
main.rs
file shows how this toolchain is put together to produce binary code
from source code.
Architecture
The main part of the compilation happens inside the parser. New opcodes
can be added by extending
opcode.rs
.
// The lexer goes over the input file and separates its content into
// tokens that get fed into a parser.
let lexer = Lexer::new(filename, source.chars());
let tokens = match lexer.lex() {
Ok(v) => v,
Err(_) => return ExitCode::FAILURE,
};
// The parser goes over the tokens provided by the lexer and builds
// the initial AST, not caring much about the semantics, just enforcing
// syntax and general structure.
let parser = Parser::new(filename, source.chars(), tokens);
let (namespace, k, constants, witnesses, statements) = match parser.parse() {
Ok(v) => v,
Err(_) => return ExitCode::FAILURE,
};
// The analyzer goes through the initial AST provided by the parser and
// converts return and variable types to their correct forms, and also
// checks that the semantics of the ZK script are correct.
let mut analyzer = Analyzer::new(filename, source.chars(), constants, witnesses, statements);
if analyzer.analyze_types().is_err() {
return ExitCode::FAILURE
}
if iflag && analyzer.analyze_semantic().is_err() {
return ExitCode::FAILURE
}
if pflag {
println!("{:#?}", analyzer.constants);
println!("{:#?}", analyzer.witnesses);
println!("{:#?}", analyzer.statements);
println!("{:#?}", analyzer.heap);
return ExitCode::SUCCESS
}
let compiler = Compiler::new(
filename,
source.chars(),
namespace,
k,
analyzer.constants,
analyzer.witnesses,
analyzer.statements,
analyzer.literals,
!sflag,
);
let bincode = match compiler.compile() {
Ok(v) => v,
Err(_) => return ExitCode::FAILURE,
};