1  /* This file is part of DarkFi (https://dark.fi)
   2   *
   3   * Copyright (C) 2020-2025 Dyne.org foundation
   4   *
   5   * This program is free software: you can redistribute it and/or modify
   6   * it under the terms of the GNU Affero General Public License as
   7   * published by the Free Software Foundation, either version 3 of the
   8   * License, or (at your option) any later version.
   9   *
  10   * This program is distributed in the hope that it will be useful,
  11   * but WITHOUT ANY WARRANTY; without even the implied warranty of
  12   * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  13   * GNU Affero General Public License for more details.
  14   *
  15   * You should have received a copy of the GNU Affero General Public License
  16   * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  17   */
  18  
  19  use std::collections::HashSet;
  20  
  21  use darkfi_sdk::crypto::{
  22      constants::{
  23          sinsemilla::{OrchardCommitDomains, OrchardHashDomains, K},
  24          util::gen_const_array,
  25          ConstBaseFieldElement, OrchardFixedBases, OrchardFixedBasesFull, ValueCommitV,
  26          MERKLE_DEPTH_ORCHARD,
  27      },
  28      smt::SMT_FP_DEPTH,
  29  };
  30  use halo2_gadgets::{
  31      ecc::{
  32          chip::{EccChip, EccConfig},
  33          FixedPoint, FixedPointBaseField, FixedPointShort, NonIdentityPoint, Point, ScalarFixed,
  34          ScalarFixedShort, ScalarVar,
  35      },
  36      poseidon::{
  37          primitives as poseidon, Hash as PoseidonHash, Pow5Chip as PoseidonChip,
  38          Pow5Config as PoseidonConfig,
  39      },
  40      sinsemilla::{
  41          chip::{SinsemillaChip, SinsemillaConfig},
  42          merkle::{
  43              chip::{MerkleChip, MerkleConfig},
  44              MerklePath,
  45          },
  46      },
  47      utilities::lookup_range_check::{LookupRangeCheck, LookupRangeCheckConfig},
  48  };
  49  use halo2_proofs::{
  50      arithmetic::Field,
  51      circuit::{floor_planner, AssignedCell, Layouter, Value},
  52      pasta::{group::Curve, pallas, Fp},
  53      plonk,
  54      plonk::{Advice, Circuit, Column, ConstraintSystem, Instance as InstanceColumn},
  55  };
  56  use tracing::{error, trace};
  57  
  58  pub use super::vm_heap::{HeapVar, Witness};
  59  use super::{
  60      assign_free_advice,
  61      gadget::{
  62          arithmetic::{ArithChip, ArithConfig, ArithInstruction},
  63          cond_select::{ConditionalSelectChip, ConditionalSelectConfig},
  64          less_than::{LessThanChip, LessThanConfig},
  65          native_range_check::{NativeRangeCheckChip, NativeRangeCheckConfig},
  66          small_range_check::{SmallRangeCheckChip, SmallRangeCheckConfig},
  67          smt,
  68          zero_cond::{ZeroCondChip, ZeroCondConfig},
  69      },
  70      tracer::ZkTracer,
  71  };
  72  use crate::zkas::{
  73      types::{HeapType, LitType},
  74      Opcode, ZkBinary,
  75  };
  76  
  77  /// Available chips/gadgets in the zkvm
  78  #[derive(Debug, Clone)]
  79  #[allow(clippy::large_enum_variant)]
  80  enum VmChip {
  81      /// ECC Chip
  82      Ecc(EccConfig<OrchardFixedBases>),
  83  
  84      /// Merkle tree chip (using Sinsemilla)
  85      Merkle(
  86          (
  87              MerkleConfig<OrchardHashDomains, OrchardCommitDomains, OrchardFixedBases>,
  88              MerkleConfig<OrchardHashDomains, OrchardCommitDomains, OrchardFixedBases>,
  89          ),
  90      ),
  91  
  92      /// Sparse merkle tree (using Poseidon)
  93      SparseTree(smt::PathConfig),
  94  
  95      /// Sinsemilla chip
  96      Sinsemilla(
  97          (
  98              SinsemillaConfig<OrchardHashDomains, OrchardCommitDomains, OrchardFixedBases>,
  99              SinsemillaConfig<OrchardHashDomains, OrchardCommitDomains, OrchardFixedBases>,
 100          ),
 101      ),
 102  
 103      /// Poseidon hash chip
 104      Poseidon(PoseidonConfig<pallas::Base, 3, 2>),
 105  
 106      /// Base field arithmetic chip
 107      Arithmetic(ArithConfig),
 108  
 109      /// 64 bit native range check
 110      NativeRange64(NativeRangeCheckConfig<K, 64>),
 111  
 112      /// 253 bit native range check
 113      NativeRange253(NativeRangeCheckConfig<K, 253>),
 114  
 115      /// 253 bit `a < b` check
 116      LessThan(LessThanConfig<K, 253>),
 117  
 118      /// Boolean check
 119      BoolCheck(SmallRangeCheckConfig),
 120  
 121      /// Conditional selection
 122      CondSelect(ConditionalSelectConfig<pallas::Base>),
 123  
 124      /// Zero-Cond selection
 125      ZeroCond(ZeroCondConfig<pallas::Base>),
 126  }
 127  
 128  /// zkvm configuration
 129  #[derive(Clone)]
 130  pub struct VmConfig {
 131      /// Chips used in the circuit
 132      chips: Vec<VmChip>,
 133      /// Instance column used for public inputs
 134      primary: Column<InstanceColumn>,
 135      /// Advice column used to witness values
 136      witness: Column<Advice>,
 137  }
 138  
 139  impl VmConfig {
 140      fn ecc_chip(&self) -> Option<EccChip<OrchardFixedBases>> {
 141          let Some(VmChip::Ecc(ecc_config)) =
 142              self.chips.iter().find(|&c| matches!(c, VmChip::Ecc(_)))
 143          else {
 144              return None
 145          };
 146  
 147          Some(EccChip::construct(ecc_config.clone()))
 148      }
 149  
 150      fn merkle_chip_1(
 151          &self,
 152      ) -> Option<MerkleChip<OrchardHashDomains, OrchardCommitDomains, OrchardFixedBases>> {
 153          let Some(VmChip::Merkle((merkle_cfg1, _))) =
 154              self.chips.iter().find(|&c| matches!(c, VmChip::Merkle(_)))
 155          else {
 156              return None
 157          };
 158  
 159          Some(MerkleChip::construct(merkle_cfg1.clone()))
 160      }
 161  
 162      fn merkle_chip_2(
 163          &self,
 164      ) -> Option<MerkleChip<OrchardHashDomains, OrchardCommitDomains, OrchardFixedBases>> {
 165          let Some(VmChip::Merkle((_, merkle_cfg2))) =
 166              self.chips.iter().find(|&c| matches!(c, VmChip::Merkle(_)))
 167          else {
 168              return None
 169          };
 170  
 171          Some(MerkleChip::construct(merkle_cfg2.clone()))
 172      }
 173  
 174      fn smt_chip(&self) -> Option<smt::PathChip> {
 175          let Some(VmChip::SparseTree(config)) =
 176              self.chips.iter().find(|&c| matches!(c, VmChip::SparseTree(_)))
 177          else {
 178              return None
 179          };
 180  
 181          Some(smt::PathChip::construct(config.clone()))
 182      }
 183  
 184      fn poseidon_chip(&self) -> Option<PoseidonChip<pallas::Base, 3, 2>> {
 185          let Some(VmChip::Poseidon(poseidon_config)) =
 186              self.chips.iter().find(|&c| matches!(c, VmChip::Poseidon(_)))
 187          else {
 188              return None
 189          };
 190  
 191          Some(PoseidonChip::construct(poseidon_config.clone()))
 192      }
 193  
 194      fn arithmetic_chip(&self) -> Option<ArithChip<pallas::Base>> {
 195          let Some(VmChip::Arithmetic(arith_config)) =
 196              self.chips.iter().find(|&c| matches!(c, VmChip::Arithmetic(_)))
 197          else {
 198              return None
 199          };
 200  
 201          Some(ArithChip::construct(arith_config.clone()))
 202      }
 203  
 204      fn condselect_chip(&self) -> Option<ConditionalSelectChip<pallas::Base>> {
 205          let Some(VmChip::CondSelect(condselect_config)) =
 206              self.chips.iter().find(|&c| matches!(c, VmChip::CondSelect(_)))
 207          else {
 208              return None
 209          };
 210  
 211          Some(ConditionalSelectChip::construct(condselect_config.clone()))
 212      }
 213  
 214      fn zerocond_chip(&self) -> Option<ZeroCondChip<pallas::Base>> {
 215          let Some(VmChip::ZeroCond(zerocond_config)) =
 216              self.chips.iter().find(|&c| matches!(c, VmChip::ZeroCond(_)))
 217          else {
 218              return None
 219          };
 220  
 221          Some(ZeroCondChip::construct(zerocond_config.clone()))
 222      }
 223  
 224      fn rangecheck64_chip(&self) -> Option<NativeRangeCheckChip<K, 64>> {
 225          let Some(VmChip::NativeRange64(range_config)) =
 226              self.chips.iter().find(|&c| matches!(c, VmChip::NativeRange64(_)))
 227          else {
 228              return None
 229          };
 230  
 231          Some(NativeRangeCheckChip::construct(range_config.clone()))
 232      }
 233  
 234      fn rangecheck253_chip(&self) -> Option<NativeRangeCheckChip<K, 253>> {
 235          let Some(VmChip::NativeRange253(range_config)) =
 236              self.chips.iter().find(|&c| matches!(c, VmChip::NativeRange253(_)))
 237          else {
 238              return None
 239          };
 240  
 241          Some(NativeRangeCheckChip::construct(range_config.clone()))
 242      }
 243  
 244      fn lessthan_chip(&self) -> Option<LessThanChip<K, 253>> {
 245          let Some(VmChip::LessThan(lessthan_config)) =
 246              self.chips.iter().find(|&c| matches!(c, VmChip::LessThan(_)))
 247          else {
 248              return None
 249          };
 250  
 251          Some(LessThanChip::construct(lessthan_config.clone()))
 252      }
 253  
 254      fn boolcheck_chip(&self) -> Option<SmallRangeCheckChip<pallas::Base>> {
 255          let Some(VmChip::BoolCheck(boolcheck_config)) =
 256              self.chips.iter().find(|&c| matches!(c, VmChip::BoolCheck(_)))
 257          else {
 258              return None
 259          };
 260  
 261          Some(SmallRangeCheckChip::construct(boolcheck_config.clone()))
 262      }
 263  }
 264  
 265  /// Configuration parameters for the circuit.
 266  /// Defines which chips we need to initialize and configure.
 267  #[derive(Default)]
 268  #[allow(dead_code)]
 269  pub struct ZkParams {
 270      init_ecc: bool,
 271      init_poseidon: bool,
 272      init_sinsemilla: bool,
 273      init_arithmetic: bool,
 274      init_nativerange: bool,
 275      init_lessthan: bool,
 276      init_boolcheck: bool,
 277      init_condselect: bool,
 278      init_zerocond: bool,
 279  }
 280  
 281  #[derive(Clone)]
 282  pub struct ZkCircuit {
 283      constants: Vec<String>,
 284      pub(super) witnesses: Vec<Witness>,
 285      literals: Vec<(LitType, String)>,
 286      pub(super) opcodes: Vec<(Opcode, Vec<(HeapType, usize)>)>,
 287      pub tracer: ZkTracer,
 288  }
 289  
 290  impl ZkCircuit {
 291      pub fn new(witnesses: Vec<Witness>, circuit_code: &ZkBinary) -> Self {
 292          let constants = circuit_code.constants.iter().map(|x| x.1.clone()).collect();
 293          let literals = circuit_code.literals.clone();
 294          Self {
 295              constants,
 296              witnesses,
 297              literals,
 298              opcodes: circuit_code.opcodes.clone(),
 299              tracer: ZkTracer::new(true),
 300          }
 301      }
 302  
 303      pub fn enable_trace(&mut self) {
 304          self.tracer.init();
 305      }
 306  }
 307  
 308  impl Circuit<pallas::Base> for ZkCircuit {
 309      type Config = VmConfig;
 310      type FloorPlanner = floor_planner::V1;
 311      type Params = ZkParams;
 312  
 313      fn without_witnesses(&self) -> Self {
 314          Self {
 315              constants: self.constants.clone(),
 316              witnesses: self.witnesses.clone(),
 317              literals: self.literals.clone(),
 318              opcodes: self.opcodes.clone(),
 319              tracer: ZkTracer::new(false),
 320          }
 321      }
 322  
 323      fn configure(_meta: &mut ConstraintSystem<pallas::Base>) -> Self::Config {
 324          unreachable!();
 325      }
 326  
 327      fn params(&self) -> Self::Params {
 328          // Gather all opcodes used in the circuit.
 329          let mut opcodes = HashSet::new();
 330          for (opcode, _) in &self.opcodes {
 331              opcodes.insert(opcode);
 332          }
 333  
 334          // Conditions on which we enable the ECC chip
 335          let init_ecc = !self.constants.is_empty() ||
 336              opcodes.contains(&Opcode::EcAdd) ||
 337              opcodes.contains(&Opcode::EcMul) ||
 338              opcodes.contains(&Opcode::EcMulBase) ||
 339              opcodes.contains(&Opcode::EcMulShort) ||
 340              opcodes.contains(&Opcode::EcMulVarBase) ||
 341              opcodes.contains(&Opcode::EcGetX) ||
 342              opcodes.contains(&Opcode::EcGetY) ||
 343              opcodes.contains(&Opcode::ConstrainEqualPoint) ||
 344              self.witnesses.iter().any(|x| {
 345                  matches!(x, Witness::EcPoint(_)) ||
 346                      matches!(x, Witness::EcNiPoint(_)) ||
 347                      matches!(x, Witness::EcFixedPoint(_)) ||
 348                      matches!(x, Witness::Scalar(_))
 349              });
 350  
 351          // Conditions on which we enable the Poseidon hash chip
 352          let init_poseidon = opcodes.contains(&Opcode::PoseidonHash);
 353  
 354          // Conditions on which we enable the Sinsemilla and Merkle chips
 355          let init_sinsemilla = opcodes.contains(&Opcode::MerkleRoot);
 356  
 357          // Conditions on which we enable the base field Arithmetic chip
 358          let init_arithmetic = opcodes.contains(&Opcode::BaseAdd) ||
 359              opcodes.contains(&Opcode::BaseSub) ||
 360              opcodes.contains(&Opcode::BaseMul);
 361  
 362          // Conditions on which we enable the native range check chips
 363          // TODO: Separate 253 and 64.
 364          let init_nativerange = opcodes.contains(&Opcode::RangeCheck) ||
 365              opcodes.contains(&Opcode::LessThanLoose) ||
 366              opcodes.contains(&Opcode::LessThanStrict);
 367  
 368          // Conditions on which we enable the less than comparison chip
 369          let init_lessthan =
 370              opcodes.contains(&Opcode::LessThanLoose) || opcodes.contains(&Opcode::LessThanStrict);
 371  
 372          // Conditions on which we enable the boolean check chip
 373          let init_boolcheck = opcodes.contains(&Opcode::BoolCheck);
 374  
 375          // Conditions on which we enable the conditional selection chip
 376          let init_condselect = opcodes.contains(&Opcode::CondSelect);
 377  
 378          // Conditions on which we enable the zero cond selection chip
 379          let init_zerocond = opcodes.contains(&Opcode::ZeroCondSelect);
 380  
 381          ZkParams {
 382              init_ecc,
 383              init_poseidon,
 384              init_sinsemilla,
 385              init_arithmetic,
 386              init_nativerange,
 387              init_lessthan,
 388              init_boolcheck,
 389              init_condselect,
 390              init_zerocond,
 391          }
 392      }
 393  
 394      fn configure_with_params(
 395          meta: &mut ConstraintSystem<pallas::Base>,
 396          _params: Self::Params,
 397      ) -> Self::Config {
 398          // Advice columns used in the circuit
 399          let mut advices = vec![];
 400          for _ in 0..10 {
 401              advices.push(meta.advice_column());
 402          }
 403  
 404          // Instance column used for public inputs
 405          let primary = meta.instance_column();
 406          meta.enable_equality(primary);
 407  
 408          // Permutation over all advice columns
 409          for advice in advices.iter() {
 410              meta.enable_equality(*advice);
 411          }
 412  
 413          // Fixed columns for the Sinsemilla generator lookup table
 414          let table_idx = meta.lookup_table_column();
 415          let lookup = (table_idx, meta.lookup_table_column(), meta.lookup_table_column());
 416  
 417          // Poseidon requires four advice columns, while ECC incomplete addition
 418          // requires six. We can reduce the proof size by sharing fixed columns
 419          // between the ECC and Poseidon chips.
 420          // TODO: For multiple invocations perhaps they could/should be configured
 421          // in parallel rather than sharing?
 422          let lagrange_coeffs = [
 423              meta.fixed_column(),
 424              meta.fixed_column(),
 425              meta.fixed_column(),
 426              meta.fixed_column(),
 427              meta.fixed_column(),
 428              meta.fixed_column(),
 429              meta.fixed_column(),
 430              meta.fixed_column(),
 431          ];
 432          let rc_a = lagrange_coeffs[2..5].try_into().unwrap();
 433          let rc_b = lagrange_coeffs[5..8].try_into().unwrap();
 434  
 435          // Also use the first Lagrange coefficient column for loading global constants.
 436          meta.enable_constant(lagrange_coeffs[0]);
 437  
 438          // Use one of the right-most advice columns for all of our range checks.
 439          let range_check = LookupRangeCheckConfig::configure(meta, advices[9], table_idx);
 440  
 441          // Configuration for curve point operations.
 442          // This uses 10 advice columns and spans the whole circuit.
 443          let ecc_config = EccChip::<OrchardFixedBases>::configure(
 444              meta,
 445              advices[0..10].try_into().unwrap(),
 446              lagrange_coeffs,
 447              range_check,
 448          );
 449  
 450          // Configuration for the Poseidon hash
 451          let poseidon_config = PoseidonChip::configure::<poseidon::P128Pow5T3>(
 452              meta,
 453              advices[6..9].try_into().unwrap(),
 454              advices[5],
 455              rc_a,
 456              rc_b,
 457          );
 458  
 459          // Configuration for the Arithmetic chip
 460          let arith_config = ArithChip::configure(meta, advices[7], advices[8], advices[6]);
 461  
 462          // Configuration for a Sinsemilla hash instantiation and a
 463          // Merkle hash instantiation using this Sinsemilla instance.
 464          // Since the Sinsemilla config uses only 5 advice columns,
 465          // we can fit two instances side-by-side.
 466          let (sinsemilla_cfg1, merkle_cfg1) = {
 467              let sinsemilla_cfg1 = SinsemillaChip::configure(
 468                  meta,
 469                  advices[..5].try_into().unwrap(),
 470                  advices[6],
 471                  lagrange_coeffs[0],
 472                  lookup,
 473                  range_check,
 474              );
 475              let merkle_cfg1 = MerkleChip::configure(meta, sinsemilla_cfg1.clone());
 476              (sinsemilla_cfg1, merkle_cfg1)
 477          };
 478  
 479          let (sinsemilla_cfg2, merkle_cfg2) = {
 480              let sinsemilla_cfg2 = SinsemillaChip::configure(
 481                  meta,
 482                  advices[5..].try_into().unwrap(),
 483                  advices[7],
 484                  lagrange_coeffs[1],
 485                  lookup,
 486                  range_check,
 487              );
 488              let merkle_cfg2 = MerkleChip::configure(meta, sinsemilla_cfg2.clone());
 489              (sinsemilla_cfg2, merkle_cfg2)
 490          };
 491  
 492          let smt_config = smt::PathChip::configure(
 493              meta,
 494              advices[0..2].try_into().unwrap(),
 495              advices[2..6].try_into().unwrap(),
 496              poseidon_config.clone(),
 497          );
 498  
 499          // K-table for 64 bit range check lookups
 500          let native_64_range_check_config =
 501              NativeRangeCheckChip::<K, 64>::configure(meta, advices[8], table_idx);
 502  
 503          // K-table for 253 bit range check lookups
 504          let native_253_range_check_config =
 505              NativeRangeCheckChip::<K, 253>::configure(meta, advices[8], table_idx);
 506  
 507          // TODO: FIXME: Configure these better, this is just a stop-gap
 508          let z1 = meta.advice_column();
 509          let z2 = meta.advice_column();
 510  
 511          let lessthan_config = LessThanChip::<K, 253>::configure(
 512              meta, advices[6], advices[7], advices[8], z1, z2, table_idx,
 513          );
 514  
 515          // Configuration for boolean checks, it uses the small_range_check
 516          // chip with a range of 2, which enforces one bit, i.e. 0 or 1.
 517          let boolcheck_config = SmallRangeCheckChip::configure(meta, advices[9], 2);
 518  
 519          // Configuration for the conditional selection chip
 520          let condselect_config =
 521              ConditionalSelectChip::configure(meta, advices[1..5].try_into().unwrap());
 522  
 523          // Configuration for the zero_cond selection chip
 524          let zerocond_config = ZeroCondChip::configure(meta, advices[1..5].try_into().unwrap());
 525  
 526          // Later we'll use this for optimisation
 527          let chips = vec![
 528              VmChip::Ecc(ecc_config),
 529              VmChip::Merkle((merkle_cfg1, merkle_cfg2)),
 530              VmChip::SparseTree(smt_config),
 531              VmChip::Sinsemilla((sinsemilla_cfg1, sinsemilla_cfg2)),
 532              VmChip::Poseidon(poseidon_config),
 533              VmChip::Arithmetic(arith_config),
 534              VmChip::NativeRange64(native_64_range_check_config),
 535              VmChip::NativeRange253(native_253_range_check_config),
 536              VmChip::LessThan(lessthan_config),
 537              VmChip::BoolCheck(boolcheck_config),
 538              VmChip::CondSelect(condselect_config),
 539              VmChip::ZeroCond(zerocond_config),
 540          ];
 541  
 542          VmConfig { primary, witness: advices[0], chips }
 543      }
 544  
 545      fn synthesize(
 546          &self,
 547          config: Self::Config,
 548          mut layouter: impl Layouter<pallas::Base>,
 549      ) -> std::result::Result<(), plonk::Error> {
 550          trace!(target: "zk::vm", "Entering synthesize()");
 551  
 552          // ===================
 553          // VM Setup
 554          //====================
 555  
 556          // Our heap which holds every variable we reference and create.
 557          let mut heap: Vec<HeapVar> = vec![];
 558  
 559          // Our heap which holds all the literal values we have in the circuit.
 560          // For now, we only support u64.
 561          let mut litheap: Vec<u64> = vec![];
 562  
 563          // Offset for public inputs
 564          let mut public_inputs_offset = 0;
 565  
 566          // Offset for literals
 567          let mut literals_offset = 0;
 568  
 569          // Load the Sinsemilla generator lookup table used by the whole circuit.
 570          if let Some(VmChip::Sinsemilla((sinsemilla_cfg1, _))) =
 571              config.chips.iter().find(|&c| matches!(c, VmChip::Sinsemilla(_)))
 572          {
 573              trace!(target: "zk::vm", "Initializing Sinsemilla generator lookup table");
 574              SinsemillaChip::load(sinsemilla_cfg1.clone(), &mut layouter)?;
 575          }
 576  
 577          let no_sinsemilla_chip = !config.chips.iter().any(|c| matches!(c, VmChip::Sinsemilla(_)));
 578  
 579          // Construct the 64-bit NativeRangeCheck chip
 580          let rangecheck64_chip = config.rangecheck64_chip();
 581          if let Some(VmChip::NativeRange64(rangecheck64_config)) =
 582              config.chips.iter().find(|&c| matches!(c, VmChip::NativeRange64(_)))
 583          {
 584              if no_sinsemilla_chip {
 585                  trace!(target: "zk::vm", "Initializing k table for 64bit NativeRangeCheck");
 586                  NativeRangeCheckChip::<K, 64>::load_k_table(
 587                      &mut layouter,
 588                      rangecheck64_config.k_values_table,
 589                  )?;
 590              }
 591          }
 592  
 593          let no_rangecheck64_chip =
 594              !config.chips.iter().any(|c| matches!(c, VmChip::NativeRange64(_)));
 595  
 596          // Construct the 253-bit NativeRangeCheck and LessThan chips.
 597          let rangecheck253_chip = config.rangecheck253_chip();
 598          let lessthan_chip = config.lessthan_chip();
 599  
 600          if let Some(VmChip::NativeRange253(rangecheck253_config)) =
 601              config.chips.iter().find(|&c| matches!(c, VmChip::NativeRange253(_)))
 602          {
 603              if no_sinsemilla_chip && no_rangecheck64_chip {
 604                  trace!(target: "zk::vm", "Initializing k table for 253bit NativeRangeCheck");
 605                  NativeRangeCheckChip::<K, 253>::load_k_table(
 606                      &mut layouter,
 607                      rangecheck253_config.k_values_table,
 608                  )?;
 609              }
 610          }
 611  
 612          // Construct the ECC chip.
 613          let ecc_chip = config.ecc_chip();
 614  
 615          // Construct the Arithmetic chip.
 616          let arith_chip = config.arithmetic_chip();
 617  
 618          // Construct the boolean check chip.
 619          let boolcheck_chip = config.boolcheck_chip();
 620  
 621          // Construct the conditional selection chip
 622          let condselect_chip = config.condselect_chip();
 623  
 624          // Construct the zero_cond selection chip
 625          let zerocond_chip = config.zerocond_chip();
 626  
 627          // Construct sparse Merkle tree chip
 628          let smt_chip = config.smt_chip().unwrap();
 629  
 630          // ==========================
 631          // Constants setup
 632          // ==========================
 633  
 634          // This constant one is used for short multiplication
 635          let one = assign_free_advice(
 636              layouter.namespace(|| "Load constant one"),
 637              config.witness,
 638              Value::known(pallas::Base::ONE),
 639          )?;
 640          layouter.assign_region(
 641              || "constrain constant",
 642              |mut region| region.constrain_constant(one.cell(), pallas::Base::ONE),
 643          )?;
 644  
 645          // ANCHOR: constant_init
 646          // Lookup and push constants onto the heap
 647          for constant in &self.constants {
 648              trace!(
 649                  target: "zk::vm",
 650                  "Pushing constant `{}` to heap address {}",
 651                  constant.as_str(),
 652                  heap.len()
 653              );
 654              match constant.as_str() {
 655                  "VALUE_COMMIT_VALUE" => {
 656                      let vcv = ValueCommitV;
 657                      let vcv = FixedPointShort::from_inner(ecc_chip.as_ref().unwrap().clone(), vcv);
 658                      heap.push(HeapVar::EcFixedPointShort(vcv));
 659                  }
 660                  "VALUE_COMMIT_RANDOM" => {
 661                      let vcr = OrchardFixedBasesFull::ValueCommitR;
 662                      let vcr = FixedPoint::from_inner(ecc_chip.as_ref().unwrap().clone(), vcr);
 663                      heap.push(HeapVar::EcFixedPoint(vcr));
 664                  }
 665                  "VALUE_COMMIT_RANDOM_BASE" => {
 666                      let vcr = ConstBaseFieldElement::value_commit_r();
 667                      let vcr =
 668                          FixedPointBaseField::from_inner(ecc_chip.as_ref().unwrap().clone(), vcr);
 669                      heap.push(HeapVar::EcFixedPointBase(vcr));
 670                  }
 671                  "NULLIFIER_K" => {
 672                      let nfk = ConstBaseFieldElement::nullifier_k();
 673                      let nfk =
 674                          FixedPointBaseField::from_inner(ecc_chip.as_ref().unwrap().clone(), nfk);
 675                      heap.push(HeapVar::EcFixedPointBase(nfk));
 676                  }
 677  
 678                  _ => {
 679                      error!(target: "zk::vm", "Invalid constant name: {}", constant.as_str());
 680                      return Err(plonk::Error::Synthesis)
 681                  }
 682              }
 683          }
 684          // ANCHOR_END: constant_init
 685  
 686          // ANCHOR: literals_init
 687          // Load the literals onto the literal heap
 688          // N.B. Only uint64 is supported right now.
 689          for literal in &self.literals {
 690              match literal.0 {
 691                  LitType::Uint64 => match literal.1.parse::<u64>() {
 692                      Ok(v) => litheap.push(v),
 693                      Err(e) => {
 694                          error!(target: "zk::vm", "Failed converting u64 literal: {e}");
 695                          return Err(plonk::Error::Synthesis)
 696                      }
 697                  },
 698                  _ => {
 699                      error!(target: "zk::vm", "Invalid literal: {literal:?}");
 700                      return Err(plonk::Error::Synthesis)
 701                  }
 702              }
 703          }
 704          // ANCHOR_END: literals_init
 705  
 706          // ANCHOR: witness_init
 707          // Push the witnesses onto the heap, and potentially, if the witness
 708          // is in the Base field (like the entire circuit is), load it into a
 709          // table cell.
 710          for witness in &self.witnesses {
 711              match witness {
 712                  Witness::EcPoint(w) => {
 713                      trace!(target: "zk::vm", "Witnessing EcPoint into circuit");
 714                      let point = Point::new(
 715                          ecc_chip.as_ref().unwrap().clone(),
 716                          layouter.namespace(|| "Witness EcPoint"),
 717                          w.as_ref().map(|cm| cm.to_affine()),
 718                      )?;
 719  
 720                      trace!(target: "zk::vm", "Pushing EcPoint to heap address {}", heap.len());
 721                      heap.push(HeapVar::EcPoint(point));
 722                  }
 723  
 724                  Witness::EcNiPoint(w) => {
 725                      trace!(target: "zk::vm", "Witnessing EcNiPoint into circuit");
 726                      let point = NonIdentityPoint::new(
 727                          ecc_chip.as_ref().unwrap().clone(),
 728                          layouter.namespace(|| "Witness EcNiPoint"),
 729                          w.as_ref().map(|cm| cm.to_affine()),
 730                      )?;
 731  
 732                      trace!(target: "zk::vm", "Pushing EcNiPoint to heap address {}", heap.len());
 733                      heap.push(HeapVar::EcNiPoint(point));
 734                  }
 735  
 736                  Witness::EcFixedPoint(_) => {
 737                      error!(target: "zk::vm", "Unable to witness EcFixedPoint, this is unimplemented.");
 738                      return Err(plonk::Error::Synthesis)
 739                  }
 740  
 741                  Witness::Base(w) => {
 742                      trace!(target: "zk::vm", "Witnessing Base into circuit");
 743                      let base = assign_free_advice(
 744                          layouter.namespace(|| "Witness Base"),
 745                          config.witness,
 746                          *w,
 747                      )?;
 748  
 749                      trace!(target: "zk::vm", "Pushing Base to heap address {}", heap.len());
 750                      heap.push(HeapVar::Base(base));
 751                  }
 752  
 753                  Witness::Scalar(w) => {
 754                      trace!(target: "zk::vm", "Witnessing Scalar into circuit");
 755                      let scalar = ScalarFixed::new(
 756                          ecc_chip.as_ref().unwrap().clone(),
 757                          layouter.namespace(|| "Witness ScalarFixed"),
 758                          *w,
 759                      )?;
 760  
 761                      trace!(target: "zk::vm", "Pushing Scalar to heap address {}", heap.len());
 762                      heap.push(HeapVar::Scalar(scalar));
 763                  }
 764  
 765                  Witness::MerklePath(w) => {
 766                      trace!(target: "zk::vm", "Witnessing MerklePath into circuit");
 767                      let path: Value<[pallas::Base; MERKLE_DEPTH_ORCHARD]> =
 768                          w.map(|typed_path| gen_const_array(|i| typed_path[i].inner()));
 769  
 770                      trace!(target: "zk::vm", "Pushing MerklePath to heap address {}", heap.len());
 771                      heap.push(HeapVar::MerklePath(path));
 772                  }
 773  
 774                  Witness::SparseMerklePath(w) => {
 775                      let path: Value<[pallas::Base; SMT_FP_DEPTH]> =
 776                          w.map(|typed_path| gen_const_array(|i| typed_path[i]));
 777  
 778                      trace!(target: "zk::vm", "Pushing SparseMerklePath to heap address {}", heap.len());
 779                      heap.push(HeapVar::SparseMerklePath(path));
 780                  }
 781  
 782                  Witness::Uint32(w) => {
 783                      trace!(target: "zk::vm", "Pushing Uint32 to heap address {}", heap.len());
 784                      heap.push(HeapVar::Uint32(*w));
 785                  }
 786  
 787                  Witness::Uint64(w) => {
 788                      trace!(target: "zk::vm", "Pushing Uint64 to heap address {}", heap.len());
 789                      heap.push(HeapVar::Uint64(*w));
 790                  }
 791              }
 792          }
 793          // ANCHOR_END: witness_init
 794  
 795          // =============================
 796          // And now, work through opcodes
 797          // =============================
 798          self.tracer.clear();
 799          // TODO: Copy constraints
 800          // ANCHOR: opcode_begin
 801          for opcode in &self.opcodes {
 802              match opcode.0 {
 803                  Opcode::EcAdd => {
 804                      trace!(target: "zk::vm", "Executing `EcAdd{:?}` opcode", opcode.1);
 805                      let args = &opcode.1;
 806  
 807                      let lhs: Point<pallas::Affine, EccChip<OrchardFixedBases>> =
 808                          heap[args[0].1].clone().try_into()?;
 809  
 810                      let rhs: Point<pallas::Affine, EccChip<OrchardFixedBases>> =
 811                          heap[args[1].1].clone().try_into()?;
 812  
 813                      let ret = lhs.add(layouter.namespace(|| "EcAdd()"), &rhs)?;
 814  
 815                      trace!(target: "zk::vm", "Pushing result to heap address {}", heap.len());
 816                      self.tracer.push_ecpoint(&ret);
 817                      heap.push(HeapVar::EcPoint(ret));
 818                  }
 819                  // ANCHOR_END: opcode_begin
 820                  Opcode::EcMul => {
 821                      trace!(target: "zk::vm", "Executing `EcMul{:?}` opcode", opcode.1);
 822                      let args = &opcode.1;
 823  
 824                      let lhs: FixedPoint<pallas::Affine, EccChip<OrchardFixedBases>> =
 825                          heap[args[1].1].clone().try_into()?;
 826  
 827                      let rhs: ScalarFixed<pallas::Affine, EccChip<OrchardFixedBases>> =
 828                          heap[args[0].1].clone().try_into()?;
 829  
 830                      let (ret, _) = lhs.mul(layouter.namespace(|| "EcMul()"), rhs)?;
 831  
 832                      trace!(target: "zk::vm", "Pushing result to heap address {}", heap.len());
 833                      self.tracer.push_ecpoint(&ret);
 834                      heap.push(HeapVar::EcPoint(ret));
 835                  }
 836  
 837                  Opcode::EcMulVarBase => {
 838                      trace!(target: "zk::vm", "Executing `EcMulVarBase{:?}` opcode", opcode.1);
 839                      let args = &opcode.1;
 840  
 841                      let lhs: NonIdentityPoint<pallas::Affine, EccChip<OrchardFixedBases>> =
 842                          heap[args[1].1].clone().try_into()?;
 843  
 844                      let rhs: AssignedCell<Fp, Fp> = heap[args[0].1].clone().try_into()?;
 845                      let rhs = ScalarVar::from_base(
 846                          ecc_chip.as_ref().unwrap().clone(),
 847                          layouter.namespace(|| "EcMulVarBase::from_base()"),
 848                          &rhs,
 849                      )?;
 850  
 851                      let (ret, _) = lhs.mul(layouter.namespace(|| "EcMulVarBase()"), rhs)?;
 852  
 853                      trace!(target: "zk::vm", "Pushing result to heap address {}", heap.len());
 854                      self.tracer.push_ecpoint(&ret);
 855                      heap.push(HeapVar::EcPoint(ret));
 856                  }
 857  
 858                  Opcode::EcMulBase => {
 859                      trace!(target: "zk::vm", "Executing `EcMulBase{:?}` opcode", opcode.1);
 860                      let args = &opcode.1;
 861  
 862                      let lhs: FixedPointBaseField<pallas::Affine, EccChip<OrchardFixedBases>> =
 863                          heap[args[1].1].clone().try_into()?;
 864  
 865                      let rhs: AssignedCell<Fp, Fp> = heap[args[0].1].clone().try_into()?;
 866  
 867                      let ret = lhs.mul(layouter.namespace(|| "EcMulBase()"), rhs)?;
 868  
 869                      trace!(target: "zk::vm", "Pushing result to heap address {}", heap.len());
 870                      self.tracer.push_ecpoint(&ret);
 871                      heap.push(HeapVar::EcPoint(ret));
 872                  }
 873  
 874                  Opcode::EcMulShort => {
 875                      trace!(target: "zk::vm", "Executing `EcMulShort{:?}` opcode", opcode.1);
 876                      let args = &opcode.1;
 877  
 878                      let lhs: FixedPointShort<pallas::Affine, EccChip<OrchardFixedBases>> =
 879                          heap[args[1].1].clone().try_into()?;
 880  
 881                      let rhs = ScalarFixedShort::new(
 882                          ecc_chip.as_ref().unwrap().clone(),
 883                          layouter.namespace(|| "EcMulShort: ScalarFixedShort::new()"),
 884                          (heap[args[0].1].clone().try_into()?, one.clone()),
 885                      )?;
 886  
 887                      let (ret, _) = lhs.mul(layouter.namespace(|| "EcMulShort()"), rhs)?;
 888  
 889                      trace!(target: "zk::vm", "Pushing result to heap address {}", heap.len());
 890                      self.tracer.push_ecpoint(&ret);
 891                      heap.push(HeapVar::EcPoint(ret));
 892                  }
 893  
 894                  Opcode::EcGetX => {
 895                      trace!(target: "zk::vm", "Executing `EcGetX{:?}` opcode", opcode.1);
 896                      let args = &opcode.1;
 897  
 898                      let point: Point<pallas::Affine, EccChip<OrchardFixedBases>> =
 899                          heap[args[0].1].clone().try_into()?;
 900  
 901                      let ret = point.inner().x();
 902  
 903                      trace!(target: "zk::vm", "Pushing result to heap address {}", heap.len());
 904                      self.tracer.push_base(&ret);
 905                      heap.push(HeapVar::Base(ret));
 906                  }
 907  
 908                  Opcode::EcGetY => {
 909                      trace!(target: "zk::vm", "Executing `EcGetY{:?}` opcode", opcode.1);
 910                      let args = &opcode.1;
 911  
 912                      let point: Point<pallas::Affine, EccChip<OrchardFixedBases>> =
 913                          heap[args[0].1].clone().try_into()?;
 914  
 915                      let ret = point.inner().y();
 916  
 917                      trace!(target: "zk::vm", "Pushing result to heap address {}", heap.len());
 918                      self.tracer.push_base(&ret);
 919                      heap.push(HeapVar::Base(ret));
 920                  }
 921  
 922                  Opcode::PoseidonHash => {
 923                      trace!(target: "zk::vm", "Executing `PoseidonHash{:?}` opcode", opcode.1);
 924                      let args = &opcode.1;
 925  
 926                      let mut poseidon_message: Vec<AssignedCell<Fp, Fp>> =
 927                          Vec::with_capacity(args.len());
 928  
 929                      for idx in args {
 930                          poseidon_message.push(heap[idx.1].clone().try_into()?);
 931                      }
 932  
 933                      macro_rules! poseidon_hash {
 934                          ($len:expr, $hasher:ident, $output:ident, $cell:ident) => {
 935                              let $hasher = PoseidonHash::<
 936                                  _,
 937                                  _,
 938                                  poseidon::P128Pow5T3,
 939                                  poseidon::ConstantLength<$len>,
 940                                  3,
 941                                  2,
 942                              >::init(
 943                                  config.poseidon_chip().unwrap(),
 944                                  layouter.namespace(|| "PoseidonHash init"),
 945                              )?;
 946  
 947                              let $output = $hasher.hash(
 948                                  layouter.namespace(|| "PoseidonHash hash"),
 949                                  poseidon_message.try_into().unwrap(),
 950                              )?;
 951  
 952                              let $cell: AssignedCell<Fp, Fp> = $output.into();
 953  
 954                              trace!(target: "zk::vm", "Pushing hash to heap address {}", heap.len());
 955                              self.tracer.push_base(&$cell);
 956                              heap.push(HeapVar::Base($cell));
 957                          };
 958                      }
 959  
 960                      macro_rules! vla {
 961                          ($args:ident, $a:ident, $b:ident, $c:ident, $($num:tt)*) => {
 962                              match $args.len() {
 963                                  $($num => {
 964                                      poseidon_hash!($num, $a, $b, $c);
 965                                  })*
 966                                  _ => {
 967                                      error!(target: "zk::vm", "Unsupported poseidon hash for {} elements", $args.len());
 968                                      return Err(plonk::Error::Synthesis)
 969                                  }
 970                              }
 971                          };
 972                      }
 973  
 974                      vla!(args, a, b, c, 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24);
 975                  }
 976  
 977                  Opcode::MerkleRoot => {
 978                      // TODO: all these trace statements could have trace!(..., args) instead
 979                      trace!(target: "zk::vm", "Executing `MerkleRoot{:?}` opcode", opcode.1);
 980                      let args = &opcode.1;
 981  
 982                      let leaf_pos = heap[args[0].1].clone().try_into()?;
 983                      let merkle_path: Value<[Fp; MERKLE_DEPTH_ORCHARD]> =
 984                          heap[args[1].1].clone().try_into()?;
 985                      let leaf = heap[args[2].1].clone().try_into()?;
 986  
 987                      let merkle_inputs = MerklePath::construct(
 988                          [config.merkle_chip_1().unwrap(), config.merkle_chip_2().unwrap()],
 989                          OrchardHashDomains::MerkleCrh,
 990                          leaf_pos,
 991                          merkle_path,
 992                      );
 993  
 994                      let root = merkle_inputs
 995                          .calculate_root(layouter.namespace(|| "MerkleRoot()"), leaf)?;
 996  
 997                      trace!(target: "zk::vm", "Pushing merkle root to heap address {}", heap.len());
 998                      self.tracer.push_base(&root);
 999                      heap.push(HeapVar::Base(root));
1000                  }
1001  
1002                  Opcode::SparseMerkleRoot => {
1003                      trace!(target: "zk::vm", "Executing `SparseTreeIsMember{:?}` opcode", opcode.1);
1004                      let args = &opcode.1;
1005  
1006                      let pos = heap[args[0].1].clone().try_into()?;
1007                      let path: Value<[Fp; SMT_FP_DEPTH]> = heap[args[1].1].clone().try_into()?;
1008                      let leaf = heap[args[2].1].clone().try_into()?;
1009  
1010                      let root = smt_chip.check_membership(&mut layouter, pos, path, leaf)?;
1011  
1012                      self.tracer.push_base(&root);
1013                      heap.push(HeapVar::Base(root));
1014                  }
1015  
1016                  Opcode::BaseAdd => {
1017                      trace!(target: "zk::vm", "Executing `BaseAdd{:?}` opcode", opcode.1);
1018                      let args = &opcode.1;
1019  
1020                      let lhs = &heap[args[0].1].clone().try_into()?;
1021                      let rhs = &heap[args[1].1].clone().try_into()?;
1022  
1023                      let sum = arith_chip.as_ref().unwrap().add(
1024                          layouter.namespace(|| "BaseAdd()"),
1025                          lhs,
1026                          rhs,
1027                      )?;
1028  
1029                      trace!(target: "zk::vm", "Pushing sum to heap address {}", heap.len());
1030                      self.tracer.push_base(&sum);
1031                      heap.push(HeapVar::Base(sum));
1032                  }
1033  
1034                  Opcode::BaseMul => {
1035                      trace!(target: "zk::vm", "Executing `BaseSub{:?}` opcode", opcode.1);
1036                      let args = &opcode.1;
1037  
1038                      let lhs = &heap[args[0].1].clone().try_into()?;
1039                      let rhs = &heap[args[1].1].clone().try_into()?;
1040  
1041                      let product = arith_chip.as_ref().unwrap().mul(
1042                          layouter.namespace(|| "BaseMul()"),
1043                          lhs,
1044                          rhs,
1045                      )?;
1046  
1047                      trace!(target: "zk::vm", "Pushing product to heap address {}", heap.len());
1048                      self.tracer.push_base(&product);
1049                      heap.push(HeapVar::Base(product));
1050                  }
1051  
1052                  Opcode::BaseSub => {
1053                      trace!(target: "zk::vm", "Executing `BaseSub{:?}` opcode", opcode.1);
1054                      let args = &opcode.1;
1055  
1056                      let lhs = &heap[args[0].1].clone().try_into()?;
1057                      let rhs = &heap[args[1].1].clone().try_into()?;
1058  
1059                      let difference = arith_chip.as_ref().unwrap().sub(
1060                          layouter.namespace(|| "BaseSub()"),
1061                          lhs,
1062                          rhs,
1063                      )?;
1064  
1065                      trace!(target: "zk::vm", "Pushing difference to heap address {}", heap.len());
1066                      self.tracer.push_base(&difference);
1067                      heap.push(HeapVar::Base(difference));
1068                  }
1069  
1070                  Opcode::WitnessBase => {
1071                      trace!(target: "zk::vm", "Executing `WitnessBase{:?}` opcode", opcode.1);
1072                      //let args = &opcode.1;
1073  
1074                      let lit = litheap[literals_offset];
1075                      literals_offset += 1;
1076  
1077                      let witness = assign_free_advice(
1078                          layouter.namespace(|| "Witness literal"),
1079                          config.witness,
1080                          Value::known(pallas::Base::from(lit)),
1081                      )?;
1082  
1083                      layouter.assign_region(
1084                          || "constrain constant",
1085                          |mut region| {
1086                              region.constrain_constant(witness.cell(), pallas::Base::from(lit))
1087                          },
1088                      )?;
1089  
1090                      trace!(target: "zk::vm", "Pushing assignment to heap address {}", heap.len());
1091                      self.tracer.push_base(&witness);
1092                      heap.push(HeapVar::Base(witness));
1093                  }
1094  
1095                  Opcode::RangeCheck => {
1096                      trace!(target: "zk::vm", "Executing `RangeCheck{:?}` opcode", opcode.1);
1097                      let args = &opcode.1;
1098  
1099                      let lit = litheap[literals_offset];
1100                      literals_offset += 1;
1101  
1102                      let arg = heap[args[1].1].clone();
1103  
1104                      match lit {
1105                          64 => {
1106                              rangecheck64_chip.as_ref().unwrap().copy_range_check(
1107                                  layouter.namespace(|| "copy range check 64"),
1108                                  arg.try_into()?,
1109                              )?;
1110                          }
1111                          253 => {
1112                              rangecheck253_chip.as_ref().unwrap().copy_range_check(
1113                                  layouter.namespace(|| "copy range check 253"),
1114                                  arg.try_into()?,
1115                              )?;
1116                          }
1117                          x => {
1118                              error!(target: "zk::vm", "Unsupported bit-range {x} for range_check");
1119                              return Err(plonk::Error::Synthesis)
1120                          }
1121                      }
1122                      self.tracer.push_void();
1123                  }
1124  
1125                  Opcode::LessThanStrict => {
1126                      trace!(target: "zk::vm", "Executing `LessThanStrict{:?}` opcode", opcode.1);
1127                      let args = &opcode.1;
1128  
1129                      let a = heap[args[0].1].clone().try_into()?;
1130                      let b = heap[args[1].1].clone().try_into()?;
1131  
1132                      lessthan_chip.as_ref().unwrap().copy_less_than(
1133                          layouter.namespace(|| "copy a<b check"),
1134                          a,
1135                          b,
1136                          0,
1137                          true,
1138                      )?;
1139                      self.tracer.push_void();
1140                  }
1141  
1142                  Opcode::LessThanLoose => {
1143                      trace!(target: "zk::vm", "Executing `LessThanLoose{:?}` opcode", opcode.1);
1144                      let args = &opcode.1;
1145  
1146                      let a = heap[args[0].1].clone().try_into()?;
1147                      let b = heap[args[1].1].clone().try_into()?;
1148  
1149                      lessthan_chip.as_ref().unwrap().copy_less_than(
1150                          layouter.namespace(|| "copy a<b check"),
1151                          a,
1152                          b,
1153                          0,
1154                          false,
1155                      )?;
1156                      self.tracer.push_void();
1157                  }
1158  
1159                  Opcode::BoolCheck => {
1160                      trace!(target: "zk::vm", "Executing `BoolCheck{:?}` opcode", opcode.1);
1161                      let args = &opcode.1;
1162  
1163                      let w = heap[args[0].1].clone().try_into()?;
1164  
1165                      boolcheck_chip
1166                          .as_ref()
1167                          .unwrap()
1168                          .small_range_check(layouter.namespace(|| "copy boolean check"), w)?;
1169                      self.tracer.push_void();
1170                  }
1171  
1172                  Opcode::CondSelect => {
1173                      trace!(target: "zk::vm", "Executing `CondSelect{:?}` opcode", opcode.1);
1174                      let args = &opcode.1;
1175  
1176                      let cond: AssignedCell<Fp, Fp> = heap[args[0].1].clone().try_into()?;
1177                      let lhs: AssignedCell<Fp, Fp> = heap[args[1].1].clone().try_into()?;
1178                      let rhs: AssignedCell<Fp, Fp> = heap[args[2].1].clone().try_into()?;
1179  
1180                      let out: AssignedCell<Fp, Fp> =
1181                          condselect_chip.as_ref().unwrap().conditional_select(
1182                              &mut layouter.namespace(|| "cond_select"),
1183                              lhs,
1184                              rhs,
1185                              cond,
1186                          )?;
1187  
1188                      trace!(target: "zk::vm", "Pushing assignment to heap address {}", heap.len());
1189                      self.tracer.push_base(&out);
1190                      heap.push(HeapVar::Base(out));
1191                  }
1192  
1193                  Opcode::ZeroCondSelect => {
1194                      trace!(target: "zk::vm", "Executing `ZeroCondSelect{:?}` opcode", opcode.1);
1195                      let args = &opcode.1;
1196  
1197                      let lhs: AssignedCell<Fp, Fp> = heap[args[0].1].clone().try_into()?;
1198                      let rhs: AssignedCell<Fp, Fp> = heap[args[1].1].clone().try_into()?;
1199  
1200                      let out: AssignedCell<Fp, Fp> = zerocond_chip.as_ref().unwrap().assign(
1201                          layouter.namespace(|| "zero_cond"),
1202                          lhs,
1203                          rhs,
1204                      )?;
1205  
1206                      trace!(target: "zk::vm", "Pushing assignment to heap address {}", heap.len());
1207                      self.tracer.push_base(&out);
1208                      heap.push(HeapVar::Base(out));
1209                  }
1210  
1211                  Opcode::ConstrainEqualBase => {
1212                      trace!(target: "zk::vm", "Executing `ConstrainEqualBase{:?}` opcode", opcode.1);
1213                      let args = &opcode.1;
1214  
1215                      let lhs: AssignedCell<Fp, Fp> = heap[args[0].1].clone().try_into()?;
1216                      let rhs: AssignedCell<Fp, Fp> = heap[args[1].1].clone().try_into()?;
1217  
1218                      layouter.assign_region(
1219                          || "constrain witnessed base equality",
1220                          |mut region| region.constrain_equal(lhs.cell(), rhs.cell()),
1221                      )?;
1222                      self.tracer.push_void();
1223                  }
1224  
1225                  Opcode::ConstrainEqualPoint => {
1226                      trace!(target: "zk::vm", "Executing `ConstrainEqualPoint{:?}` opcode", opcode.1);
1227                      let args = &opcode.1;
1228  
1229                      let lhs: Point<pallas::Affine, EccChip<OrchardFixedBases>> =
1230                          heap[args[0].1].clone().try_into()?;
1231  
1232                      let rhs: Point<pallas::Affine, EccChip<OrchardFixedBases>> =
1233                          heap[args[1].1].clone().try_into()?;
1234  
1235                      lhs.constrain_equal(
1236                          layouter.namespace(|| "constrain ec point equality"),
1237                          &rhs,
1238                      )?;
1239                      self.tracer.push_void();
1240                  }
1241  
1242                  Opcode::ConstrainInstance => {
1243                      trace!(target: "zk::vm", "Executing `ConstrainInstance{:?}` opcode", opcode.1);
1244                      let args = &opcode.1;
1245  
1246                      let var: AssignedCell<Fp, Fp> = heap[args[0].1].clone().try_into()?;
1247  
1248                      layouter.constrain_instance(
1249                          var.cell(),
1250                          config.primary,
1251                          public_inputs_offset,
1252                      )?;
1253  
1254                      public_inputs_offset += 1;
1255                      self.tracer.push_void();
1256                  }
1257  
1258                  Opcode::DebugPrint => {
1259                      trace!(target: "zk::vm", "Executing `DebugPrint{:?}` opcode", opcode.1);
1260                      let args = &opcode.1;
1261  
1262                      println!("[ZKVM DEBUG] HEAP INDEX: {}", args[0].1);
1263                      println!("[ZKVM DEBUG] {:#?}", heap[args[0].1]);
1264                      self.tracer.push_void();
1265                  }
1266  
1267                  Opcode::Noop => {
1268                      error!(target: "zk::vm", "Unsupported opcode");
1269                      return Err(plonk::Error::Synthesis)
1270                  }
1271              }
1272          }
1273          self.tracer.assert_correct(self.opcodes.len());
1274  
1275          trace!(target: "zk::vm", "Exiting synthesize() successfully");
1276          Ok(())
1277      }
1278  }