proof-systems icon indicating copy to clipboard operation
proof-systems copied to clipboard

Published 20 hours ago • verified publisher icon o1-labs

Fix MIPS failing constraints

Open querolita opened this issue 10 months ago • 7 comments

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.

querolita avatar Apr 15 '24 13:04 querolita

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 avatar Apr 16 '24 19:04 querolita

Update:

After merging https://github.com/o1-labs/proof-systems/pull/2093, this is the status of the MIPS trace:

RType

  • [x] ShiftLeftLogical
  • [x] ShiftRightLogical
  • [x] ShiftRightArithmetic,
  • [x] ShiftLeftLogicalVariable,
  • [x] ShiftRightLogicalVariable,
  • [x] ShiftRightArithmeticVariable,
  • [ ] JumpRegister

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

  • [x] JumpAndLinkRegister,
  • [ ] SyscallMmap,
  • [ ] SyscallExitGroup,
  • [x] SyscallReadHint,
  • [ ] 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])))")',

  • [x] SyscallReadOther,
  • [x] 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)")'

  • [x] 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)")'

  • [x] MoveZero,
  • [x] MoveNonZero,
  • [ ] Sync

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

  • [x] MoveFromHi,
  • [ ] ~MoveToHi~ NOT IMPLEMENTED
  • [x] MoveFromLo,
  • [x] MoveToLo,
  • [x] Multiply,
  • [x] MultiplyUnsigned,
  • [x] Div,
  • [x] DivUnsigned,
  • [ ] Add,
  • [x] AddUnsigned,
  • [ ] Sub,
  • [x] SubUnsigned,
  • [x] And,
  • [x] Or,
  • [x] Xor,
  • [x] Nor,
  • [x] SetLessThan,
  • [x] SetLessThanUnsigned,
  • [x] MultiplyToRegister,
  • [ ] ~CountLeadingOnes~ NOT IMPLEMENTED
  • [x] CountLeadingZeros,

JType

  • [ ] Jump

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

  • [x] 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

  • [x] AddImmediate,
  • [x] AddImmediateUnsigned,
  • [x] SetLessThanImmediate,
  • [x] SetLessThanImmediateUnsigned,
  • [x] AndImmediate,
  • [x] OrImmediate,
  • [x] XorImmediate,
  • [x] LoadUpperImmediate,
  • [x] Load8,
  • [ ] Load16,
  • [x] Load32,
  • [x] Load8Unsigned,
  • [x] Load16Unsigned,
  • [ ] 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)")'

  • [ ] 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

  • [x] 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 avatar Apr 22 '24 20:04 querolita

Update:

After https://github.com/o1-labs/proof-systems/pull/2100 https://github.com/o1-labs/proof-systems/pull/2101 https://github.com/o1-labs/proof-systems/pull/2102 https://github.com/o1-labs/proof-systems/pull/2103 https://github.com/o1-labs/proof-systems/pull/2104 https://github.com/o1-labs/proof-systems/pull/2105 https://github.com/o1-labs/proof-systems/pull/2106 https://github.com/o1-labs/proof-systems/pull/2107

RType

  • [x] ShiftLeftLogical
  • [x] ShiftRightLogical
  • [x] ShiftRightArithmetic,
  • [x] ShiftLeftLogicalVariable,
  • [x] ShiftRightLogicalVariable,
  • [x] ShiftRightArithmeticVariable,
  • [ ] JumpRegister -> 0 CONSTRAINTS
  • [x] JumpAndLinkRegister,
  • [x] SyscallMmap,
  • [ ] SyscallExitGroup,
  • [x] SyscallReadHint,
  • [ ] 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))")'

  • [x] SyscallReadOther,
  • [x] 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)")'

  • [x] 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)")',

  • [x] SyscallOther,
  • [x] MoveZero,
  • [x] MoveNonZero,
  • [ ] Sync -> 0 CONSTRAINTS
  • [x] MoveFromHi,
  • [ ] MoveToHi -> 0 CONSTRAINTS
  • [x] MoveFromLo,
  • [x] MoveToLo,
  • [x] Multiply,
  • [x] MultiplyUnsigned,
  • [x] Div,
  • [x] DivUnsigned,
  • [x] Add,
  • [x] AddUnsigned,
  • [ ] Sub,
  • [x] SubUnsigned,
  • [x] And,
  • [x] Or,
  • [x] Xor,
  • [x] Nor,
  • [x] SetLessThan,
  • [x] SetLessThanUnsigned,
  • [x] MultiplyToRegister,
  • [ ] CountLeadingOnes -> 0 CONSTRAINTS
  • [x] CountLeadingZeros,

