Fix MIPS failing constraints #2075

querolita · 2024-04-15T13:53:55Z

When running the main.rs with the generic prover I could observe some MIPS constraints not passing. Figure out why and which and fix it.

The text was updated successfully, but these errors were encountered:

querolita · 2024-04-16T19:00:52Z

I have been trying to identify the instructions and concrete constraints that are failing (this might not be a complete list, as I believe some of the instruction variants have not occurred in my demo run):

Inside is_zero() the constraint fails

self.add_constraint(x.clone() * x_inv_or_zero.clone() + res.clone() - Self::constant(1));

RType(JumpRegister) kills the prover process
RType(JumpAndLinkRegister) kills the prover and fails in

env.write_register(&rd, instruction_pointer + Env::constant(8u32));

RType(SyscallExitGroup) kills the prover process
RType(SyscallReadOther) aborts and these constraints fail

let v0 = other_fd.clone() * Env::constant(0xFFFFFFFF);
let v1 = other_fd * Env::constant(0x9); // EBADF

env.write_register(&Env::constant(2), v0);
env.write_register(&Env::constant(7), v1);

RType(SyscallWriteOther) kills the prover and fails in

let v0 = known_fd * write_length + other_fd.clone() * Env::constant(0xFFFFFFFF);
let v1 = other_fd * Env::constant(0x9); // EBADF

env.write_register(&Env::constant(2), v0);
env.write_register(&Env::constant(7), v1);

RType(SyscallFcntl) fails in

let v0 = is_getfl.clone()
          * (is_write.clone()
             + (Env::constant(1) - is_read.clone() - is_write.clone())
             * Env::constant(0xFFFFFFFF))
           + (Env::constant(1) - is_getfl.clone()) * Env::constant(0xFFFFFFFF);
let v1 =
         is_getfl.clone() * (Env::constant(1) - is_read - is_write.clone())
         * Env::constant(0x9) /* EBADF */
         + (Env::constant(1) - is_getfl.clone()) * Env::constant(0x16) /* EINVAL */;

env.write_register(&Env::constant(2), v0);
env.write_register(&Env::constant(7), v1);

RType(Sync) kills the prover
RType(MoveToHi) kills the prover
JType(Jump) kills the prover
JType(Jump) kills the prover
JType(JumpAndLink) fails with

ConstraintNotSatisfied("Unsatisfied expression: (((0x0100000000000000000000000000000000000000000000000000000000000000 - Curr(x[14])) * (Curr(x[0]) + 0x0800000000000000000000000000000000000000000000000000000000000000)) - Curr(x[16]))")

IType(BranchLeqZero) kills the prover
IType(BranchGtZero) kills the prover
IType(BranchLtZero) kills the prover
IType(BranchGeqZero) kills the prover
IType(Store8) kills the prover
IType(Store16) kills the prover
IType(Store32) kills the prover
IType(Store32Conditional) fails with

ConstraintNotSatisfied("Unsatisfied expression: ((0x0100000000000000000000000000000000000000000000000000000000000000 - Curr(x[34])) - Curr(x[36]))")

querolita · 2024-04-22T20:36:47Z

Update:

After merging #2093, this is the status of the MIPS trace:

RType

./run-vm.sh: line 23: 36660 Killed: 9

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((Curr(x[82]) * (((Curr(x[45]) - 0x0200000000000000000000000000000000000000000000000000000000000000) * (Curr(x[45]) - 0x0300000000000000000000000000000000000000000000000000000000000000)) * (Curr(x[45]) - 0x0400000000000000000000000000000000000000000000000000000000000000))) * (Curr(x[22]) - Curr(x[85])))")',

SyscallReadOther,
SyscallWriteHint,
SyscallWritePreimage,

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((((Curr(x[16]) - Curr(x[20])) + 0x0100000000000000000000000000000000000000000000000000000000000000) - ((Curr(x[16]) + 0x0400000000000000000000000000000000000000000000000000000000000000) - Curr(x[39]))) * Curr(x[43])) + Curr(x[42])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

