@@ -916,278 +916,13 @@ end
916916
917917M .logic = M .create_logic
918918
919- function M .bip340_circuit ()
920- local artifact = native .bip340_circuit_native ()
921- return wrap_artifact (artifact , make_bip340_schema (artifact ))
922- end
923-
924- if M .load_circuit_artifact_bip340 then
925- local native_load_bip340 = M .load_circuit_artifact_bip340
926- M .load_circuit_artifact_bip340 = function (octet )
927- local artifact = native_load_bip340 (octet )
928- return wrap_artifact (artifact , make_bip340_schema (artifact ))
929- end
930- end
931-
932- if M .witness and native .bip340_compute_inputs_native then
933- M .witness .bip340_compute_inputs = function (circuit , sig , pk , msg )
934- local raw_circuit = is_named_artifact (circuit ) and circuit :raw () or circuit
935- local inputs , public_inputs =
936- native .bip340_compute_inputs_native (raw_circuit , sig , pk , msg )
937- return {
938- inputs = inputs ,
939- public_inputs = public_inputs ,
940- }
941- end
942- end
943-
944- -- ===========================================================================
945- -- BIP340 Lua-Authored Circuit Helpers
946- -- ===========================================================================
947- -- These helpers allow Lua to author the BIP340 verification sequence using
948- -- granular gadget primitives while C++ emits the production-tested
949- -- constraint formulas.
950-
951- --- Convert multi-return (x, y, z) from gadget calls into a point table.
952- -- Usage: local sG = M.bip340_point(L:bip340_scalar_mult(...))
953- function M .bip340_point (x , y , z )
954- return { x = x , y = y , z = z }
955- end
956-
957- --- Declare all BIP340 witness wires on a named logic and return a
958- --- structured table of named wire references for use in gadget calls.
959- ---
960- --- Layout matches Bip340Verify::Witness::input():
961- --- Public: rx, px, e
962- --- Private: bits_s[256], int_s.{x,y,z}[255],
963- --- bits_e[256], int_e.{x,y,z}[255],
964- --- py, ry, rz_inv, bits_ry[256]
965- ---
966- --- Returns:
967- --- {
968- --- rx = <EltW>, px = <EltW>, e = <EltW>,
969- --- bits_s = { [1..256] = <EltW> },
970- --- int_s = { x = { [1..256] }, y = { [1..256] }, z = { [1..256] } },
971- --- bits_e = { [1..256] = <EltW> },
972- --- int_e = { x = { [1..256] }, y = { [1..256] }, z = { [1..256] } },
973- --- py = <EltW>, ry = <EltW>, rz_inv = <EltW>,
974- --- bits_ry = { [1..256] = <EltW> },
975- --- }
976- function M .declare_bip340_witness (L )
977- -- Public inputs
978- local rx = L :public_input { name = " rx" , desc = " R.x (x-only)" , type = " field" }
979- local px = L :public_input { name = " px" , desc = " P.x (x-only public key)" , type = " field" }
980- local e = L :public_input { name = " e" , desc = " Fiat-Shamir challenge" , type = " field" }
981-
982- -- s·G trace: bits + intermediates (interleaved)
983- local bits_s = {}
984- local int_sx , int_sy , int_sz = {}, {}, {}
985- for i = 1 , 256 do
986- bits_s [i ] = L :private_input {
987- name = string.format (" bits_s_%03d" , i ),
988- desc = string.format (" s bit %d (MSB-first)" , i ),
989- type = " field" ,
990- }
991- if i < 256 then
992- int_sx [i ] = L :private_input {
993- name = string.format (" int_sx_%03d" , i ),
994- desc = string.format (" s·G intermediate x %d" , i ),
995- type = " field" ,
996- }
997- int_sy [i ] = L :private_input {
998- name = string.format (" int_sy_%03d" , i ),
999- desc = string.format (" s·G intermediate y %d" , i ),
1000- type = " field" ,
1001- }
1002- int_sz [i ] = L :private_input {
1003- name = string.format (" int_sz_%03d" , i ),
1004- desc = string.format (" s·G intermediate z %d" , i ),
1005- type = " field" ,
1006- }
1007- end
1008- end
1009-
1010- -- e·P trace: bits + intermediates (interleaved)
1011- -- int_e arrays are padded to 256 elements for API compatibility.
1012- local bits_e = {}
1013- local int_ex , int_ey , int_ez = {}, {}, {}
1014- for i = 1 , 256 do
1015- bits_e [i ] = L :private_input {
1016- name = string.format (" bits_e_%03d" , i ),
1017- desc = string.format (" e bit %d (MSB-first)" , i ),
1018- type = " field" ,
1019- }
1020- if i < 256 then
1021- int_ex [i ] = L :private_input {
1022- name = string.format (" int_ex_%03d" , i ),
1023- desc = string.format (" e·P intermediate x %d" , i ),
1024- type = " field" ,
1025- }
1026- int_ey [i ] = L :private_input {
1027- name = string.format (" int_ey_%03d" , i ),
1028- desc = string.format (" e·P intermediate y %d" , i ),
1029- type = " field" ,
1030- }
1031- int_ez [i ] = L :private_input {
1032- name = string.format (" int_ez_%03d" , i ),
1033- desc = string.format (" e·P intermediate z %d" , i ),
1034- type = " field" ,
1035- }
1036- else
1037- int_ex [i ] = bits_e [i ]
1038- int_ey [i ] = bits_e [i ]
1039- int_ez [i ] = bits_e [i ]
1040- end
1041- end
1042-
1043- -- P.y (the even square root)
1044- local py = L :private_input {
1045- name = " py" , desc = " P.y (even square root)" , type = " field" ,
1046- }
1047-
1048- -- R.y (affine, the canonical even y), rz_inv, and ry bits
1049- local ry = L :private_input {
1050- name = " ry" , desc = " R.y (affine, even)" , type = " field" ,
1051- }
1052- local rz_inv = L :private_input {
1053- name = " rz_inv" , desc = " R.z inverse" , type = " field" ,
1054- }
1055-
1056- local bits_ry = {}
1057- for i = 1 , 256 do
1058- bits_ry [i ] = L :private_input {
1059- name = string.format (" bits_ry_%03d" , i ),
1060- desc = string.format (" ry bit %d (MSB-first)" , i ),
1061- type = " field" ,
1062- }
1063- end
1064-
1065- return {
1066- rx = rx , px = px , e = e ,
1067- bits_s = bits_s ,
1068- int_s = { x = int_sx , y = int_sy , z = int_sz },
1069- bits_e = bits_e ,
1070- int_e = { x = int_ex , y = int_ey , z = int_ez },
1071- py = py , ry = ry , rz_inv = rz_inv ,
1072- bits_ry = bits_ry ,
1073- }
1074- end
1075-
1076- --- Build a named witness inputs table from a native bip340_compute result.
1077- --- This maps the native witness OCTET values to named keys matching
1078- --- declare_bip340_witness output.
1079- --- Returns { inputs = {...}, public_inputs = {...} } with string keys.
1080- function M .bip340_witness_named (witness_result )
1081- local named = {
1082- rx = witness_result .rx ,
1083- px = witness_result .px ,
1084- e = witness_result .e ,
1085- }
1086-
1087- -- s·G trace (bits: 256, ints: 255)
1088- for i = 1 , 256 do
1089- named [string.format (" bits_s_%03d" , i )] = witness_result .bits_s [i ]
1090- if i < 256 then
1091- named [string.format (" int_sx_%03d" , i )] = witness_result .int_sx [i ]
1092- named [string.format (" int_sy_%03d" , i )] = witness_result .int_sy [i ]
1093- named [string.format (" int_sz_%03d" , i )] = witness_result .int_sz [i ]
1094- end
1095- end
1096-
1097- -- e·P trace (bits: 256, ints: 255)
1098- for i = 1 , 256 do
1099- named [string.format (" bits_e_%03d" , i )] = witness_result .bits_e [i ]
1100- if i < 256 then
1101- named [string.format (" int_ex_%03d" , i )] = witness_result .int_ex [i ]
1102- named [string.format (" int_ey_%03d" , i )] = witness_result .int_ey [i ]
1103- named [string.format (" int_ez_%03d" , i )] = witness_result .int_ez [i ]
1104- end
1105- end
1106-
1107- named .py = witness_result .py
1108- named .ry = witness_result .ry
1109- named .rz_inv = witness_result .rz_inv
1110-
1111- for i = 1 , 256 do
1112- named [string.format (" bits_ry_%03d" , i )] = witness_result .bits_ry [i ]
1113- end
1114-
1115- return named
1116- end
1117-
1118- --- Compile a Lua-authored BIP340 circuit, build witness inputs from a
1119- --- valid signature, prove, and verify.
1120- ---
1121- --- Design: Lua authors the verification sequence using granular gadget
1122- --- primitives (bip340_addE, bip340_doubleE, bip340_scalar_mult, etc.).
1123- --- C++ gadgets emit the production-tested constraint formulas — there is
1124- --- exactly one C++ implementation of each EC formula, shared by the
1125- --- native monolithic Bip340Verify and this Lua-authored path.
1126- ---
1127- --- BIP-340 tagged SHA-256 and input parsing (r < p, s < n, pk lift)
1128- --- are deliberately NOT proven in-circuit. The circuit proves the
1129- --- algebraic relation given a public challenge e; the binding between e
1130- --- and the message/public-key is established by the verifier's own hash
1131- --- computation outside the proof system (matching Bip340Witness).
1132- ---
1133- --- This is the recommended entry point for the Lua-authored BIP340 flow.
1134- --- Usage:
1135- --- local compiled = M.bip340_lua_circuit_compile()
1136- --- local result = M.bip340_lua_prove_verify(compiled, sig, pk, msg, seed)
1137- function M .bip340_lua_circuit_compile ()
1138- local L = M .named_logic (" bip340" )
1139- L :set_version (" 1.0.0" )
1140- L :set_author (" Lua-authored BIP340 gadget circuit" )
1141-
1142- -- Declare witness wires
1143- local w = M .declare_bip340_witness (L )
1144- L :bind_inputs ()
1145-
1146- -- Generator point (constant)
1147- local Gx = L :bip340_gx ()
1148- local Gy = L :bip340_gy ()
1149- local one = L :konst (L :one ())
1150- local zero = L :konst (L :zero ())
1151-
1152- -- 0. Verify e matches bits_e decomposition (MSB-first)
1153- L :bip340_assert_field_from_bits_msb (w .bits_e , w .e )
1154-
1155- -- 1. Verify s is a canonical secp256k1 scalar (0 <= s < n)
1156- L :bip340_assert_scalar_lt_order (w .bits_s )
1157-
1158- -- 2. Verify P is on the curve (py² = px³ + 7)
1159- L :bip340_assert_point_on_curve (w .px , w .py )
1160-
1161- -- 3. Compute s·G
1162- local sG_x , sG_y , sG_z = L :bip340_scalar_mult (
1163- Gx , Gy , one ,
1164- w .bits_s , w .int_s .x , w .int_s .y , w .int_s .z )
1165-
1166- -- 4. Compute e·P
1167- local eP_x , eP_y , eP_z = L :bip340_scalar_mult (
1168- w .px , w .py , one ,
1169- w .bits_e , w .int_e .x , w .int_e .y , w .int_e .z )
1170-
1171- local neg_eP_y = L :sub (zero , eP_y )
1172- local R_x , R_y , R_z = L :bip340_addE (
1173- sG_x , sG_y , sG_z ,
1174- eP_x , neg_eP_y , eP_z )
1175-
1176- -- 6. Verify R is on the curve and finite
1177- L :bip340_assert_point_on_curve (w .rx , w .ry )
1178- -- Use L:mul to ensure placeholder resolution (R_z is EltW, w.rz_inv is placeholder)
1179- L :assert_eq (L :mul (R_z , w .rz_inv ), one )
1180-
1181- -- 7. Check R.x == rx (projective equality)
1182- L :assert_eq (R_x , L :mul (w .rx , R_z ))
1183-
1184- -- 8. Check R.y == ry (projective equality)
1185- L :assert_eq (R_y , L :mul (w .ry , R_z ))
1186-
1187- -- 9. Verify ry bitness, reconstruction, and even parity
1188- L :bip340_assert_ry_bitness_and_even (w .bits_ry , w .ry )
1189-
1190- return L :compile ()
1191- end
919+ -- Expose internals for bip340 module
920+ M .native = native
921+ M .wrap_artifact = wrap_artifact
922+ M .make_bip340_schema = make_bip340_schema
923+ M .is_named_artifact = is_named_artifact
924+
925+ -- Load BIP340-specific circuit helpers (attaches to M).
926+ require (" crypto_zkcc_bip340" ).setup (M )
1192927
1193928return M
0 commit comments