Summary
Currently, no constraints are generated for input memories (i.e. ROMs) in ZkC. Therefore, the purpose of this feature is to add initial support for generating such constraints.
Example
Consider the following very simple ZkC program:
input rom(address:u16) -> (byte:u8)
We can view the MIR constraints generated for this file using the following command:
> zkc compile --mir test.zkc
And this currently gives the following:
(module rom)
(inputs (address u16 0x0))
(outputs (byte u8 0x0))
The point being: there are no constraints generated.
Assumptions
A read-only memory maps consecutive addresses to values, starting from address 0. For our example above, an initial set of constraints might be something like this:
;; address starts from 0
(defconstraint rom$init (:domain {0}) (== 0 address))
;; address increments exactly by one
(defconstraint rom$inc (address == (+ 1 (prev address)))
The question is: what additional constraints do we need? In particular, we at least need a mechanism for handling padding.
Approach
For the purposes of this PR, we'll assume exactly one address line and zero or more data lines. This simplifies the logic for incrementing address in our constraints (this can be done in a subsequent PR). In the file pkg/zkc/constraints/translator.go we have the following:
func translateReadOnlyMemory[F field.Element[F]](_ schema.ModuleId, fm vm.InputOutputMemory[F]) mir.Module[F] {
var (
mod *schema.Table[F, mir.Constraint[F]]
name = trace.ModuleName{Name: fm.Name(), Multiplier: 1}
)
// Initialise module
mod = mod.Init(name, false, true, false, fm.IsNative(), false, 0)
// Add all registers
mod.AddRegisters(fm.Registers()...)
// TODO: implement ROM constraints
return mod
}
In particular, the TODO marks the place where constraints need to be generated. Looking at how constraints are generated for functions, particularly in initMultiLineFraming(), should be helpful in understanding how to actually construct the constraint objects.
Summary
Currently, no constraints are generated for
inputmemories (i.e. ROMs) in ZkC. Therefore, the purpose of this feature is to add initial support for generating such constraints.Example
Consider the following very simple ZkC program:
We can view the MIR constraints generated for this file using the following command:
And this currently gives the following:
The point being: there are no constraints generated.
Assumptions
A read-only memory maps consecutive addresses to values, starting from address
0. For our example above, an initial set of constraints might be something like this:The question is: what additional constraints do we need? In particular, we at least need a mechanism for handling padding.
Approach
For the purposes of this PR, we'll assume exactly one address line and zero or more data lines. This simplifies the logic for incrementing
addressin our constraints (this can be done in a subsequent PR). In the filepkg/zkc/constraints/translator.gowe have the following:In particular, the
TODOmarks the place where constraints need to be generated. Looking at how constraints are generated for functions, particularly ininitMultiLineFraming(), should be helpful in understanding how to actually construct the constraint objects.