logos-storage/circom-witnessgen
1
0
Fork 0
mirror of https://github.com/logos-storage/circom-witnessgen.git synced 2026-06-05 15:29:25 +00:00
Code Issues Packages Projects Releases Wiki Activity

partial witness generation

Browse Source
This commit is contained in:
Balazs Komuves 2026-01-15 18:14:02 +01:00
parent 89679e2f05
commit 9f7cc651a2
No known key found for this signature in database
GPG Key ID: F63B7AEF18435562
12 changed files with 385 additions and 51 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
README.md
View File

@ -7,13 +7,16 @@ files generated by [`circom-witnesscalc`](https://github.com/iden3/circom-witnes
and either interpret or compile them to various algebra backends.
While this is quite straightforward in principle, and seems to work on particular
examples, it turns out that `circom-witnesscalc` itself has some serious limitations.
examples, it turns out that (the legacy version of) `circom-witnesscalc` itself
has some serious limitations.
The biggest one is that it doesn't support any kind of dynamic computation (which should
be obvious from the fact that it produces a static graph). But even if one uses only
static computations, there are further very annoying things which just don't work.
However at the end this is still a useful thing, as many circuits still work.
However at the end this is still a useful thing, as many (most?) circuits still work, and
the resulting static graph is much simpler than a VM bytecode (and easy to statically
analyse too!).
### Compiler
@ -42,7 +45,7 @@ Haskell compiler:
- [ ] zikkurat backend
- [ ] arkworks backend
Nim witness generator (to be used with [`nim-groth16`](https://github.com/codex-storage/nim-groth16))
Nim witness generator (to be used with [`nim-groth16`](https://github.com/logos-storage/nim-groth16))
- [x] parsing the graph file
- [x] parsing json input
@ -68,9 +71,12 @@ by `circom-witnesscalc`.
### Graph file format
`circom-witnesscalc` produces binary files encoding a computation graph.
The (legacy version of) `circom-witnesscalc` produces binary files encoding a computation graph.
This has the following format:
Note: `circom-witnesscalc` since changed to a VM based approach to support dynamic
computations (see above). However here we require the legacy version, called `build-circuit`.
This computation graph description file has the following format:
- magic header: `"wtns.graph.001"` (14 bytes)
- number of nodes (8 bytes little endian)

4
nim/.gitignore vendored
View File

@ -1 +1,3 @@
main
.DS_Store
main
tmp/

78
nim/circom_witnessgen/dependencies.nim Normal file
View File

@ -0,0 +1,78 @@
# figure out the part of the witness which depends on a given set of inputs
#
# this is intended to be used when a significant part of the witness is
# either constant or rarely changes, so a part of the proof generation
# can be precomputed
#-------------------------------------------------------------------------------
import std/sequtils
import std/sets
import ./types
import ./graph
#-------------------------------------------------------------------------------
func isElem[T](what: T, list: seq[T]): bool = count(list,what) > 0
# note: the resulting set contains the _normal_ witness indices of the _unchanging_ inputs
# these indices are _different_ from the graph indices, because normally there
# are much more graph nodes than witness elements
proc unchangingInputIndices(circuitInputs: seq[(string, SignalDescription)], unchanging: seq[string]): HashSet[int] =
var table: HashSet[int]
incl(table, 0) # index 0 is constant 1, it never changes
for (key, desc) in circuitInputs:
if isElem(key,unchanging):
let k: int = int(desc.length)
let o: int = int(desc.offset)
for i in 0..<k:
incl(table, o + i)
return table
#-------------------------------------------------------------------------------
func symbolicEvalNode( inputs: HashSet[int] , node: Node[bool] ): bool =
case node.kind:
of Input: return contains(inputs, int(node.inp.idx))
of Const: return true
of Uno: return node.uno.arg1
of Duo: return (node.duo.arg1 and node.duo.arg2)
of Tres: return (node.tres.arg1 and node.tres.arg2 and node.tres.arg3)
#-------------------------------------------------------------------------------
# this returns an bool for each graph node
proc runSymbolicComputation(graph: Graph, unchanging: seq[string]): seq[bool] =
let sequence : seq[Node[uint32]] = graph.nodes
let graphMeta : GraphMetaData = graph.meta
var markedInputs : HashSet[int] = unchangingInputIndices(graphMeta.inputSignals, unchanging)
var output: seq[bool] = newSeq[bool]( sequence.len )
for (i, node_orig) in sequence.pairs():
let node: Node[bool] = fmap[uint32,bool]( proc (idx: uint32): bool = output[int(idx)] , node_orig )
output[i] = symbolicEvalNode( markedInputs , node )
return output
proc calcWitnessMask*(graph: Graph, unchanging: seq[string]): WitnessMask =
let mapping: seq[uint32] = graph.meta.witnessMapping.mapping
let pre_witness = runSymbolicComputation(graph, unchanging)
var mask: seq[bool] = newSeq[bool](mapping.len)
for (j, idx) in mapping.pairs():
mask[j] = pre_witness[int(idx)]
let full = mapping.len
let cnt = countMask(mask)
echo "witness size = " & $full
echo "unchanging = " & $cnt
echo "remaining = " & $(full-cnt)
return mask
#-------------------------------------------------------------------------------

3
nim/circom_witnessgen/export_wtns.nim
View File

@ -3,6 +3,7 @@ import std/streams
import pkg/constantine/math/io/io_bigints
import ./types
import ./field
#-------------------------------------------------------------------------------
@ -44,7 +45,7 @@ proc exportFeltSequence*(filepath: string, values: seq[F]) =
for i in 0..<values.len:
stream.writeFelt( values[i] )
proc exportWitness*(filepath: string, witness: seq[F]) =
proc exportWitness*(filepath: string, witness: Witness) =
var stream = newFileStream(filepath, fmWrite)
stream.writeHeader(witness.len)
for i in 0..<witness.len:

80
nim/circom_witnessgen/field.nim
View File

@ -1,9 +1,15 @@
import std/bitops
import pkg/constantine/math/arithmetic
import pkg/constantine/math/io/io_bigints
import pkg/constantine/math/io/io_fields
import pkg/constantine/named/properties_fields
import pkg/constantine/platforms/abstractions
#import pkg/constantine/math_arbitrary_precision/arithmetic/limbs_divmod
#import pkg/constantine/math_arbitrary_precision/arithmetic/limbs_divmod_vartime
#-------------------------------------------------------------------------------
type
@ -13,14 +19,17 @@ type
const zeroB* : B = fromHex( BigInt[254], "0x00" )
const oneB* : B = fromHex( BigInt[254], "0x01" )
func isZeroB* (x: B ) : bool = bool(isZero(x))
func isEqualB* (x, y: B ) : bool = bool(x == y)
const zeroF* : F = fromHex( Fr[BN254Snarks], "0x00" )
const oneF* : F = fromHex( Fr[BN254Snarks], "0x01" )
func isZeroB* (x: B ) : bool = bool(isZero(x))
func isZeroF* (x: F ) : bool = bool(isZero(x))
func isNonZeroF*(x: F ) : bool = not isZeroF(x)
func isEqualF* (x, y: F ) : bool = bool(x == y)
func `===`* (x, y: F ) : bool = isEqualF(x,y)
func `!==`* (x, y: F ) : bool = not isEqualF(x,y)
const fieldMask* : B = fromHex( BigInt[254] , "0x3fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", bigEndian )
const fieldPrime* : B = fromHex( BigInt[254] , "0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", bigEndian )
@ -77,12 +86,57 @@ func fToDecimal*(x: F): string =
#-------------------------------------------------------------------------------
func mulTruncB(x: B, y: B): B =
var z: BigInt[512]
prod[512,254,254](z,x,y)
let us: array[8, SecretWord] = z.limbs
var vs: array[4, SecretWord]
vs[0] = us[0]
vs[1] = us[1]
vs[2] = us[2]
vs[3] = SecretWord( bitand( uint64(us[3]) , 0x3fffffffffffffff'u64 ) )
return BigInt[254](limbs: vs)
#[
# note: constantine's `divRem_vartime` doesn't seem to function correctly...
func divB*(x: B, y: B): B =
if isZeroB(y):
return zeroB
else:
let a: array[4, SecretWord] = x.limbs
let b: array[4, SecretWord] = y.limbs
var q: array[4, SecretWord]
var r: array[4, SecretWord]
let _ = divRem_vartime(q,r,a,b)
return BigInt[254](limbs: q)
func modB*(x: B, y: B): B =
if isZeroB(y):
return zeroB
else:
let a: array[4, SecretWord] = x.limbs
let b: array[4, SecretWord] = y.limbs
var q: array[4, SecretWord]
var r: array[4, SecretWord]
let _ = divRem_vartime(q,r,a,b)
return BigInt[254](limbs: r)
]#
#-------------------------------------------------------------------------------
func negB* (y: B ): B = ( var z : B = zeroB ; z -= y ; return z )
func negF* (y: F ): F = ( var z : F = zeroF ; z -= y ; return z )
func invF* (y: F ): F = ( var z : F = y ; if isNonZeroF(y): z.inv() ; return z )
func `+`*[n](x, y: BigInt[n] ): BigInt[n] = ( var z : BigInt[n] = x ; z += y ; return z )
func `-`*[n](x, y: BigInt[n] ): BigInt[n] = ( var z : BigInt[n] = x ; z -= y ; return z )
func `*`*[n](x, y: BigInt[n] ): BigInt[n] = mulTruncB(x,y)
#---------------------------------------
func negF* (y: F ): F = ( var z : F = zeroF ; z -= y ; return z )
func invF* (y: F ): F = ( var z : F = y ; if isNonZeroF(y): z.inv() ; return z )
func `+`*(x, y: F ): F = ( var z : F = x ; z += y ; return z )
func `-`*(x, y: F ): F = ( var z : F = x ; z -= y ; return z )
@ -95,3 +149,23 @@ func powF*(x: F, y: B): F =
return z
#-------------------------------------------------------------------------------
#[
proc divModSanityCheck*() =
# let x: B = decimalToB("12345678901234567890666");
# let y: B = decimalToB("7654321");
let x: B = decimalToB("18446744073709551618");
let y: B = decimalToB("7654321");
let q = divB(x,y)
let r = modB(x,y)
echo "x = " & bigToDecimal(x)
echo "y = " & bigToDecimal(y)
echo "q = " & bigToDecimal(q)
echo "r = " & bigToDecimal(r)
let check = q * y + r
echo "reconstr = " & bigToDecimal(check)
echo "ok = " & $(isEqualB(check,x))
]#

2
nim/circom_witnessgen/graph.nim
View File

@ -10,8 +10,6 @@ import ./field
type
Inputs* = Table[string, seq[F]]
UnoOp* = enum
Neg,
Id,

2
nim/circom_witnessgen/input_json.nim
View File

@ -4,7 +4,7 @@ import std/json
import std/tables
import ./field
import ./graph
import ./types
#-------------------------------------------------------------------------------

114
nim/circom_witnessgen/partial.nim Normal file
View File

@ -0,0 +1,114 @@
# compute *partial* witness (based on partially set inputs)
import std/tables
import std/options
#import std/strformat
import ./field
import ./types
import ./graph
import ./semantics
#-------------------------------------------------------------------------------
# the indices here are the witness indices, not the graph node indices!
proc expandPartialInputs(circuitInputs: seq[(string, SignalDescription)] , partialInputs: Inputs): Table[int, F] =
var table: Table[int, F]
table[0] = oneF
for (key, desc) in circuitInputs:
let k: int = int(desc.length)
let o: int = int(desc.offset)
if partialInputs.hasKey(key):
let list: seq[F] = partialInputs[key]
assert( list.len == k , "(partial) input signal `" & key & "` has unexpected size" )
for i in 0..<k:
table[o + i] = list[i]
# echo "input value " & (fToDecimal(list[i])) & " at offset " & ($(o+i))
return table
#-------------------------------------------------------------------------------
func fromOptionF(mbF: Option[F]): F = mbF.get(zeroF)
# please nim, just go home, you are drunk!! (again!!!)
proc fromOptionNode(mbNode: Node[Option[F]] ): Option[Node[F]] =
case mbNode.kind:
of Input: return some( Node[F](kind: Input, inp: mbNode.inp) )
of Const: return some( Node[F](kind: Const, kst: mbNode.kst) )
of Uno:
if isSome(mbNode.uno.arg1):
return some( fmap[Option[F],F]( fromOptionF , mbNode ) )
else:
return none(Node[F])
of Duo:
if isSome(mbNode.duo.arg1) and isSome(mbNode.duo.arg2):
return some( fmap[Option[F],F]( fromOptionF , mbNode ) )
else:
return none(Node[F])
of Tres:
if isSome(mbNode.tres.arg1) and isSome(mbNode.tres.arg2) and isSome(mbNode.tres.arg3):
return some( fmap[Option[F],F]( fromOptionF , mbNode ) )
else:
return none(Node[F])
#---------------------------------------
func lookup[T](table: Table[int,T], idx: int): Option[T] =
if table.hasKey(idx):
return some(table[idx])
else:
return none(T)
proc maybeEvalNode( partialInputs: Table[int,F] , almost_node: Node[Option[F]] ): Option[F] =
let mb_node: Option[Node[F]] = fromOptionNode(almost_node)
if isSome(mb_node):
let node: Node[F] = unsafeGet(mb_node)
case node.kind:
of Input: return lookup[F]( partialInputs, int(node.inp.idx) ) # we still may have undefined input!
of Const: return some( evalNode( partialInputs, node ) )
of Uno: return some( evalNode( partialInputs, node ) )
of Duo: return some( evalNode( partialInputs, node ) )
of Tres: return some( evalNode( partialInputs, node ) )
else:
return none(F)
#-------------------------------------------------------------------------------
# note: this contains temporary values which are not present in the actual witness
proc runPartialComputation(graph: Graph, partialInputs: Inputs): seq[Option[F]] =
let sequence : seq[Node[uint32]] = graph.nodes
let graphMeta : GraphMetaData = graph.meta
let circuitInputs : seq[(string, SignalDescription)] = graphMeta.inputSignals
let inpTable = expandPartialInputs(circuitInputs, partialInputs)
var output: seq[Option[F]] = newSeq[Option[F]]( sequence.len )
for (i, node_orig) in sequence.pairs():
let node: Node[Option[F]] = fmap[uint32,Option[F]]( proc (idx: uint32): Option[F] = output[int(idx)] , node_orig )
output[i] = maybeEvalNode( inpTable , node )
return output
proc generatePartialWitness*(graph: Graph, inputs: Inputs): PartialWitness =
let mapping: seq[uint32] = graph.meta.witnessMapping.mapping
let pre_witness = runPartialComputation(graph, inputs)
var output: seq[Option[F]] = newSeq[Option[F]](mapping.len)
for (j, idx) in mapping.pairs():
output[j] = pre_witness[int(idx)]
let full = mapping.len
let cnt = countSome(output)
echo "full witness size = " & $full
echo "computed values = " & $cnt
echo "unknown values = " & $(full-cnt)
return output
#-------------------------------------------------------------------------------

14
nim/circom_witnessgen/semantics.nim
View File

@ -136,22 +136,24 @@ proc shiftSanityCheck*() =
#-------------------------------------------------------------------------------
func evalUnoOpNode(op: UnoOp, x: F): F =
func evalUnoOpNode*(op: UnoOp, x: F): F =
case op:
of Neg: return negF(x)
of Id: return x
of LNot: return boolToF( not (fToBool x) )
of Bnot: return fieldComplement(x)
func evalDuoOpNode(op: DuoOp, x: F, y: F): F =
func evalDuoOpNode*(op: DuoOp, x: F, y: F): F =
case op:
of Mul: return x * y
of Div: return if isZeroF(y): zeroF else: x / y
of Add: return x + y
of Sub: return x - y
of Pow: return powF(x, fToBig(y)) # assert( false, "Pow: not yet implemented" )
of Idiv: assert( false, "Idiv: not yet implemented" ) # return bigToF( fToBig(x) div fToBig(y) )
of Mod: assert( false, "Mod: not yet implemented" ) # return bigToF( fToBig(x) mod fToBig(y) )
of Pow: return powF(x, fToBig(y))
# of Idiv: return bigToF( divB( fToBig(x) , fToBig(y) ) )
# of Mod: return bigToF( modB( fToBig(x) , fToBig(y) ) )
of Idiv: assert( false, "Idiv: not yet implemented" )
of Mod: assert( false, "Mod: not yet implemented" )
of Eq: return boolToF( x === y )
of Neq: return boolToF( not (x === y) )
of Lt: return boolToF( bool( fToBig(x) < fToBig(y) ) )
@ -166,7 +168,7 @@ func evalDuoOpNode(op: DuoOp, x: F, y: F): F =
of Band: return bigToF( bigIntBitwiseAnd( fToBig(x) , fToBig(y) ) )
of Bxor: return bigToF( bigIntBitwiseXor( fToBig(x) , fToBig(y) ) )
func evalTresOpNode(op: TresOp, x: F, y: F, z: F): F =
func evalTresOpNode*(op: TresOp, x: F, y: F, z: F): F =
case op:
of TernCond:
return (if fToBool(x): y else: z)

34
nim/circom_witnessgen/types.nim Normal file
View File

@ -0,0 +1,34 @@
# some more types (other than the graph type)
import std/options
import std/tables
import ./field
#-------------------------------------------------------------------------------
type
Inputs* = Table[string, seq[F]]
Witness* = seq[F]
WitnessMask* = seq[bool]
PartialWitness* = seq[Option[F]]
#-------------------------------------------------------------------------------
func countMask*(mask: WitnessMask): int =
var cnt = 0
for b in mask:
if b:
cnt += 1
return cnt
func countSome*[T](maybes: seq[Option[T]]): int =
var cnt = 0
for mb in maybes:
if isSome(mb):
cnt += 1
return cnt
#-------------------------------------------------------------------------------

29
nim/circom_witnessgen/witness.nim
View File

@ -1,13 +1,15 @@
import std/tables
import std/strformat
#import std/strformat
import ./field
import ./types
import ./graph
import ./semantics
#-------------------------------------------------------------------------------
# the indices here are the witness indices, not the graph node indices!
proc expandInputs*(circuitInputs: seq[(string, SignalDescription)] , inputs: Inputs): Table[int, F] =
var table: Table[int, F]
table[0] = oneF
@ -23,7 +25,7 @@ proc expandInputs*(circuitInputs: seq[(string, SignalDescription)] , inputs: Inp
return table
# note: this contains temporary values which are not present in the actual witness
proc generateFullComputation*(graph: Graph, inputs: Inputs): seq[F] =
proc runFullComputation*(graph: Graph, inputs: Inputs): seq[F] =
let sequence : seq[Node[uint32]] = graph.nodes
let graphMeta : GraphMetaData = graph.meta
@ -39,32 +41,13 @@ proc generateFullComputation*(graph: Graph, inputs: Inputs): seq[F] =
return output
#[
let node_orig = sequence[i]
let o = 32*i
let hexo = fmt"{o=:x}"
if (i == 11838): # o == 0x4fcc:
echo " i = " & ($i) & " | ofs = " & hexo & " | node = " & ($node_orig)
case node_orig.kind:
of Duo:
echo node_orig.duo.arg1
echo node_orig.duo.arg2
echo fToDecimal(output[int(node_orig.duo.arg1)])
echo fToDecimal(output[int(node_orig.duo.arg2)])
else:
discard
echo "result = " & fToDecimal(output[i])
echo " "
]#
proc generateWitness*(graph: Graph, inputs: Inputs): seq[F] =
proc generateWitness*(graph: Graph, inputs: Inputs): Witness =
let mapping: seq[uint32] = graph.meta.witnessMapping.mapping
let pre_witness = generateFullComputation(graph, inputs)
let pre_witness = runFullComputation(graph, inputs)
var output: seq[F] = newSeq[F](mapping.len)
for (j, idx) in mapping.pairs():
output[j] = pre_witness[int(idx)]
# echo " - " & ($j) & " -> " & fToDecimal(output[j]) & " | from " & ($idx)
return output
#-------------------------------------------------------------------------------

60
nim/main.nim
View File

@ -1,17 +1,25 @@
import std/options
import circom_witnessgen/field
# import circom_witnessgen/div_mod
import circom_witnessgen/types
import circom_witnessgen/load
import circom_witnessgen/input_json
import circom_witnessgen/dependencies
import circom_witnessgen/witness
import circom_witnessgen/partial
import circom_witnessgen/export_wtns
#-------------------------------------------------------------------------------
const graph_file: string = "../tmp/graph3.bin"
const input_file: string = "../tmp/input3.json"
const wtns_file: string = "../tmp/nim3.wtns"
const graph_file: string = "./tmp/rln_main.graph"
const input_file: string = "./tmp/input.json"
const partial_file: string = "./tmp/partial.json"
const wtns_file: string = "./tmp/output.wtns"
const unchanging_inputs: seq[string] = @["secret_key","msg_limit","merkle_root","leaf_idx","merkle_path"]
#-------------------------------------------------------------------------------
@ -24,15 +32,49 @@ when isMainModule:
when isMainModule:
echo "loading in " & input_file
echo "\nloading in " & graph_file
let gr = loadGraph(graph_file)
# echo $gr
echo $gr.meta.inputSignals
echo "\ncalculating witness mask"
let mask = calcWitnessMask(gr, unchanging_inputs)
echo $countMask(mask) & " filled out of " & $(mask.len)
echo "\nloading in " & partial_file
let partial_inp = loadInputJSON(partial_file)
# printInputs(partial_inp)
echo "\ngenerating partial witness"
let partial_wtns = generatePartialWitness(gr, partial_inp)
let cnt = countSome(partial_wtns)
echo $cnt & " filled out of " & $(partial_wtns.len)
echo "\nloading in " & input_file
let inp = loadInputJSON(input_file)
# printInputs(inp)
echo "loading in " & graph_file
let gr = loadGraph(graph_file)
echo $gr
echo "generating witness"
echo "\ngenerating witness"
let wtns = generateWitness( gr, inp )
exportWitness(wtns_file, wtns)
echo "\ncomparing partial and full witness"
var ok = true
for i in 0..<wtns.len:
if isSome(partial_wtns[i]):
let old_val = wtns[i]
let new_val = partial_wtns[i].unsafeGet()
if old_val !== new_val:
if ok:
echo "first witness index disagreeing = " & $i
echo " - full = " & fToDecimal(old_val)
echo " - partial = " & fToDecimal(new_val)
ok = false
if ok:
echo "OK."
else:
echo "FAILED!"
#-------------------------------------------------------------------------------