vm.rs 21 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574
  1. use halo2_gadgets::{
  2. ecc::{
  3. chip::{EccChip, EccConfig},
  4. FixedPoint, FixedPointBaseField, FixedPointShort, Point,
  5. },
  6. poseidon::{Hash as PoseidonHash, Pow5Chip as PoseidonChip, Pow5Config as PoseidonConfig},
  7. primitives::poseidon::{ConstantLength, P128Pow5T3},
  8. sinsemilla::{
  9. chip::{SinsemillaChip, SinsemillaConfig},
  10. merkle::{
  11. chip::{MerkleChip, MerkleConfig},
  12. MerklePath,
  13. },
  14. },
  15. utilities::{lookup_range_check::LookupRangeCheckConfig, UtilitiesInstructions},
  16. };
  17. use halo2_proofs::{
  18. circuit::{AssignedCell, Layouter, SimpleFloorPlanner},
  19. plonk,
  20. plonk::{Advice, Circuit, Column, ConstraintSystem, Instance as InstanceColumn},
  21. };
  22. use log::debug;
  23. use pasta_curves::{group::Curve, pallas, Fp};
  24. use super::arith_chip::{ArithmeticChip, ArithmeticChipConfig};
  25. pub use super::vm_stack::{StackVar, Witness};
  26. use crate::{
  27. crypto::constants::{
  28. sinsemilla::{OrchardCommitDomains, OrchardHashDomains},
  29. util::gen_const_array,
  30. NullifierK, OrchardFixedBases, OrchardFixedBasesFull, ValueCommitV, MERKLE_DEPTH_ORCHARD,
  31. },
  32. zkas::{decoder::ZkBinary, opcode::Opcode},
  33. };
  34. #[derive(Clone)]
  35. pub struct VmConfig {
  36. primary: Column<InstanceColumn>,
  37. advices: [Column<Advice>; 10],
  38. ecc_config: EccConfig<OrchardFixedBases>,
  39. merkle_cfg1: MerkleConfig<OrchardHashDomains, OrchardCommitDomains, OrchardFixedBases>,
  40. merkle_cfg2: MerkleConfig<OrchardHashDomains, OrchardCommitDomains, OrchardFixedBases>,
  41. sinsemilla_cfg1: SinsemillaConfig<OrchardHashDomains, OrchardCommitDomains, OrchardFixedBases>,
  42. _sinsemilla_cfg2: SinsemillaConfig<OrchardHashDomains, OrchardCommitDomains, OrchardFixedBases>,
  43. poseidon_config: PoseidonConfig<pallas::Base, 3, 2>,
  44. arith_config: ArithmeticChipConfig,
  45. }
  46. impl VmConfig {
  47. fn ecc_chip(&self) -> EccChip<OrchardFixedBases> {
  48. EccChip::construct(self.ecc_config.clone())
  49. }
  50. /*
  51. fn sinsemilla_chip_1(
  52. &self,
  53. ) -> SinsemillaChip<OrchardHashDomains, OrchardCommitDomains, OrchardFixedBases> {
  54. SinsemillaChip::construct(self.sinsemilla_cfg1.clone())
  55. }
  56. fn sinsemilla_chip_2(
  57. &self,
  58. ) -> SinsemillaChip<OrchardHashDomains, OrchardCommitDomains, OrchardFixedBases> {
  59. SinsemillaChip::construct(self.sinsemilla_cfg2.clone())
  60. }
  61. */
  62. fn merkle_chip_1(
  63. &self,
  64. ) -> MerkleChip<OrchardHashDomains, OrchardCommitDomains, OrchardFixedBases> {
  65. MerkleChip::construct(self.merkle_cfg1.clone())
  66. }
  67. fn merkle_chip_2(
  68. &self,
  69. ) -> MerkleChip<OrchardHashDomains, OrchardCommitDomains, OrchardFixedBases> {
  70. MerkleChip::construct(self.merkle_cfg2.clone())
  71. }
  72. fn poseidon_chip(&self) -> PoseidonChip<pallas::Base, 3, 2> {
  73. PoseidonChip::construct(self.poseidon_config.clone())
  74. }
  75. fn arithmetic_chip(&self) -> ArithmeticChip {
  76. ArithmeticChip::construct(self.arith_config.clone())
  77. }
  78. }
  79. #[derive(Clone, Default)]
  80. pub struct ZkCircuit {
  81. constants: Vec<String>,
  82. witnesses: Vec<Witness>,
  83. opcodes: Vec<(Opcode, Vec<usize>)>,
  84. }
  85. impl ZkCircuit {
  86. pub fn new(witnesses: Vec<Witness>, circuit_code: ZkBinary) -> Self {
  87. let constants = circuit_code.constants.iter().map(|x| x.1.clone()).collect();
  88. Self { constants, witnesses, opcodes: circuit_code.opcodes }
  89. }
  90. }
  91. impl UtilitiesInstructions<pallas::Base> for ZkCircuit {
  92. type Var = AssignedCell<Fp, Fp>;
  93. }
  94. impl Circuit<pallas::Base> for ZkCircuit {
  95. type Config = VmConfig;
  96. type FloorPlanner = SimpleFloorPlanner;
  97. fn without_witnesses(&self) -> Self {
  98. Self {
  99. constants: self.constants.clone(),
  100. witnesses: self.witnesses.clone(),
  101. opcodes: self.opcodes.clone(),
  102. }
  103. }
  104. fn configure(meta: &mut ConstraintSystem<pallas::Base>) -> Self::Config {
  105. // Advice columns used in the circuit
  106. let advices = [
  107. meta.advice_column(),
  108. meta.advice_column(),
  109. meta.advice_column(),
  110. meta.advice_column(),
  111. meta.advice_column(),
  112. meta.advice_column(),
  113. meta.advice_column(),
  114. meta.advice_column(),
  115. meta.advice_column(),
  116. meta.advice_column(),
  117. ];
  118. // Fixed columns for the Sinsemilla generator lookup table
  119. let table_idx = meta.lookup_table_column();
  120. let lookup = (table_idx, meta.lookup_table_column(), meta.lookup_table_column());
  121. // Instance column used for public inputs
  122. let primary = meta.instance_column();
  123. meta.enable_equality(primary);
  124. // Permutation over all advice columns
  125. for advice in advices.iter() {
  126. meta.enable_equality(*advice);
  127. }
  128. // Poseidon requires four advice columns, while ECC incomplete addition
  129. // requires six. We can reduce the proof size by sharing fixed columns
  130. // between the ECC and Poseidon chips.
  131. // TODO: For multiple invocations perhaps they could/should be configured
  132. // in parallel rather than sharing?
  133. let lagrange_coeffs = [
  134. meta.fixed_column(),
  135. meta.fixed_column(),
  136. meta.fixed_column(),
  137. meta.fixed_column(),
  138. meta.fixed_column(),
  139. meta.fixed_column(),
  140. meta.fixed_column(),
  141. meta.fixed_column(),
  142. ];
  143. let rc_a = lagrange_coeffs[2..5].try_into().unwrap();
  144. let rc_b = lagrange_coeffs[5..8].try_into().unwrap();
  145. // Also use the first Lagrange coefficient column for loading global constants.
  146. meta.enable_constant(lagrange_coeffs[0]);
  147. // Use one of the right-most advice columns for all of our range checks.
  148. let range_check = LookupRangeCheckConfig::configure(meta, advices[9], table_idx);
  149. // Configuration for curve point operations.
  150. // This uses 10 advice columns and spans the whole circuit.
  151. let ecc_config = EccChip::<OrchardFixedBases>::configure(
  152. meta,
  153. advices,
  154. lagrange_coeffs,
  155. range_check.clone(),
  156. );
  157. // Configuration for the Poseidon hash
  158. let poseidon_config = PoseidonChip::configure::<P128Pow5T3>(
  159. meta,
  160. advices[6..9].try_into().unwrap(),
  161. advices[5],
  162. rc_a,
  163. rc_b,
  164. );
  165. // Configuration for the Arithmetic chip
  166. let arith_config = ArithmeticChip::configure(meta);
  167. // Configuration for a Sinsemilla hash instantiation and a
  168. // Merkle hash instantiation using this Sinsemilla instance.
  169. // Since the Sinsemilla config uses only 5 advice columns,
  170. // we can fit two instances side-by-side.
  171. let (sinsemilla_cfg1, merkle_cfg1) = {
  172. let sinsemilla_cfg1 = SinsemillaChip::configure(
  173. meta,
  174. advices[..5].try_into().unwrap(),
  175. advices[6],
  176. lagrange_coeffs[0],
  177. lookup,
  178. range_check.clone(),
  179. );
  180. let merkle_cfg1 = MerkleChip::configure(meta, sinsemilla_cfg1.clone());
  181. (sinsemilla_cfg1, merkle_cfg1)
  182. };
  183. let (_sinsemilla_cfg2, merkle_cfg2) = {
  184. let sinsemilla_cfg2 = SinsemillaChip::configure(
  185. meta,
  186. advices[5..].try_into().unwrap(),
  187. advices[7],
  188. lagrange_coeffs[1],
  189. lookup,
  190. range_check,
  191. );
  192. let merkle_cfg2 = MerkleChip::configure(meta, sinsemilla_cfg2.clone());
  193. (sinsemilla_cfg2, merkle_cfg2)
  194. };
  195. VmConfig {
  196. primary,
  197. advices,
  198. ecc_config,
  199. merkle_cfg1,
  200. merkle_cfg2,
  201. sinsemilla_cfg1,
  202. _sinsemilla_cfg2,
  203. poseidon_config,
  204. arith_config,
  205. }
  206. }
  207. fn synthesize(
  208. &self,
  209. config: Self::Config,
  210. mut layouter: impl Layouter<pallas::Base>,
  211. ) -> std::result::Result<(), plonk::Error> {
  212. debug!("Entering synthesize()");
  213. // Our stack which holds everything we reference.
  214. let mut stack: Vec<StackVar> = vec![];
  215. // Offset for public inputs
  216. let mut public_inputs_offset = 0;
  217. // Load the Sinsemilla generator lookup table used by the whole circuit.
  218. SinsemillaChip::load(config.sinsemilla_cfg1.clone(), &mut layouter)?;
  219. // Construct the ECC chip.
  220. let ecc_chip = config.ecc_chip();
  221. // Construct the Arithmetic chip.
  222. let arith_chip = config.arithmetic_chip();
  223. // This constant one is used for short multiplication
  224. let one = self.load_private(
  225. layouter.namespace(|| "Load constant one"),
  226. config.advices[0],
  227. Some(pallas::Base::one()),
  228. )?;
  229. // Lookup and push the constants onto the stack
  230. for constant in &self.constants {
  231. debug!("Pushing constant `{}` to stack index {}", constant.as_str(), stack.len());
  232. match constant.as_str() {
  233. "VALUE_COMMIT_VALUE" => {
  234. let vcv = ValueCommitV;
  235. let vcv = FixedPointShort::from_inner(ecc_chip.clone(), vcv);
  236. stack.push(StackVar::EcFixedPointShort(vcv));
  237. }
  238. "VALUE_COMMIT_RANDOM" => {
  239. let vcr = OrchardFixedBasesFull::ValueCommitR;
  240. let vcr = FixedPoint::from_inner(ecc_chip.clone(), vcr);
  241. stack.push(StackVar::EcFixedPoint(vcr));
  242. }
  243. "NULLIFIER_K" => {
  244. let nfk = NullifierK;
  245. let nfk = FixedPointBaseField::from_inner(ecc_chip.clone(), nfk);
  246. stack.push(StackVar::EcFixedPointBase(nfk));
  247. }
  248. _ => unimplemented!(),
  249. }
  250. }
  251. // Push the witnesses onto the stack, and potentially, if the witness
  252. // is in the Base field (like the entire circuit is), load it into a
  253. // table cell.
  254. for witness in &self.witnesses {
  255. match witness {
  256. Witness::EcPoint(w) => {
  257. debug!("Witnessing EcPoint into circuit");
  258. let point = Point::new(
  259. ecc_chip.clone(),
  260. layouter.namespace(|| "Witness EcPoint"),
  261. w.as_ref().map(|cm| cm.to_affine()),
  262. )?;
  263. debug!("Pushing EcPoint to stack index {}", stack.len());
  264. stack.push(StackVar::EcPoint(point));
  265. }
  266. Witness::EcFixedPoint(_) => {
  267. unimplemented!()
  268. }
  269. Witness::Base(w) => {
  270. debug!("Witnessing Base into circuit");
  271. let base = self.load_private(
  272. layouter.namespace(|| "Witness Base"),
  273. config.advices[0],
  274. *w,
  275. )?;
  276. debug!("Pushing Base to stack index {}", stack.len());
  277. stack.push(StackVar::Base(base));
  278. }
  279. Witness::Scalar(w) => {
  280. debug!("Pushing Scalar to stack index {}", stack.len());
  281. stack.push(StackVar::Scalar(*w));
  282. }
  283. Witness::MerklePath(w) => {
  284. debug!("Witnessing MerklePath into circuit");
  285. let path: Option<[pallas::Base; MERKLE_DEPTH_ORCHARD]> =
  286. w.map(|typed_path| gen_const_array(|i| typed_path[i].inner()));
  287. debug!("Pushing MerklePath to stack index {}", stack.len());
  288. stack.push(StackVar::MerklePath(path));
  289. }
  290. Witness::Uint32(w) => {
  291. debug!("Pushing Uint32 to stack index {}", stack.len());
  292. stack.push(StackVar::Uint32(*w));
  293. }
  294. Witness::Uint64(w) => {
  295. debug!("Pushing Uint64 to stack index {}", stack.len());
  296. stack.push(StackVar::Uint64(*w));
  297. }
  298. }
  299. }
  300. // And now, work through opcodes
  301. for opcode in &self.opcodes {
  302. match opcode.0 {
  303. Opcode::EcAdd => {
  304. debug!("Executing `EcAdd{:?}` opcode", opcode.1);
  305. let args = &opcode.1;
  306. let lhs: Point<pallas::Affine, EccChip<OrchardFixedBases>> =
  307. stack[args[0]].clone().into();
  308. let rhs: Point<pallas::Affine, EccChip<OrchardFixedBases>> =
  309. stack[args[1]].clone().into();
  310. let ret = lhs.add(layouter.namespace(|| "EcAdd()"), &rhs)?;
  311. debug!("Pushing result to stack index {}", stack.len());
  312. stack.push(StackVar::EcPoint(ret));
  313. }
  314. Opcode::EcMul => {
  315. debug!("Executing `EcMul{:?}` opcode", opcode.1);
  316. let args = &opcode.1;
  317. let lhs: FixedPoint<pallas::Affine, EccChip<OrchardFixedBases>> =
  318. stack[args[1]].clone().into();
  319. let rhs: Option<pallas::Scalar> = stack[args[0]].clone().into();
  320. let (ret, _) = lhs.mul(layouter.namespace(|| "EcMul()"), rhs)?;
  321. debug!("Pushing result to stack index {}", stack.len());
  322. stack.push(StackVar::EcPoint(ret));
  323. }
  324. Opcode::EcMulBase => {
  325. debug!("Executing `EcMulBase{:?}` opcode", opcode.1);
  326. let args = &opcode.1;
  327. let lhs: FixedPointBaseField<pallas::Affine, EccChip<OrchardFixedBases>> =
  328. stack[args[1]].clone().into();
  329. let rhs: AssignedCell<Fp, Fp> = stack[args[0]].clone().into();
  330. let ret = lhs.mul(layouter.namespace(|| "EcMulBase()"), rhs)?;
  331. debug!("Pushing result to stack index {}", stack.len());
  332. stack.push(StackVar::EcPoint(ret));
  333. }
  334. Opcode::EcMulShort => {
  335. debug!("Executing `EcMulShort{:?}` opcode", opcode.1);
  336. let args = &opcode.1;
  337. let lhs: FixedPointShort<pallas::Affine, EccChip<OrchardFixedBases>> =
  338. stack[args[1]].clone().into();
  339. let rhs: AssignedCell<Fp, Fp> = stack[args[0]].clone().into();
  340. let (ret, _) =
  341. lhs.mul(layouter.namespace(|| "EcMulShort()"), (rhs, one.clone()))?;
  342. debug!("Pushing result to stack index {}", stack.len());
  343. stack.push(StackVar::EcPoint(ret));
  344. }
  345. Opcode::EcGetX => {
  346. debug!("Executing `EcGetX{:?}` opcode", opcode.1);
  347. let args = &opcode.1;
  348. let point: Point<pallas::Affine, EccChip<OrchardFixedBases>> =
  349. stack[args[0]].clone().into();
  350. let ret = point.inner().x();
  351. debug!("Pushing result to stack index {}", stack.len());
  352. stack.push(StackVar::Base(ret));
  353. }
  354. Opcode::EcGetY => {
  355. debug!("Executing `EcGetY{:?}` opcode", opcode.1);
  356. let args = &opcode.1;
  357. let point: Point<pallas::Affine, EccChip<OrchardFixedBases>> =
  358. stack[args[0]].clone().into();
  359. let ret = point.inner().y();
  360. debug!("Pushing result to stack index {}", stack.len());
  361. stack.push(StackVar::Base(ret));
  362. }
  363. Opcode::PoseidonHash => {
  364. debug!("Executing `PoseidonHash{:?}` opcode", opcode.1);
  365. let args = &opcode.1;
  366. let mut poseidon_message: Vec<AssignedCell<Fp, Fp>> =
  367. Vec::with_capacity(args.len());
  368. for idx in args {
  369. poseidon_message.push(stack[*idx].clone().into());
  370. }
  371. macro_rules! poseidon_hash {
  372. ($len:expr, $hasher:ident, $output:ident, $cell:ident) => {
  373. // let $hasher = PoseidonHash::<_, _, P128Pow5T3, _, 3, 2>::init(
  374. // config.poseidon_chip(),
  375. // layouter.namespace(|| "PoseidonHash init"),
  376. // ConstantLength::<$len>,
  377. // )?;
  378. let $hasher =
  379. PoseidonHash::<_, _, P128Pow5T3, ConstantLength<$len>, 3, 2>::init(
  380. config.poseidon_chip(),
  381. layouter.namespace(|| "PoseidonHash init"),
  382. )?;
  383. let $output = $hasher.hash(
  384. layouter.namespace(|| "PoseidonHash hash"),
  385. poseidon_message.try_into().unwrap(),
  386. )?;
  387. //let $cell: AssignedCell<Fp, Fp> = $output.inner().into();
  388. let $cell: AssignedCell<Fp, Fp> = $output.into();
  389. debug!("Pushing hash to stack index {}", stack.len());
  390. stack.push(StackVar::Base($cell));
  391. };
  392. }
  393. macro_rules! vla {
  394. ($args:ident, $a: ident, $b:ident, $c:ident, $($num:tt)*) => {
  395. match $args.len() {
  396. $($num => {
  397. poseidon_hash!($num, $a, $b, $c);
  398. })*
  399. _ => unimplemented!()
  400. }
  401. };
  402. }
  403. vla!(args, a, b, c, 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16);
  404. }
  405. Opcode::CalculateMerkleRoot => {
  406. debug!("Executing `CalculateMerkleRoot{:?}` opcode", opcode.1);
  407. let args = &opcode.1;
  408. let leaf_pos = stack[args[0]].clone().into();
  409. let merkle_path = stack[args[1]].clone().into();
  410. let leaf = stack[args[2]].clone().into();
  411. let merkle_inputs = MerklePath::construct(
  412. config.merkle_chip_1(),
  413. config.merkle_chip_2(),
  414. OrchardHashDomains::MerkleCrh,
  415. leaf_pos,
  416. merkle_path,
  417. );
  418. let root = merkle_inputs
  419. .calculate_root(layouter.namespace(|| "CalculateMerkleRoot()"), leaf)?;
  420. debug!("Pushing merkle root to stack index {}", stack.len());
  421. stack.push(StackVar::Base(root));
  422. }
  423. Opcode::BaseAdd => {
  424. debug!("Executing `BaseAdd{:?}` opcode", opcode.1);
  425. let args = &opcode.1;
  426. let lhs = stack[args[0]].clone().into();
  427. let rhs = stack[args[1]].clone().into();
  428. let sum = arith_chip.add(layouter.namespace(|| "BaseAdd()"), lhs, rhs)?;
  429. debug!("Pushing sum to stack index {}", stack.len());
  430. stack.push(StackVar::Base(sum));
  431. }
  432. Opcode::BaseMul => {
  433. debug!("Executing `BaseMul{:?}` opcode", opcode.1);
  434. let args = &opcode.1;
  435. let lhs = stack[args[0]].clone().into();
  436. let rhs = stack[args[1]].clone().into();
  437. let product = arith_chip.mul(layouter.namespace(|| "BaseMul()"), lhs, rhs)?;
  438. debug!("Pushing product to stack index {}", stack.len());
  439. stack.push(StackVar::Base(product));
  440. }
  441. Opcode::BaseSub => {
  442. debug!("Executing `BaseSub{:?}` opcode", opcode.1);
  443. let args = &opcode.1;
  444. let lhs = stack[args[0]].clone().into();
  445. let rhs = stack[args[1]].clone().into();
  446. let difference =
  447. arith_chip.sub(layouter.namespace(|| "BaseSub()"), lhs, rhs)?;
  448. debug!("Pushing difference to stack index {}", stack.len());
  449. stack.push(StackVar::Base(difference));
  450. }
  451. Opcode::ConstrainInstance => {
  452. debug!("Executing `ConstrainInstance{:?}` opcode", opcode.1);
  453. let args = &opcode.1;
  454. let var: AssignedCell<Fp, Fp> = stack[args[0]].clone().into();
  455. layouter.constrain_instance(
  456. var.cell(),
  457. config.primary,
  458. public_inputs_offset,
  459. )?;
  460. public_inputs_offset += 1;
  461. }
  462. _ => unimplemented!(),
  463. }
  464. }
  465. debug!("Exiting synthesize()");
  466. Ok(())
  467. }
  468. }