[go: nahoru, domu]
Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix MIPS failing constraints #2075

Open
querolita opened this issue Apr 15, 2024 · 6 comments
Open

Fix MIPS failing constraints #2075

querolita opened this issue Apr 15, 2024 · 6 comments
Assignees
@querolita

Comments

@querolita
Copy link
Member

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 querolita self-assigned this Apr 15, 2024
@querolita querolita mentioned this issue Apr 15, 2024
Merged
@querolita
Copy link
Member Author
querolita commented Apr 16, 2024 •
edited
Loading
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 querolita mentioned this issue Apr 19, 2024
Merged
@querolita
Copy link
Member Author
querolita commented Apr 22, 2024 •
edited
Loading
Update:

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

RType

  • ShiftLeftLogical
  • ShiftRightLogical
  • ShiftRightArithmetic,
  • ShiftLeftLogicalVariable,
  • ShiftRightLogicalVariable,
  • ShiftRightArithmeticVariable,
  • JumpRegister

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

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

  • 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

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

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

  • AddImmediate,
  • AddImmediateUnsigned,
  • SetLessThanImmediate,
  • SetLessThanImmediateUnsigned,
  • AndImmediate,
  • OrImmediate,
  • XorImmediate,
  • LoadUpperImmediate,
  • Load8,
  • Load16,
  • Load32,
  • Load8Unsigned,
  • 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

  • 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
Copy link
Member Author
querolita commented Apr 23, 2024 •
edited
Loading
Update:

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

RType

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

  • 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,
  • MoveZero,
  • MoveNonZero,
  • Sync -> 0 CONSTRAINTS
  • MoveFromHi,
  • MoveToHi -> 0 CONSTRAINTS
  • MoveFromLo,
  • MoveToLo,
  • Multiply,
  • MultiplyUnsigned,
  • Div,
  • DivUnsigned,
  • Add,
  • AddUnsigned,
  • Sub,
  • SubUnsigned,
  • And,
  • Or,
  • Xor,
  • Nor,
  • SetLessThan,
  • SetLessThanUnsigned,
  • MultiplyToRegister,
  • CountLeadingOnes -> 0 CONSTRAINTS
  • CountLeadingZeros,

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

  • BranchLeqZero -> 0 CONSTRAINTS
  • BranchGtZero -> 0 CONSTRAINTS
  • BranchLtZero -> 0 CONSTRAINTS
  • BranchGeqZero -> 0 CONSTRAINTS
  • AddImmediate,
  • AddImmediateUnsigned,
  • SetLessThanImmediate,
  • SetLessThanImmediateUnsigned,
  • AndImmediate,
  • OrImmediate,
  • XorImmediate,
  • LoadUpperImmediate,
  • Load8,
  • Load16,
  • Load32,
  • Load8Unsigned,
  • 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
  • Store32
  • 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 querolita mentioned this issue Apr 23, 2024
Merged
@querolita
Copy link
Member Author
querolita commented May 31, 2024 •
edited
Loading
Update:

After
#2274
#2280
#2228

RType

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

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

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

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

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

@joseandro joseandro mentioned this issue May 31, 2024
Open
12 tasks
@querolita querolita mentioned this issue Jun 3, 2024
Merged
@querolita querolita mentioned this issue Jun 13, 2024
Draft
@querolita
Copy link
Member Author
querolita commented Jun 13, 2024 •
edited
Loading

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
Copy link
Member Author
Update:

After
#2355
#2351
#2357

RType

  • ShiftLeftLogical
  • ShiftRightLogical
  • ShiftRightArithmetic,
  • ShiftLeftLogicalVariable,
  • ShiftRightLogicalVariable,
  • ShiftRightArithmeticVariable,
  • JumpRegister,
  • JumpAndLinkRegister,
  • SyscallMmap,
  • SyscallExitGroup,
  • SyscallReadHint,
  • SyscallReadPreimage,
  • SyscallReadOther,
  • 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)")'

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

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

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

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@querolita querolita

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@querolita