Skip to content

Commit

Permalink
[r1cs] finish parser of R1CS files (w/o custom gate list / apps)
Browse files Browse the repository at this point in the history
  • Loading branch information
@Vindaar
Vindaar committed Jun 7, 2024
1 parent 0b92196 commit ac6bc11
Showing 1 changed file with 186 additions and 26 deletions.
212 changes: 186 additions & 26 deletions constantine/proof_systems/constraint_systems/r1cs_circom_parser.nim
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,15 +20,20 @@ import
../../serialization/[io_limbs, parsing],
../../platforms/[fileio, abstractions]

# We use `sortedByIt` to sort the different sections in the file by their
# `R1csSectionKind`
from std / algorithm import sortedByIt

type
R1csSectionKind = enum
kHeader = 1
kConstraints = 2
kWire2LabelId = 3
kCustomGatesList = 4
kGustomGatesApplication = 5
R1csSectionKind = enum # Actual values according to spec in comments. To use it as discriminator in variant object
kHeader = 0 # 1
kConstraints = 1 # 2
kWire2LabelId = 2 # 3
kCustomGatesList = 3 # 4
kCustomGatesApplication = 4 # 5

Factor = tuple[index: int32, value: seq[BaseType]]
#Factor = tuple[index: int32, value: seq[byte]]
LinComb = seq[Factor]
# A struct-of-arrays (SoA) is more efficient than seq[Constraint] array-of-structs (AoS)
# but at the moment we use a seq[BaseType] indirection for field elements
Expand All @@ -40,22 +45,82 @@ type
Constraint = tuple[A, B, C: LinComb]
# A .* B = C with .* pointwise/elementwise mul (Hadamard Product)

#[
Header section example
┏━━━━┳━━━━━━━━━━━━━━━━━┓
┃ 4 │ 20 00 00 00 ┃ Field Size in bytes (fs)
┗━━━━┻━━━━━━━━━━━━━━━━━┛
┏━━━━┳━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┓
┃ fs │ 010000f0 93f5e143 9170b979 48e83328 5d588181 b64550b8 29a031e1 724e6430 ┃ Prime size
┗━━━━┻━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┛
┏━━━━┳━━━━━━━━━━━━━━━━━┓
┃ 32 │ 01 00 00 00 ┃ nWires
┗━━━━┻━━━━━━━━━━━━━━━━━┛
┏━━━━┳━━━━━━━━━━━━━━━━━┓
┃ 32 │ 01 00 00 00 ┃ nPubOut
┗━━━━┻━━━━━━━━━━━━━━━━━┛
┏━━━━┳━━━━━━━━━━━━━━━━━┓
┃ 32 │ 01 00 00 00 ┃ nPubIn
┗━━━━┻━━━━━━━━━━━━━━━━━┛
┏━━━━┳━━━━━━━━━━━━━━━━━┓
┃ 32 │ 01 00 00 00 ┃ nPrvIn
┗━━━━┻━━━━━━━━━━━━━━━━━┛
┏━━━━┳━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┓
┃ 64 │ 01 00 00 00 00 00 00 00 ┃ nLabels
┗━━━━┻━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┛
┏━━━━┳━━━━━━━━━━━━━━━━━┓
┃ 32 │ 01 00 00 00 ┃ mConstraints
┗━━━━┻━━━━━━━━━━━━━━━━━┛
]#
Header = object
fieldSize: uint32 # field size in bytes (fs)
prime: seq[byte] # XXX: What type to use with RT size info?
nWires: uint32
nPubOut: uint32
nPubIn: uint32
nPrvIn: uint32
nLabels: uint64
nConstraints: uint32

#[
Wire 2 Label section example
┏━━━━┳━━━━━━━━━━━━━━━━━━━┳━━━━┳━━━━━━━━━━━━━━━━━━━┓ ┏━━━━┳━━━━━━━━━━━━━━━━━━━┓
┃ 64 │ labelId of Wire_0 ┃ 64 │ labelId of Wire_1 ┃ ... ┃ 64 │ labelId of Wire_n ┃
┗━━━━┻━━━━━━━━━━━━━━━━━━━┻━━━━┻━━━━━━━━━━━━━━━━━━━┛ ┗━━━━┻━━━━━━━━━━━━━━━━━━━┛
]#
Wire2Label = object
wireIds: seq[uint64]