SyscallWriteOther,
SyscallFcntl,

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[16]) - 0x0600000000000000000000000000000000000000000000000000000000000000) * Curr(x[27])) + Curr(x[26])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")',

SyscallOther,

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[16]) - 0xcd0f000000000000000000000000000000000000000000000000000000000000) * Curr(x[19])) + Curr(x[18])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

MoveZero,
MoveNonZero,
Sync

./run-vm.sh: line 23: 44331 Killed: 9

JType

Jump

./run-vm.sh: line 23: 47025 Killed: 9

JumpAndLink,

## IType

BranchEq

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[15]) - Curr(x[17])) * Curr(x[20])) + Curr(x[19])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

BranchNeq

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[15]) - Curr(x[17])) * Curr(x[20])) + Curr(x[19])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

BranchLeqZero

./run-vm.sh: line 23: 48647 Killed: 9

BranchGtZero

./run-vm.sh: line 23: 49163 Killed: 9

BranchLtZero

./run-vm.sh: line 23: 49756 Killed: 9

BranchGeqZero

./run-vm.sh: line 23: 50189 Killed: 9

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0100000000000000000000000000000000000000000000000000000000000000) * Curr(x[23])) + Curr(x[22])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

LoadWordRight

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0300000000000000000000000000000000000000000000000000000000000000) * Curr(x[21])) + Curr(x[20])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

Store8

./run-vm.sh: line 23: 51691 Killed: 9

Store16

./run-vm.sh: line 23: 52127 Killed: 9

Store32

./run-vm.sh: line 23: 52813 Killed: 9

Store32Conditional,
StoreWordLeft

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0200000000000000000000000000000000000000000000000000000000000000) * Curr(x[25])) + Curr(x[24])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

StoreWordRight

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0300000000000000000000000000000000000000000000000000000000000000) * Curr(x[21])) + Curr(x[20])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

querolita · 2024-04-23T11:33:26Z

Update:

After
#2100
#2101
#2102
#2103
#2104
#2105
#2106
#2107

RType

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((Curr(x[82]) * (((Curr(x[45]) - 0x0200000000000000000000000000000000000000000000000000000000000000) * (Curr(x[45]) - 0x0300000000000000000000000000000000000000000000000000000000000000)) * (Curr(x[45]) - 0x0400000000000000000000000000000000000000000000000000000000000000))) * (Curr(x[22]) - Curr(x[85])))")',
thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[82]) * (Curr(x[45]) - 0x0100000000000000000000000000000000000000000000000000000000000000)) * (Curr(x[45]) - 0x0200000000000000000000000000000000000000000000000000000000000000)) * (Curr(x[45]) - 0x0300000000000000000000000000000000000000000000000000000000000000)) * (Curr(x[45]) - 0x0400000000000000000000000000000000000000000000000000000000000000))")'

SyscallReadOther,
SyscallWriteHint,
SyscallWritePreimage,

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((((Curr(x[16]) - Curr(x[20])) + 0x0100000000000000000000000000000000000000000000000000000000000000) - ((Curr(x[16]) + 0x0400000000000000000000000000000000000000000000000000000000000000) - Curr(x[39]))) * Curr(x[43])) + Curr(x[42])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

SyscallWriteOther,
SyscallFcntl,

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[16]) - 0x0600000000000000000000000000000000000000000000000000000000000000) * Curr(x[27])) + Curr(x[26])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")',

JType

Jump -> 0 CONSTRAINTS
JumpAndLink,

## IType

BranchEq

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[15]) - Curr(x[17])) * Curr(x[20])) + Curr(x[19])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

BranchNeq

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[15]) - Curr(x[17])) * Curr(x[20])) + Curr(x[19])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0100000000000000000000000000000000000000000000000000000000000000) * Curr(x[23])) + Curr(x[22])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

LoadWordRight

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0300000000000000000000000000000000000000000000000000000000000000) * Curr(x[21])) + Curr(x[20])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0200000000000000000000000000000000000000000000000000000000000000) * Curr(x[25])) + Curr(x[24])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