JType

  • [ ] Jump -> 0 CONSTRAINTS
  • [x] 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 -> 0 CONSTRAINTS
  • [ ] BranchGtZero -> 0 CONSTRAINTS
  • [ ] BranchLtZero -> 0 CONSTRAINTS
  • [ ] BranchGeqZero -> 0 CONSTRAINTS
  • [x] AddImmediate,
  • [x] AddImmediateUnsigned,
  • [x] SetLessThanImmediate,
  • [x] SetLessThanImmediateUnsigned,
  • [x] AndImmediate,
  • [x] OrImmediate,
  • [x] XorImmediate,
  • [x] LoadUpperImmediate,
  • [x] Load8,
  • [ ] Load16,
  • [x] Load32,
  • [x] Load8Unsigned,
  • [x] Load16Unsigned,
  • [ ] 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)")'

  • [ ] Store8 -> 0 CONSTRAINTS
  • [ ] Store16 -> 0 CONSTRAINTS
  • [x] Store32
  • [x] 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 avatar Apr 23 '24 11:04 querolita

Update:

After https://github.com/o1-labs/proof-systems/pull/2274 https://github.com/o1-labs/proof-systems/pull/2280 https://github.com/o1-labs/proof-systems/pull/2228

RType

  • [x] ShiftLeftLogical
  • [x] ShiftRightLogical
  • [x] ShiftRightArithmetic,
  • [x] ShiftLeftLogicalVariable,
  • [x] ShiftRightLogicalVariable,
  • [x] ShiftRightArithmeticVariable,
  • [ ] JumpRegister -> 0 CONSTRAINTS
  • [x] JumpAndLinkRegister,
  • [x] SyscallMmap,
  • [ ] SyscallExitGroup,
  • [x] SyscallReadHint,
  • [x] SyscallReadPreimage,
  • [x] SyscallReadOther,
  • [x] SyscallWriteHint,
  • [ ] SyscallWritePreimage,

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)")'

  • [x] 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)")',

  • [x] SyscallOther,
  • [x] MoveZero,
  • [x] MoveNonZero,
  • [ ] Sync -> 0 CONSTRAINTS
  • [x] MoveFromHi,
  • [ ] MoveToHi -> 0 CONSTRAINTS
  • [x] MoveFromLo,
  • [x] MoveToLo,
  • [x] Multiply,
  • [x] MultiplyUnsigned,
  • [x] Div,
  • [x] DivUnsigned,
  • [x] Add,
  • [x] AddUnsigned,
  • [x] Sub: test_unit_sub_instruction passes
  • [x] SubUnsigned,
  • [x] And,
  • [x] Or,
  • [x] Xor,
  • [x] Nor,
  • [x] SetLessThan,
  • [x] SetLessThanUnsigned,
  • [x] MultiplyToRegister,
  • [ ] CountLeadingOnes -> 0 CONSTRAINTS
  • [x] CountLeadingZeros,