Section = object
size: uint64 # NOTE: in the real file the section type is *FIRST* and then the size
# But we cannot map this with a variant type in Nim (without using different
# names for each variant branch)
case sectionType: R1csSectionKind
of kHeader: header: Header
of kConstraints: constraints: seq[Constraint]
of kWire2LabelId: w2l: Wire2Label
of kCustomGatesList: cGatesList: R1csCustomGatesList
of kCustomGatesApplication: cGatesApp: R1csCustomGatesApp

## `R1csBin` is binary compatible with an R1CS binary file. Meaning it follows the structure
## of the file (almost) exactly. The only difference is in the section header. The size comes
## *after* the kind, which we don't reproduce in `Section` above
R1csBin = object
magic: array[4, char]
version: uint32
# ---- Header ----
fieldSize: int32 # Field size in bytes, MUST be a multiple of 8
prime: seq[BaseType]
# ---- Sections ----
constraints: seq[Constraint]
wireIdToLabelId: seq[int64]
# ---- Plonk ----
customGatesList: R1csCustomGatesList
customGatesApp: R1csCustomGatesApp
numberSections: uint32
sections: seq[Section] # Note: Because of the unordered nature of the sections
# the `sections` seq won't follow the binary order of
# the data in the file. Instead, we first record (kind, file position)
# of each different section in the file and then parse them in increasing
# order of the section types

R1csCustomGatesList = object
R1csCustomGatesApp = object

proc initSection(kind: R1csSectionKind, size: uint64): Section =
result = Section(sectionType: kind, size: size)

proc parseLinComb(f: File, lincomb: var LinComb, fieldSize: int32): bool =
## Parse a linear combination, returns true on success
## This does not validate that the elements parsed are part of the field
Expand All @@ -64,7 +129,8 @@ proc parseLinComb(f: File, lincomb: var LinComb, fieldSize: int32): bool =
lincomb.setLen(int(nnz))

var last = low(int32)
let len = fieldSize.ceilDiv_vartime(WordBitWidth)
# fieldSize is in bytes!
let len = (fieldSize * 8).ceilDiv_vartime(WordBitWidth)
var buf = newSeq[byte](fieldSize)

for i in 0 ..< nnz:
Expand All @@ -83,23 +149,117 @@ proc parseConstraint(f: File, constraint: var Constraint, fieldSize: int32): boo
?f.parseLinComb(constraint.C, fieldSize)
return true

template r1csSection(body: untyped): untyped =
var sectionSize: int64
?f.parseInt(sectionSize, littleEndian)
template r1csSection(sectionSize, body: untyped): untyped =
let startOffset = f.getFilePosition()

body

return sectionSize == f.getFilePosition() - startOffset
return sectionSize.int == f.getFilePosition() - startOffset

proc parseConstraints(f: File, constraints: var seq[Constraint], numConstraints, fieldSize: int32): bool =
r1csSection:
proc parseConstraints(f: File, constraints: var seq[Constraint], sectionSize: uint64, numConstraints, fieldSize: int32): bool =
r1csSection(sectionSize):
constraints.setLen(numConstraints)
for constraint in constraints.mitems():
?f.parseConstraint(constraint, fieldSize)

proc parseWireLabelMap(f: File, wireIdToLabelId: var seq[int64], numWires: int32): bool =
r1csSection:
wireIdToLabelId.setLen(numWires)
for labelId in wireIdToLabelId.mitems():
proc parseMagicHeader(f: File, mh: var array[4, char]): bool =
let num = f.readChars(mh, 0, 4) # from start of file!
result = num == 4

proc parseSectionKind(f: File, v: var R1csSectionKind): bool =
var val: uint32
result = f.parseInt(val, littleEndian)
# convert from uint32 value and correct for -1 in definition of enum
v = R1csSectionKind(val.int - 1)

