From a38b72723492d4a3b9c2a0a626868ad7dadcb622 Mon Sep 17 00:00:00 2001 From: Thibaut Schaeffer Date: Sun, 26 Nov 2017 00:37:53 +0100 Subject: [PATCH 01/22] add private field to params. WIP --- examples/factorization.code | 2 +- examples/private.code | 13 ++++++++ out | Bin 0 -> 130 bytes out.code | 3 ++ proving.key | Bin 0 -> 2299 bytes src/absy.rs | 1 + src/flatten.rs | 3 ++ src/parser.rs | 59 +++++++++++++++++++++++++++++++++++- src/r1cs.rs | 6 +++- variables.inf | 4 +++ verification.key | 13 ++++++++ witness | 5 +++ 12 files changed, 106 insertions(+), 3 deletions(-) create mode 100644 examples/private.code create mode 100644 out create mode 100644 out.code create mode 100644 proving.key create mode 100644 variables.inf create mode 100644 verification.key create mode 100644 witness diff --git a/examples/factorization.code b/examples/factorization.code index e5da5267..4984ace0 100644 --- a/examples/factorization.code +++ b/examples/factorization.code @@ -1,4 +1,4 @@ // a and b are factorization of c -def main(c): +def main(c, private a, private b): c == a * b return 1 diff --git a/examples/private.code b/examples/private.code new file mode 100644 index 00000000..6c8a6af0 --- /dev/null +++ b/examples/private.code @@ -0,0 +1,13 @@ +// only using sub, no need to flatten +def main(x, private y): + a = 5 + b = 7 + c = if a == b then 4 else 3 fi + c == 3 + d = if a == 5 then 1 else 2 fi + d == 1 + e = if a < b then 5 else 6 fi + e == 5 + f = if b < a then 7 else 8 fi + f == 8 + return x diff --git a/out b/out new file mode 100644 index 0000000000000000000000000000000000000000..0f6635bfd706bb6a559f0098b3627a097470aaf4 GIT binary patch literal 130 zcmZQ%fB+UKotv1M#|&jNLg{1%7%Pzx#!6yjg35wukSI(h8Dtc)Kq4|H391XOoDl#= Cdjt;v literal 0 HcmV?d00001 diff --git a/out.code b/out.code new file mode 100644 index 00000000..49c4e0a8 --- /dev/null +++ b/out.code @@ -0,0 +1,3 @@ +def main(c,a,b): + c == (a * b) + return 1 diff --git a/proving.key b/proving.key new file mode 100644 index 0000000000000000000000000000000000000000..c4bbdda777295f7a11886dc100375c5ac46cb58f GIT binary patch literal 2299 zcmVw3NZ>b3NZ>WOTF|2RVQ#_v8KB7_JqXlhs&~)NbLp^=U4>bTZ?!rJF=@^ zPsx$Q?_V=5f_Zei0bEr!R?je&_`GEZ6Xee>ATTkp#x<-D@-|X@Iy^}4Y`_}``abH> zVZsQ>2%ToZUoiDCs*6fwEniS}UayY=T|8llW7ecbmk?2VL7Xfey%Y*I3Ns2Y3N#8e z3Ns2YKt<7*@?>1YB;W9{TCeQS%Ppg9BhwBj4_~9&0yfPC_8XC6bi0U>3xf7}`chSe zno4~jxIAvsw$OrlJO5lPe&i8JgR$*)@%OYvMGa`2wMDv9kO-TN{P9++&#veJb`)bb z1-t|G3%W@Ih5%~jY|^sePBUY9bX2Al(cAX~ATSa;?gVYMV|160tEp+h`YSZIiG%wk z)o6G_EN#nAMIQYAT&>Zr>xQf04o1SF`$Yf_j2Af0C?XJm{uM7=S{e#458ygE8C2YI z00v`>w-;ZuhGPYuwF>zh_hz&Ve7t%H0C#3O_dMtC2o3c5@)-p_v&Bz^%T&)UM#`L1 zGZcRiHvfT$wM5iX7IMgO_QT;t7eMq~Rt4{bU}*=UpwLPx!gz&zr5@sxGSces&|P## z4xQ@3CZEaC-_Rg!c5kT)ATW$l>)$jnga@BumxsT#;XVWpi-Aelv3aEhXtG1MMg|wW zM(1wxxpJzRqq;kjt|{S?9T?;m6AXJ4Fvk6%`6CK2TP-8GNaB+~|DvHWKsDHU<4<>%GxQic9Xj_b);2@>Xi0#q{&4HW;K3|Qymfe<*GfqphQD`^ zWuq+_ATVDfkeliYZUCTKVA7!6b1vt5%&g0ExU+|Yu!BonC>*$zz9F&TeuFUX4ZkP) zF>vR*M~`eOQ}u-U97C{hbtnop3Ns2Z3Ni{c3Ns2YM8D!4y`{ufoU<)H(gdVi-@mdH zcx&#iin>H7CXWsV+*oBnQI^KPpYJze#5~Xsse1DW=}p68aq&Aa!789DATYY@_qj#7 z^=r^@)XgJZ7W4N3($i4tD)|SGvLFCnejet}--lB>;m25QklPJ_LN<(ZuY3tG4+IcE zWiGYEw*?9?YhMt~oBl=1{WHePSnxVRZaWq2b{+C3XC9b6f>!Agd2;*eQ-v8AgZ*e? zQ#6%JxJF^VRo4Ld6KgB5AXr@uATU$~YV_0X+r-x>2TRS(*_{SoHG_?ZVXeJ@pjBYhf|=}C1GDZOJH_3#YbXQ5>|@hkGq~jhNUA^|ATXD8 zWdDD_r{?t6TuXU*M>6551%t_TcDR&ZG%M1Nf+zaP8cEneorK?C@CBr#gg|3(=|9$e z*X?ggwLQ6Sc?AkN3NW1wkHw8cUDG`a$Mq=dcnT~=d3bN5Ze}mv2b#fm3Jy9O9*Y}? zx~6*;j_Xm@@f28$^6=h9-OOIT4>W`C6dW*7-r!5;uV$tpd|BC%b>2B!+gP-=gpoF3 zQ{lFGSTQa7*t{_hPlrs7h=sUYgl>}0pgw_0?8>SlUho&lhe-o4q17lHEh?!4fhZnF z%Q#N7xvT6=ntL2C=ulM#5t}q30a0MO%edV-#-1NdswZrvrMALwWsl*XcJ&IFjkMe% zF#k4@Wqq5&M!jBxv$=x?eXaX31T<(_E8O~?wDU$$B?^X6}0 zqvDQcnFOX_8-MpY5it24D4MU#oILun!;pb8}%FUl-t*-q57SHzeq2SJ<=QR>O#G{^{COix<8$20#A<&j}E*xkJ zv4;U)V?PJohezE6X9NOYOHq$2io*0!nXV7^PKzOYlP)0Cg!xrCe*$htVaTEAlDXX^ zFs}JrG_ljTr*lXgWl3NVMMuZa=!mvNA(K#(yp{cWy$#;an$l%`c~PLIddQVI+|PEF-e)f!V#*puP?SAoDy4?NO=cL{>yDlp7j60zt3vKejT zP!dM&i*{X=WG0WR*G{mhtF-*oDk_#ZS~ia4@!E>^I|%5WMl@cSW8{#U_k3H*TJwe< zV=XYuk0>I{M>Kt;Hc(B!e&i%s1b=MQi7+FJ@f-L{h0iYq=IHY!)oqie@!WGQv4c$@ z8s+Xej{&~!SaFw6m~|2`oe>aR5Bmwdh=%nbsA~XoVOo|0Mn#Af$56CRcwyBq>a%EJ z2o*dANo!goT2!!iFa7wOOqSqj=t&1|IgmbjrIpu7w1)4=|<`0;a1)CB@yZ z`=gFEx+T;3R{?(W_)G@9QEN%xy$!B#d(hWwYs{)wMOjUU8BYWx3M*r1FnlfR&0^~W zKq@e8eJOY3^+Lz97;}+_Q!a&si4|Bs6RXyXCWasbk4qE3CUWzT)D$2p%d1za)qUQv zR=%2@2}CTQY+tH;Ak-o-w=Jr|AVwyU-0)(I6(X=R`rW>3u{Fa7ME*=L6V3Y}wY=}Y z&MFd=4hT)3%C2|E6NqK6NaXEvBvK4SjIoL(Gzu^ZG72#YGYT;ZF$y#aF$ysXF$ysX VF$ypWF$ysXFbXjWF$yvYF$(PSEcgHb literal 0 HcmV?d00001 diff --git a/src/absy.rs b/src/absy.rs index a53573de..e1408f72 100644 --- a/src/absy.rs +++ b/src/absy.rs @@ -195,6 +195,7 @@ impl fmt::Debug for Statement { #[derive(Clone, PartialEq, Serialize, Deserialize)] pub struct Parameter { pub id: String, + pub private: bool, } impl fmt::Display for Parameter { diff --git a/src/flatten.rs b/src/flatten.rs index 37f7e33f..5b74813d 100644 --- a/src/flatten.rs +++ b/src/flatten.rs @@ -424,6 +424,7 @@ impl Flattener { match param_expr.apply_substitution(&self.substitution) { Expression::Identifier(ref x) => params_flattened.push(Parameter { id: x.clone().to_string(), + private: false }), _ => { let expr_subbed = param_expr.apply_substitution(&self.substitution); @@ -439,6 +440,7 @@ impl Flattener { .push(Statement::Definition(intermediate_var.clone(), rhs)); params_flattened.push(Parameter { id: intermediate_var.clone().to_string(), + private: false }); } } @@ -626,6 +628,7 @@ impl Flattener { for arg in funct.arguments { arguments_flattened.push(Parameter { id: arg.id.to_string(), + private: arg.private }); } // flatten statements in functions and apply substitution diff --git a/src/parser.rs b/src/parser.rs index c3c133f3..f747e3f7 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -150,6 +150,7 @@ enum Token { Mult, Div, Pow, + Private, Ide(String), Num(T), Unknown(String), @@ -188,6 +189,7 @@ impl fmt::Display for Token { Token::Mult => write!(f, "*"), Token::Div => write!(f, "/"), Token::Pow => write!(f, "**"), + Token::Private => write!(f, "private"), Token::Ide(ref x) => write!(f, "{}", x), Token::Num(ref x) => write!(f, "{}", x), Token::Unknown(ref x) => write!(f, "{}", x), @@ -502,6 +504,14 @@ fn next_token(input: &String, pos: &Position) -> (Token, String, Po }, ) } + Some(_) if input[offset..].starts_with("private ") => ( + Token::Private, + input[offset + 8..].to_string(), + Position { + line: pos.line, + col: pos.col + offset + 8, + }, + ), Some(x) => match x { '0'...'9' => parse_num( &input[offset..].to_string(), @@ -1132,8 +1142,55 @@ fn parse_function( let mut p = p3; loop { match next_token(&s, &p) { + (Token::Private, s4, p4) => { + match next_token(&s4, &p4) { + (Token::Ide(x), s5, p5) => { + args.push(Parameter { id: x, private: true }); + match next_token(&s5, &p5) { + (Token::Comma, s6, p6) => { + s = s6; + p = p6; + } + (Token::Close, s5, p5) => match next_token(&s5, &p5) { + (Token::Colon, s6, p6) => match next_token(&s6, &p6) { + (Token::InlineComment(_), _, _) => break, + (Token::Unknown(ref x6), ..) if x6 == "" => break, + (t6, _, p6) => { + return Err(Error { + expected: vec![Token::Unknown("".to_string())], + got: t6, + pos: p6, + }) + } + }, + (t6, _, p6) => { + return Err(Error { + expected: vec![Token::Colon], + got: t6, + pos: p6, + }) + } + }, + (t5, _, p5) => { + return Err(Error { + expected: vec![Token::Comma, Token::Close], + got: t5, + pos: p5, + }) + } + } + } + (t5, _, p5) => { + return Err(Error { + expected: vec![Token::Comma, Token::Close], + got: t5, + pos: p5, + }) + } + } + } (Token::Ide(x), s4, p4) => { - args.push(Parameter { id: x }); + args.push(Parameter { id: x, private: false }); match next_token(&s4, &p4) { (Token::Comma, s5, p5) => { s = s5; diff --git a/src/r1cs.rs b/src/r1cs.rs index 80c0ff49..1e5b92f0 100644 --- a/src/r1cs.rs +++ b/src/r1cs.rs @@ -290,7 +290,8 @@ pub fn r1cs_program( .iter() .find(|x: &&Function| x.id == "main".to_string()) .unwrap(); - variables.extend(main.arguments.iter().map(|x| format!("{}", x))); + variables.extend(main.arguments.iter().filter(|x| x.private == false).map(|x| format!("{}", x))); + // ~out is added after main's arguments as we want variables (columns) // in the r1cs to be aligned like "public inputs | private inputs" variables.push("~out".to_string()); @@ -298,6 +299,9 @@ pub fn r1cs_program( // position where private part of witness starts let private_inputs_offset = variables.len(); + variables.extend(main.arguments.iter().filter(|x| x.private == true).map(|x| format!("{}", x))); + + for def in &main.statements { let mut a_row: Vec<(usize, T)> = Vec::new(); let mut b_row: Vec<(usize, T)> = Vec::new(); diff --git a/variables.inf b/variables.inf new file mode 100644 index 00000000..50241d18 --- /dev/null +++ b/variables.inf @@ -0,0 +1,4 @@ +Private inputs offset: +3 +R1CS variable order: +~one c ~out a b diff --git a/verification.key b/verification.key new file mode 100644 index 00000000..dfbf4750 --- /dev/null +++ b/verification.key @@ -0,0 +1,13 @@ + vk.A = [0x31794eb3a1691cc21bc9c964ee68db7ae28106b82787eef92fcae4a9c0e483, 0x2852286171b3eb1fff063874ef396d5c87d28b156a46a6ced7679780a681925e], [0x23a5d861d726720339f2861a861ee210604638ee1ead2af2c6f625d56cfda2d1, 0x16e92a3994f5a1d5809dcf62cf954fa9ae908a31b3080da065330850e9dfc543] + vk.B = 0x2b943f88d3bf0f6e2a822c6403c2c65a1d15450140b3f16a88f57e341c803b9f, 0x1c2dfce4287fb58ffe48044b396f9a988af57f58b778bbe395d73b3ebd40ac52 + vk.C = [0x17d0522fa7e63bbdbefac9977e8787dbca5493f4d5b8001478944ab0be9474d2, 0x234356e7b44810bda6a4bb5ff7a17f01cd2be0356d1477912a9b97557e428341], [0x14893eb4d934af54b57b983239d5dc3b4074d809a87399f40626d685579d41c, 0x257802281a9aa9825bc886e6d9a0251a82fa50758bcd2677019ef6612e581819] + vk.gamma = [0x2ab2532debf0b5223ec3212b4e7b0afd66a3e10b6bc24282ea9780b40b06427b, 0x68d5b8e053f64c547a4363171733e75ca6cb692eaed3fd062bb810b42731e43], [0x15b3a5a27e97d8850ccb7a8f7be16835fd069c8982852ba0a19ca6699fed1f65, 0x3f7228f46f64d11bcba6540de41036d25dcad2b05b3f7066557c0b675692cb7] + vk.gammaBeta1 = 0x27602b76a313ceecf3afd6417563cb03de4e74799dd16fef8c28171313679571, 0x10ac0cd595cfdaf433efc2d4464271c62f7dc0f4e3c6b137f11ead282f03f76c + vk.gammaBeta2 = [0x12ffa58b224c0656664d1dd439cbb6b339e4f2d28a8efd3592cb418b0bb71e7f, 0x1431c785fb238f1c42f96aed8118b3abb575dc75335435b33f3266eb796ff26c], [0x55e2b2ba927eee3bc8aecbab1a72e1702f692f66b3cfa3c41069dde61ba0649, 0x9fff9db01e86a749b3a7e47767e11fbf10c16dbc8f74379f67af61eeb3c1bba] + vk.Z = [0x11b12fe6a6dcd649d8c634e506a4aa176ca70fde632fdfda06b9b28073732517, 0x2646ea2adcd0c0726548ecaa03dae29070f95c286985c8e07c2e18863be619c1], [0x256579f8d1321a4ca8e6a807e103c2e8d08d9b88b930e9b17d4c3313a7454851, 0x225eca3599e7f392017bb5dde4df4c974422e2377828ed91a1a6b56e2f278184] + vk.IC.len() = 5 + vk.IC[0] = 0x1bb9cf704f62808123097642c9fc34dfa360451e8f8dcb6ea438793d45fa082d, 0x11729b4322acb068e76e0db12bf08825c77271879b241908d70ee7597efa4460 + vk.IC[1] = 0x2644885e567a696deb2169d46cde807af0344e5d29fd86bd2a2fd94ce07fe4a3, 0xde1853871c61add0694c4f0c86575fde5b53e504c9ae799f54726c096f5496e + vk.IC[2] = 0x1abeee45d3bb30bc7f335e4e118ce7c50252e7f5998efafe1d68b1582fd0bdeb, 0x267ff3cc655bdf4aa2eb413fd64d6782af4d763670ec3c984e36a1c10bad7064 + vk.IC[3] = 0x28f8d04e1314fff7541495e1798bd3d9e16e59c6744e42747cd71032979f6fb9, 0x2f696b7f7a693e24461c733af0252bbb55ad38af1341d98bc1e5fe1470acd13b + vk.IC[4] = 0x100dfc176ee1c80cb185857765fe74db10cf2b967ea9cf09e75955a9d3d72475, 0x2d391ecaaefbb947add78ed0ad7f2d9efec162aef33779027016018ba8c799f6 diff --git a/witness b/witness new file mode 100644 index 00000000..45e75d8c --- /dev/null +++ b/witness @@ -0,0 +1,5 @@ +~out 1 +a 2 +~one 1 +c 8 +b 4 From bd64a5a7b105d36c4f8d9bb64c2f506a81236829 Mon Sep 17 00:00:00 2001 From: Thibaut Schaeffer Date: Sun, 26 Nov 2017 00:39:56 +0100 Subject: [PATCH 02/22] remove artifacts --- out | Bin 130 -> 0 bytes out.code | 3 --- proving.key | Bin 2299 -> 0 bytes variables.inf | 4 ---- verification.key | 13 ------------- witness | 5 ----- 6 files changed, 25 deletions(-) delete mode 100644 out delete mode 100644 out.code delete mode 100644 proving.key delete mode 100644 variables.inf delete mode 100644 verification.key delete mode 100644 witness diff --git a/out b/out deleted file mode 100644 index 0f6635bfd706bb6a559f0098b3627a097470aaf4..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 130 zcmZQ%fB+UKotv1M#|&jNLg{1%7%Pzx#!6yjg35wukSI(h8Dtc)Kq4|H391XOoDl#= Cdjt;v diff --git a/out.code b/out.code deleted file mode 100644 index 49c4e0a8..00000000 --- a/out.code +++ /dev/null @@ -1,3 +0,0 @@ -def main(c,a,b): - c == (a * b) - return 1 diff --git a/proving.key b/proving.key deleted file mode 100644 index c4bbdda777295f7a11886dc100375c5ac46cb58f..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 2299 zcmVw3NZ>b3NZ>WOTF|2RVQ#_v8KB7_JqXlhs&~)NbLp^=U4>bTZ?!rJF=@^ zPsx$Q?_V=5f_Zei0bEr!R?je&_`GEZ6Xee>ATTkp#x<-D@-|X@Iy^}4Y`_}``abH> zVZsQ>2%ToZUoiDCs*6fwEniS}UayY=T|8llW7ecbmk?2VL7Xfey%Y*I3Ns2Y3N#8e z3Ns2YKt<7*@?>1YB;W9{TCeQS%Ppg9BhwBj4_~9&0yfPC_8XC6bi0U>3xf7}`chSe zno4~jxIAvsw$OrlJO5lPe&i8JgR$*)@%OYvMGa`2wMDv9kO-TN{P9++&#veJb`)bb z1-t|G3%W@Ih5%~jY|^sePBUY9bX2Al(cAX~ATSa;?gVYMV|160tEp+h`YSZIiG%wk z)o6G_EN#nAMIQYAT&>Zr>xQf04o1SF`$Yf_j2Af0C?XJm{uM7=S{e#458ygE8C2YI z00v`>w-;ZuhGPYuwF>zh_hz&Ve7t%H0C#3O_dMtC2o3c5@)-p_v&Bz^%T&)UM#`L1 zGZcRiHvfT$wM5iX7IMgO_QT;t7eMq~Rt4{bU}*=UpwLPx!gz&zr5@sxGSces&|P## z4xQ@3CZEaC-_Rg!c5kT)ATW$l>)$jnga@BumxsT#;XVWpi-Aelv3aEhXtG1MMg|wW zM(1wxxpJzRqq;kjt|{S?9T?;m6AXJ4Fvk6%`6CK2TP-8GNaB+~|DvHWKsDHU<4<>%GxQic9Xj_b);2@>Xi0#q{&4HW;K3|Qymfe<*GfqphQD`^ zWuq+_ATVDfkeliYZUCTKVA7!6b1vt5%&g0ExU+|Yu!BonC>*$zz9F&TeuFUX4ZkP) zF>vR*M~`eOQ}u-U97C{hbtnop3Ns2Z3Ni{c3Ns2YM8D!4y`{ufoU<)H(gdVi-@mdH zcx&#iin>H7CXWsV+*oBnQI^KPpYJze#5~Xsse1DW=}p68aq&Aa!789DATYY@_qj#7 z^=r^@)XgJZ7W4N3($i4tD)|SGvLFCnejet}--lB>;m25QklPJ_LN<(ZuY3tG4+IcE zWiGYEw*?9?YhMt~oBl=1{WHePSnxVRZaWq2b{+C3XC9b6f>!Agd2;*eQ-v8AgZ*e? zQ#6%JxJF^VRo4Ld6KgB5AXr@uATU$~YV_0X+r-x>2TRS(*_{SoHG_?ZVXeJ@pjBYhf|=}C1GDZOJH_3#YbXQ5>|@hkGq~jhNUA^|ATXD8 zWdDD_r{?t6TuXU*M>6551%t_TcDR&ZG%M1Nf+zaP8cEneorK?C@CBr#gg|3(=|9$e z*X?ggwLQ6Sc?AkN3NW1wkHw8cUDG`a$Mq=dcnT~=d3bN5Ze}mv2b#fm3Jy9O9*Y}? zx~6*;j_Xm@@f28$^6=h9-OOIT4>W`C6dW*7-r!5;uV$tpd|BC%b>2B!+gP-=gpoF3 zQ{lFGSTQa7*t{_hPlrs7h=sUYgl>}0pgw_0?8>SlUho&lhe-o4q17lHEh?!4fhZnF z%Q#N7xvT6=ntL2C=ulM#5t}q30a0MO%edV-#-1NdswZrvrMALwWsl*XcJ&IFjkMe% zF#k4@Wqq5&M!jBxv$=x?eXaX31T<(_E8O~?wDU$$B?^X6}0 zqvDQcnFOX_8-MpY5it24D4MU#oILun!;pb8}%FUl-t*-q57SHzeq2SJ<=QR>O#G{^{COix<8$20#A<&j}E*xkJ zv4;U)V?PJohezE6X9NOYOHq$2io*0!nXV7^PKzOYlP)0Cg!xrCe*$htVaTEAlDXX^ zFs}JrG_ljTr*lXgWl3NVMMuZa=!mvNA(K#(yp{cWy$#;an$l%`c~PLIddQVI+|PEF-e)f!V#*puP?SAoDy4?NO=cL{>yDlp7j60zt3vKejT zP!dM&i*{X=WG0WR*G{mhtF-*oDk_#ZS~ia4@!E>^I|%5WMl@cSW8{#U_k3H*TJwe< zV=XYuk0>I{M>Kt;Hc(B!e&i%s1b=MQi7+FJ@f-L{h0iYq=IHY!)oqie@!WGQv4c$@ z8s+Xej{&~!SaFw6m~|2`oe>aR5Bmwdh=%nbsA~XoVOo|0Mn#Af$56CRcwyBq>a%EJ z2o*dANo!goT2!!iFa7wOOqSqj=t&1|IgmbjrIpu7w1)4=|<`0;a1)CB@yZ z`=gFEx+T;3R{?(W_)G@9QEN%xy$!B#d(hWwYs{)wMOjUU8BYWx3M*r1FnlfR&0^~W zKq@e8eJOY3^+Lz97;}+_Q!a&si4|Bs6RXyXCWasbk4qE3CUWzT)D$2p%d1za)qUQv zR=%2@2}CTQY+tH;Ak-o-w=Jr|AVwyU-0)(I6(X=R`rW>3u{Fa7ME*=L6V3Y}wY=}Y z&MFd=4hT)3%C2|E6NqK6NaXEvBvK4SjIoL(Gzu^ZG72#YGYT;ZF$y#aF$ysXF$ysX VF$ypWF$ysXFbXjWF$yvYF$(PSEcgHb diff --git a/variables.inf b/variables.inf deleted file mode 100644 index 50241d18..00000000 --- a/variables.inf +++ /dev/null @@ -1,4 +0,0 @@ -Private inputs offset: -3 -R1CS variable order: -~one c ~out a b diff --git a/verification.key b/verification.key deleted file mode 100644 index dfbf4750..00000000 --- a/verification.key +++ /dev/null @@ -1,13 +0,0 @@ - vk.A = [0x31794eb3a1691cc21bc9c964ee68db7ae28106b82787eef92fcae4a9c0e483, 0x2852286171b3eb1fff063874ef396d5c87d28b156a46a6ced7679780a681925e], [0x23a5d861d726720339f2861a861ee210604638ee1ead2af2c6f625d56cfda2d1, 0x16e92a3994f5a1d5809dcf62cf954fa9ae908a31b3080da065330850e9dfc543] - vk.B = 0x2b943f88d3bf0f6e2a822c6403c2c65a1d15450140b3f16a88f57e341c803b9f, 0x1c2dfce4287fb58ffe48044b396f9a988af57f58b778bbe395d73b3ebd40ac52 - vk.C = [0x17d0522fa7e63bbdbefac9977e8787dbca5493f4d5b8001478944ab0be9474d2, 0x234356e7b44810bda6a4bb5ff7a17f01cd2be0356d1477912a9b97557e428341], [0x14893eb4d934af54b57b983239d5dc3b4074d809a87399f40626d685579d41c, 0x257802281a9aa9825bc886e6d9a0251a82fa50758bcd2677019ef6612e581819] - vk.gamma = [0x2ab2532debf0b5223ec3212b4e7b0afd66a3e10b6bc24282ea9780b40b06427b, 0x68d5b8e053f64c547a4363171733e75ca6cb692eaed3fd062bb810b42731e43], [0x15b3a5a27e97d8850ccb7a8f7be16835fd069c8982852ba0a19ca6699fed1f65, 0x3f7228f46f64d11bcba6540de41036d25dcad2b05b3f7066557c0b675692cb7] - vk.gammaBeta1 = 0x27602b76a313ceecf3afd6417563cb03de4e74799dd16fef8c28171313679571, 0x10ac0cd595cfdaf433efc2d4464271c62f7dc0f4e3c6b137f11ead282f03f76c - vk.gammaBeta2 = [0x12ffa58b224c0656664d1dd439cbb6b339e4f2d28a8efd3592cb418b0bb71e7f, 0x1431c785fb238f1c42f96aed8118b3abb575dc75335435b33f3266eb796ff26c], [0x55e2b2ba927eee3bc8aecbab1a72e1702f692f66b3cfa3c41069dde61ba0649, 0x9fff9db01e86a749b3a7e47767e11fbf10c16dbc8f74379f67af61eeb3c1bba] - vk.Z = [0x11b12fe6a6dcd649d8c634e506a4aa176ca70fde632fdfda06b9b28073732517, 0x2646ea2adcd0c0726548ecaa03dae29070f95c286985c8e07c2e18863be619c1], [0x256579f8d1321a4ca8e6a807e103c2e8d08d9b88b930e9b17d4c3313a7454851, 0x225eca3599e7f392017bb5dde4df4c974422e2377828ed91a1a6b56e2f278184] - vk.IC.len() = 5 - vk.IC[0] = 0x1bb9cf704f62808123097642c9fc34dfa360451e8f8dcb6ea438793d45fa082d, 0x11729b4322acb068e76e0db12bf08825c77271879b241908d70ee7597efa4460 - vk.IC[1] = 0x2644885e567a696deb2169d46cde807af0344e5d29fd86bd2a2fd94ce07fe4a3, 0xde1853871c61add0694c4f0c86575fde5b53e504c9ae799f54726c096f5496e - vk.IC[2] = 0x1abeee45d3bb30bc7f335e4e118ce7c50252e7f5998efafe1d68b1582fd0bdeb, 0x267ff3cc655bdf4aa2eb413fd64d6782af4d763670ec3c984e36a1c10bad7064 - vk.IC[3] = 0x28f8d04e1314fff7541495e1798bd3d9e16e59c6744e42747cd71032979f6fb9, 0x2f696b7f7a693e24461c733af0252bbb55ad38af1341d98bc1e5fe1470acd13b - vk.IC[4] = 0x100dfc176ee1c80cb185857765fe74db10cf2b967ea9cf09e75955a9d3d72475, 0x2d391ecaaefbb947add78ed0ad7f2d9efec162aef33779027016018ba8c799f6 diff --git a/witness b/witness deleted file mode 100644 index 45e75d8c..00000000 --- a/witness +++ /dev/null @@ -1,5 +0,0 @@ -~out 1 -a 2 -~one 1 -c 8 -b 4 From 580a83e988de98a2e8174d2d28a6e75ad9135c32 Mon Sep 17 00:00:00 2001 From: Thibaut Schaeffer Date: Sun, 26 Nov 2017 13:25:40 +0100 Subject: [PATCH 03/22] fixing wrong input size --- out | Bin 0 -> 130 bytes out.code | 3 +++ proving.key | Bin 0 -> 2299 bytes src/absy.rs | 3 ++- src/main.rs | 2 ++ src/r1cs.rs | 13 +++---------- variables.inf | 4 ++++ verification.key | 13 +++++++++++++ witness | 5 +++++ 9 files changed, 32 insertions(+), 11 deletions(-) create mode 100644 out create mode 100644 out.code create mode 100644 proving.key create mode 100644 variables.inf create mode 100644 verification.key create mode 100644 witness diff --git a/out b/out new file mode 100644 index 0000000000000000000000000000000000000000..0f6635bfd706bb6a559f0098b3627a097470aaf4 GIT binary patch literal 130 zcmZQ%fB+UKotv1M#|&jNLg{1%7%Pzx#!6yjg35wukSI(h8Dtc)Kq4|H391XOoDl#= Cdjt;v literal 0 HcmV?d00001 diff --git a/out.code b/out.code new file mode 100644 index 00000000..4f47d3eb --- /dev/null +++ b/out.code @@ -0,0 +1,3 @@ +def main(c,private a,private b): + c == (a * b) + return 1 diff --git a/proving.key b/proving.key new file mode 100644 index 0000000000000000000000000000000000000000..181d3ef10a2b61b2f0bf8c11dd137353e43099ca GIT binary patch literal 2299 zcmVw3NZ>b3NZ>WOfZ$B74JJP=Uh$@`35NnBA%?X9|cf$Ttc`M#crx7w%|6# z{CeFU#{R8ATS;^h4qX`MNPU2Ma?=xAF58S1}G&m z9QirrLzERLycUtKhR?*t0!q^{=4^}?ua4NrqX_zIJ3Ns2Y3N#8e z3Ns2YYtEyS0cs7SpQyVK$VnZ7tJv9rqv9*6kO|pQaOy@Q1@Fo$B0(2UYggT(Pf6R$ zFG+_CSf3=3*@0~RhDtUUbv5X1D?RAQxCWMK6?9^YR=BK40LLIiKpkWM0YTInAOz{7 zyW!yc(8_@B>bjnElLH-amY0{C5YXwB@ksV5ATT-b85q7nGKc&ad|m)?1IwT`?|*Mg zr-`xpV0F~^MIs@&<_WdP?1q&rSH?QK+Is?i?M_&TXX+=5*9qo@dKU^XJWY0)Hj>uw z0A2r(md9?+)l$q%;(U0TNCfZN&WRBYI}74CFj*-M*0?+Si-ntMc=iNQ_5vC$Ch+9Q!1Gr9>dytt=3B!fURD90?nj$Lek|?;5iSG z(2gtV?Ca&15e|qhg;x?RATT;z{NAgyxZY(H*2_I-$a)`g3*#ft`9kJwK>zqXphW(cOs6Fpc%x?I)R7hMWsNbx2&;$gNKw1uKEU+vnW~p7Nu!Fhk zy@!pwt!XBVPQ~g*rfAiSilE*A%af!5IH(bzzDA!@Vr%09FH6{e5XUf|0s{y@EU2H* z`=ez5ATX?P*|>^!j{G-Mj+a_Kqz(jOBNh}8ZSQ#PYTx=)vlTC>?m>IyfwH+VLVCsG z+UqX*Hg^FdW#Q^B;0J>j5C#f13Ns2Z3Ni{c3Ns2YKj+i#5nZLNXPO4W$=>l75le;D zUz%ehm5-c>G;AdUEmU!|xn=_~KJsWVYpGmmjCSYU=`U1+bjFj0>WZNaATR+Ey0Z&# zC6X(;G*%qYN8Y4Oe=f|9uVfn;MuObb+XP1?9!YNn@}`{2$T`CoPrq~a&?`H93_laL z)lmF6_b3W5He18bK@ktq7bSOFSmuhSK{0g%B`&$9UI$X)JEIIB<=swW^Z!v0RyR9< z^`7_Lla$+eNJwDU=!rK>LmE3GATWoQSnIV7ZN@_dMY1uB;MkZ{8yzL;4S^5?#Jqi( z;wtI3c)_#`*qJg8$bpy5Hy;u@9f!8C5T*I~BHtLRlnM$khGqOkd9K1$0HU)`YJEsH z8~tzX?O{NJCkFrxD0MroZfh?d<9PP|D^OATS73 z5T&pdA0|mrf)PW%hkpya^AI6=4UTVFaRM7-l?u59NE~v(%9zGVlh$W`C6dW)-?g+4XX$FEct_I$lFtm{BJesG?1)3%6OkkWf|?a=i^O)gsfoa^*3m&Xd^% zqnEOB#}QFQB^PIWHRE6{qXym{PFua6VIWNsMteK_6`=DA5hPlk{=|M*)Ux^R%|o*n zFrGP@w`B-~)a%gG6kOYwBy}0~L_r?4nNDKTB|?^vDl~7HeYrT^2T={Nfn(`=Ph*W5 zR1!7#gbx3I8{`>p1Te$-Nt~K(Qtj^~OW@fTHhX*5miLh0A=O3wq%k_=S1tUB0;WCO zlfAJcmpD_Ubn{eaPa}QBkVwZK6z=#BLLD%6ms;?jHw)uXNh}kgYBQl9yX*o`Gqdp zCwG;Z#c~G^8&&_kC%2sCj759cEeB3dT!BK@y&Vk4;9Naf1!v_eFfdJidXB8}T~ESB zrA%*0u{}BZ^(s~khrVZH+)kpWN*Fn!W=@T%t@Fr9qhg~S4xMs<(?J)Yo7jSE!mC{m{c)D&*G!=JzcXl3|YepKt3PMDJ?ddR=jO1|eJqq%T+) z<-0+ki7}Z}#4j^-H{hsysx^i&#WJmwg*woej_&kLBQVk@j%_nJ!=`v)aH$d(afQyWBR?)=&aYs zWusvB>rAA+H$X{;UG?uD;|WdiO6R zpOZ6ltt$E(o9OwBIb=ypWot9&)eo#fZtNQ-Gzu^ZG72#YGYT;ZF$y#aF$ysXF$ysX VF$ypWF$ysXFbXjWF$yvYF$zr>CQASS literal 0 HcmV?d00001 diff --git a/src/absy.rs b/src/absy.rs index e1408f72..122b54a2 100644 --- a/src/absy.rs +++ b/src/absy.rs @@ -200,7 +200,8 @@ pub struct Parameter { impl fmt::Display for Parameter { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - write!(f, "{}", self.id) + let visibility = if self.private { "private " } else { "" }; + write!(f, "{}{}", visibility, self.id) } } diff --git a/src/main.rs b/src/main.rs index 48789d31..8acb6520 100644 --- a/src/main.rs +++ b/src/main.rs @@ -357,6 +357,7 @@ fn main() { // transform to R1CS let (variables, private_inputs_offset, a, b, c) = r1cs_program(&program_ast); + println!("\nvars\n{:?}\noffset\n{:?}\na\n{:?}\nb\n{:?}\nc\n{:?}", variables, private_inputs_offset, a, b, c); // write variables meta information to file let var_inf_path = Path::new(sub_matches.value_of("meta-information").unwrap()); @@ -507,6 +508,7 @@ fn main() { } println!("Using Witness: {:?}", witness_map); + println!("{:?}", variables); let witness: Vec<_> = variables.iter().map(|x| witness_map[x].clone()).collect(); diff --git a/src/r1cs.rs b/src/r1cs.rs index 1e5b92f0..421c4613 100644 --- a/src/r1cs.rs +++ b/src/r1cs.rs @@ -290,7 +290,7 @@ pub fn r1cs_program( .iter() .find(|x: &&Function| x.id == "main".to_string()) .unwrap(); - variables.extend(main.arguments.iter().filter(|x| x.private == false).map(|x| format!("{}", x))); + variables.extend(main.arguments.iter().filter(|x| !x.private).map(|x| format!("{}", x))); // ~out is added after main's arguments as we want variables (columns) // in the r1cs to be aligned like "public inputs | private inputs" @@ -299,7 +299,7 @@ pub fn r1cs_program( // position where private part of witness starts let private_inputs_offset = variables.len(); - variables.extend(main.arguments.iter().filter(|x| x.private == true).map(|x| format!("{}", x))); + //variables.extend(main.arguments.iter().filter(|x| x.private).map(|x| format!("{}", x.id.to_string()))); for def in &main.statements { @@ -315,14 +315,7 @@ pub fn r1cs_program( &mut b_row, &mut c_row, ), - Statement::Definition(ref id, ref expr) => r1cs_expression( - Identifier(id.to_string()), - expr.clone(), - &mut variables, - &mut a_row, - &mut b_row, - &mut c_row, - ), + Statement::Definition(ref id, ref expr) => continue, Statement::Condition(ref expr1, ref expr2) => r1cs_expression( expr1.clone(), expr2.clone(), diff --git a/variables.inf b/variables.inf new file mode 100644 index 00000000..50241d18 --- /dev/null +++ b/variables.inf @@ -0,0 +1,4 @@ +Private inputs offset: +3 +R1CS variable order: +~one c ~out a b diff --git a/verification.key b/verification.key new file mode 100644 index 00000000..5a71b721 --- /dev/null +++ b/verification.key @@ -0,0 +1,13 @@ + vk.A = [0x266e7eaf966e822ad67df2910d73845a5f6f84357b9a4b9f268f86132af68acc, 0x28e8d74d1acabb6f12b677b104dbdede11dc65d996aff7024379878cfdbee0ac], [0x1c44d164d2a2cc9ad9d1cf657a79e1aca93418f7bfdf23038d108a207e85947d, 0x69c08ecfae6f687d6169fb8e0bda5928d4cecf6c0594156ee4d524b155605f1] + vk.B = 0xa1f97fbcf835a5d6c5bbfa51271c777becf9258ca44ebf5ea95f6623ca5ec3d, 0x1cfb02b14ecc2afe1d28442daeff2de5ddb32666824b52172a5004b37b01e1b8 + vk.C = [0x20bc704965f49aabab8cb48662d44e7607507a77d5a0b534854d4f41f291686a, 0x12b4846c1a68e1d5532cdb0d8845ad647ac342d3f59fab0bb38c3ee54c87cfa9], [0x2e68a6b86a772c0c3795b0408d055ed11f5edd820e37cb12ed64b3bb437cf689, 0xe63fac1b2b5b701a6e1c2434f1d2d2e14ab447b54201663d7d11acd4f742697] + vk.gamma = [0x2f83d95a24903e869333837260e4cfe093d38c793a2f0fb729c0151b4de1d12c, 0x24f2703c855f1fe175710638f4285a87e4f5c0eb44d9dd244e4f0f122bd6388], [0x11099e7a5417fdf1d7187e0758897e7b23ee416d17a89102593d45a7382d4517, 0x191d11e8bd087b2149eae6bd39b18d8dc52cb66f7d4e11f1cb287503a25c2672] + vk.gammaBeta1 = 0x26dba0aa9489f99298b132d71dad6b357ae3966eb779a1627e976403516c9d2b, 0x121fa218710bdc8c46e04189de8fc87c71c38b20d1bc308d6b6776ff3f40e58e + vk.gammaBeta2 = [0x2cf8945fa72e7888350cfb628dbd51a410c70c9ccd894eeac8e7cec7c1247112, 0x25b814c38b7a1688d330e65227c42c938ac9dbb726ed739429e2620224bcbe41], [0x515716d220659ee56d101f6decba47448f2f08a90a4a8356dcbf8f52a01fa42, 0x269fc99862f80116d8056e37561f0af799d662b07d5f5f3f026577af24de8e04] + vk.Z = [0x8177f58bf220749854973a5506c50e2322d2e71e3b37a541769912309632624, 0x24809a8325352314065f4358b2a5add05bac35bda0c97b076fadd3fe5bb970e4], [0x368bdbb340065e8c1c32ea178cccc07db257dbb9aba5db1f42a39deb990d838, 0x2937bd2682119fdc74b462c58f77b9c1c8f59fc9f39d953caacfa25b2640e289] + vk.IC.len() = 5 + vk.IC[0] = 0x2c6a375ea005c3b538be391c1cf3e247e92307d99946c270432cc70962537cd4, 0xe618adba9796b2d5620f344168500268f92707cd4695b1967571b7a74caf6f6 + vk.IC[1] = 0x296202906feb10bfa6c362faca9ec6cb093a56c3c9449facb5151be67e139277, 0x260e867ec4581cc8c709341b2919fe867c7740f1b624e9921120abafea857ac6 + vk.IC[2] = 0x13d7b366f4703d9b50c8f1acdd7e7956f04f129c3d620ec4d27f92c55dc7979c, 0xfac1a26e067d3e05e10d7ec7c236ab463100e822191a13bca37cc613e521746 + vk.IC[3] = 0x14ba5755c2cfa6a606bbe66611d2528ae7f20bac1a96712959d5099a02d11907, 0x13316e64b46d2f18a649803da0621a150af3076039d1597d505f1f073fe231a8 + vk.IC[4] = 0x1c459f97b080e17647b1937a9dfedb48caf92d6f08097d16bb82070bb832ea55, 0x2ff33110d33bb728b2dec637238b07a59747fe0928b87c7e590c2a1585fddd67 diff --git a/witness b/witness new file mode 100644 index 00000000..5bdbf191 --- /dev/null +++ b/witness @@ -0,0 +1,5 @@ +c 8 +b 4 +~one 1 +a 2 +~out 1 From 4d13959fa09c57f66f4f9d6ee67814d38e0f4790 Mon Sep 17 00:00:00 2001 From: Thibaut Schaeffer Date: Sun, 26 Nov 2017 13:52:55 +0100 Subject: [PATCH 04/22] fix wrong number of inputs for setup, clean --- out | Bin 130 -> 0 bytes out.code | 3 --- proving.key | Bin 2299 -> 0 bytes src/main.rs | 3 +-- variables.inf | 4 ---- verification.key | 13 ------------- witness | 5 ----- 7 files changed, 1 insertion(+), 27 deletions(-) delete mode 100644 out delete mode 100644 out.code delete mode 100644 proving.key delete mode 100644 variables.inf delete mode 100644 verification.key delete mode 100644 witness diff --git a/out b/out deleted file mode 100644 index 0f6635bfd706bb6a559f0098b3627a097470aaf4..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 130 zcmZQ%fB+UKotv1M#|&jNLg{1%7%Pzx#!6yjg35wukSI(h8Dtc)Kq4|H391XOoDl#= Cdjt;v diff --git a/out.code b/out.code deleted file mode 100644 index 4f47d3eb..00000000 --- a/out.code +++ /dev/null @@ -1,3 +0,0 @@ -def main(c,private a,private b): - c == (a * b) - return 1 diff --git a/proving.key b/proving.key deleted file mode 100644 index 181d3ef10a2b61b2f0bf8c11dd137353e43099ca..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 2299 zcmVw3NZ>b3NZ>WOfZ$B74JJP=Uh$@`35NnBA%?X9|cf$Ttc`M#crx7w%|6# z{CeFU#{R8ATS;^h4qX`MNPU2Ma?=xAF58S1}G&m z9QirrLzERLycUtKhR?*t0!q^{=4^}?ua4NrqX_zIJ3Ns2Y3N#8e z3Ns2YYtEyS0cs7SpQyVK$VnZ7tJv9rqv9*6kO|pQaOy@Q1@Fo$B0(2UYggT(Pf6R$ zFG+_CSf3=3*@0~RhDtUUbv5X1D?RAQxCWMK6?9^YR=BK40LLIiKpkWM0YTInAOz{7 zyW!yc(8_@B>bjnElLH-amY0{C5YXwB@ksV5ATT-b85q7nGKc&ad|m)?1IwT`?|*Mg zr-`xpV0F~^MIs@&<_WdP?1q&rSH?QK+Is?i?M_&TXX+=5*9qo@dKU^XJWY0)Hj>uw z0A2r(md9?+)l$q%;(U0TNCfZN&WRBYI}74CFj*-M*0?+Si-ntMc=iNQ_5vC$Ch+9Q!1Gr9>dytt=3B!fURD90?nj$Lek|?;5iSG z(2gtV?Ca&15e|qhg;x?RATT;z{NAgyxZY(H*2_I-$a)`g3*#ft`9kJwK>zqXphW(cOs6Fpc%x?I)R7hMWsNbx2&;$gNKw1uKEU+vnW~p7Nu!Fhk zy@!pwt!XBVPQ~g*rfAiSilE*A%af!5IH(bzzDA!@Vr%09FH6{e5XUf|0s{y@EU2H* z`=ez5ATX?P*|>^!j{G-Mj+a_Kqz(jOBNh}8ZSQ#PYTx=)vlTC>?m>IyfwH+VLVCsG z+UqX*Hg^FdW#Q^B;0J>j5C#f13Ns2Z3Ni{c3Ns2YKj+i#5nZLNXPO4W$=>l75le;D zUz%ehm5-c>G;AdUEmU!|xn=_~KJsWVYpGmmjCSYU=`U1+bjFj0>WZNaATR+Ey0Z&# zC6X(;G*%qYN8Y4Oe=f|9uVfn;MuObb+XP1?9!YNn@}`{2$T`CoPrq~a&?`H93_laL z)lmF6_b3W5He18bK@ktq7bSOFSmuhSK{0g%B`&$9UI$X)JEIIB<=swW^Z!v0RyR9< z^`7_Lla$+eNJwDU=!rK>LmE3GATWoQSnIV7ZN@_dMY1uB;MkZ{8yzL;4S^5?#Jqi( z;wtI3c)_#`*qJg8$bpy5Hy;u@9f!8C5T*I~BHtLRlnM$khGqOkd9K1$0HU)`YJEsH z8~tzX?O{NJCkFrxD0MroZfh?d<9PP|D^OATS73 z5T&pdA0|mrf)PW%hkpya^AI6=4UTVFaRM7-l?u59NE~v(%9zGVlh$W`C6dW)-?g+4XX$FEct_I$lFtm{BJesG?1)3%6OkkWf|?a=i^O)gsfoa^*3m&Xd^% zqnEOB#}QFQB^PIWHRE6{qXym{PFua6VIWNsMteK_6`=DA5hPlk{=|M*)Ux^R%|o*n zFrGP@w`B-~)a%gG6kOYwBy}0~L_r?4nNDKTB|?^vDl~7HeYrT^2T={Nfn(`=Ph*W5 zR1!7#gbx3I8{`>p1Te$-Nt~K(Qtj^~OW@fTHhX*5miLh0A=O3wq%k_=S1tUB0;WCO zlfAJcmpD_Ubn{eaPa}QBkVwZK6z=#BLLD%6ms;?jHw)uXNh}kgYBQl9yX*o`Gqdp zCwG;Z#c~G^8&&_kC%2sCj759cEeB3dT!BK@y&Vk4;9Naf1!v_eFfdJidXB8}T~ESB zrA%*0u{}BZ^(s~khrVZH+)kpWN*Fn!W=@T%t@Fr9qhg~S4xMs<(?J)Yo7jSE!mC{m{c)D&*G!=JzcXl3|YepKt3PMDJ?ddR=jO1|eJqq%T+) z<-0+ki7}Z}#4j^-H{hsysx^i&#WJmwg*woej_&kLBQVk@j%_nJ!=`v)aH$d(afQyWBR?)=&aYs zWusvB>rAA+H$X{;UG?uD;|WdiO6R zpOZ6ltt$E(o9OwBIb=ypWot9&)eo#fZtNQ-Gzu^ZG72#YGYT;ZF$y#aF$ysXF$ysX VF$ypWF$ysXFbXjWF$yvYF$zr>CQASS diff --git a/src/main.rs b/src/main.rs index 8acb6520..4a4ea805 100644 --- a/src/main.rs +++ b/src/main.rs @@ -357,7 +357,6 @@ fn main() { // transform to R1CS let (variables, private_inputs_offset, a, b, c) = r1cs_program(&program_ast); - println!("\nvars\n{:?}\noffset\n{:?}\na\n{:?}\nb\n{:?}\nc\n{:?}", variables, private_inputs_offset, a, b, c); // write variables meta information to file let var_inf_path = Path::new(sub_matches.value_of("meta-information").unwrap()); @@ -382,7 +381,7 @@ fn main() { // run setup phase #[cfg(not(feature="nolibsnark"))]{ // number of inputs in the zkSNARK sense, i.e., input variables + output variables - let num_inputs = main_flattened.arguments.len() + 1; //currently exactly one output variable + let num_inputs = main_flattened.arguments.iter().filter(|x| !x.private).count() + 1; println!("setup successful: {:?}", setup(variables, a, b, c, num_inputs, pk_path, vk_path)); } } diff --git a/variables.inf b/variables.inf deleted file mode 100644 index 50241d18..00000000 --- a/variables.inf +++ /dev/null @@ -1,4 +0,0 @@ -Private inputs offset: -3 -R1CS variable order: -~one c ~out a b diff --git a/verification.key b/verification.key deleted file mode 100644 index 5a71b721..00000000 --- a/verification.key +++ /dev/null @@ -1,13 +0,0 @@ - vk.A = [0x266e7eaf966e822ad67df2910d73845a5f6f84357b9a4b9f268f86132af68acc, 0x28e8d74d1acabb6f12b677b104dbdede11dc65d996aff7024379878cfdbee0ac], [0x1c44d164d2a2cc9ad9d1cf657a79e1aca93418f7bfdf23038d108a207e85947d, 0x69c08ecfae6f687d6169fb8e0bda5928d4cecf6c0594156ee4d524b155605f1] - vk.B = 0xa1f97fbcf835a5d6c5bbfa51271c777becf9258ca44ebf5ea95f6623ca5ec3d, 0x1cfb02b14ecc2afe1d28442daeff2de5ddb32666824b52172a5004b37b01e1b8 - vk.C = [0x20bc704965f49aabab8cb48662d44e7607507a77d5a0b534854d4f41f291686a, 0x12b4846c1a68e1d5532cdb0d8845ad647ac342d3f59fab0bb38c3ee54c87cfa9], [0x2e68a6b86a772c0c3795b0408d055ed11f5edd820e37cb12ed64b3bb437cf689, 0xe63fac1b2b5b701a6e1c2434f1d2d2e14ab447b54201663d7d11acd4f742697] - vk.gamma = [0x2f83d95a24903e869333837260e4cfe093d38c793a2f0fb729c0151b4de1d12c, 0x24f2703c855f1fe175710638f4285a87e4f5c0eb44d9dd244e4f0f122bd6388], [0x11099e7a5417fdf1d7187e0758897e7b23ee416d17a89102593d45a7382d4517, 0x191d11e8bd087b2149eae6bd39b18d8dc52cb66f7d4e11f1cb287503a25c2672] - vk.gammaBeta1 = 0x26dba0aa9489f99298b132d71dad6b357ae3966eb779a1627e976403516c9d2b, 0x121fa218710bdc8c46e04189de8fc87c71c38b20d1bc308d6b6776ff3f40e58e - vk.gammaBeta2 = [0x2cf8945fa72e7888350cfb628dbd51a410c70c9ccd894eeac8e7cec7c1247112, 0x25b814c38b7a1688d330e65227c42c938ac9dbb726ed739429e2620224bcbe41], [0x515716d220659ee56d101f6decba47448f2f08a90a4a8356dcbf8f52a01fa42, 0x269fc99862f80116d8056e37561f0af799d662b07d5f5f3f026577af24de8e04] - vk.Z = [0x8177f58bf220749854973a5506c50e2322d2e71e3b37a541769912309632624, 0x24809a8325352314065f4358b2a5add05bac35bda0c97b076fadd3fe5bb970e4], [0x368bdbb340065e8c1c32ea178cccc07db257dbb9aba5db1f42a39deb990d838, 0x2937bd2682119fdc74b462c58f77b9c1c8f59fc9f39d953caacfa25b2640e289] - vk.IC.len() = 5 - vk.IC[0] = 0x2c6a375ea005c3b538be391c1cf3e247e92307d99946c270432cc70962537cd4, 0xe618adba9796b2d5620f344168500268f92707cd4695b1967571b7a74caf6f6 - vk.IC[1] = 0x296202906feb10bfa6c362faca9ec6cb093a56c3c9449facb5151be67e139277, 0x260e867ec4581cc8c709341b2919fe867c7740f1b624e9921120abafea857ac6 - vk.IC[2] = 0x13d7b366f4703d9b50c8f1acdd7e7956f04f129c3d620ec4d27f92c55dc7979c, 0xfac1a26e067d3e05e10d7ec7c236ab463100e822191a13bca37cc613e521746 - vk.IC[3] = 0x14ba5755c2cfa6a606bbe66611d2528ae7f20bac1a96712959d5099a02d11907, 0x13316e64b46d2f18a649803da0621a150af3076039d1597d505f1f073fe231a8 - vk.IC[4] = 0x1c459f97b080e17647b1937a9dfedb48caf92d6f08097d16bb82070bb832ea55, 0x2ff33110d33bb728b2dec637238b07a59747fe0928b87c7e590c2a1585fddd67 diff --git a/witness b/witness deleted file mode 100644 index 5bdbf191..00000000 --- a/witness +++ /dev/null @@ -1,5 +0,0 @@ -c 8 -b 4 -~one 1 -a 2 -~out 1 From 1371d8048b102b1f1ad32c6f8547a242194921c2 Mon Sep 17 00:00:00 2001 From: Thibaut Schaeffer Date: Sun, 26 Nov 2017 13:57:03 +0100 Subject: [PATCH 05/22] clean --- examples/private.code | 2 +- src/main.rs | 1 - src/r1cs.rs | 5 +---- 3 files changed, 2 insertions(+), 6 deletions(-) diff --git a/examples/private.code b/examples/private.code index 6c8a6af0..e0d267dc 100644 --- a/examples/private.code +++ b/examples/private.code @@ -1,5 +1,5 @@ // only using sub, no need to flatten -def main(x, private y): +def main(x): a = 5 b = 7 c = if a == b then 4 else 3 fi diff --git a/src/main.rs b/src/main.rs index 4a4ea805..e52d11ca 100644 --- a/src/main.rs +++ b/src/main.rs @@ -507,7 +507,6 @@ fn main() { } println!("Using Witness: {:?}", witness_map); - println!("{:?}", variables); let witness: Vec<_> = variables.iter().map(|x| witness_map[x].clone()).collect(); diff --git a/src/r1cs.rs b/src/r1cs.rs index 421c4613..40c7e6ee 100644 --- a/src/r1cs.rs +++ b/src/r1cs.rs @@ -299,9 +299,6 @@ pub fn r1cs_program( // position where private part of witness starts let private_inputs_offset = variables.len(); - //variables.extend(main.arguments.iter().filter(|x| x.private).map(|x| format!("{}", x.id.to_string()))); - - for def in &main.statements { let mut a_row: Vec<(usize, T)> = Vec::new(); let mut b_row: Vec<(usize, T)> = Vec::new(); @@ -315,7 +312,7 @@ pub fn r1cs_program( &mut b_row, &mut c_row, ), - Statement::Definition(ref id, ref expr) => continue, + Statement::Definition(_, _) => continue, Statement::Condition(ref expr1, ref expr2) => r1cs_expression( expr1.clone(), expr2.clone(), From 9e78b0a9ea9949cc1bb0601f1c560ca22339eabc Mon Sep 17 00:00:00 2001 From: Thibaut Schaeffer Date: Sun, 26 Nov 2017 14:00:32 +0100 Subject: [PATCH 06/22] remove example --- examples/private.code | 13 ------------- out | Bin 0 -> 130 bytes out.code | 3 +++ 3 files changed, 3 insertions(+), 13 deletions(-) delete mode 100644 examples/private.code create mode 100644 out create mode 100644 out.code diff --git a/examples/private.code b/examples/private.code deleted file mode 100644 index e0d267dc..00000000 --- a/examples/private.code +++ /dev/null @@ -1,13 +0,0 @@ -// only using sub, no need to flatten -def main(x): - a = 5 - b = 7 - c = if a == b then 4 else 3 fi - c == 3 - d = if a == 5 then 1 else 2 fi - d == 1 - e = if a < b then 5 else 6 fi - e == 5 - f = if b < a then 7 else 8 fi - f == 8 - return x diff --git a/out b/out new file mode 100644 index 0000000000000000000000000000000000000000..20f907dae363ad05c363c90e5b5b3b496d482b96 GIT binary patch literal 130 zcmZQ%fB+UKotv1M#|&jNLg_?C7%Q0p#!6yjg35wukSI(h8Dtc)Kq4|H391XOoDl#= CaRd(l literal 0 HcmV?d00001 diff --git a/out.code b/out.code new file mode 100644 index 00000000..2ddb8b1b --- /dev/null +++ b/out.code @@ -0,0 +1,3 @@ +def main(private a,c,private b): + c == (a * b) + return 1 From 4f78542592cbda6fd8a71667f19a42d7e003f4d8 Mon Sep 17 00:00:00 2001 From: Thibaut Schaeffer Date: Sun, 26 Nov 2017 14:00:50 +0100 Subject: [PATCH 07/22] remove artifacts --- out | Bin 130 -> 0 bytes out.code | 3 --- 2 files changed, 3 deletions(-) delete mode 100644 out delete mode 100644 out.code diff --git a/out b/out deleted file mode 100644 index 20f907dae363ad05c363c90e5b5b3b496d482b96..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 130 zcmZQ%fB+UKotv1M#|&jNLg_?C7%Q0p#!6yjg35wukSI(h8Dtc)Kq4|H391XOoDl#= CaRd(l diff --git a/out.code b/out.code deleted file mode 100644 index 2ddb8b1b..00000000 --- a/out.code +++ /dev/null @@ -1,3 +0,0 @@ -def main(private a,c,private b): - c == (a * b) - return 1 From 5b388b5980641a5d4c0d772831266b9a18519207 Mon Sep 17 00:00:00 2001 From: Thibaut Schaeffer Date: Sun, 26 Nov 2017 14:28:43 +0100 Subject: [PATCH 08/22] change message for undefined variable --- out | Bin 0 -> 120 bytes out.code | 3 +++ src/absy.rs | 13 ++----------- witness | 5 +++++ 4 files changed, 10 insertions(+), 11 deletions(-) create mode 100644 out create mode 100644 out.code create mode 100644 witness diff --git a/out b/out new file mode 100644 index 0000000000000000000000000000000000000000..da096ac07191ba1b920f2cfea2da13867d86a607 GIT binary patch literal 120 xcmZQ%fB+UKotv1M#{^|FLg{1%7%PzxCI_NHqA;0ckO9a7iO8HJs7Y|;i~tdq1F8T3 literal 0 HcmV?d00001 diff --git a/out.code b/out.code new file mode 100644 index 00000000..eb97b00d --- /dev/null +++ b/out.code @@ -0,0 +1,3 @@ +def main(c,private a): + c == (a * b) + return 1 diff --git a/src/absy.rs b/src/absy.rs index 122b54a2..34fa8334 100644 --- a/src/absy.rs +++ b/src/absy.rs @@ -7,7 +7,6 @@ use std::fmt; use std::collections::HashMap; -use std::io::{stdin, BufRead}; use field::Field; #[derive(Serialize, Deserialize)] @@ -290,19 +289,11 @@ impl Expression { } assert_eq!(num, T::zero()); } else { - println!( - "Could not calculate variable {:?}, inputs: {:?}", + panic!( + "Variable {:?} is undeclared in inputs: {:?}", var, inputs ); - println!("Please enter a value for {:?}:", var); - let mut input = String::new(); - let stdin = stdin(); - stdin - .lock() - .read_line(&mut input) - .expect("Did not enter a correct String"); - inputs.insert(var.to_string(), T::from(input.trim())); } } inputs[var].clone() diff --git a/witness b/witness new file mode 100644 index 00000000..238a5085 --- /dev/null +++ b/witness @@ -0,0 +1,5 @@ +a 2 +~one 1 +b 4 +~out 1 +c 8 From f8a706bff0e1ebadad7b4c529e54b92857d78be3 Mon Sep 17 00:00:00 2001 From: Thibaut Schaeffer Date: Sun, 26 Nov 2017 14:28:43 +0100 Subject: [PATCH 09/22] change message for undefined variable --- src/absy.rs | 13 ++----------- 1 file changed, 2 insertions(+), 11 deletions(-) diff --git a/src/absy.rs b/src/absy.rs index 122b54a2..34fa8334 100644 --- a/src/absy.rs +++ b/src/absy.rs @@ -7,7 +7,6 @@ use std::fmt; use std::collections::HashMap; -use std::io::{stdin, BufRead}; use field::Field; #[derive(Serialize, Deserialize)] @@ -290,19 +289,11 @@ impl Expression { } assert_eq!(num, T::zero()); } else { - println!( - "Could not calculate variable {:?}, inputs: {:?}", + panic!( + "Variable {:?} is undeclared in inputs: {:?}", var, inputs ); - println!("Please enter a value for {:?}:", var); - let mut input = String::new(); - let stdin = stdin(); - stdin - .lock() - .read_line(&mut input) - .expect("Did not enter a correct String"); - inputs.insert(var.to_string(), T::from(input.trim())); } } inputs[var].clone() From 76fb3a1eff8a9f1bcb5b8a6f74db819ca696ae3c Mon Sep 17 00:00:00 2001 From: Thibaut Schaeffer Date: Sun, 26 Nov 2017 14:31:46 +0100 Subject: [PATCH 10/22] remove artifacts. really need to ignore them --- out | Bin 120 -> 0 bytes out.code | 3 --- witness | 5 ----- 3 files changed, 8 deletions(-) delete mode 100644 out delete mode 100644 out.code delete mode 100644 witness diff --git a/out b/out deleted file mode 100644 index da096ac07191ba1b920f2cfea2da13867d86a607..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 120 xcmZQ%fB+UKotv1M#{^|FLg{1%7%PzxCI_NHqA;0ckO9a7iO8HJs7Y|;i~tdq1F8T3 diff --git a/out.code b/out.code deleted file mode 100644 index eb97b00d..00000000 --- a/out.code +++ /dev/null @@ -1,3 +0,0 @@ -def main(c,private a): - c == (a * b) - return 1 diff --git a/witness b/witness deleted file mode 100644 index 238a5085..00000000 --- a/witness +++ /dev/null @@ -1,5 +0,0 @@ -a 2 -~one 1 -b 4 -~out 1 -c 8 From e27fdd1190cd83fa2b14bb76ad4779e8cd2e1a57 Mon Sep 17 00:00:00 2001 From: schaeff Date: Sun, 10 Dec 2017 00:03:39 +0100 Subject: [PATCH 11/22] add semantic analysis --- src/absy.rs | 4 +- src/main.rs | 6 ++ src/semantics.rs | 151 +++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 159 insertions(+), 2 deletions(-) create mode 100644 src/semantics.rs diff --git a/src/absy.rs b/src/absy.rs index 34fa8334..f4a50253 100644 --- a/src/absy.rs +++ b/src/absy.rs @@ -9,7 +9,7 @@ use std::fmt; use std::collections::HashMap; use field::Field; -#[derive(Serialize, Deserialize)] +#[derive(Serialize, Deserialize, Clone)] pub struct Prog { /// Functions of the program pub functions: Vec>, @@ -55,7 +55,7 @@ impl fmt::Debug for Prog { } } -#[derive(Serialize, Deserialize)] +#[derive(Serialize, Deserialize, Clone)] pub struct Function { /// Name of the program pub id: String, diff --git a/src/main.rs b/src/main.rs index e52d11ca..b8169a57 100644 --- a/src/main.rs +++ b/src/main.rs @@ -18,6 +18,7 @@ extern crate regex; mod absy; mod parser; +mod semantics; mod flatten; mod r1cs; mod field; @@ -33,6 +34,7 @@ use std::io::prelude::*; use field::{Field, FieldPrime}; use absy::Prog; use parser::parse_program; +use semantics::Checker; use flatten::Flattener; use r1cs::r1cs_program; use clap::{App, AppSettings, Arg, SubCommand}; @@ -209,6 +211,10 @@ fn main() { } }; + // check semantics + let semantics_ok = Checker::new().check_program(program_ast.clone()); + println!("Semantics ok? {:?}", semantics_ok); + // flatten input program let program_flattened = Flattener::new(FieldPrime::get_required_bits()).flatten_program(program_ast); diff --git a/src/semantics.rs b/src/semantics.rs new file mode 100644 index 00000000..41aad115 --- /dev/null +++ b/src/semantics.rs @@ -0,0 +1,151 @@ +//! Module containing semantic analysis tools to run at compile time +//! +//! @file flatten.rs +//! @author Dennis Kuhnert +//! @author Jacob Eberhardt +//! @date 2017 + +use std::collections::{HashMap, HashSet}; +use absy::*; +use field::Field; + +#[derive(Clone, PartialEq, Eq, Hash)] +pub struct Symbol { + id: String, + level: usize +} + +// Checker, checks the semantics of a program. +pub struct Checker { + scope: HashSet, + level: usize +} + +impl Checker { + pub fn new() -> Checker { + Checker { + scope: HashSet::new(), + level: 0 + } + } + + pub fn new_with_args(scope: HashSet, level: usize) -> Checker { + Checker { + scope: scope, + level: level + } + } + + pub fn check_program(&mut self, prog: Prog) -> bool { + let mut res = true; + for func in prog.functions { + let function_checked = self.check_function(func); + res = res && function_checked; + } + res + } + + fn check_function(&mut self, funct: Function) -> bool { + self.level += 1; + for arg in funct.arguments { + self.scope.insert(Symbol { + id: arg.id.to_string(), + level: 0 + }); + } + let mut res = true; + for stat in funct.statements { + let statement_checked = self.check_statement( + stat + ); + res = res && statement_checked; + } + self.level -= 1; + // TODO: cleanup scope of all symbols of level i + res + } + + fn check_statement(&mut self, stat: Statement) -> bool { + match stat { + Statement::Return(expr) => { + self.check_expression(expr) + } + Statement::Definition(id, expr) => { + let expr_checked = self.check_expression(expr); + self.scope.insert(Symbol { + id: id.to_string(), + level: 0 + }); + expr_checked + + } + Statement::Condition(lhs, rhs) => { + self.check_expression(lhs) && self.check_expression(rhs) + } + _ => true, + } + } + + fn check_expression(&mut self, expr: Expression) -> bool { + match expr { + Expression::Identifier(id) => { + self.scope.contains(&Symbol {id: id.to_string(), level: 0}) + } + Expression::Add(box e1, box e2) | Expression::Sub(box e1, box e2) | Expression::Mult(box e1, box e2) | + Expression::Div(box e1, box e2) | Expression::Pow(box e1, box e2) => { + self.check_expression(e1) && self.check_expression(e2) + } + Expression::IfElse(box condition, box consequent, box alternative) => { + self.check_condition(condition) && self.check_expression(consequent) && self.check_expression(alternative) + } + _ => true, + } + } + + fn check_condition(&mut self, cond: Condition) -> bool { + match cond { + Condition::Lt(e1, e2) | + Condition::Le(e1, e2) | + Condition::Eq(e1, e2) | + Condition::Ge(e1, e2) | + Condition::Gt(e1, e2) => { + self.check_expression(e1) && self.check_expression(e2) + } + } + } +} + +#[cfg(test)] +mod tests { + use super::*; + use field::FieldPrime; + + #[test] + fn undefined_variable_in_statement() { + // a = b + // b undefined + let statement: Statement = Statement::Definition( + String::from("a"), + Expression::Identifier(String::from("b")) + ); + let mut checker = Checker::new(); + assert_eq!(checker.check_statement(statement), false); + } + + #[test] + fn defined_variable_in_statement() { + // a = b + // b undefined + let statement: Statement = Statement::Definition( + String::from("a"), + Expression::Identifier(String::from("b")) + ); + let mut scope = HashSet::new(); + scope.insert(Symbol { + id: String::from("b"), + level: 0 + }); + let mut checker = Checker::new_with_args(scope, 1); + assert_eq!(checker.check_statement(statement), true); + } +} \ No newline at end of file From 9f6ceb499de70c6cbfadac6413e448d09f33a1ad Mon Sep 17 00:00:00 2001 From: schaeff Date: Sun, 10 Dec 2017 15:15:37 +0100 Subject: [PATCH 12/22] refactor to use Result rather than bool --- src/main.rs | 6 +++-- src/semantics.rs | 61 +++++++++++++++++++++++++++--------------------- 2 files changed, 38 insertions(+), 29 deletions(-) diff --git a/src/main.rs b/src/main.rs index b8169a57..4ac86ba8 100644 --- a/src/main.rs +++ b/src/main.rs @@ -212,8 +212,10 @@ fn main() { }; // check semantics - let semantics_ok = Checker::new().check_program(program_ast.clone()); - println!("Semantics ok? {:?}", semantics_ok); + match Checker::new().check_program(program_ast.clone()) { + Ok(_) => println!("Semantics ok"), + Err(why) => panic!("Semantic analysis failed with: {}", why) + }; // flatten input program let program_flattened = diff --git a/src/semantics.rs b/src/semantics.rs index 41aad115..ebc7f80b 100644 --- a/src/semantics.rs +++ b/src/semantics.rs @@ -36,16 +36,14 @@ impl Checker { } } - pub fn check_program(&mut self, prog: Prog) -> bool { - let mut res = true; + pub fn check_program(&mut self, prog: Prog) -> Result { for func in prog.functions { - let function_checked = self.check_function(func); - res = res && function_checked; + self.check_function(func)?; } - res + Ok(true) } - fn check_function(&mut self, funct: Function) -> bool { + fn check_function(&mut self, funct: Function) -> Result { self.level += 1; for arg in funct.arguments { self.scope.insert(Symbol { @@ -53,63 +51,72 @@ impl Checker { level: 0 }); } - let mut res = true; for stat in funct.statements { - let statement_checked = self.check_statement( - stat - ); - res = res && statement_checked; + self.check_statement(stat)?; } self.level -= 1; // TODO: cleanup scope of all symbols of level i - res + Ok(true) } - fn check_statement(&mut self, stat: Statement) -> bool { + fn check_statement(&mut self, stat: Statement) -> Result { match stat { Statement::Return(expr) => { - self.check_expression(expr) + self.check_expression(expr)?; + Ok(true) } Statement::Definition(id, expr) => { - let expr_checked = self.check_expression(expr); + self.check_expression(expr)?; self.scope.insert(Symbol { id: id.to_string(), level: 0 }); - expr_checked + Ok(true) } Statement::Condition(lhs, rhs) => { - self.check_expression(lhs) && self.check_expression(rhs) + self.check_expression(lhs)?; + self.check_expression(rhs)?; + Ok(true) } - _ => true, + _ => Ok(true), } } - fn check_expression(&mut self, expr: Expression) -> bool { + fn check_expression(&mut self, expr: Expression) -> Result { match expr { Expression::Identifier(id) => { - self.scope.contains(&Symbol {id: id.to_string(), level: 0}) + match self.scope.contains(&Symbol {id: id.to_string(), level: 0}) { + true => Ok(true), + false => Err(format!("{:?} is undefined", id.to_string())), + } } Expression::Add(box e1, box e2) | Expression::Sub(box e1, box e2) | Expression::Mult(box e1, box e2) | Expression::Div(box e1, box e2) | Expression::Pow(box e1, box e2) => { - self.check_expression(e1) && self.check_expression(e2) + self.check_expression(e1)?; + self.check_expression(e2)?; + Ok(true) } Expression::IfElse(box condition, box consequent, box alternative) => { - self.check_condition(condition) && self.check_expression(consequent) && self.check_expression(alternative) + self.check_condition(condition)?; + self.check_expression(consequent)?; + self.check_expression(alternative)?; + Ok(true) } - _ => true, + _ => Ok(true), } } - fn check_condition(&mut self, cond: Condition) -> bool { + fn check_condition(&mut self, cond: Condition) -> Result { match cond { Condition::Lt(e1, e2) | Condition::Le(e1, e2) | Condition::Eq(e1, e2) | Condition::Ge(e1, e2) | Condition::Gt(e1, e2) => { - self.check_expression(e1) && self.check_expression(e2) + self.check_expression(e1)?; + self.check_expression(e2)?; + Ok(true) } } } @@ -129,7 +136,7 @@ mod tests { Expression::Identifier(String::from("b")) ); let mut checker = Checker::new(); - assert_eq!(checker.check_statement(statement), false); + assert_eq!(checker.check_statement(statement), Err("\"b\" is undefined".to_string())); } #[test] @@ -146,6 +153,6 @@ mod tests { level: 0 }); let mut checker = Checker::new_with_args(scope, 1); - assert_eq!(checker.check_statement(statement), true); + assert_eq!(checker.check_statement(statement), Ok(true)); } } \ No newline at end of file From 2b0ac4ab12a947d43619991c41347a62776daa29 Mon Sep 17 00:00:00 2001 From: schaeff Date: Sun, 10 Dec 2017 16:46:12 +0100 Subject: [PATCH 13/22] make scope function specific --- src/semantics.rs | 107 +++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 100 insertions(+), 7 deletions(-) diff --git a/src/semantics.rs b/src/semantics.rs index ebc7f80b..fa4bf4c8 100644 --- a/src/semantics.rs +++ b/src/semantics.rs @@ -9,7 +9,7 @@ use std::collections::{HashMap, HashSet}; use absy::*; use field::Field; -#[derive(Clone, PartialEq, Eq, Hash)] +#[derive(Clone, PartialEq, Eq, Hash, Debug)] pub struct Symbol { id: String, level: usize @@ -48,14 +48,19 @@ impl Checker { for arg in funct.arguments { self.scope.insert(Symbol { id: arg.id.to_string(), - level: 0 + level: self.level }); } for stat in funct.statements { self.check_statement(stat)?; } + let current_level = self.level.clone(); + let current_scope = self.scope.clone(); + let to_remove = current_scope.iter().filter(|symbol| symbol.level == current_level); + for symbol in to_remove { + self.scope.remove(symbol); + } self.level -= 1; - // TODO: cleanup scope of all symbols of level i Ok(true) } @@ -69,7 +74,7 @@ impl Checker { self.check_expression(expr)?; self.scope.insert(Symbol { id: id.to_string(), - level: 0 + level: self.level }); Ok(true) @@ -86,9 +91,10 @@ impl Checker { fn check_expression(&mut self, expr: Expression) -> Result { match expr { Expression::Identifier(id) => { - match self.scope.contains(&Symbol {id: id.to_string(), level: 0}) { - true => Ok(true), - false => Err(format!("{:?} is undefined", id.to_string())), + // check that `id` is defined in the scope + match self.scope.iter().filter(|symbol| symbol.id == id.to_string()).count() { + 0 => Err(format!("{:?} is undefined", id.to_string())), + _ => Ok(true), } } Expression::Add(box e1, box e2) | Expression::Sub(box e1, box e2) | Expression::Mult(box e1, box e2) | @@ -155,4 +161,91 @@ mod tests { let mut checker = Checker::new_with_args(scope, 1); assert_eq!(checker.check_statement(statement), Ok(true)); } + + #[test] + fn declared_in_other_function() { + // def foo(): + // a = 1 + // def bar(): + // return a + // should fail + let foo_args = Vec::::new(); + let mut foo_statements = Vec::>::new(); + foo_statements.push(Statement::Definition( + String::from("a"), + Expression::Number(FieldPrime::from(1))) + ); + let foo = Function { + id: "foo".to_string(), + arguments: foo_args, + statements: foo_statements, + }; + + let bar_args = Vec::::new(); + let mut bar_statements = Vec::>::new(); + bar_statements.push(Statement::Return( + Expression::Identifier(String::from("a")) + )); + let bar = Function { + id: "bar".to_string(), + arguments: bar_args, + statements: bar_statements, + }; + + let mut funcs = Vec::>::new(); + funcs.push(foo); + funcs.push(bar); + let prog = Prog { + functions: funcs + }; + + let mut checker = Checker::new(); + assert_eq!(checker.check_program(prog), Err("\"a\" is undefined".to_string())); + } + + #[test] + fn declared_in_two_scopes() { + // def foo(): + // a = 1 + // def bar(): + // a = 2 + // return a + // should pass + let foo_args = Vec::::new(); + let mut foo_statements = Vec::>::new(); + foo_statements.push(Statement::Definition( + String::from("a"), + Expression::Number(FieldPrime::from(1))) + ); + let foo = Function { + id: "foo".to_string(), + arguments: foo_args, + statements: foo_statements, + }; + + let bar_args = Vec::::new(); + let mut bar_statements = Vec::>::new(); + bar_statements.push(Statement::Definition( + String::from("a"), + Expression::Number(FieldPrime::from(2)) + )); + bar_statements.push(Statement::Return( + Expression::Identifier(String::from("a")) + )); + let bar = Function { + id: "bar".to_string(), + arguments: bar_args, + statements: bar_statements, + }; + + let mut funcs = Vec::>::new(); + funcs.push(foo); + funcs.push(bar); + let prog = Prog { + functions: funcs + }; + + let mut checker = Checker::new(); + assert_eq!(checker.check_program(prog), Ok(true)); + } } \ No newline at end of file From 7032e95c8e4fd0be356b95e66e21a8f764cb2753 Mon Sep 17 00:00:00 2001 From: schaeff Date: Mon, 11 Dec 2017 01:01:16 +0100 Subject: [PATCH 14/22] support function calls --- src/semantics.rs | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/semantics.rs b/src/semantics.rs index fa4bf4c8..3a7b91d2 100644 --- a/src/semantics.rs +++ b/src/semantics.rs @@ -5,7 +5,7 @@ //! @author Jacob Eberhardt //! @date 2017 -use std::collections::{HashMap, HashSet}; +use std::collections::HashSet; use absy::*; use field::Field; @@ -109,7 +109,13 @@ impl Checker { self.check_expression(alternative)?; Ok(true) } - _ => Ok(true), + Expression::FunctionCall(_, param_expressions) => { + for expr in param_expressions { + self.check_expression(expr)?; + } + Ok(true) + } + Expression::Number(_) => Ok(true) } } @@ -148,7 +154,7 @@ mod tests { #[test] fn defined_variable_in_statement() { // a = b - // b undefined + // b defined let statement: Statement = Statement::Definition( String::from("a"), Expression::Identifier(String::from("b")) From 1ef90d6fcffed67d7c8478b29915787958a890d4 Mon Sep 17 00:00:00 2001 From: schaeff Date: Fri, 15 Dec 2017 23:43:29 +0100 Subject: [PATCH 15/22] update examples --- examples/sudokuchecker.code | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/sudokuchecker.code b/examples/sudokuchecker.code index 1428cbdc..9078fed7 100644 --- a/examples/sudokuchecker.code +++ b/examples/sudokuchecker.code @@ -22,7 +22,7 @@ def validateInput(x): return (x-1)*(x-2)*(x-3)*(x-4) // variables naming: box'row''column' -def main(a21,b11,b22,c11,c22,d21): +def main(private a21, private b11, private b22, private c11, private c22, private d21): // validate inputs 0 == validateInput(a11) From ac458170ebd937253d0cf906ca9ff344a91b805e Mon Sep 17 00:00:00 2001 From: schaeff Date: Fri, 15 Dec 2017 23:54:48 +0100 Subject: [PATCH 16/22] change result type to () --- src/main.rs | 2 +- src/semantics.rs | 38 +++++++++++++++++++------------------- 2 files changed, 20 insertions(+), 20 deletions(-) diff --git a/src/main.rs b/src/main.rs index 4ac86ba8..faf23113 100644 --- a/src/main.rs +++ b/src/main.rs @@ -213,7 +213,7 @@ fn main() { // check semantics match Checker::new().check_program(program_ast.clone()) { - Ok(_) => println!("Semantics ok"), + Ok(()) => (), Err(why) => panic!("Semantic analysis failed with: {}", why) }; diff --git a/src/semantics.rs b/src/semantics.rs index 3a7b91d2..f4c5f307 100644 --- a/src/semantics.rs +++ b/src/semantics.rs @@ -36,14 +36,14 @@ impl Checker { } } - pub fn check_program(&mut self, prog: Prog) -> Result { + pub fn check_program(&mut self, prog: Prog) -> Result<(), String> { for func in prog.functions { self.check_function(func)?; } - Ok(true) + Ok(()) } - fn check_function(&mut self, funct: Function) -> Result { + fn check_function(&mut self, funct: Function) -> Result<(), String> { self.level += 1; for arg in funct.arguments { self.scope.insert(Symbol { @@ -61,14 +61,14 @@ impl Checker { self.scope.remove(symbol); } self.level -= 1; - Ok(true) + Ok(()) } - fn check_statement(&mut self, stat: Statement) -> Result { + fn check_statement(&mut self, stat: Statement) -> Result<(), String> { match stat { Statement::Return(expr) => { self.check_expression(expr)?; - Ok(true) + Ok(()) } Statement::Definition(id, expr) => { self.check_expression(expr)?; @@ -76,50 +76,50 @@ impl Checker { id: id.to_string(), level: self.level }); - Ok(true) + Ok(()) } Statement::Condition(lhs, rhs) => { self.check_expression(lhs)?; self.check_expression(rhs)?; - Ok(true) + Ok(()) } - _ => Ok(true), + _ => Ok(()), } } - fn check_expression(&mut self, expr: Expression) -> Result { + fn check_expression(&mut self, expr: Expression) -> Result<(), String> { match expr { Expression::Identifier(id) => { // check that `id` is defined in the scope match self.scope.iter().filter(|symbol| symbol.id == id.to_string()).count() { 0 => Err(format!("{:?} is undefined", id.to_string())), - _ => Ok(true), + _ => Ok(()), } } Expression::Add(box e1, box e2) | Expression::Sub(box e1, box e2) | Expression::Mult(box e1, box e2) | Expression::Div(box e1, box e2) | Expression::Pow(box e1, box e2) => { self.check_expression(e1)?; self.check_expression(e2)?; - Ok(true) + Ok(()) } Expression::IfElse(box condition, box consequent, box alternative) => { self.check_condition(condition)?; self.check_expression(consequent)?; self.check_expression(alternative)?; - Ok(true) + Ok(()) } Expression::FunctionCall(_, param_expressions) => { for expr in param_expressions { self.check_expression(expr)?; } - Ok(true) + Ok(()) } - Expression::Number(_) => Ok(true) + Expression::Number(_) => Ok(()) } } - fn check_condition(&mut self, cond: Condition) -> Result { + fn check_condition(&mut self, cond: Condition) -> Result<(), String> { match cond { Condition::Lt(e1, e2) | Condition::Le(e1, e2) | @@ -128,7 +128,7 @@ impl Checker { Condition::Gt(e1, e2) => { self.check_expression(e1)?; self.check_expression(e2)?; - Ok(true) + Ok(()) } } } @@ -165,7 +165,7 @@ mod tests { level: 0 }); let mut checker = Checker::new_with_args(scope, 1); - assert_eq!(checker.check_statement(statement), Ok(true)); + assert_eq!(checker.check_statement(statement), Ok(())); } #[test] @@ -252,6 +252,6 @@ mod tests { }; let mut checker = Checker::new(); - assert_eq!(checker.check_program(prog), Ok(true)); + assert_eq!(checker.check_program(prog), Ok(())); } } \ No newline at end of file From 3b8effcf8ecafff421d51f393da904ee7abf56d4 Mon Sep 17 00:00:00 2001 From: schaeff Date: Sat, 16 Dec 2017 00:55:08 +0100 Subject: [PATCH 17/22] add for statement --- src/semantics.rs | 75 ++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 72 insertions(+), 3 deletions(-) diff --git a/src/semantics.rs b/src/semantics.rs index f4c5f307..e1c6eee9 100644 --- a/src/semantics.rs +++ b/src/semantics.rs @@ -1,8 +1,7 @@ //! Module containing semantic analysis tools to run at compile time //! -//! @file flatten.rs -//! @author Dennis Kuhnert -//! @author Jacob Eberhardt +//! @file semantics.rs +//! @author Thibaut Schaeffer //! @date 2017 use std::collections::HashSet; @@ -84,6 +83,20 @@ impl Checker { self.check_expression(rhs)?; Ok(()) } + Statement::For(id, _, _, statements) => { + self.level += 1; + let index = Symbol { + id: id.to_string(), + level: self.level + }; + self.scope.insert(index.clone()); + for stat in statements { + self.check_statement(stat)?; + } + self.scope.remove(&index); + self.level -= 1; + Ok(()) + } _ => Ok(()), } } @@ -254,4 +267,60 @@ mod tests { let mut checker = Checker::new(); assert_eq!(checker.check_program(prog), Ok(())); } + + #[test] + fn for_index_after_end() { + // def foo(): + // for i in 0..10 do + // endfor + // return i + // should fail + let mut foo_statements = Vec::>::new(); + foo_statements.push(Statement::For( + String::from("i"), + FieldPrime::from(0), + FieldPrime::from(10), + Vec::>::new()) + ); + foo_statements.push(Statement::Return( + Expression::Identifier(String::from("i")) + )); + let foo = Function { + id: "foo".to_string(), + arguments: Vec::::new(), + statements: foo_statements + }; + + let mut checker = Checker::new(); + assert_eq!(checker.check_function(foo), Err("\"i\" is undefined".to_string())); + } + + #[test] + fn for_index_in_for() { + // def foo(): + // for i in 0..10 do + // a = i + // endfor + // should pass + let mut foo_statements = Vec::>::new(); + let mut for_statements = Vec::>::new(); + for_statements.push(Statement::Definition( + String::from("a"),q + Expression::Identifier(String::from("i")) + )); + foo_statements.push(Statement::For( + String::from("i"), + FieldPrime::from(0), + FieldPrime::from(10), + for_statements + )); + let foo = Function { + id: "foo".to_string(), + arguments: Vec::::new(), + statements: foo_statements + }; + + let mut checker = Checker::new(); + assert_eq!(checker.check_function(foo), Ok(())); + } } \ No newline at end of file From 80745b47debe0ee961d6149a31eb2779629cb06c Mon Sep 17 00:00:00 2001 From: schaeff Date: Sat, 16 Dec 2017 01:11:56 +0100 Subject: [PATCH 18/22] add compiler statements --- src/semantics.rs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/semantics.rs b/src/semantics.rs index e1c6eee9..d29afd3c 100644 --- a/src/semantics.rs +++ b/src/semantics.rs @@ -69,7 +69,7 @@ impl Checker { self.check_expression(expr)?; Ok(()) } - Statement::Definition(id, expr) => { + Statement::Definition(id, expr) | Statement::Compiler(id, expr) => { self.check_expression(expr)?; self.scope.insert(Symbol { id: id.to_string(), @@ -97,7 +97,6 @@ impl Checker { self.level -= 1; Ok(()) } - _ => Ok(()), } } @@ -305,7 +304,7 @@ mod tests { let mut foo_statements = Vec::>::new(); let mut for_statements = Vec::>::new(); for_statements.push(Statement::Definition( - String::from("a"),q + String::from("a"), Expression::Identifier(String::from("i")) )); foo_statements.push(Statement::For( From ecf7c69abd2a33c86c2348832b3521d46e88d359 Mon Sep 17 00:00:00 2001 From: schaeff Date: Sat, 16 Dec 2017 01:18:07 +0100 Subject: [PATCH 19/22] add test flag to constructor --- src/semantics.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/semantics.rs b/src/semantics.rs index d29afd3c..4e64ccf4 100644 --- a/src/semantics.rs +++ b/src/semantics.rs @@ -28,6 +28,7 @@ impl Checker { } } + #[test] pub fn new_with_args(scope: HashSet, level: usize) -> Checker { Checker { scope: scope, From 173fc90f9b64dedc3e99a55e353a4fcfa55b51df Mon Sep 17 00:00:00 2001 From: schaeff Date: Mon, 18 Dec 2017 23:27:39 +0100 Subject: [PATCH 20/22] add interactive flag --- src/main.rs | 50 +++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 43 insertions(+), 7 deletions(-) diff --git a/src/main.rs b/src/main.rs index faf23113..18afa07a 100644 --- a/src/main.rs +++ b/src/main.rs @@ -27,7 +27,7 @@ mod libsnark; use std::fs::File; use std::path::Path; -use std::io::{BufWriter, Write, BufReader, BufRead}; +use std::io::{BufWriter, Write, BufReader, BufRead, stdin}; use std::collections::HashMap; use std::string::String; use std::io::prelude::*; @@ -141,7 +141,7 @@ fn main() { .arg(Arg::with_name("input") .short("i") .long("input") - .help("path of comiled code.") + .help("path of compiled code.") .value_name("FILE") .takes_value(true) .required(false) @@ -161,6 +161,10 @@ fn main() { .takes_value(true) .multiple(true) // allows multiple values .required(false) + ).arg(Arg::with_name("interactive") + .long("interactive") + .help("enter private inputs interactively.") + .required(false) ) ) .subcommand(SubCommand::with_name("generate-proof") @@ -294,22 +298,54 @@ fn main() { println!("{}", main_flattened); // validate #arguments - let mut args: Vec = Vec::new(); + let mut cli_arguments: Vec = Vec::new(); match sub_matches.values_of("arguments"){ Some(p) => { let arg_strings: Vec<&str> = p.collect(); - args = arg_strings.into_iter().map(|x| FieldPrime::from(x)).collect(); + cli_arguments = arg_strings.into_iter().map(|x| FieldPrime::from(x)).collect(); }, None => { } } - if main_flattened.arguments.len() != args.len() { - println!("Wrong number of arguments. Given: {}, Required: {}.", args.len(), main_flattened.arguments.len()); + // handle interactive and non-interactive modes + let is_interactive = sub_matches.occurrences_of("interactive") > 0; + + // in interactive mode, only public inputs are expected + let expected_cli_args_count = main_flattened.arguments.iter().filter(|x| !(x.private && is_interactive)).count(); + + if cli_arguments.len() != expected_cli_args_count { + println!("Wrong number of arguments. Given: {}, Required: {}.", cli_arguments.len(), expected_cli_args_count); std::process::exit(1); } - let witness_map = main_flattened.get_witness(args); + let mut cli_arguments_iter = cli_arguments.into_iter(); + let arguments = main_flattened.arguments.clone().into_iter().map(|x| { + match x.private && is_interactive { + // private inputs are passed interactively when the flag is present + true => { + println!("Please enter a value for {:?}:", x.id); + let mut input = String::new(); + let stdin = stdin(); + stdin + .lock() + .read_line(&mut input) + .expect("Did not enter a correct String"); + FieldPrime::from(input.trim()) + } + // otherwise, they are taken from the CLI arguments + false => { + match cli_arguments_iter.next() { + Some(x) => x, + None => { + std::process::exit(1); + } + } + } + } + }).collect(); + + let witness_map = main_flattened.get_witness(arguments); // let witness_map: HashMap = main_flattened.get_witness(args); println!("Witness: {:?}", witness_map); match witness_map.get("~out") { From 38bdb941a197fd78e122d4ca6887ef18b1c925a8 Mon Sep 17 00:00:00 2001 From: schaeff Date: Mon, 18 Dec 2017 23:42:05 +0100 Subject: [PATCH 21/22] fix sudoku --- examples/sudokuchecker.code | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/sudokuchecker.code b/examples/sudokuchecker.code index 9078fed7..2fb3c3f5 100644 --- a/examples/sudokuchecker.code +++ b/examples/sudokuchecker.code @@ -22,7 +22,7 @@ def validateInput(x): return (x-1)*(x-2)*(x-3)*(x-4) // variables naming: box'row''column' -def main(private a21, private b11, private b22, private c11, private c22, private d21): +def main(a21, b11, b22, c11, c22, d21, private a11, private a12, private a22, private b12, private b21, private c12, private c21, private d11, private d12, private d22): // validate inputs 0 == validateInput(a11) From 4f1404e682b9b345d979a2005f4b4ea02f9f0d30 Mon Sep 17 00:00:00 2001 From: schaeff Date: Tue, 19 Dec 2017 00:01:59 +0100 Subject: [PATCH 22/22] teaks following review --- src/flatten.rs | 4 ++-- src/semantics.rs | 6 ++++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/flatten.rs b/src/flatten.rs index 5b74813d..4a59ef4f 100644 --- a/src/flatten.rs +++ b/src/flatten.rs @@ -424,7 +424,7 @@ impl Flattener { match param_expr.apply_substitution(&self.substitution) { Expression::Identifier(ref x) => params_flattened.push(Parameter { id: x.clone().to_string(), - private: false + private: true }), _ => { let expr_subbed = param_expr.apply_substitution(&self.substitution); @@ -440,7 +440,7 @@ impl Flattener { .push(Statement::Definition(intermediate_var.clone(), rhs)); params_flattened.push(Parameter { id: intermediate_var.clone().to_string(), - private: false + private: true }); } } diff --git a/src/semantics.rs b/src/semantics.rs index 4e64ccf4..7045de48 100644 --- a/src/semantics.rs +++ b/src/semantics.rs @@ -1,4 +1,6 @@ //! Module containing semantic analysis tools to run at compile time +//! The goal is to detect semantic errors such as undefined variables +//! A variable is undefined if it isn't present in the static scope //! //! @file semantics.rs //! @author Thibaut Schaeffer @@ -116,9 +118,9 @@ impl Checker { self.check_expression(e2)?; Ok(()) } - Expression::IfElse(box condition, box consequent, box alternative) => { + Expression::IfElse(box condition, box consequence, box alternative) => { self.check_condition(condition)?; - self.check_expression(consequent)?; + self.check_expression(consequence)?; self.check_expression(alternative)?; Ok(()) }