search

o1-labs / proof-systems

The proof systems used by Mina
https://o1-labs.github.io/proof-systems/
Apache License 2.0
387 stars 89 forks source link

Fix MIPS failing constraints #2075

Open querolita opened 2 months ago

querolita commented 2 months ago

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 commented 2 months ago
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 commented 2 months ago
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 commented 2 months ago
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 commented 1 month ago
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 commented 3 weeks ago
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](https://github.com/o1-labs/proof-systems/pull/2305/commits/b3e29959086a71b211300fee30d84accb024bebc) - [ ] `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](https://github.com/o1-labs/proof-systems/pull/2305/commits/6e0eedec5b02219455fab15a02de59150f9024fd) - [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 commented 2 weeks ago
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)")'