JType

  • [ ] Jump -> 0 CONSTRAINTS
  • [x] 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 -> 0 CONSTRAINTS
  • [ ] BranchGtZero -> 0 CONSTRAINTS
  • [ ] BranchLtZero -> 0 CONSTRAINTS
  • [ ] BranchGeqZero -> 0 CONSTRAINTS
  • [x] AddImmediate,
  • [x] AddImmediateUnsigned,
  • [x] SetLessThanImmediate,
  • [x] SetLessThanImmediateUnsigned,
  • [x] AndImmediate,
  • [x] OrImmediate,
  • [x] XorImmediate,
  • [x] LoadUpperImmediate,
  • [x] Load8,
  • [x] Load16: test_unit_load16_instruction passes
  • [x] Load32,
  • [x] Load8Unsigned,
  • [x] Load16Unsigned,
  • [ ] 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)")'

  • [ ] Store8 -> 0 CONSTRAINTS
  • [ ] Store16 -> 0 CONSTRAINTS
  • [x] Store32
  • [x] 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 avatar May 31 '24 11:05 querolita

After: https://github.com/o1-labs/proof-systems/pull/2310 https://github.com/o1-labs/proof-systems/pull/2311 https://github.com/o1-labs/proof-systems/pull/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 https://github.com/o1-labs/proof-systems/pull/2310 https://github.com/o1-labs/proof-systems/pull/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 https://github.com/o1-labs/proof-systems/pull/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 https://github.com/o1-labs/proof-systems/pull/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 https://github.com/o1-labs/proof-systems/pull/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 https://github.com/o1-labs/proof-systems/pull/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 https://github.com/o1-labs/proof-systems/pull/2274

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

https://github.com/o1-labs/proof-systems/pull/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

https://github.com/o1-labs/proof-systems/pull/2305 6e0eede

  • [x] 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 avatar Jun 13 '24 15:06 querolita

Update:

After https://github.com/o1-labs/proof-systems/pull/2355 https://github.com/o1-labs/proof-systems/pull/2351 https://github.com/o1-labs/proof-systems/pull/2357

RType

  • [x] ShiftLeftLogical
  • [x] ShiftRightLogical
  • [x] ShiftRightArithmetic,
  • [x] ShiftLeftLogicalVariable,
  • [x] ShiftRightLogicalVariable,
  • [x] ShiftRightArithmeticVariable,
  • [x] JumpRegister,
  • [x] JumpAndLinkRegister,
  • [x] SyscallMmap,
  • [ ] SyscallExitGroup,
  • [x] SyscallReadHint,
  • [x] SyscallReadPreimage,
  • [x] SyscallReadOther,
  • [x] SyscallWriteHint,
  • [ ] SyscallWritePreimage,

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)")'

  • [x] 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)")',

  • [x] SyscallOther,
  • [x] MoveZero,
  • [x] MoveNonZero,
  • [x] Sync,
  • [x] MoveFromHi,
  • [ ] MoveToHi
  • [x] MoveFromLo,
  • [x] MoveToLo,
  • [x] Multiply,
  • [x] MultiplyUnsigned,
  • [x] Div,
  • [x] DivUnsigned,
  • [x] Add,
  • [x] AddUnsigned,
  • [x] Sub: test_unit_sub_instruction passes
  • [x] SubUnsigned,
  • [x] And,
  • [x] Or,
  • [x] Xor,
  • [x] Nor,
  • [x] SetLessThan,
  • [x] SetLessThanUnsigned,
  • [x] MultiplyToRegister,
  • [ ] CountLeadingOnes -> 0 CONSTRAINTS
  • [x] CountLeadingZeros,

JType

  • [x] Jump
  • [x] 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)")'

  • [x] BranchLeqZero
  • [x] BranchGtZero
  • [x] BranchLtZero
  • [x] BranchGeqZero
  • [x] AddImmediate,
  • [x] AddImmediateUnsigned,
  • [x] SetLessThanImmediate,
  • [x] SetLessThanImmediateUnsigned,
  • [x] AndImmediate,
  • [x] OrImmediate,
  • [x] XorImmediate,
  • [x] LoadUpperImmediate,
  • [x] Load8,
  • [x] Load16: test_unit_load16_instruction passes
  • [x] Load32,
  • [x] Load8Unsigned,
  • [x] Load16Unsigned,
  • [ ] 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)")'

  • [x] Store8
  • [x] Store16
  • [x] Store32
  • [x] 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 avatar Jun 18 '24 15:06 querolita