transform.rs 25 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724
  1. //! A module for operations that transform a [`StatementTree`].
  2. //! Every transformation must maintain the [disjunction invariant].
  3. //!
  4. //! [disjunction invariant]: StatementTree::check_disjunction_invariant
  5. use super::codegen::CodeGen;
  6. use super::pedersen::{
  7. convert_commitment, convert_randomness, recognize_pedersen_assignment, unique_random_scalars,
  8. LinScalar, PedersenAssignment,
  9. };
  10. use super::sigma::combiners::*;
  11. use super::syntax::{collect_cind_points, taggedvardict_to_vardict};
  12. use super::{TaggedIdent, TaggedScalar, TaggedVarDict};
  13. use quote::{format_ident, quote};
  14. use std::collections::{HashMap, HashSet};
  15. use syn::visit_mut::{self, VisitMut};
  16. use syn::{parse_quote, Error, Expr, Ident, Result};
  17. /// Simplify a [`StatementTree`] by pruning leaves that are the constant
  18. /// `true`, and simplifying `And`, `Or`, and `Thresh` combiners that
  19. /// have fewer than two children.
  20. pub fn prune_statement_tree(st: &mut StatementTree) {
  21. match st {
  22. // If the StatementTree is just a Leaf, just keep it unmodified,
  23. // even if it is leaf_true.
  24. StatementTree::Leaf(_) => {}
  25. // For the And combiner, recursively simplify each child, and then
  26. // prune the child if it is leaf_true. If we end up with 1
  27. // child replace ourselves with that child. If we end up with 0
  28. // children, replace ourselves with leaf_true.
  29. StatementTree::And(v) => {
  30. let mut i: usize = 0;
  31. // Note that v.len _can change_ during this loop
  32. while i < v.len() {
  33. prune_statement_tree(&mut v[i]);
  34. if v[i].is_leaf_true() {
  35. // Remove this child, and _do not_ increment i
  36. v.remove(i);
  37. } else {
  38. i += 1;
  39. }
  40. }
  41. if v.is_empty() {
  42. *st = StatementTree::leaf_true();
  43. } else if v.len() == 1 {
  44. let child = v.remove(0);
  45. *st = child;
  46. }
  47. }
  48. // For the Or combiner, recursively simplify each child, and if
  49. // it ends up leaf_true, replace ourselves with leaf_true.
  50. // If we end up with 1 child, we must have started wth 1 child.
  51. // Replace ourselves with that child anyway.
  52. StatementTree::Or(v) => {
  53. let mut i: usize = 0;
  54. // Note that v.len _can change_ during this loop
  55. while i < v.len() {
  56. prune_statement_tree(&mut v[i]);
  57. if v[i].is_leaf_true() {
  58. *st = StatementTree::leaf_true();
  59. return;
  60. } else {
  61. i += 1;
  62. }
  63. }
  64. if v.len() == 1 {
  65. let child = v.remove(0);
  66. *st = child;
  67. }
  68. }
  69. // For the Thresh combiner, recursively simplify each child, and
  70. // if it ends up leaf_true, prune it, and subtract 1 from the
  71. // thresh. If the thresh hits 0, replace ourselves with
  72. // leaf_true. If we end up with 1 child and thresh is 1,
  73. // replace ourselves with that child.
  74. StatementTree::Thresh(thresh, v) => {
  75. let mut i: usize = 0;
  76. // Note that v.len _can change_ during this loop
  77. while i < v.len() {
  78. prune_statement_tree(&mut v[i]);
  79. if v[i].is_leaf_true() {
  80. // Remove this child, and _do not_ increment i
  81. v.remove(i);
  82. // But decrement thresh
  83. *thresh -= 1;
  84. if *thresh == 0 {
  85. *st = StatementTree::leaf_true();
  86. return;
  87. }
  88. } else {
  89. i += 1;
  90. }
  91. }
  92. if v.len() == 1 {
  93. // If thresh == 0, we would have exited above
  94. assert!(*thresh == 1);
  95. let child = v.remove(0);
  96. *st = child;
  97. }
  98. }
  99. }
  100. }
  101. /// Add parentheses around an [`Expr`] (which represents an [arithmetic
  102. /// expression]) if needed.
  103. ///
  104. /// The parentheses are needed if the [`Expr`] would parse as multiple
  105. /// tokens. For example, `a+b` turns into `(a+b)`, but `c`
  106. /// remains `c` and `(a+b)` remains `(a+b)`.
  107. ///
  108. /// [arithmetic expression]: super::sigma::types::expr_type
  109. pub fn paren_if_needed(expr: Expr) -> Expr {
  110. match expr {
  111. Expr::Unary(_) | Expr::Binary(_) => parse_quote! { (#expr) },
  112. _ => expr,
  113. }
  114. }
  115. /// Transform the [`StatementTree`] so that it satisfies the
  116. /// [disjunction invariant].
  117. ///
  118. /// [disjunction invariant]: StatementTree::check_disjunction_invariant
  119. #[allow(non_snake_case)] // so that Points can be capital letters
  120. pub fn enforce_disjunction_invariant(
  121. codegen: &mut CodeGen,
  122. st: &mut StatementTree,
  123. vars: &mut TaggedVarDict,
  124. ) -> Result<()> {
  125. // Make the VarDict version of the variable dictionary
  126. let mut vardict = taggedvardict_to_vardict(vars);
  127. // A HashSet of the unique random Scalars in the macro input
  128. let mut randoms = unique_random_scalars(vars, st);
  129. // A list of the computationally independent (non-vector) Points in
  130. // the macro input. If we need to do any transformations, there
  131. // must be at least two of them in order to create Pedersen
  132. // commitments.
  133. // If we're testing, sort cind_points so that we get a deterministic
  134. // choice of cind_A and cind_B
  135. #[cfg(not(test))]
  136. let cind_points = collect_cind_points(vars);
  137. #[cfg(test)]
  138. let mut cind_points = collect_cind_points(vars);
  139. #[cfg(test)]
  140. cind_points.sort_unstable();
  141. // Extra statements to be added to the root disjunction branch
  142. let mut root_extra_statements: Vec<StatementTree> = Vec::new();
  143. // The generated variable name for the rng
  144. let rng_var = codegen.gen_ident(&format_ident!("rng"));
  145. // Find any statements that look like Pedersen commitments in the
  146. // root disjunction branch of the StatementTree, and make a HashMap
  147. // mapping the committed private variable to the parsed commitment.
  148. let mut root_pedersens: HashMap<Ident, PedersenAssignment> = HashMap::new();
  149. st.for_each_disjunction_branch_leaf(&mut |leaf| {
  150. // See if we recognize this leaf expression as a
  151. // PedersenAssignment, and if so, map its variable to the
  152. // PedersenAssignment.
  153. if let StatementTree::Leaf(leafexpr) = leaf {
  154. if let Some(ped_assign) =
  155. recognize_pedersen_assignment(vars, &randoms, &vardict, leafexpr)
  156. {
  157. root_pedersens.insert(ped_assign.var(), ped_assign);
  158. }
  159. }
  160. Ok(())
  161. })?;
  162. // Count how many disjunction branches contain each private Scalar
  163. let mut branch_count: HashMap<Ident, usize> = HashMap::new();
  164. st.for_each_disjunction_branch(&mut |branch, _path| {
  165. branch
  166. .disjunction_branch_priv_scalars(&vardict)
  167. .drain()
  168. .for_each(|id| {
  169. if let Some(n) = branch_count.get(&id) {
  170. branch_count.insert(id, n + 1);
  171. } else {
  172. branch_count.insert(id, 1);
  173. }
  174. });
  175. Ok(())
  176. })?;
  177. // Make a HashSet of any of those private Scalars whose count is
  178. // strictly larger than 1. (Those private Scalars are the ones
  179. // that are in violation of the disjunction invariant.)
  180. let mut invariant_violators: HashSet<Ident> = branch_count
  181. .drain()
  182. .filter_map(|(id, n)| if n > 1 { Some(id) } else { None })
  183. .collect();
  184. // If there are no invariant violators, we're done.
  185. if invariant_violators.is_empty() {
  186. return Ok(());
  187. }
  188. // Otherwise, ensure there are at least two computationally
  189. // independent points, since we'll need to construct Pedersen
  190. // commitments.
  191. if cind_points.len() < 2 {
  192. return Err(Error::new(
  193. proc_macro2::Span::call_site(),
  194. "At least two cind Points must be declared to support Pedersen commitments",
  195. ));
  196. }
  197. let cind_A = &cind_points[0];
  198. let cind_B = &cind_points[1];
  199. // For each invariant violator, find (or create) a Pedersen
  200. // commitment in the root disjunction branch for it.
  201. let invariant_violator_pedersens: HashMap<Ident, PedersenAssignment> = invariant_violators
  202. .drain()
  203. .map(|id| {
  204. // Check if the private Scalar is a vector variable or
  205. // not
  206. let is_vec = if let Some(TaggedIdent::Scalar(TaggedScalar { is_vec, .. })) =
  207. vars.get(&id.to_string())
  208. {
  209. *is_vec
  210. } else {
  211. false
  212. };
  213. // See if we already have a PedersenAssignment in the
  214. // root disjunction branch for this private Scalar
  215. let ped_assign = if let Some(ped_assign) = root_pedersens.get(&id) {
  216. ped_assign.clone()
  217. } else {
  218. // Create new variables for the Pedersen commitment and its
  219. // random Scalar.
  220. let commitment_var = codegen.gen_point(
  221. vars,
  222. &format_ident!("disj_{}_genC", id),
  223. is_vec, // is_vec
  224. true, // send_to_verifier
  225. );
  226. let rand_var = codegen.gen_scalar(
  227. vars,
  228. &format_ident!("disj_{}_genr", id),
  229. true, // is_rand
  230. is_vec, // is_vec
  231. );
  232. // Update vardict and randoms with the new vars
  233. vardict = taggedvardict_to_vardict(vars);
  234. randoms.insert(rand_var.to_string());
  235. let ped_assign_expr: Expr = parse_quote! {
  236. #commitment_var = #id * #cind_A + #rand_var * #cind_B
  237. };
  238. let ped_assign =
  239. recognize_pedersen_assignment(vars, &randoms, &vardict, &ped_assign_expr)
  240. .unwrap();
  241. if is_vec {
  242. codegen.prove_append(quote! {
  243. let #rand_var: Vec<Scalar> = #id
  244. .map(|_| Scalar::random(#rng_var))
  245. .collect();
  246. let #commitment_var = (0..#id.len())
  247. .map(|i| {
  248. #id[i] * #cind_A + #rand_var[i] * #cind_B
  249. })
  250. .collect();
  251. });
  252. } else {
  253. codegen.prove_append(quote! {
  254. let #rand_var = Scalar::random(#rng_var);
  255. let #ped_assign_expr;
  256. });
  257. }
  258. root_extra_statements.push(StatementTree::Leaf(ped_assign_expr));
  259. ped_assign
  260. };
  261. // At this point, we have a Pedersen commitment for some linear
  262. // function of id (given by
  263. // ped_assign.pedersen.var_term.coeff), using some linear
  264. // function of rand_var (given by
  265. // ped_assign.pedersen.rand_term.coeff) as the randomness. But
  266. // what we need is a Pedersen commitment for id itself.
  267. // So we output runtime code for both the prover and the
  268. // verifier that converts the commitment, and code for just
  269. // the prover that converts the randomness.
  270. // Make new runtime variables to hold the converted
  271. // commitment and randomness
  272. let commitment_var = codegen.gen_point(
  273. vars,
  274. &format_ident!("disj_{}_C", id),
  275. is_vec, // is_vec
  276. false, // send_to_verifier
  277. );
  278. let rand_var = codegen.gen_ident(&format_ident!("disj_{}_r", id));
  279. // Update vardict and randoms with the new vars
  280. vardict = taggedvardict_to_vardict(vars);
  281. randoms.insert(rand_var.to_string());
  282. // The identity LinScalar for this id
  283. let id_linscalar = LinScalar {
  284. coeff: 1i128,
  285. pub_scalar_expr: None,
  286. id: id.clone(),
  287. is_vec,
  288. };
  289. codegen.prove_verify_append(
  290. convert_commitment(&commitment_var, &ped_assign, &id_linscalar, &vardict).unwrap(),
  291. );
  292. codegen.prove_append(
  293. convert_randomness(&rand_var, &ped_assign, &id_linscalar, &vardict).unwrap(),
  294. );
  295. (id, ped_assign)
  296. })
  297. .collect();
  298. // Do another pass over each disjunction branch (other than the
  299. // root). In each non-root branch, if there are any instances of an
  300. // invariant violator, then change all instances of that violating
  301. // identifier to a fresh identifier, and insert a Pedersen
  302. // commitment (to the same commitment variable that exists in the
  303. // root disjunction branch) to bind the new identifier to the
  304. // original.
  305. let mut disjunction_branch_num = 0usize;
  306. st.for_each_disjunction_branch(&mut |branch, path| {
  307. // Skip the root disjunction branch, which is represented by an
  308. // empty path
  309. if path.is_empty() {
  310. return Ok(());
  311. }
  312. disjunction_branch_num += 1;
  313. // Keep track of the ids in invariant_violator_pedersens
  314. // that we encounter and rename in this disjunction branch
  315. let mut ids_renamed: HashSet<Ident> = HashSet::new();
  316. // Extra statements to be added to this disjunction branch
  317. let mut branch_extra_statements: Vec<StatementTree> = Vec::new();
  318. struct Renamer<'a> {
  319. codegen: &'a CodeGen,
  320. disjunction_branch_num: usize,
  321. invariant_violators: &'a HashMap<Ident, PedersenAssignment>,
  322. ids_renamed: &'a mut HashSet<Ident>,
  323. }
  324. impl<'a> VisitMut for Renamer<'a> {
  325. fn visit_expr_mut(&mut self, node: &mut Expr) {
  326. if let Expr::Path(expath) = node {
  327. if let Some(id) = expath.path.get_ident() {
  328. if self.invariant_violators.contains_key(id) {
  329. let replacement_ident = self.codegen.gen_ident(&format_ident!(
  330. "disj{}_{}",
  331. self.disjunction_branch_num,
  332. id
  333. ));
  334. self.ids_renamed.insert(id.clone());
  335. *node = parse_quote! { #replacement_ident };
  336. return;
  337. }
  338. }
  339. }
  340. // Unless we bailed out above, continue with the default
  341. // traversal
  342. visit_mut::visit_expr_mut(self, node);
  343. }
  344. }
  345. let mut renamer = Renamer {
  346. codegen,
  347. disjunction_branch_num,
  348. invariant_violators: &invariant_violator_pedersens,
  349. ids_renamed: &mut ids_renamed,
  350. };
  351. branch.for_each_disjunction_branch_leaf(&mut |leaf| {
  352. let StatementTree::Leaf(ref mut leafexpr) = leaf else {
  353. panic!(
  354. "Should not happen: leaf {:?} is not a StatementTree::Leaf",
  355. leaf
  356. );
  357. };
  358. renamer.visit_expr_mut(leafexpr);
  359. Ok(())
  360. })?;
  361. // For each id we renamed, insert a Pedersen commitment to the
  362. // new name (using the _same_ commitment value we computed in
  363. // the root Pedersen commitment) into this disjunction branch.
  364. // This binds the new name to the old name.
  365. for id in ids_renamed {
  366. // Is it a vector variable?
  367. let is_vec = if let Some(TaggedIdent::Scalar(TaggedScalar { is_vec, .. })) =
  368. vars.get(&id.to_string())
  369. {
  370. *is_vec
  371. } else {
  372. false
  373. };
  374. // Variables for the renamed private Scalar and the randomness
  375. let id_var = codegen.gen_scalar(
  376. vars,
  377. &format_ident!("disj{}_{}", disjunction_branch_num, id,),
  378. false, // is_rand
  379. is_vec, // is_vec
  380. );
  381. let rand_var = codegen.gen_scalar(
  382. vars,
  383. &format_ident!("disj{}_{}_r", disjunction_branch_num, id,),
  384. true, // is_rand
  385. is_vec, // is_vec
  386. );
  387. let root_commitment_var = codegen.gen_ident(&format_ident!("disj_{}_C", id));
  388. let root_rand_var = codegen.gen_ident(&format_ident!("disj_{}_r", id));
  389. if is_vec {
  390. codegen.prove_append(quote! {
  391. let #id_var = #id.clone();
  392. let #rand_var = #root_rand_var.clone();
  393. });
  394. } else {
  395. codegen.prove_append(quote! {
  396. let #id_var = #id;
  397. let #rand_var = #root_rand_var;
  398. });
  399. }
  400. branch_extra_statements.push(StatementTree::Leaf(parse_quote! {
  401. #root_commitment_var = #id_var * #cind_A + #rand_var * #cind_B
  402. }));
  403. }
  404. // Now add the branch_extra_statements to the top node of this
  405. // disjunction branch. If it's already an And node, just add
  406. // them to the vector. Otherwise, make a new And node
  407. // containing the old node and the branch_extra_statements.
  408. if let StatementTree::And(ref mut stvec) = branch {
  409. stvec.append(&mut root_extra_statements);
  410. } else {
  411. let old_branch = std::mem::replace(branch, StatementTree::leaf_true());
  412. branch_extra_statements.push(old_branch);
  413. *branch = StatementTree::And(branch_extra_statements);
  414. }
  415. Ok(())
  416. })?;
  417. // Add the root_extra_statements to the root of the StatementTree.
  418. // If it's already an And node, just add them to the vector.
  419. // Otherwise, make a new And node containing the old root and the
  420. // root_extra_statements
  421. if let StatementTree::And(ref mut stvec) = st {
  422. stvec.append(&mut root_extra_statements);
  423. } else {
  424. let old_st = std::mem::replace(st, StatementTree::leaf_true());
  425. root_extra_statements.push(old_st);
  426. *st = StatementTree::And(root_extra_statements);
  427. }
  428. // Sanity check
  429. st.check_disjunction_invariant(&vardict)
  430. }
  431. #[cfg(test)]
  432. mod tests {
  433. use super::super::syntax::taggedvardict_from_strs;
  434. use super::*;
  435. fn prune_tester(e: Expr, pruned_e: Expr) {
  436. let mut st = StatementTree::parse(&e).unwrap();
  437. prune_statement_tree(&mut st);
  438. assert_eq!(st, StatementTree::parse(&pruned_e).unwrap());
  439. }
  440. #[test]
  441. fn prune_statement_tree_test() {
  442. prune_tester(
  443. parse_quote! {
  444. AND (
  445. true,
  446. e = f,
  447. )
  448. },
  449. parse_quote! {
  450. e = f
  451. },
  452. );
  453. prune_tester(
  454. parse_quote! {
  455. AND (
  456. e = f,
  457. true,
  458. )
  459. },
  460. parse_quote! {
  461. e = f
  462. },
  463. );
  464. prune_tester(
  465. parse_quote! {
  466. AND (
  467. e = f,
  468. true,
  469. b = c,
  470. )
  471. },
  472. parse_quote! {
  473. AND (
  474. e = f,
  475. b = c,
  476. )
  477. },
  478. );
  479. prune_tester(
  480. parse_quote! {
  481. OR (
  482. true,
  483. e = f,
  484. )
  485. },
  486. parse_quote! {
  487. true
  488. },
  489. );
  490. prune_tester(
  491. parse_quote! {
  492. AND (
  493. a = b,
  494. true,
  495. OR (
  496. c = d,
  497. true,
  498. e = f
  499. )
  500. )
  501. },
  502. parse_quote! {
  503. a = b
  504. },
  505. );
  506. prune_tester(
  507. parse_quote! {
  508. THRESH (3,
  509. a = b,
  510. true,
  511. THRESH (1,
  512. c = d,
  513. true,
  514. e = f
  515. )
  516. )
  517. },
  518. parse_quote! {
  519. a = b
  520. },
  521. );
  522. prune_tester(
  523. parse_quote! {
  524. THRESH (3,
  525. a = b,
  526. true,
  527. THRESH (2,
  528. c = d,
  529. true,
  530. e = f
  531. )
  532. )
  533. },
  534. parse_quote! {
  535. THRESH (2,
  536. a = b,
  537. THRESH (1,
  538. c = d,
  539. e = f
  540. )
  541. )
  542. },
  543. );
  544. }
  545. fn enforce_disjunction_invariant_tester(vars: (&[&str], &[&str]), e: Expr, expect: Expr) {
  546. let mut codegen = CodeGen::new_empty();
  547. let mut st = StatementTree::parse(&e).unwrap();
  548. let mut vars = taggedvardict_from_strs(vars);
  549. enforce_disjunction_invariant(&mut codegen, &mut st, &mut vars).unwrap();
  550. assert_eq!(st, StatementTree::parse(&expect).unwrap());
  551. }
  552. #[test]
  553. fn enforce_disjunction_invariant_test() {
  554. let vars = (
  555. [
  556. "x", "y", "z", "pub a", "pub b", "pub c", "rand r", "rand s", "rand t",
  557. ]
  558. .as_slice(),
  559. ["C", "D", "cind A", "cind B"].as_slice(),
  560. );
  561. enforce_disjunction_invariant_tester(
  562. vars,
  563. parse_quote! {
  564. C = x*A
  565. },
  566. parse_quote! {
  567. C = x*A
  568. },
  569. );
  570. enforce_disjunction_invariant_tester(
  571. vars,
  572. parse_quote! {
  573. AND (
  574. C = x*A + r*B,
  575. OR (
  576. y=1,
  577. z=2,
  578. )
  579. )
  580. },
  581. parse_quote! {
  582. AND (
  583. C = x*A + r*B,
  584. OR (
  585. y=1,
  586. z=2,
  587. )
  588. )
  589. },
  590. );
  591. enforce_disjunction_invariant_tester(
  592. vars,
  593. parse_quote! {
  594. AND (
  595. C = x*A + r*B,
  596. OR (
  597. x=1,
  598. x=2,
  599. )
  600. )
  601. },
  602. parse_quote! {
  603. AND (
  604. C = x*A + r*B,
  605. OR (
  606. AND (
  607. gen__disj_x_C = gen__disj1_x * A + gen__disj1_x_r * B,
  608. gen__disj1_x=1,
  609. ),
  610. AND (
  611. gen__disj_x_C = gen__disj2_x * A + gen__disj2_x_r * B,
  612. gen__disj2_x=2,
  613. ),
  614. )
  615. )
  616. },
  617. );
  618. enforce_disjunction_invariant_tester(
  619. vars,
  620. parse_quote! {
  621. AND (
  622. C = x*A,
  623. OR (
  624. x=1,
  625. x=2,
  626. )
  627. )
  628. },
  629. parse_quote! {
  630. AND (
  631. C = x*A,
  632. OR (
  633. AND (
  634. gen__disj_x_C = gen__disj1_x * A + gen__disj1_x_r * B,
  635. gen__disj1_x=1,
  636. ),
  637. AND (
  638. gen__disj_x_C = gen__disj2_x * A + gen__disj2_x_r * B,
  639. gen__disj2_x=2,
  640. ),
  641. ),
  642. gen__disj_x_genC = x*A + gen__disj_x_genr*B,
  643. )
  644. },
  645. );
  646. enforce_disjunction_invariant_tester(
  647. vars,
  648. parse_quote! {
  649. OR (
  650. x=1,
  651. x=2,
  652. )
  653. },
  654. parse_quote! {
  655. AND (
  656. gen__disj_x_genC = x*A + gen__disj_x_genr*B,
  657. OR (
  658. AND (
  659. gen__disj_x_C = gen__disj1_x * A + gen__disj1_x_r * B,
  660. gen__disj1_x=1,
  661. ),
  662. AND (
  663. gen__disj_x_C = gen__disj2_x * A + gen__disj2_x_r * B,
  664. gen__disj2_x=2,
  665. ),
  666. ),
  667. )
  668. },
  669. );
  670. }
  671. }