proc parseHeader(f: File, h: var Header): bool =
?f.parseInt(h.fieldSize, littleEndian) # byte size of the prime number
# allocate for the prime
h.prime = newSeq[byte](h.fieldSize)
?f.readInto(h.prime)
?f.parseInt(h.nWires, littleEndian)
?f.parseInt(h.nPubOut, littleEndian)
?f.parseInt(h.nPubIn, littleEndian)
?f.parseInt(h.nPrvIn, littleEndian)
?f.parseInt(h.nLabels, littleEndian)
?f.parseInt(h.nConstraints, littleEndian)
result = true # would have returned before due to `?` otherwise

proc parseWire2Label(f: File, v: var Wire2Label, sectionSize: uint64): bool =
r1csSection(sectionSize):
let numWires = sectionSize div 8
v.wireIds.setLen(numWires)
for labelId in v.wireIds.mitems():
?f.parseInt(labelId, littleEndian)

## TODO: to be written :)
proc parseCustomGatesList(f: File, v: var R1csCustomGatesList): bool = discard
proc parseCustomGatesApplication(f: File, v: var R1csCustomGatesApp): bool = discard

proc getNumConstraints(r1cs: R1csBin): int32 =
## Returns the number of constraints in the file, based on the header
## This means the header must have been parsed and is located in `sections[0]`.
doAssert r1cs.sections[0].sectionType == kHeader
result = r1cs.sections[0].header.nConstraints.int32

proc getFieldSize(r1cs: R1csBin): int32 =
## Returns the field size (size of the prime) in the file, based on the header
## This means the header must have been parsed and is located in `sections[0]`.
doAssert r1cs.sections[0].sectionType == kHeader
result = r1cs.sections[0].header.fieldSize.int32

proc parseSection(f: File, s: var Section, kind: R1csSectionKind, size: uint64, r1cs: R1csBin): bool =
# NOTE: The `r1cs` object is there to provide the header information to
# the constraints section
s = initSection(kind, size)
case kind
of kHeader: ?f.parseHeader(s.header)
of kConstraints: ?f.parseConstraints(s.constraints, size, r1cs.getNumConstraints(), r1cs.getFieldSize())
of kWire2LabelId: ?f.parseWire2Label(s.w2l, size)
of kCustomGatesList: ?f.parseCustomGatesList(s.cGatesList)
of kCustomGatesApplication: ?f.parseCustomGatesApplication(s.cGatesApp)

result = true # would have returned otherwise due to `?`

proc parseR1csFile(path: string): R1csBin =
var f = fileio.open(path, kRead)

doAssert f.parseMagicHeader(result.magic), "Failed to read magic header"
doAssert f.parseInt(result.version, littleEndian), "Failed to read version"
doAssert f.parseInt(result.numberSections, littleEndian), "Failed to read number of sections"

result.sections = newSeq[Section](result.numberSections)
# 1. determine the section kind, size & file position for each section in the file
var pos = newSeq[(R1csSectionKind, uint64, int)](result.numberSections)
let fp = f.getFilePosition()
for i in 0 ..< result.numberSections:
var kind: R1csSectionKind
var size: uint64 # section size
doAssert f.parseSectionKind(kind), "Failed to read section type in section " & $i
doAssert f.parseInt(size, littleEndian), "Failed to read section size in section " & $i
# compute position of next section
pos[i] = (kind, size, f.getFilePosition())
let np = f.getFilePosition() + size.int # compute beginning of next section header
# set file pos to after
doAssert f.setFilePosition(np) == 0, "Failed to set file position to " & $np

# Sort the positions by the section type
pos = pos.sortedByIt(it[0]) # sort by the section kind
doAssert pos[0][0] == kHeader, "No header present in the file"

# 2. iterate the different kinds / positions & parse them
for i, (kind, size, p) in pos: # set position to start of section & parse
doAssert f.setFilePosition(p) == 0, "Failed to set file position to " & $p
doAssert f.parseSection(result.sections[i], kind, size, result), "Failed to parse section " & $i
if i == 0: # assert we read the header!
doAssert kind == kHeader

fileio.close(f)
echo result

when isMainModule:
# let's try to parse a files
const path = "/t/example.r1cs"
#const path = "/t/circuitCG.r1cs"

let r1cs = parseR1csFile(path)

0 comments on commit ac6bc11

Please sign in to comment.