From f00d976a36fa6235cc0cca322348b9d0fff5c210 Mon Sep 17 00:00:00 2001 From: Andrei Kashin Date: Mon, 11 Dec 2023 15:15:49 +0000 Subject: [PATCH] Add support for WASM Global Variables --- cranelift/codegen/src/isa/zkasm/inst.isle | 15 + cranelift/codegen/src/isa/zkasm/inst/args.rs | 15 +- cranelift/codegen/src/isa/zkasm/inst/emit.rs | 12 + cranelift/codegen/src/isa/zkasm/lower.isle | 4 +- cranelift/codegen/src/isa/zkasm/lower/isle.rs | 20 + cranelift/filetests/src/test_zkasm.rs | 41 +- cranelift/wasm/src/environ/zkasm.rs | 11 +- .../fibonacci/generated/from_rust.zkasm | 6 + .../sha256/generated/from_rust.zkasm | 392 +++++++++--------- cranelift/zkasm_data/generated/global.zkasm | 33 ++ cranelift/zkasm_data/global.wat | 12 + cranelift/zkasm_data/state.csv | 1 + docs/zkasm/test_summary.csv | 2 +- 13 files changed, 359 insertions(+), 205 deletions(-) create mode 100644 cranelift/zkasm_data/generated/global.zkasm create mode 100644 cranelift/zkasm_data/global.wat diff --git a/cranelift/codegen/src/isa/zkasm/inst.isle b/cranelift/codegen/src/isa/zkasm/inst.isle index 209136a282d9..54b94c8f91dd 100644 --- a/cranelift/codegen/src/isa/zkasm/inst.isle +++ b/cranelift/codegen/src/isa/zkasm/inst.isle @@ -327,6 +327,11 @@ (Fsd) )) +(type ZkasmBase (enum + (Heap) + (Global) +)) + (type AluOPRRR (enum ;; base set (Add) @@ -1176,6 +1181,10 @@ (decl gen_fp_offset_amode (i64 Type) AMode) (extern constructor gen_fp_offset_amode gen_fp_offset_amode) +;; Generates a AMode that an access to a global variable at given index. +(decl gen_global_amode (i64 Type) AMode) +(extern constructor gen_global_amode gen_global_amode) + ;; Generates an AMode that points to a stack slot + offset. (decl gen_stack_slot_amode (StackSlot i64 Type) AMode) (extern constructor gen_stack_slot_amode gen_stack_slot_amode) @@ -1216,6 +1225,9 @@ (rule 1 (amode_inner (get_stack_pointer) offset ty) (gen_sp_offset_amode offset ty)) +(rule 1 (amode_inner (symbol_value (zkasm_base ZkasmBase.Global)) index ty) + (gen_global_amode index ty)) + ;; Similarly if the value is a `stack_addr` we can also turn that into an sp offset. (rule 1 (amode_inner (stack_addr ss ss_offset) amode_offset ty) (if-let combined_offset (s32_add_fallible ss_offset amode_offset)) @@ -1302,6 +1314,9 @@ (decl store_op (Type) StoreOP) (extern constructor store_op store_op) +(decl zkasm_base (ZkasmBase) GlobalValue) +(extern extractor zkasm_base zkasm_base) + ;;;; load extern name (decl load_ext_name (ExternalName i64) Reg) (extern constructor load_ext_name load_ext_name) diff --git a/cranelift/codegen/src/isa/zkasm/inst/args.rs b/cranelift/codegen/src/isa/zkasm/inst/args.rs index 056fe1e95515..51895e508c74 100644 --- a/cranelift/codegen/src/isa/zkasm/inst/args.rs +++ b/cranelift/codegen/src/isa/zkasm/inst/args.rs @@ -107,6 +107,9 @@ pub enum AMode { /// A reference to a label. Label(MachLabel), + + /// Access to a global variable. + Global(i64, Type), } impl AMode { @@ -117,7 +120,8 @@ impl AMode { | AMode::FPOffset(..) | AMode::NominalSPOffset(..) | AMode::Const(..) - | AMode::Label(..) => self, + | AMode::Label(..) + | AMode::Global(..) => self, } } @@ -130,7 +134,8 @@ impl AMode { | AMode::FPOffset(..) | AMode::NominalSPOffset(..) | AMode::Const(..) - | AMode::Label(..) => None, + | AMode::Label(..) + | AMode::Global(..) => None, } } @@ -140,7 +145,7 @@ impl AMode { &AMode::SPOffset(..) => Some(stack_reg()), &AMode::FPOffset(..) => Some(fp_reg()), &AMode::NominalSPOffset(..) => Some(stack_reg()), - &AMode::Const(..) | AMode::Label(..) => None, + &AMode::Const(..) | AMode::Label(..) | AMode::Global(..) => None, } } @@ -158,6 +163,7 @@ impl AMode { &AMode::FPOffset(offset, _) => offset, &AMode::NominalSPOffset(offset, _) => offset, &AMode::Const(_) | &AMode::Label(_) => 0, + &AMode::Global(offset, _) => offset, } } @@ -187,6 +193,9 @@ impl Display for AMode { &AMode::Label(label) => { write!(f, "[label{}]", label.as_u32()) } + &AMode::Global(offset, ..) => { + write!(f, "{}(global)", offset) + } } } } diff --git a/cranelift/codegen/src/isa/zkasm/inst/emit.rs b/cranelift/codegen/src/isa/zkasm/inst/emit.rs index 476024aeb341..ba59ae102e4a 100644 --- a/cranelift/codegen/src/isa/zkasm/inst/emit.rs +++ b/cranelift/codegen/src/isa/zkasm/inst/emit.rs @@ -622,6 +622,12 @@ impl MachInstEmit for Inst { } AMode::Const(_) => unimplemented!("Load, AMode::Const"), AMode::Label(_) => unimplemented!("Load, AMode::Label"), + AMode::Global(index, _) => { + put_string( + &format!("$ => {} :MLOAD(global_{})\n", reg_name(rd.to_reg()), index), + sink, + ); + } }; } &Inst::Store { op, src, flags, to } => { @@ -662,6 +668,12 @@ impl MachInstEmit for Inst { } AMode::Const(_) => unimplemented!("Store, AMode::Const"), AMode::Label(_) => unimplemented!("Store, AMode::Label"), + AMode::Global(index, _) => { + put_string( + &format!("{} :MSTORE(global_{})\n", reg_name(src), index), + sink, + ); + } }; } &Inst::Args { .. } => { diff --git a/cranelift/codegen/src/isa/zkasm/lower.isle b/cranelift/codegen/src/isa/zkasm/lower.isle index 09db2a8ba993..41ebfef233f8 100644 --- a/cranelift/codegen/src/isa/zkasm/lower.isle +++ b/cranelift/codegen/src/isa/zkasm/lower.isle @@ -355,8 +355,8 @@ ;;;;; Rules for `symbol_value`;;;;;;;;; (rule (lower (symbol_value (symbol_value_data name _ offset))) - (load_ext_name name offset) -) + (load_ext_name name offset)) + ;;;;; Rules for `bitcast`;;;;;;;;; (rule (lower (has_type out_ty (bitcast _ v @ (value_type in_ty)))) diff --git a/cranelift/codegen/src/isa/zkasm/lower/isle.rs b/cranelift/codegen/src/isa/zkasm/lower/isle.rs index 8b29bfb86523..77039081a207 100644 --- a/cranelift/codegen/src/isa/zkasm/lower/isle.rs +++ b/cranelift/codegen/src/isa/zkasm/lower/isle.rs @@ -3,6 +3,7 @@ // Pull in the ISLE generated code. #[allow(unused)] pub mod generated_code; +use cranelift_entity::EntityRef; use generated_code::{Context, ExtendOp, MInst}; // Types that the generated ISLE code uses via `use super::*`. @@ -351,6 +352,10 @@ impl generated_code::Context for ZkAsmIsleContext<'_, '_, MInst, ZkAsmBackend> { AMode::Const(c) } + fn gen_global_amode(&mut self, offset: i64, ty: Type) -> AMode { + AMode::Global(offset, ty) + } + fn valid_atomic_transaction(&mut self, ty: Type) -> Option { if ty.is_int() && ty.bits() <= 64 { Some(ty) @@ -364,6 +369,21 @@ impl generated_code::Context for ZkAsmIsleContext<'_, '_, MInst, ZkAsmBackend> { fn store_op(&mut self, ty: Type) -> StoreOP { StoreOP::from_type(ty) } + + fn zkasm_base(&mut self, global_value: GlobalValue) -> Option { + if let Some((name, _, _)) = self.symbol_value_data(global_value) { + match name { + ExternalName::User(user_name_ref) => { + if user_name_ref.index() == 0 { + return Some(generated_code::ZkasmBase::Global); + } + } + _ => {} + } + } + None + } + fn load_ext_name(&mut self, name: ExternalName, offset: i64) -> Reg { let tmp = self.temp_writable_reg(I64); self.emit(&MInst::LoadExtName { diff --git a/cranelift/filetests/src/test_zkasm.rs b/cranelift/filetests/src/test_zkasm.rs index b468a7d226ff..81ac0a0c4e55 100644 --- a/cranelift/filetests/src/test_zkasm.rs +++ b/cranelift/filetests/src/test_zkasm.rs @@ -18,9 +18,41 @@ mod tests { let _ = env_logger::builder().is_test(true).try_init(); } - fn generate_preamble(start_func_index: usize) -> Vec { + fn generate_preamble( + start_func_index: usize, + globals: &[(cranelift_wasm::GlobalIndex, cranelift_wasm::GlobalInit)], + ) -> Vec { let mut program: Vec = Vec::new(); + + // Generate global variable definitions. + for (key, _) in globals { + program.push(format!("VAR GLOBAL global_{}", key.index())); + } + program.push("start:".to_string()); + for (key, init) in globals { + match init { + cranelift_wasm::GlobalInit::I32Const(v) => { + // ZKASM stores constants in 2-complement form, so we need a cast to unsigned. + program.push(format!( + " {} :MSTORE(global_{}) ;; Global32({})", + *v as u32, + key.index(), + v + )); + } + cranelift_wasm::GlobalInit::I64Const(v) => { + // ZKASM stores constants in 2-complement form, so we need a cast to unsigned. + program.push(format!( + " {} :MSTORE(global_{}) ;; Global64({})", + *v as u64, + key.index(), + v + )); + } + _ => unimplemented!("Global type is not supported"), + } + } program.push(" zkPC + 2 => RR".to_string()); program.push(format!(" :JMP(function_{})", start_func_index)); program.push(" :JMP(finalizeExecution)".to_string()); @@ -146,12 +178,16 @@ mod tests { translate_module(wasm_module, &mut zkasm_environ).unwrap(); let mut program: Vec = Vec::new(); + let start_func = zkasm_environ .info .start_func .expect("Must have a start function"); // TODO: Preamble should be generated by a linker and/or clift itself. - program.append(&mut generate_preamble(start_func.index())); + program.append(&mut generate_preamble( + start_func.index(), + &zkasm_environ.info.global_inits, + )); let num_func_imports = zkasm_environ.get_num_func_imports(); let mut context = cranelift_codegen::Context::new(); @@ -321,6 +357,7 @@ mod tests { add, locals, locals_simple, + global, memory, counter, add_func, diff --git a/cranelift/wasm/src/environ/zkasm.rs b/cranelift/wasm/src/environ/zkasm.rs index 07d433ce9d45..e908c0e8b122 100644 --- a/cranelift/wasm/src/environ/zkasm.rs +++ b/cranelift/wasm/src/environ/zkasm.rs @@ -82,6 +82,9 @@ pub struct ZkasmModuleInfo { /// Globals as provided by `declare_global`. pub globals: PrimaryMap>, + /// Inits for globals when available. + pub global_inits: Vec<(GlobalIndex, GlobalInit)>, + /// The start function. pub start_func: Option, } @@ -101,6 +104,7 @@ impl ZkasmModuleInfo { tables: PrimaryMap::new(), memories: PrimaryMap::new(), globals: PrimaryMap::new(), + global_inits: Vec::new(), start_func: None, } } @@ -312,7 +316,7 @@ impl<'zkasm_environment> FuncEnvironment for ZkasmFuncEnvironment<'zkasm_environ func: &mut ir::Function, index: GlobalIndex, ) -> WasmResult { - let offset = i32::try_from((index.index() * 8) + 8).unwrap().into(); + let offset = i32::try_from(index.index()).unwrap().into(); Ok(GlobalVariable::Memory { gv: ZkasmFuncEnvironment::globals_base(func), offset, @@ -770,8 +774,9 @@ impl<'data> ModuleEnvironment<'data> for ZkasmEnvironment { Ok(()) } - fn declare_global(&mut self, global: Global, _init: GlobalInit) -> WasmResult<()> { - self.info.globals.push(Exportable::new(global)); + fn declare_global(&mut self, global: Global, init: GlobalInit) -> WasmResult<()> { + let index = self.info.globals.push(Exportable::new(global)); + self.info.global_inits.push((index, init)); Ok(()) } diff --git a/cranelift/zkasm_data/benchmarks/fibonacci/generated/from_rust.zkasm b/cranelift/zkasm_data/benchmarks/fibonacci/generated/from_rust.zkasm index da622ffefc80..01406ad40e12 100644 --- a/cranelift/zkasm_data/benchmarks/fibonacci/generated/from_rust.zkasm +++ b/cranelift/zkasm_data/benchmarks/fibonacci/generated/from_rust.zkasm @@ -1,4 +1,10 @@ +VAR GLOBAL global_0 +VAR GLOBAL global_1 +VAR GLOBAL global_2 start: + 1048576 :MSTORE(global_0) ;; Global32(1048576) + 1048576 :MSTORE(global_1) ;; Global32(1048576) + 1048576 :MSTORE(global_2) ;; Global32(1048576) zkPC + 2 => RR :JMP(function_1) :JMP(finalizeExecution) diff --git a/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm b/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm index f8d901cc415c..7e606cefb836 100644 --- a/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm +++ b/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm @@ -1,4 +1,10 @@ +VAR GLOBAL global_0 +VAR GLOBAL global_1 +VAR GLOBAL global_2 start: + 1048576 :MSTORE(global_0) ;; Global32(1048576) + 1048619 :MSTORE(global_1) ;; Global32(1048619) + 1048624 :MSTORE(global_2) ;; Global32(1048624) zkPC + 2 => RR :JMP(function_1) :JMP(finalizeExecution) @@ -10,33 +16,31 @@ function_1: D :MSTORE(SP - 2) E :MSTORE(SP - 3) B :MSTORE(SP - 4) - 65536 => E ;; LoadExtName(User(userextname0)) - $ => A :MLOAD(MEM:E + 8) + $ => A :MLOAD(global_0) 240n => B ;; LoadConst32 $ => A :SUB 4294967295n => B ;; LoadConst64 $ => A :AND A :MSTORE(SP + 88) - 65536 => E ;; LoadExtName(User(userextname0)) - A :MSTORE(MEM:E + 8) + A :MSTORE(global_0) 8n => B ;; LoadConst32 - $ => B :ADD - B => A + $ => D :ADD + D => A 4294967295n => B ;; LoadConst64 $ => A :AND 8n => B ;; LoadConst32 $ => A :ADD 4294967295n => B ;; LoadConst64 $ => B :AND - 0n => D ;; LoadConst64 + 0n => C ;; LoadConst64 0 => A ;; LoadExtName(User(userextname1)) $ => E :ADD - B :MSTORE(SP + 16) - D :MSTORE(MEM:E) + B :MSTORE(SP + 8) + C :MSTORE(MEM:E) 8n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => C :ADD - C => A + $ => E :ADD + E => A 4294967295n => B ;; LoadConst64 $ => A :AND 16n => B ;; LoadConst32 @@ -46,12 +50,12 @@ function_1: 0n => C ;; LoadConst64 0 => A ;; LoadExtName(User(userextname1)) $ => E :ADD - B :MSTORE(SP + 8) + B :MSTORE(SP) C :MSTORE(MEM:E) 8n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => D :ADD - D => A + $ => B :ADD + B => A 4294967295n => B ;; LoadConst64 $ => A :AND 24n => B ;; LoadConst32 @@ -61,45 +65,45 @@ function_1: 0n => C ;; LoadConst64 0 => A ;; LoadExtName(User(userextname1)) $ => E :ADD - B :MSTORE(SP) + B :MSTORE(SP + 80) C :MSTORE(MEM:E) 40n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => E :ADD - E => A + $ => B :ADD + B => A 4294967295n => B ;; LoadConst64 $ => B :AND - B :MSTORE(SP + 80) - 0n => C ;; LoadConst64 + B :MSTORE(SP + 72) + 0n => D ;; LoadConst64 0 => A ;; LoadExtName(User(userextname1)) $ => E :ADD - C :MSTORE(MEM:E) + D :MSTORE(MEM:E) 8n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => B :ADD - B => A + $ => C :ADD + C => A 4294967295n => B ;; LoadConst64 $ => A :AND 40n => B ;; LoadConst32 $ => A :ADD 4294967295n => B ;; LoadConst64 $ => B :AND - B :MSTORE(SP + 72) + B :MSTORE(SP + 64) 0n => C ;; LoadConst64 0 => A ;; LoadExtName(User(userextname1)) $ => E :ADD C :MSTORE(MEM:E) 53n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => B :ADD - B => A + $ => D :ADD + D => A 4294967295n => B ;; LoadConst64 $ => B :AND - B :MSTORE(SP + 64) - 0n => D ;; LoadConst64 + B :MSTORE(SP + 56) + 0n => C ;; LoadConst64 0 => A ;; LoadExtName(User(userextname1)) $ => E :ADD - D :MSTORE(MEM:E) + C :MSTORE(MEM:E) 0n => C ;; LoadConst64 0 => A ;; LoadExtName(User(userextname1)) $ => B :MLOAD(SP + 88) @@ -107,8 +111,8 @@ function_1: C :MSTORE(MEM:E + 8) 64n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => D :ADD - D => A + $ => B :ADD + B => A 4294967295n => B ;; LoadConst64 $ => A :AND 24n => B ;; LoadConst32 @@ -126,27 +130,27 @@ function_1: C :MSTORE(MEM:E) 64n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => E :ADD - E => A + $ => B :ADD + B => A 4294967295n => B ;; LoadConst64 $ => A :AND 16n => B ;; LoadConst32 $ => A :ADD 4294967295n => B ;; LoadConst64 $ => B :AND - B => D + B => C 0n => B ;; LoadConst32 0 => A ;; LoadExtName(User(userextname1)) $ => E :ADD - $ => C :MLOAD(MEM:E + 1048592) + $ => D :MLOAD(MEM:E + 1048592) 0 => A ;; LoadExtName(User(userextname1)) - D => B + C => B $ => E :ADD - C :MSTORE(MEM:E) + D :MSTORE(MEM:E) 64n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => B :ADD - B => A + $ => C :ADD + C => A 4294967295n => B ;; LoadConst64 $ => A :AND 8n => B ;; LoadConst32 @@ -164,19 +168,19 @@ function_1: C :MSTORE(MEM:E) 111n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => B :ADD - B => A + $ => D :ADD + D => A 4294967295n => B ;; LoadConst64 $ => B :AND - B => C + B => D 0n => B ;; LoadConst32 0 => A ;; LoadExtName(User(userextname1)) $ => E :ADD - $ => D :MLOAD(MEM:E + 1048615) + $ => C :MLOAD(MEM:E + 1048615) 0 => A ;; LoadExtName(User(userextname1)) - C => B + D => B $ => E :ADD - D :MSTORE(MEM:E) + C :MSTORE(MEM:E) 0n => B ;; LoadConst32 0 => A ;; LoadExtName(User(userextname1)) $ => E :ADD @@ -192,50 +196,50 @@ function_1: 0n => B ;; LoadConst32 0 => A ;; LoadExtName(User(userextname1)) $ => E :ADD - $ => C :MLOAD(MEM:E + 1048608) + $ => D :MLOAD(MEM:E + 1048608) 0 => A ;; LoadExtName(User(userextname1)) $ => B :MLOAD(SP + 88) $ => E :ADD - C :MSTORE(MEM:E + 104) + D :MSTORE(MEM:E + 104) 115n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => B :ADD - B => A + $ => C :ADD + C => A 4294967295n => B ;; LoadConst64 $ => B :AND - B :MSTORE(SP + 56) + B :MSTORE(SP + 48) 0 => A ;; LoadExtName(User(userextname1)) $ => B :MLOAD(SP + 88) $ => E :ADD $ => C :MLOAD(MEM:E + 8) 0 => A ;; LoadExtName(User(userextname1)) - $ => B :MLOAD(SP + 56) + $ => B :MLOAD(SP + 48) $ => E :ADD C :MSTORE(MEM:E) 123n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => B :ADD - B => A + $ => D :ADD + D => A 4294967295n => B ;; LoadConst64 $ => B :AND - B => C + B => D 0 => A ;; LoadExtName(User(userextname1)) - $ => B :MLOAD(SP + 16) + $ => B :MLOAD(SP + 8) $ => E :ADD - $ => D :MLOAD(MEM:E) + $ => C :MLOAD(MEM:E) 0 => A ;; LoadExtName(User(userextname1)) - C => B + D => B $ => E :ADD - D :MSTORE(MEM:E) + C :MSTORE(MEM:E) 131n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => C :ADD - C => A + $ => E :ADD + E => A 4294967295n => B ;; LoadConst64 $ => B :AND B => D 0 => A ;; LoadExtName(User(userextname1)) - $ => B :MLOAD(SP + 8) + $ => B :MLOAD(SP) $ => E :ADD $ => C :MLOAD(MEM:E) 0 => A ;; LoadExtName(User(userextname1)) @@ -244,13 +248,13 @@ function_1: C :MSTORE(MEM:E) 139n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => D :ADD - D => A + $ => B :ADD + B => A 4294967295n => B ;; LoadConst64 $ => B :AND B => D 0 => A ;; LoadExtName(User(userextname1)) - $ => B :MLOAD(SP) + $ => B :MLOAD(SP + 80) $ => E :ADD $ => C :MLOAD(MEM:E) 0 => A ;; LoadExtName(User(userextname1)) @@ -259,28 +263,28 @@ function_1: C :MSTORE(MEM:E) 147n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => E :ADD - E => A + $ => B :ADD + B => A 4294967295n => B ;; LoadConst64 $ => B :AND - B => D + B => C 0 => A ;; LoadExtName(User(userextname1)) - $ => B :MLOAD(SP + 80) + $ => B :MLOAD(SP + 72) $ => E :ADD - $ => C :MLOAD(MEM:E) + $ => D :MLOAD(MEM:E) 0 => A ;; LoadExtName(User(userextname1)) - D => B + C => B $ => E :ADD - C :MSTORE(MEM:E) + D :MSTORE(MEM:E) 155n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => B :ADD - B => A + $ => C :ADD + C => A 4294967295n => B ;; LoadConst64 $ => B :AND B => D 0 => A ;; LoadExtName(User(userextname1)) - $ => B :MLOAD(SP + 72) + $ => B :MLOAD(SP + 64) $ => E :ADD $ => C :MLOAD(MEM:E) 0 => A ;; LoadExtName(User(userextname1)) @@ -289,19 +293,19 @@ function_1: C :MSTORE(MEM:E) 160n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => B :ADD - B => A + $ => D :ADD + D => A 4294967295n => B ;; LoadConst64 $ => B :AND - B => C + B => D 0 => A ;; LoadExtName(User(userextname1)) - $ => B :MLOAD(SP + 64) + $ => B :MLOAD(SP + 56) $ => E :ADD - $ => D :MLOAD(MEM:E) + $ => C :MLOAD(MEM:E) 0 => A ;; LoadExtName(User(userextname1)) - C => B + D => B $ => E :ADD - D :MSTORE(MEM:E) + C :MSTORE(MEM:E) 11n => C ;; LoadConst32 0 => A ;; LoadExtName(User(userextname1)) $ => B :MLOAD(SP + 88) @@ -309,34 +313,35 @@ function_1: C :MSTORE(MEM:E + 168) 172n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => D :ADD - D => A + $ => B :ADD + B => A 4294967295n => B ;; LoadConst64 $ => B :AND - B :MSTORE(SP + 48) + B => D 4n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => D :ADD - D => A + $ => B :ADD + B => A 4294967295n => B ;; LoadConst64 $ => B :AND 0 => A ;; LoadExtName(User(userextname1)) $ => E :ADD $ => C :MLOAD(MEM:E) 0 => A ;; LoadExtName(User(userextname1)) - $ => B :MLOAD(SP + 48) + D => B $ => E :ADD C :MSTORE(MEM:E) 0 => A ;; LoadExtName(User(userextname1)) $ => B :MLOAD(SP + 88) $ => E :ADD - $ => C :MLOAD(MEM:E + 1) + $ => D :MLOAD(MEM:E + 1) 0 => A ;; LoadExtName(User(userextname1)) + $ => B :MLOAD(SP + 88) $ => E :ADD - C :MSTORE(MEM:E + 169) + D :MSTORE(MEM:E + 169) 128n => C ;; LoadConst32 0 => A ;; LoadExtName(User(userextname1)) - $ => B :MLOAD(SP + 56) + $ => B :MLOAD(SP + 48) $ => E :ADD C :MSTORE(MEM:E) 0 => A ;; LoadExtName(User(userextname1)) @@ -362,8 +367,8 @@ function_1: D :MSTORE(SP + 32) 65024n => B ;; LoadConst64 $ => A :MLOAD(SP + 32) - $ => D :AND - D => C + $ => B :AND + B => C 40n => A ;; LoadConst64 63n => B ;; LoadConst64 $ => E :AND @@ -378,8 +383,8 @@ function_1: E :MSTORE(SP + 24) 16711680n => B ;; LoadConst64 $ => A :MLOAD(SP + 32) - $ => D :AND - D => C + $ => B :AND + B => C 24n => A ;; LoadConst64 63n => B ;; LoadConst64 $ => E :AND @@ -482,8 +487,8 @@ function_1: A => E 64n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => B :ADD - B => A + $ => D :ADD + D => A 4294967295n => B ;; LoadConst64 $ => A :AND 40n => B ;; LoadConst32 @@ -491,8 +496,8 @@ function_1: 4294967295n => B ;; LoadConst64 $ => B :AND B :MSTORE(SP) - 0n => D ;; LoadConst32 - D => B + 0n => A ;; LoadConst32 + A => B 0 => A $ => A :EQ A :JMPZ(label_1_1) @@ -520,8 +525,8 @@ label_1_2: label_1_3: 6341068275337658368n => B ;; LoadConst64 E => A - $ => C :OR - C :MSTORE(SP + 80) + $ => D :OR + D :MSTORE(SP + 80) 11n => A ;; LoadConst32 56n => B ;; LoadConst32 $ => A :XOR @@ -533,23 +538,23 @@ label_1_3: A :JMPZ(label_1_5) 160n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => B :ADD - B => A + $ => C :ADD + C => A 4294967295n => B ;; LoadConst64 $ => B :AND 0 => A ;; LoadExtName(User(userextname1)) $ => E :ADD - $ => C :MLOAD(SP + 80) - C :MSTORE(MEM:E) + $ => D :MLOAD(SP + 80) + D :MSTORE(MEM:E) 64n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => B :ADD - B => A + $ => D :ADD + D => A 4294967295n => B ;; LoadConst64 $ => A :AND - 1n => D ;; LoadConst32 + 1n => B ;; LoadConst32 SP + 1 => SP - D :MSTORE(SP) + B :MSTORE(SP) $ => B :MLOAD(SP) zkPC + 2 => RR :JMP(function_2) @@ -558,8 +563,8 @@ label_1_3: label_1_5: 64n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => D :ADD - D => A + $ => B :ADD + B => A 4294967295n => B ;; LoadConst64 $ => A :AND 1n => C ;; LoadConst32 @@ -571,18 +576,18 @@ label_1_5: SP - 1 => SP 224n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => E :ADD - E => A + $ => B :ADD + B => A 4294967295n => B ;; LoadConst64 $ => B :AND - 0n => C ;; LoadConst64 + 0n => D ;; LoadConst64 0 => A ;; LoadExtName(User(userextname1)) $ => E :ADD - C :MSTORE(MEM:E) + D :MSTORE(MEM:E) 216n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => B :ADD - B => A + $ => C :ADD + C => A 4294967295n => B ;; LoadConst64 $ => B :AND 0n => C ;; LoadConst64 @@ -591,18 +596,18 @@ label_1_5: C :MSTORE(MEM:E) 208n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => B :ADD - B => A + $ => D :ADD + D => A 4294967295n => B ;; LoadConst64 $ => B :AND - 0n => D ;; LoadConst64 + 0n => C ;; LoadConst64 0 => A ;; LoadExtName(User(userextname1)) $ => E :ADD - D :MSTORE(MEM:E) + C :MSTORE(MEM:E) 200n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => C :ADD - C => A + $ => E :ADD + E => A 4294967295n => B ;; LoadConst64 $ => B :AND 0n => C ;; LoadConst64 @@ -611,8 +616,8 @@ label_1_5: C :MSTORE(MEM:E) 192n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => D :ADD - D => A + $ => B :ADD + B => A 4294967295n => B ;; LoadConst64 $ => B :AND 0n => C ;; LoadConst64 @@ -621,14 +626,14 @@ label_1_5: C :MSTORE(MEM:E) 184n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => E :ADD - E => A + $ => B :ADD + B => A 4294967295n => B ;; LoadConst64 $ => B :AND - 0n => C ;; LoadConst64 + 0n => D ;; LoadConst64 0 => A ;; LoadExtName(User(userextname1)) $ => E :ADD - C :MSTORE(MEM:E) + D :MSTORE(MEM:E) 0n => C ;; LoadConst64 0 => A ;; LoadExtName(User(userextname1)) $ => B :MLOAD(SP + 88) @@ -636,24 +641,24 @@ label_1_5: C :MSTORE(MEM:E + 176) 0 => A ;; LoadExtName(User(userextname1)) $ => E :ADD - $ => C :MLOAD(SP + 80) - C :MSTORE(MEM:E + 232) + $ => D :MLOAD(SP + 80) + D :MSTORE(MEM:E + 232) 64n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => C :ADD - C => A + $ => E :ADD + E => A 4294967295n => B ;; LoadConst64 $ => A :AND A => D 176n => B ;; LoadConst32 $ => A :MLOAD(SP + 88) - $ => C :ADD - C => A + $ => E :ADD + E => A 4294967295n => B ;; LoadConst64 $ => B :AND - 1n => E ;; LoadConst32 + 1n => C ;; LoadConst32 SP + 1 => SP - E :MSTORE(SP) + C :MSTORE(SP) D => A zkPC + 2 => RR :JMP(function_2) @@ -706,8 +711,8 @@ label_1_6: A :MSTORE(SP + 16) 65280n => B ;; LoadConst32 $ => A :MLOAD(SP + 32) - $ => B :AND - B => C + $ => D :AND + D => C 8n => A ;; LoadConst32 31n => B ;; LoadConst64 $ => E :AND @@ -758,15 +763,14 @@ label_1_6: 4294967295n => B ;; LoadConst64 $ => B :AND $ => A :MLOAD(SP + 24) - $ => C :OR + $ => D :OR $ => A :MLOAD(SP) - C => D B => C D => B $ => A :OR 65280n => B ;; LoadConst32 - $ => B :AND - B :MSTORE(SP + 16) + $ => D :AND + D :MSTORE(SP + 16) A :MSTORE(SP + 24) 16n => A ;; LoadConst32 31n => B ;; LoadConst64 @@ -837,11 +841,11 @@ label_1_6: E :ARITH 4294967295n => B ;; LoadConst64 $ => A :AND - A => C + A => D 16n => A ;; LoadConst32 31n => B ;; LoadConst64 $ => E :AND - C => A + D => A ;;NEED_INCLUDE: 2-exp zkPC + 2 => RR :JMP(@two_power + E) @@ -876,8 +880,8 @@ label_1_6: A :MSTORE(SP + 16) 65280n => B ;; LoadConst32 $ => A :MLOAD(SP) - $ => B :AND - B => C + $ => D :AND + D => C 8n => A ;; LoadConst32 31n => B ;; LoadConst64 $ => E :AND @@ -911,11 +915,11 @@ label_1_6: $ => B :OR $ => A :MLOAD(SP + 24) $ => A :OR - A => C + A => D 8n => A ;; LoadConst64 63n => B ;; LoadConst64 $ => E :AND - C => A + D => A ;;NEED_INCLUDE: 2-exp zkPC + 2 => RR :JMP(@two_power + E) @@ -923,11 +927,11 @@ label_1_6: $${var _mul = A * B} ${_mul >> 64} => D ${_mul} => E :ARITH - E => D + E => C 255n => B ;; LoadConst32 $ => A :MLOAD(SP) $ => B :AND - D => A + C => A $ => A :OR 13352372148217134600n => B ;; LoadConst64 B :ASSERT @@ -948,7 +952,8 @@ label_1_6: A :MSTORE(SP + 16) 65280n => B ;; LoadConst32 $ => A :MLOAD(SP + 40) - $ => C :AND + $ => E :AND + E => C 8n => A ;; LoadConst32 31n => B ;; LoadConst64 $ => E :AND @@ -999,19 +1004,19 @@ label_1_6: 4294967295n => B ;; LoadConst64 $ => B :AND $ => A :MLOAD(SP + 24) - $ => C :OR + $ => E :OR $ => A :MLOAD(SP) - B => D - C => B + B => C + E => B $ => A :OR 65280n => B ;; LoadConst32 - $ => C :AND - C :MSTORE(SP + 16) + $ => E :AND + E :MSTORE(SP + 16) A :MSTORE(SP + 24) 16n => A ;; LoadConst32 31n => B ;; LoadConst64 $ => E :AND - D => A + C => A ;;NEED_INCLUDE: 2-exp zkPC + 2 => RR :JMP(@two_power + E) @@ -1111,11 +1116,12 @@ label_1_6: A :MSTORE(SP) 65280n => B ;; LoadConst32 $ => A :MLOAD(SP + 48) - $ => C :AND + $ => E :AND + E => D 8n => A ;; LoadConst32 31n => B ;; LoadConst64 $ => E :AND - C => A + D => A ;;NEED_INCLUDE: 2-exp zkPC + 2 => RR :JMP(@two_power + E) @@ -1157,11 +1163,10 @@ label_1_6: $${var _mul = A * B} ${_mul >> 64} => D ${_mul} => E :ARITH - E => C 255n => B ;; LoadConst32 $ => A :MLOAD(SP + 48) $ => B :AND - C => A + E => A $ => A :OR 11902541952223915002n => B ;; LoadConst64 B :ASSERT @@ -1182,12 +1187,12 @@ label_1_6: A :MSTORE(SP) 65280n => B ;; LoadConst32 $ => A :MLOAD(SP + 56) - $ => D :AND - D => C + $ => B :AND + B => D 8n => A ;; LoadConst32 31n => B ;; LoadConst64 $ => E :AND - C => A + D => A ;;NEED_INCLUDE: 2-exp zkPC + 2 => RR :JMP(@two_power + E) @@ -1234,15 +1239,15 @@ label_1_6: 4294967295n => B ;; LoadConst64 $ => B :AND $ => A :MLOAD(SP) - $ => D :OR - $ => A :MLOAD(SP + 8) + $ => A :OR B => C - D => B + A => B + $ => A :MLOAD(SP + 8) $ => A :OR 65280n => B ;; LoadConst32 - $ => D :AND + $ => B :AND A :MSTORE(SP) - D :MSTORE(SP + 16) + B :MSTORE(SP + 16) 16n => A ;; LoadConst32 31n => B ;; LoadConst64 $ => E :AND @@ -1276,11 +1281,11 @@ label_1_6: $ => B :AND $ => A :MLOAD(SP + 16) $ => A :OR - A => C + A => D 32n => A ;; LoadConst64 63n => B ;; LoadConst64 $ => E :AND - C => A + D => A ;;NEED_INCLUDE: 2-exp zkPC + 2 => RR :JMP(@two_power + E) @@ -1307,11 +1312,11 @@ label_1_6: E :ARITH 4294967295n => B ;; LoadConst64 $ => A :AND - A => D + A => C 16n => A ;; LoadConst32 31n => B ;; LoadConst64 $ => E :AND - D => A + C => A ;;NEED_INCLUDE: 2-exp zkPC + 2 => RR :JMP(@two_power + E) @@ -1346,8 +1351,8 @@ label_1_6: A :MSTORE(SP) 65280n => B ;; LoadConst32 $ => A :MLOAD(SP + 64) - $ => D :AND - D => C + $ => B :AND + B => C 8n => A ;; LoadConst32 31n => B ;; LoadConst64 $ => E :AND @@ -1362,11 +1367,11 @@ label_1_6: E => A 4294967295n => B ;; LoadConst64 $ => A :AND - A => C + A => D 16n => A ;; LoadConst32 31n => B ;; LoadConst64 $ => E :AND - C => A + D => A ;;NEED_INCLUDE: 2-exp zkPC + 2 => RR :JMP(@two_power + E) @@ -1381,11 +1386,11 @@ label_1_6: $ => B :OR $ => A :MLOAD(SP + 8) $ => A :OR - A => D + A => C 8n => A ;; LoadConst64 63n => B ;; LoadConst64 $ => E :AND - D => A + C => A ;;NEED_INCLUDE: 2-exp zkPC + 2 => RR :JMP(@two_power + E) @@ -1393,11 +1398,11 @@ label_1_6: $${var _mul = A * B} ${_mul >> 64} => D ${_mul} => E :ARITH - E => C + E => D 255n => B ;; LoadConst32 $ => A :MLOAD(SP + 64) $ => B :AND - C => A + D => A $ => A :OR 14160706888648589550n => B ;; LoadConst64 B :ASSERT @@ -1418,8 +1423,8 @@ label_1_6: A :MSTORE(SP) 65280n => B ;; LoadConst32 $ => A :MLOAD(SP + 72) - $ => E :AND - E => C + $ => B :AND + B => C 8n => A ;; LoadConst32 31n => B ;; LoadConst64 $ => E :AND @@ -1470,19 +1475,19 @@ label_1_6: 4294967295n => B ;; LoadConst64 $ => B :AND $ => A :MLOAD(SP + 8) - $ => E :OR + $ => C :OR $ => A :MLOAD(SP) - B => C - E => B + B => D + C => B $ => A :OR 65280n => B ;; LoadConst32 - $ => E :AND - E :MSTORE(SP) + $ => B :AND + B :MSTORE(SP) A :MSTORE(SP + 8) 16n => A ;; LoadConst32 31n => B ;; LoadConst64 $ => E :AND - C => A + D => A ;;NEED_INCLUDE: 2-exp zkPC + 2 => RR :JMP(@two_power + E) @@ -1582,12 +1587,12 @@ label_1_6: A :MSTORE(SP) 65280n => B ;; LoadConst32 $ => A :MLOAD(SP + 80) - $ => E :AND - E => D + $ => B :AND + B => C 8n => A ;; LoadConst32 31n => B ;; LoadConst64 $ => E :AND - D => A + C => A ;;NEED_INCLUDE: 2-exp zkPC + 2 => RR :JMP(@two_power + E) @@ -1641,9 +1646,8 @@ label_1_6: $ => A :MLOAD(SP + 88) $ => A :ADD 4294967295n => B ;; LoadConst64 - $ => C :AND - 65536 => E ;; LoadExtName(User(userextname0)) - C :MSTORE(MEM:E + 8) + $ => E :AND + E :MSTORE(global_0) $ => C :MLOAD(SP - 1) $ => D :MLOAD(SP - 2) $ => E :MLOAD(SP - 3) diff --git a/cranelift/zkasm_data/generated/global.zkasm b/cranelift/zkasm_data/generated/global.zkasm new file mode 100644 index 000000000000..986adbb630ee --- /dev/null +++ b/cranelift/zkasm_data/generated/global.zkasm @@ -0,0 +1,33 @@ +VAR GLOBAL global_0 +VAR GLOBAL global_1 +start: + 4294967294 :MSTORE(global_0) ;; Global32(-2) + 5 :MSTORE(global_1) ;; Global32(5) + zkPC + 2 => RR + :JMP(function_1) + :JMP(finalizeExecution) +function_1: + SP + 1 => SP + RR :MSTORE(SP - 1) + SP + 2 => SP + D :MSTORE(SP - 1) + B :MSTORE(SP - 2) + 3n => D ;; LoadConst32 + D :MSTORE(global_1) + $ => A :MLOAD(global_0) + $ => B :MLOAD(global_1) + $ => A :ADD + 4294967295n => B ;; LoadConst64 + $ => A :AND + 1n => B ;; LoadConst32 + B :ASSERT + $ => D :MLOAD(SP - 1) + $ => B :MLOAD(SP - 2) + SP - 2 => SP + $ => RR :MLOAD(SP - 1) + SP - 1 => SP + :JMP(RR) +finalizeExecution: + ${beforeLast()} :JMPN(finalizeExecution) + :JMP(start) +INCLUDE "helpers/2-exp.zkasm" \ No newline at end of file diff --git a/cranelift/zkasm_data/global.wat b/cranelift/zkasm_data/global.wat new file mode 100644 index 000000000000..e4c6a82314b2 --- /dev/null +++ b/cranelift/zkasm_data/global.wat @@ -0,0 +1,12 @@ +(module + (import "env" "assert_eq" (func $assert_eq (param i32) (param i32))) + (global $a i32 (i32.const -2)) + (global $b (mut i32) (i32.const 5)) + (func $main + (global.set $b (i32.const 3)) + (global.get $a) + (global.get $b) + i32.add + i32.const 1 + call $assert_eq) + (start $main)) diff --git a/cranelift/zkasm_data/state.csv b/cranelift/zkasm_data/state.csv index 3f8fc1a86d39..501841ff48a8 100644 --- a/cranelift/zkasm_data/state.csv +++ b/cranelift/zkasm_data/state.csv @@ -7,6 +7,7 @@ counter,pass,153 div,pass,26 eqz,pass,26 fibonacci,pass,224 +global,pass,25 i32_add_overflows,pass,19 i32_const,pass,15 i32_mul_overflows,pass,25 diff --git a/docs/zkasm/test_summary.csv b/docs/zkasm/test_summary.csv index a0b5315c43c3..38196c6e0090 100644 --- a/docs/zkasm/test_summary.csv +++ b/docs/zkasm/test_summary.csv @@ -1,5 +1,5 @@ Suite path,Passing count,Total count,Total cycles -cranelift/zkasm_data,26,27,1002 +cranelift/zkasm_data,27,28,1027 cranelift/zkasm_data/benchmarks/fibonacci,3,3,273054 cranelift/zkasm_data/benchmarks/sha256,0,1,0 cranelift/zkasm_data/spectest/conversions,12,24,180