{"id":"W4415006871","doi":"10.1145/3763110","title":"Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits","year":2025,"lang":"en","type":"article","venue":"Proceedings of the ACM on Programming Languages","topic":"Cryptography and Data Security","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"Defense Advanced Research Projects Agency; Ethereum Foundation; Google; National Science Foundation","keywords":"Correctness; Compiler; Formal equivalence checking; Construct (python library); Equivalence (formal languages); Implementation; Proof assistant; Process (computing); High-level synthesis; Compiler construction","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.001126522,0.0008656827,0.0005429757,0.0007754501,0.0004340728,0.001495489,0.00139133,0.0007742735,0.01014935],"category_scores_gemma":[0.005128262,0.0007433447,0.000825477,0.0005889744,0.0007600873,0.00189225,0.001443717,0.001308988,0.003137885],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0007113327,"about_ca_system_score_gemma":0.002485754,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0009866247,"about_ca_topic_score_gemma":0.00168385,"domain_scores_codex":[0.999146,0.0002039006,0.00007901723,0.0001078481,0.0003476453,0.0001156038],"domain_scores_gemma":[0.9977748,0.001260655,0.0001366332,0.0003970181,0.0003825023,0.00004835365],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"not_applicable","study_design_scores_codex":[0.001023045,0.0002530544,0.002272496,0.00169302,0.0001460636,0.0006898132,0.000575214,0.1985585,0.09030319,0.1829525,0.07070917,0.450824],"study_design_scores_gemma":[0.0003929253,0.0002726902,0.0004326776,0.000218064,0.00008285935,0.0004561465,0.0001247484,0.730634,0.1109247,0.07828672,0.07809532,0.00007909821],"study_design_candidate":"not_applicable","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"software","genre_scores_codex":[0.01041142,0.0002528369,0.9512922,0.0002065193,0.00009832281,0.0001403199,0.0007428855,0.03183275,0.005022673],"genre_scores_gemma":[0.1616576,0.0003819098,0.8234692,0.000295267,0.00004489052,0.0004059868,0.002138001,0.0068833,0.00472375],"genre_candidate":"software","genre_consensus":null,"teacher_disagreement_score":0.01014935,"threshold_uncertainty_score":0.03395301,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01584355999408433,"score_gpt":0.2696909591242602,"score_spread":0.2538473991301759,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}