Skip to content

Commit 3721199

Browse files
OlivierBBBOlivierBBB
committed
feat: unified memory
Signed-off-by: Olivier Bégassat <olivier.begassat.cours@gmail.com>
1 parent 6671d63 commit 3721199

1 file changed

Lines changed: 84 additions & 61 deletions

File tree

‎pkg/zkc/constraints/translator.go‎

Lines changed: 84 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -92,29 +92,46 @@ func translateStaticMemory[F field.Element[F]](_ schema.ModuleId, m vm.InputOutp
9292
return mod
9393
}
9494

95-
func translateReadOnlyMemory[F field.Element[F]](ctx schema.ModuleId, fm vm.InputOutputMemory[F]) mir.Module[F] {
95+
func translateReadOnlyMemory[F field.Element[F]](
96+
ctx schema.ModuleId, fm vm.InputOutputMemory[F]) mir.Module[F] {
97+
var name = trace.ModuleName{Name: fm.Name(), Multiplier: 1}
98+
return translateMemoryCommon(ctx, fm, name)
99+
}
100+
101+
// Write once memory and read only memory are equivalent on the constraints level
102+
func translateWriteOnceMemory[F field.Element[F]](
103+
ctx schema.ModuleId, fm vm.InputOutputMemory[F]) mir.Module[F] {
104+
var name = trace.ModuleName{Name: fm.Name(), Multiplier: 1}
105+
return translateMemoryCommon(ctx, fm, name)
106+
}
107+
108+
func translateReadWriteMemory[F field.Element[F]](
109+
ctx schema.ModuleId, fm vm.Memory[F]) mir.Module[F] {
110+
var name = trace.ModuleName{Name: fm.Name(), Multiplier: 1}
111+
return translateMemoryCommon(ctx, fm, name)
112+
}
113+
114+
func translateMemoryCommon[F field.Element[F]](
115+
ctx schema.ModuleId, fm vm.Memory[F], name trace.ModuleName) mir.Module[F] {
96116
var (
97-
romModule *schema.Table[F, mir.Constraint[F]]
98-
name = trace.ModuleName{Name: fm.Name(), Multiplier: 1}
117+
memoryModule *schema.Table[F, mir.Constraint[F]]
99118
padding big.Int
100119
timestampWidth = uint(32)
101120
)
102121

103-
// Initialise module
104-
romModule = romModule.Init(name, false, true, false, fm.IsNative(), false, 0)
105-
// Add all registers
106-
romModule.AddRegisters(fm.Registers()...)
122+
// Initialise module and add all registers
123+
memoryModule = memoryModule.Init(name, false, true, false, fm.IsNative(), false, 0)
124+
memoryModule.AddRegisters(fm.Registers()...)
107125

108-
// mod.AddRegisters(register.NewComputed(io.PC_NAME, pcWidth, padding))
109126
var (
110-
timestampRead = register.NewId(romModule.Width() + 0)
111-
timestampWritten = register.NewId(romModule.Width() + 1)
112-
timestampDelta = register.NewId(romModule.Width() + 2)
127+
timestampRead = register.NewId(memoryModule.Width() + 0)
128+
timestampWritten = register.NewId(memoryModule.Width() + 1)
129+
timestampDelta = register.NewId(memoryModule.Width() + 2)
113130
)
114131

115-
romModule.AddRegisters(register.NewComputed("timestamp_read", timestampWidth, padding))
116-
romModule.AddRegisters(register.NewComputed("timestamp_write", timestampWidth, padding))
117-
romModule.AddRegisters(register.NewComputed("timestamp_delta", timestampWidth, padding))
132+
memoryModule.AddRegisters(register.NewComputed("timestamp_read", timestampWidth, padding))
133+
memoryModule.AddRegisters(register.NewComputed("timestamp_write", timestampWidth, padding))
134+
memoryModule.AddRegisters(register.NewComputed("timestamp_delta", timestampWidth, padding))
118135

119136
var (
120137
addressWidth uint
@@ -124,89 +141,95 @@ func translateReadOnlyMemory[F field.Element[F]](ctx schema.ModuleId, fm vm.Inpu
124141
for i, l := range fm.Registers() {
125142
if uint(i) < fm.Geometry().AddressLines() {
126143
addressWidth += l.Width()
127-
} else {
144+
} else if uint(i) < fm.Geometry().AddressLines()+fm.Geometry().DataLines() {
128145
valueWidth += l.Width()
129146
}
130147
}
131148

132-
// var address = register.NewId(romModule.Width() + 0)
133-
// var value = register.NewId(romModule.Width() + 1)
134-
romModule.AddRegisters(register.NewComputed("address", addressWidth, padding))
135-
romModule.AddRegisters(register.NewComputed("value", valueWidth, padding))
149+
// var address = register.NewId(memoryModule.Width() + 0)
150+
// var valueRead = register.NewId(memoryModule.Width() + 1)
151+
memoryModule.AddRegisters(register.NewComputed("address", addressWidth, padding))
152+
memoryModule.AddRegisters(register.NewComputed("valueRead", valueWidth, padding))
136153

137154
var (
138-
executionPhase = register.NewId(romModule.Width() + 0)
139-
finalizationPhase = register.NewId(romModule.Width() + 1)
155+
execPhase = register.NewId(memoryModule.Width() + 0)
156+
finlPhase = register.NewId(memoryModule.Width() + 1)
140157
)
141158

142-
romModule.AddRegisters(register.NewComputed("exec", 1, padding))
143-
romModule.AddRegisters(register.NewComputed("finl", 1, padding))
159+
memoryModule.AddRegisters(register.NewComputed("exec", 1, padding))
160+
memoryModule.AddRegisters(register.NewComputed("finl", 1, padding))
144161

145162
var (
146163
rTime = mirc.Variable[register.Id, Expr[F]](timestampRead, timestampWidth, 0)
147164
wTime = mirc.Variable[register.Id, Expr[F]](timestampWritten, timestampWidth, 0)
148165
dTime = mirc.Variable[register.Id, Expr[F]](timestampDelta, timestampWidth, 0)
149166
// addr = mirc.Variable[register.Id, Expr[F]](address, addressWidth, 0)
150167
// val = mirc.Variable[register.Id, Expr[F]](value, valueWidth, 0)
151-
execPrev = mirc.Variable[register.Id, Expr[F]](executionPhase, 1, -1)
152-
finlPrev = mirc.Variable[register.Id, Expr[F]](finalizationPhase, 1, -1)
153-
exec = mirc.Variable[register.Id, Expr[F]](executionPhase, 1, 0)
154-
finl = mirc.Variable[register.Id, Expr[F]](finalizationPhase, 1, 0)
168+
execPrev = mirc.Variable[register.Id, Expr[F]](execPhase, 1, -1)
169+
finlPrev = mirc.Variable[register.Id, Expr[F]](finlPhase, 1, -1)
170+
exec = mirc.Variable[register.Id, Expr[F]](execPhase, 1, 0)
171+
finl = mirc.Variable[register.Id, Expr[F]](finlPhase, 1, 0)
155172
zero = mirc.Number[register.Id, Expr[F]](0)
156173
one = mirc.Number[register.Id, Expr[F]](1)
157174
)
158175

176+
// ================================================
159177
// constraints
178+
// ================================================
179+
180+
// (non padding) rows are either created during standard execution (exec ≡ true)
181+
// or during the finalization phase (finl ≡ true)
160182
flagExclusivity := mir.NewVanishingConstraint("flag_exclusivity", ctx, util.None[int](),
161183
mirc.Product([]Expr[F]{exec, finl}).Equals(zero).AsLogical())
184+
185+
// both exec and (exec + finl) should, on any trace segment, look like one of these :
186+
//
187+
// ¹ ┼ ┌───── ¹ ┼
188+
// │ │ │
189+
// ⁰ ┴ ─────┘ or ⁰ ┴ ───────────
190+
//
191+
// exec may not be nondecreasing; the (exec, finl) pair may look like so :
192+
//
193+
// ¹ ┼ ┌─────┐∙∙∙∙∙∙ ( ∙ ≡ finl)
194+
// │ │ │
195+
// ⁰ ┴ ─────┘∙∙∙∙∙└────── ( ─ ≡ exec)
162196
flagMonotony1 := mir.NewVanishingConstraint("finl_monotony", ctx, util.None[int](),
163197
mirc.If(finlPrev.NotEquals(zero), finl.Equals(one)).AsLogical())
164198
flagMonotony2 := mir.NewVanishingConstraint("exec+finl_monotony", ctx, util.None[int](),
165199
mirc.If(mirc.Sum([]Expr[F]{execPrev, finlPrev}).NotEquals(zero),
166200
mirc.Sum([]Expr[F]{exec, finl}).Equals(one)).AsLogical())
201+
167202
// we want to prove WT - RT = 1 + ΔT (which forces WT > RT given that ΔT is ≥ 0)
168203
// instead we prove WT = RT + 1 + ΔT
169204
timestampMonotony := mir.NewVanishingConstraint("timestamp_monotony", ctx, util.None[int](),
170205
mirc.If(exec.NotEquals(zero), wTime.Equals(rTime.Add(dTime, one))).AsLogical())
206+
207+
// var isImmutable bool
208+
// switch fm.(type) {
209+
// case vm.InputOutputMemory[F]: isImmutable = true
210+
// case vm.Memory[F]: isImmutable = false
211+
// default: panic("unknown memory type")
212+
// }
213+
//
214+
// var valueWritten = register.Id
215+
// if isImmutable {
216+
// valueWritten = valueRead
217+
// } else {
218+
// valueWritten = register.NewId(memoryModule.Width() + 0)
219+
// memoryModule.AddRegisters(register.NewComputed("valueWritten", valueWidth, padding))
220+
// }
221+
//
222+
// // we impose value constancy by enforcing that the received value be the same as the sent value
171223
// rcvExec := mir.NewReceiveConstraint[F]("reading_in_execution_phase",
172-
// []register.Id{address, timestampRead, value})
224+
// []register.Id{address, timestampRead, valueRead})
173225
// sndExec := mir.NewSendConstraint[F]("writing_in_execution_phase",
174-
// []register.Id{address, timestampWritten, value})
175-
// first := mir.NewVanishingConstraint("first", ctx, util.Some(0),
176-
// mirc.If(pc_i.NotEquals(zero), pc_i.Equals(one)).AsLogical())
177-
//
226+
// []register.Id{address, timestampWritten, valueWritten})
227+
178228
constraints := []mir.Constraint[F]{flagExclusivity, flagMonotony1,
179229
flagMonotony2, timestampMonotony} // , rcvExec, sndExec}
180-
romModule.AddConstraints(constraints...)
230+
memoryModule.AddConstraints(constraints...)
181231

182-
// TODO: implement ROM constraints
183-
return romModule
184-
}
185-
186-
func translateWriteOnceMemory[F field.Element[F]](_ schema.ModuleId, fm vm.InputOutputMemory[F]) mir.Module[F] {
187-
var (
188-
mod *schema.Table[F, mir.Constraint[F]]
189-
name = trace.ModuleName{Name: fm.Name(), Multiplier: 1}
190-
)
191-
// Initialise module
192-
mod = mod.Init(name, false, true, false, fm.IsNative(), false, 0)
193-
// Add all registers
194-
mod.AddRegisters(fm.Registers()...)
195-
// TODO: implement WOM constraints
196-
return mod
197-
}
198-
199-
func translateReadWriteMemory[F field.Element[F]](_ schema.ModuleId, fm vm.Memory[F]) mir.Module[F] {
200-
var (
201-
mod *schema.Table[F, mir.Constraint[F]]
202-
name = trace.ModuleName{Name: fm.Name(), Multiplier: 1}
203-
)
204-
// Initialise module
205-
mod = mod.Init(name, false, true, false, fm.IsNative(), false, 0)
206-
// Add all registers
207-
mod.AddRegisters(fm.Registers()...)
208-
// TODO: implement WOM constraints
209-
return mod
232+
return memoryModule
210233
}
211234

212235
func translateFunction[F field.Element[F]](ctx schema.ModuleId, fm vm.FieldFunction) mir.Module[F] {

0 commit comments

Comments
 (0)