initialize RAM non-deterministically

Also rework interface for all non-determinism:
 - what used to be `secret_input` is now `individual_tokens`
 - digests are listed explicitly, and are of type `Digest`
 - initial RAM can be specified

specification/src/data-structures.md

@@ -10,6 +10,7 @@ There are four separate notions of memory:
 4. *Jump Stack Memory*, which stores the entire jump stack.
 
 ## Operational Stack
+
 The stack is a last-in;first-out data structure that allows the program to store intermediate variables, pass arguments, and keep pointers to objects held in RAM.
 In this document, the operational stack is either referred to as just “stack” or, if more clarity is desired, “OpStack.”
 
@@ -23,6 +24,23 @@ For reasons of arithmetization, the stack is actually split into two distinct pa
 
 The motivation and the interplay between the two parts is described and exemplified in [arithmetization of the OpStack table](operational-stack-table.md).
 
+## Random Access Memory
+
+Triton VM has dedicated Random Access Memory.
+It can hold up to $p$ many base field elements, where $p$ is the Oxfoi prime[^1].
+Programs can read from and write to RAM using [instructions](instructions.md#memory-access) `read_mem` and `write_mem`.
+
+The initial RAM is determined by the entity running Triton VM.
+Populating RAM this way can be beneficial for a program's execution and proving time, especially if substantial amounts of data from the input streams needs to be persisted in RAM.
+This initialization is one form of secret input, and one of two mechanisms that make Triton VM a non-deterministic virtual machine.
+The other mechanism is [dedicated instructions](instructions.md#opstack-manipulation).
+
 ## Jump Stack
 Another last-in;first-out data structure that keeps track of return and destination addresses.
 This stack changes only when control follows a `call` or `return` instruction.
+
+---
+
+[^1]:
+Of course, the machine running Triton VM might have stricter limitations:
+storing or accessing $(2^{64} - 2^{32} + 1)^2$ bits $\approx 4\cdot10^{25}$ TiB of data is a non-trivial engineering feat.

specification/src/processor-table.md

@@ -89,7 +89,6 @@ See [program attestation](program-attestation.md) for more details.
 1. The operational stack pointer `osp` is 16.
 1. The operational stack value `osv` is 0.
 1. The RAM pointer `ramp` is 0.
-1. The RAM value `ramv` is 0.
 1. `RunningEvaluationStandardInput` is 1.
 1. `RunningEvaluationStandardOutput` is 1.
 1. `InstructionLookupClientLogDerivative` has absorbed the first row with respect to challenges 🥝, 🥥, and 🫐 and indeterminate 🪥.
@@ -125,7 +124,6 @@ See [program attestation](program-attestation.md) for more details.
 1. `osp`
 1. `osv`
 1. `ramp`
-1. `ramv`
 1. `RunningEvaluationStandardInput - 1`
 1. `RunningEvaluationStandardOutput - 1`
 1. `InstructionLookupClientLogDerivative · (🪥 - 🥝·ip - 🥥·ci - 🫐·nia) - 1`

specification/src/random-access-memory-table.md

@@ -159,7 +159,6 @@ Both types of challenges are X-field elements, _i.e._, elements of $\mathbb{F}_{
 
 ## Initial Constraints
 
-1. RAM value `ramv` is 0 or `previous_instruction` is `write_mem`.
 1. The first coefficient of the Bézout coefficient polynomial 0 `bcpc0` is 0.
 1. The Bézout coefficient 0 `bc0` is 0.
 1. The Bézout coefficient 1 `bc1` is equal to the first coefficient of the Bézout coefficient polynomial `bcpc1`.
@@ -170,7 +169,6 @@ Both types of challenges are X-field elements, _i.e._, elements of $\mathbb{F}_{
 
 ### Initial Constraints as Polynomials
 
-1. `ramv·(previous_instruction - opcode(write_mem))`
 1. `bcpc0`
 1. `bc0`
 1. `bc1 - bcpc1`
@@ -186,7 +184,6 @@ None.
 ## Transition Constraints
 
 1. If `(ramp - ramp')` is 0, then `iord` is 0, else `iord` is the multiplicative inverse of `(ramp' - ramp)`.
-1. If the `ramp` changes and `previous_instruction` in the next row is not `write_mem`, then the RAM value `ramv` in the next row is 0.
 1. If the `ramp` does not change and `previous_instruction` in the next row is not `write_mem`, then the RAM value `ramv` does not change.
 1. The Bézout coefficient polynomial coefficients are allowed to change only when the `ramp` changes.
 1. The running product polynomial `rpp` accumulates a factor `(🧼 - ramp)` whenever `ramp` changes.
@@ -197,7 +194,6 @@ None.
 Written as Disjunctive Normal Form, the same constraints can be expressed as:
 1. `iord` is 0 or `iord` is the inverse of `(ramp' - ramp)`.
 1. `(ramp' - ramp)` is zero or `iord` is the inverse of `(ramp' - ramp)`.
-1. `(ramp' - ramp)` is zero or `previous_instruction'` is `opcode(write_mem)` or `ramv'` 0.
 1. `(ramp' - ramp)` non-zero or `previous_instruction'` is `opcode(write_mem)` or `ramv'` is `ramv`.
 1. `bcpc0' - bcpc0` is zero or `(ramp' - ramp)` is nonzero.
 1. `bcpc1' - bcpc1` is zero or `(ramp' - ramp)` is nonzero.
@@ -213,7 +209,6 @@ Written as Disjunctive Normal Form, the same constraints can be expressed as:
 
 1. `iord·(iord·(ramp' - ramp) - 1)`
 1. `(ramp' - ramp)·(iord·(ramp' - ramp) - 1)`
-1. `(ramp' - ramp)·(previous_instruction - opcode(write_mem))·ramv'`
 1. `(1 - iord·(ramp' - ramp))·(previous_instruction - opcode(write_mem))·(ramv' - ramv)`
 1. `(iord·(ramp' - ramp) - 1)·(bcpc0' - bcpc0)`
 1. `(iord·(ramp' - ramp) - 1)·(bcpc1' - bcpc1)`

specification/src/registers.md

@@ -48,10 +48,6 @@ They exist only to allow efficient arithmetization.
 
 ## RAM
 
-TritonVM has dedicated Random-Access Memory.
-Programs can read from and write to RAM using instructions `read_mem` and `write_mem`.
-The address to read from – respectively, to write to – is the stack's second-to-top-most OpStack element, i.e, `st1`.
-
 The registers `ramp` and `ramv` are not directly accessible by the program running in TritonVM.
 They exist only to allow efficient arithmetization.
 

triton-vm/benches/proof_size.rs

@@ -23,14 +23,15 @@ use triton_vm::prove_program;
 use triton_vm::stark::Stark;
 use triton_vm::stark::StarkHasher;
 use triton_vm::triton_program;
+use triton_vm::NonDeterminism;
 use triton_vm::Proof;
 use triton_vm::StarkParameters;
 
 /// Ties together a program and its inputs.
 struct ProgramAndInput {
     program: Program,
     public_input: Vec<u64>,
-    secret_input: Vec<u64>,
+    non_determinism: NonDeterminism<u64>,
 }
 
 /// The measurement unit for Criterion.
@@ -157,7 +158,7 @@ fn program_verify_sudoku() -> ProgramAndInput {
     ProgramAndInput {
         program: VERIFY_SUDOKU.clone(),
         public_input: sudoku.to_vec(),
-        secret_input: vec![],
+        non_determinism: [].into(),
     }
 }
 
@@ -167,15 +168,15 @@ fn program_fib(nth_element: u64) -> ProgramAndInput {
     ProgramAndInput {
         program: FIBONACCI_SEQUENCE.clone(),
         public_input: vec![nth_element],
-        secret_input: vec![],
+        non_determinism: [].into(),
     }
 }
 
 fn program_halt() -> ProgramAndInput {
     ProgramAndInput {
         program: triton_program!(halt),
         public_input: vec![],
-        secret_input: vec![],
+        non_determinism: [].into(),
     }
 }
 
@@ -244,7 +245,7 @@ fn sum_of_proof_lengths_for_source_code(
         let (_, _, proof) = prove_program(
             &program_and_input.program,
             &program_and_input.public_input,
-            &program_and_input.secret_input,
+            &program_and_input.non_determinism,
         )
         .unwrap();
         sum_of_proof_lengths += proof.encode().len();
@@ -261,7 +262,7 @@ fn generate_proof_and_benchmark_id(
     let (parameters, _, proof) = prove_program(
         &program_and_input.program,
         &program_and_input.public_input,
-        &program_and_input.secret_input,
+        &program_and_input.non_determinism,
     )
     .unwrap();
     let log_2_fri_domain_length = log_2_fri_domain_length(&parameters, &proof);

triton-vm/benches/prove_fib_100.rs

@@ -2,7 +2,6 @@ use criterion::criterion_group;
 use criterion::criterion_main;
 use criterion::BenchmarkId;
 use criterion::Criterion;
-use twenty_first::shared_math::b_field_element::BFieldElement;
 
 use triton_vm::example_programs::FIBONACCI_SEQUENCE;
 use triton_vm::prof_start;
@@ -12,6 +11,7 @@ use triton_vm::profiler::TritonProfiler;
 use triton_vm::proof::Claim;
 use triton_vm::stark::Stark;
 use triton_vm::stark::StarkHasher;
+use triton_vm::PublicInput;
 use triton_vm::StarkParameters;
 
 /// cargo criterion --bench prove_fib_100
@@ -28,16 +28,16 @@ fn prove_fib_100(criterion: &mut Criterion) {
     prof_start!(maybe_profiler, "parse program");
     let program = FIBONACCI_SEQUENCE.clone();
     prof_stop!(maybe_profiler, "parse program");
-    let public_input = [100].map(BFieldElement::new).to_vec();
+    let public_input: PublicInput = vec![100].into();
     prof_start!(maybe_profiler, "generate AET");
     let (aet, output) = program
-        .trace_execution(public_input.clone(), vec![])
+        .trace_execution(public_input.clone(), [].into())
         .unwrap();
     prof_stop!(maybe_profiler, "generate AET");
 
     let parameters = StarkParameters::default();
     let claim = Claim {
-        input: public_input,
+        input: public_input.individual_tokens,
         program_digest: program.hash::<StarkHasher>(),
         output,
     };

triton-vm/benches/prove_halt.rs

@@ -23,7 +23,7 @@ fn prove_halt(criterion: &mut Criterion) {
     prof_stop!(maybe_profiler, "parse program");
 
     prof_start!(maybe_profiler, "generate AET");
-    let (aet, output) = program.trace_execution(vec![], vec![]).unwrap();
+    let (aet, output) = program.trace_execution([].into(), [].into()).unwrap();
     prof_stop!(maybe_profiler, "generate AET");
 
     let cycle_count = aet.processor_trace.nrows();

triton-vm/benches/verify_halt.rs

@@ -21,7 +21,7 @@ fn verify_halt(criterion: &mut Criterion) {
         output: vec![],
     };
 
-    let (aet, _) = program.trace_execution(vec![], vec![]).unwrap();
+    let (aet, _) = program.trace_execution([].into(), [].into()).unwrap();
     let proof = Stark::prove(&parameters, &claim, &aet, &mut None);
 
     let mut profiler = Some(TritonProfiler::new("Verify Halt"));

triton-vm/src/error.rs

@@ -73,62 +73,62 @@ mod tests {
     #[should_panic(expected = "Instruction pointer 1 points outside of program")]
     fn test_vm_err() {
         let program = triton_program!(nop);
-        program.run(vec![], vec![]).unwrap();
+        program.run([].into(), [].into()).unwrap();
     }
 
     #[test]
     #[should_panic(expected = "Operational stack is too shallow")]
     fn shrink_op_stack_too_much_test() {
         let program = triton_program!(pop halt);
-        program.run(vec![], vec![]).unwrap();
+        program.run([].into(), [].into()).unwrap();
     }
 
     #[test]
     #[should_panic(expected = "Jump stack is empty.")]
     fn return_without_call_test() {
         let program = triton_program!(return halt);
-        program.run(vec![], vec![]).unwrap();
+        program.run([].into(), [].into()).unwrap();
     }
 
     #[test]
     #[should_panic(expected = "Jump stack is empty.")]
     fn recurse_without_call_test() {
         let program = triton_program!(recurse halt);
-        program.run(vec![], vec![]).unwrap();
+        program.run([].into(), [].into()).unwrap();
     }
 
     #[test]
     #[should_panic(expected = "Assertion failed: st0 must be 1. ip: 2, clk: 1, st0: 0")]
     fn assert_false_test() {
         let program = triton_program!(push 0 assert halt);
-        program.run(vec![], vec![]).unwrap();
+        program.run([].into(), [].into()).unwrap();
     }
 
     #[test]
     #[should_panic(expected = "0 does not have a multiplicative inverse")]
     fn inverse_of_zero_test() {
         let program = triton_program!(push 0 invert halt);
-        program.run(vec![], vec![]).unwrap();
+        program.run([].into(), [].into()).unwrap();
     }
 
     #[test]
     #[should_panic(expected = "Division by 0 is impossible")]
     fn division_by_zero_test() {
         let program = triton_program!(push 0 push 5 div halt);
-        program.run(vec![], vec![]).unwrap();
+        program.run([].into(), [].into()).unwrap();
     }
 
     #[test]
     #[should_panic(expected = "The logarithm of 0 does not exist")]
     fn log_of_zero_test() {
         let program = triton_program!(push 0 log_2_floor halt);
-        program.run(vec![], vec![]).unwrap();
+        program.run([].into(), [].into()).unwrap();
     }
 
     #[test]
     #[should_panic(expected = "Failed to convert BFieldElement 4294967297 into u32")]
     fn failed_u32_conversion_test() {
         let program = triton_program!(push 4294967297 push 1 and halt);
-        program.run(vec![], vec![]).unwrap();
+        program.run([].into(), [].into()).unwrap();
     }
 }