StoreWordRight

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0300000000000000000000000000000000000000000000000000000000000000) * Curr(x[21])) + Curr(x[20])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

querolita · 2024-05-31T11:35:11Z

Update:

After
#2274
#2280
#2228

RType

overwrite_0.clone() - env.equal(&(read_address.clone() + Env::constant(1)), &next_word_addr) + env.equal(&bytes_to_preserve_in_register, &Env::constant(1));
thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((((Curr(x[16]) - Curr(x[20])) + 0x0100000000000000000000000000000000000000000000000000000000000000) - ((Curr(x[16]) + 0x0400000000000000000000000000000000000000000000000000000000000000) - Curr(x[39]))) * Curr(x[43])) + Curr(x[42])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

SyscallWriteOther,
SyscallFcntl,

env.equal(&fd_id, &Env::constant(FD_HINT_WRITE));
thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[16]) - 0x0400000000000000000000000000000000000000000000000000000000000000) * Curr(x[27])) + Curr(x[26])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")',
env.equal(&fd_id, &Env::constant(FD_PREIMAGE_READ));
thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[16]) - 0x0500000000000000000000000000000000000000000000000000000000000000) * Curr(x[27])) + Curr(x[26])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")',
env.equal(&fd_id, &Env::constant(FD_PREIMAGE_WRITE));
thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[16]) - 0x0600000000000000000000000000000000000000000000000000000000000000) * Curr(x[27])) + Curr(x[26])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")',

JType

Jump -> 0 CONSTRAINTS
JumpAndLink,

IType

BranchEq

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[15]) - Curr(x[17])) * Curr(x[20])) + Curr(x[19])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

BranchNeq

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[15]) - Curr(x[17])) * Curr(x[20])) + Curr(x[19])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0100000000000000000000000000000000000000000000000000000000000000) * Curr(x[23])) + Curr(x[22])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

LoadWordRight

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0300000000000000000000000000000000000000000000000000000000000000) * Curr(x[21])) + Curr(x[20])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0200000000000000000000000000000000000000000000000000000000000000) * Curr(x[25])) + Curr(x[24])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

StoreWordRight

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0300000000000000000000000000000000000000000000000000000000000000) * Curr(x[21])) + Curr(x[20])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

querolita · 2024-06-13T15:54:17Z

After:
#2310
#2311
#2305

Subset of the failing constraints:

SyscallReadPreimage

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((Curr(x[82]) * (((Curr(x[45]) - 0x0200000000000000000000000000000000000000000000000000000000000000) * (Curr(x[45]) - 0x0300000000000000000000000000000000000000000000000000000000000000)) * (Curr(x[45]) - 0x0400000000000000000000000000000000000000000000000000000000000000))) * (Curr(x[22]) - Curr(x[85])))")',
thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[82]) * (Curr(x[45]) - 0x0100000000000000000000000000000000000000000000000000000000000000)) * (Curr(x[45]) - 0x0200000000000000000000000000000000000000000000000000000000000000)) * (Curr(x[45]) - 0x0300000000000000000000000000000000000000000000000000000000000000)) * (Curr(x[45]) - 0x0400000000000000000000000000000000000000000000000000000000000000))")'

LoadWordLeft

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0100000000000000000000000000000000000000000000000000000000000000) * Curr(x[23])) + Curr(x[22])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

LoadWordRight

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0300000000000000000000000000000000000000000000000000000000000000) * Curr(x[21])) + Curr(x[20])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

StoreWordLeft

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0200000000000000000000000000000000000000000000000000000000000000) * Curr(x[25])) + Curr(x[24])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

StoreWordRight

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0300000000000000000000000000000000000000000000000000000000000000) * Curr(x[21])) + Curr(x[20])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

After FIXME
#2310
#2311

Unchanged

LoadWordLeft

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0100000000000000000000000000000000000000000000000000000000000000) * Curr(x[23])) + Curr(x[22])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

LoadWordRight

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0300000000000000000000000000000000000000000000000000000000000000) * Curr(x[21])) + Curr(x[20])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

StoreWordLeft

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0200000000000000000000000000000000000000000000000000000000000000) * Curr(x[25])) + Curr(x[24])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

StoreWordRight

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0300000000000000000000000000000000000000000000000000000000000000) * Curr(x[21])) + Curr(x[20])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

After
#2299

LoadWordLeft : halts and fails (a different) constraint

Exited with code 2 at step 4863183
Halted at step=4863184 instruction=RType(SyscallExitGroup)
Checking MIPS circuit IType(LoadWordLeft)
thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0100000000000000000000000000000000000000000000000000000000000000) * Curr(x[36])) + Curr(x[35])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

After
#2293

LoadWordRight : halts and fails the same constraint

Exited with code 2 at step 4865370
Halted at step=4865371 instruction=RType(SyscallExitGroup)
Checking MIPS circuit IType(LoadWordRight)
thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0100000000000000000000000000000000000000000000000000000000000000) * Curr(x[23])) + Curr(x[22])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

After
#2318

StoreWordLeft : halts and fails the same constraint

Exited with code 2 at step 15726562
Halted at step=15726563 instruction=RType(SyscallExitGroup)
Checking MIPS circuit IType(StoreWordLeft)
thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0200000000000000000000000000000000000000000000000000000000000000) * Curr(x[25])) + Curr(x[24])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

After
#2319

StoreWordRight : halts and fails the same constraint

Exited with code 2 at step 4858355
Halted at step=4858356 instruction=RType(SyscallExitGroup)
Checking MIPS circuit IType(StoreWordRight)
thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0100000000000000000000000000000000000000000000000000000000000000) * Curr(x[23])) + Curr(x[22])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

After
#2274

SyscallReadPreimage : constraints are satisfied and does not halt. Same instructions are executed in the same order as master.

#2305 b3e2995

SyscallReadPreimage : halts but all constraints are satisfied. In master it should run a Or followed by a Store32 but instead it executes a different set of instructions:

Instruction 61394907 -> IType(AddImmediateUnsigned)
Instruction 61394908
Executing instruction RType(SyscallExitGroup)
Exited with code 2 at step 61394907
Halted at step=61394908 instruction=RType(SyscallExitGroup)
Checking MIPS circuit RType(SyscallReadPreimage)
Generated a MIPS RType(SyscallReadPreimage) proof:
The MIPS RType(SyscallReadPreimage) proof verifies

#2305 6e0eede

SyscallReadPreimage : constraints are satisfied and does not halt. Same instructions are executed in the same order as master. The unit test faithfully represents the interpreter now.

querolita · 2024-06-18T15:23:36Z

Update:

After
#2355
#2351
#2357

RType

overwrite_0.clone() - env.equal(&(read_address.clone() + Env::constant(1)), &next_word_addr) + env.equal(&bytes_to_preserve_in_register, &Env::constant(1));
thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((((Curr(x[16]) - Curr(x[20])) + 0x0100000000000000000000000000000000000000000000000000000000000000) - ((Curr(x[16]) + 0x0400000000000000000000000000000000000000000000000000000000000000) - Curr(x[39]))) * Curr(x[43])) + Curr(x[42])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

SyscallWriteOther,
SyscallFcntl,

env.equal(&fd_id, &Env::constant(FD_HINT_WRITE));
thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[16]) - 0x0400000000000000000000000000000000000000000000000000000000000000) * Curr(x[27])) + Curr(x[26])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")',
env.equal(&fd_id, &Env::constant(FD_PREIMAGE_READ));
thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[16]) - 0x0500000000000000000000000000000000000000000000000000000000000000) * Curr(x[27])) + Curr(x[26])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")',
env.equal(&fd_id, &Env::constant(FD_PREIMAGE_WRITE));
thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[16]) - 0x0600000000000000000000000000000000000000000000000000000000000000) * Curr(x[27])) + Curr(x[26])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")',

JType

Jump
JumpAndLink,

IType

BranchEq

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[15]) - Curr(x[17])) * Curr(x[20])) + Curr(x[19])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

BranchNeq

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[15]) - Curr(x[17])) * Curr(x[20])) + Curr(x[19])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0100000000000000000000000000000000000000000000000000000000000000) * Curr(x[23])) + Curr(x[22])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

LoadWordRight

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0300000000000000000000000000000000000000000000000000000000000000) * Curr(x[21])) + Curr(x[20])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0200000000000000000000000000000000000000000000000000000000000000) * Curr(x[25])) + Curr(x[24])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

StoreWordRight

thread 'main' panicked at 'called Result::unwrap() on an Err value: ConstraintNotSatisfied("Unsatisfied expression: ((((Curr(x[19]) - 0x0300000000000000000000000000000000000000000000000000000000000000) * Curr(x[21])) + Curr(x[20])) - 0x0100000000000000000000000000000000000000000000000000000000000000)")'

marcbeunardeau88 · 2024-10-22T15:07:17Z

Here is a branch which fixes the remaining instructions
https://github.com/o1-labs/proof-systems/tree/marc/working-vm-with-field-elt
It does two things :

the equality eq(x,y) was calling is_zero(x-y), while sometime permuting the argument on the witness side.
this causes a value to be its negation
It was doing that to avoid underflowing the substraction of y>x. To avoid that the second fix is to change the witness interpreter variable type from u64 to Fp.

However this is not satysfying, since the resulting witness interpreter is slower.
Hopefully the equality underflow was the only one and we can use field values only there.

querolita self-assigned this Apr 15, 2024

querolita mentioned this issue Apr 15, 2024

Fix indexing in MIPS constraints environment #2076

Merged

querolita mentioned this issue Apr 19, 2024

Use non-zero dummy rows to pad witnesses for testing #2093

Merged

querolita mentioned this issue Apr 23, 2024

[easy] Ignore instructions with no constraints in main #2107

Merged

joseandro mentioned this issue May 31, 2024

Testing all the instructions for the whole zkVM. MinaProtocol/mina#15689

Open

12 tasks

querolita mentioned this issue Jun 3, 2024

Unit test for Load16 #2280

Merged

querolita mentioned this issue Jun 13, 2024

Unit test for StoreWordLeft #2318

Closed

This was referenced Oct 24, 2024

o1vm/mips: fix failing constraints #2729

Merged

Fix the equality function in the o1vm interpreter #2736

Merged

dannywillems closed this as completed in #2736 Oct 30, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Fix MIPS failing constraints #2075

Fix MIPS failing constraints #2075

querolita commented Apr 15, 2024

querolita commented Apr 16, 2024 •

edited

Loading

Uh oh!

querolita commented Apr 22, 2024 •

edited

Loading

RType

JType

Uh oh!

querolita commented Apr 23, 2024 •

edited

Loading

RType

JType

Uh oh!

querolita commented May 31, 2024 •

edited

Loading

RType

JType

IType

Uh oh!

querolita commented Jun 13, 2024 •

edited

Loading

Uh oh!

querolita commented Jun 18, 2024

RType

JType

IType

Uh oh!

marcbeunardeau88 commented Oct 22, 2024

Uh oh!

Fix MIPS failing constraints #2075

Fix MIPS failing constraints #2075

Comments

querolita commented Apr 15, 2024

querolita commented Apr 16, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

querolita commented Apr 22, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

RType

JType

Uh oh!

querolita commented Apr 23, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

RType

JType

Uh oh!

querolita commented May 31, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

RType

JType

IType

Uh oh!

querolita commented Jun 13, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

querolita commented Jun 18, 2024

RType

JType

IType

Uh oh!

marcbeunardeau88 commented Oct 22, 2024

Uh oh!

querolita commented Apr 16, 2024 •

edited

Loading

querolita commented Apr 22, 2024 •

edited

Loading

querolita commented Apr 23, 2024 •

edited

Loading

querolita commented May 31, 2024 •

edited

Loading

querolita commented Jun 13, 2024 •

edited

Loading