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.

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

Make partial functions total #78

Open
morganthomas opened this issue Oct 30, 2023 · 0 comments
Open

Make partial functions total #78

morganthomas opened this issue Oct 30, 2023 · 0 comments

Comments

@morganthomas
Copy link
Collaborator

Various Valida functions might exhibit partiality; on some inputs, they might fail to terminate with a result of the output type. Instead of panicking or non-terminating, functions should return a result indicating an error. The public functions which are currently partial should be modified to return a Result type.

It is okay to use functions which may panic in unreachable code sections and in cases where it is impossible for the functions to get inputs which result in a panic. However, attainable conditions should never result in a panic.

The reason for this issue is that Valida is going to be used in services, and those services can't panic. They have to stay running even when errors occur.

The following code sections (as far as I know) may potentially result in partiality. Line numbers are relative to commit eddd2b031a13278bc4855dea802fbc045f1378d8.

There are three instances of panic!() , excluding macro code which is only executed at compile-time, and code which is only used for debugging:

  1. In the quoted code for run in the implementation of the run_method macro in derive/src/lib.rs.
  2. In the implementation of AirBuilder::is_transition_window for ConstraintFolder<’a, F, EF, M> in machine/src/__internal/folding_builder.rs.
  3. In the implementation of MemoryChip::read, in memory/src/lib.rs.

There are no instances of .expect() in non-test code, except for some instances in macro code which runs exclusively at compile time. It is okay for code which runs exclusively at compile time to be partial, as long as it terminates.

There are 16 instances of .unwrap() in non-test-code, excluding macro code which runs exclusively at compile time:

  1. In the implementation of main in basic/src/bin/valida.rs, on the call to load_program_rom.
  2. In the implementation of main in basic/src/bin/valida.rs, on the call to std::io::stdin().read_to_end.
  3. In the implementation of main in basic/src/bin/valida.rs, on the call to std::io::stdout().write_all.
  4. In the implementation of check_constraints in machine/src/__internal/check_constraints.rs, on line 30.
  5. In the implementation of check_constraints in machine/src/__internal/check_constraints.rs, on line 39.
  6. In the implementation of check_constraints in machine/src/__internal/check_constraints.rs, on line 44.
  7. In the implementation of check_cumulative_sums in machine/src/__internal/check_constraints.rs, on line 90.
  8. In the implementation of generate_permutation_trace in machine/src/chip.rs, on line 40.
  9. In the implementation of generate_permutation_trace in machine/src/chip.rs, on line 169.
  10. In the implementation of generate_permutation_trace in machine/src/chip.rs, on line 189.
  11. In the implementation of eval_permutation_constraints in machine/src/chip.rs, on line 268.
  12. In the implementation of eval_permutation_constraints in machine/src/chip.rs, on line 270.
  13. In the implementation of MemoryChip::insert_dummy_reads in memory/src/lib.rs, on line 257.
  14. In the implementation of MemoryChip::insert_dummy_reads in memory/src/lib.rs, on line 258.
  15. In the implementation of MemoryChip::insert_dummy_reads in memory/src/lib.rs, on line 259.
  16. In the implementation of Instruction<M>::execute for WriteInstruction in output/src/lib.rs, on line 154.

There are 4 instances of assert_eq!() in non-test code which is run after compile time:

  1. In the implementation of check_constraints in machine/src/__internal/check_constraints.rs.
  2. In the implementation of check_cumulative_sums in machine/src/__internal/check_constraints.rs.
  3. In the implementation of Instruction<M>::execute for WriteInstruction in output/src/lib.rs, on lines 162 and 163.

There is one instance of assert!() in non-test code which runs after compile time:

  1. In the default implementation of read_word in the MachineWithProgramChip trait definition, in program/src/lib.rs.

The following files contain unsafe blocks, which should be assumed pending further review to potentially result in partiality:

  1. alu_u32/src/add/columns.rs
  2. alu_u32/src/add/mod.rs
  3. alu_u32/src/bitwise/columns.rs
  4. alu_u32/src/bitwise/mod.rs
  5. alu_u32/src/div/columns.rs
  6. alu_u32/src/lt/columns.rs
  7. alu_u32/src/lt/mod.rs
  8. alu_u32/src/mul/columns.rs
  9. alu_u32/src/shift/columns.rs
  10. alu_u32/src/shift/mod.rs
  11. alu_u32/src/sub/columns.rs
  12. alu_u32/src/sub/mod.rs
  13. cpu/src/columns.rs
  14. cpu/src/lib.rs
  15. derive/src/lib.rs
  16. memory/src/columns.rs
  17. memory/src/lib.rs
  18. native_field/src/columns.rs
  19. native_field/src/lib.rs
  20. output/src/columns.rs
  21. output/src/lib.rs
  22. program/src/columns.rs
  23. range/src/columns.rs
  24. range/src/lib.rs

The following arithmetic operations may result in division by zero and a panic:

  1. In the implementation of Div::div for Word<u8>, in machine/src/core.rs, line 87.
  2. In the implementation of MemoryChip::insert_dummy_reads in memory/src/lib.rs, line 222.
  3. In the implementation of Instruction<M>::execute for Div32Instruction, in alu_u32/src/div/mod.rs, line 89.

The following unchecked array indexes may result in an out of bounds error and a panic:

  1. In the implementation of generate_permutation_trace in machine/src/chip.rs, lines 120, 166, 179, 182, and 189.
  2. In the implementation of generate_rlc_elements in machine/src/chip.rs, lines 285 and 300.
  3. In the implementation of CpuChip::set_instruction_values in cpu/src/lib.rs, line 248.
  4. In the implementation of CpuChip::pad_to_power_of_two in cpu/src/lib.rs, lines 328, 329, 330, 346, 347, 348, 351, 352, 355, 356, and 357.

The zk-VM run method is capable of non-terminating; see derive/src/lib.rs, lines 158-176. This is to be expected, because Valida is Turing complete. Perhaps, however, we should code in a maximum number of steps, in order to avoid partiality. We can even pass in the maximum number of steps as an input to the method.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant