Skip to content

Commit

Permalink
Add rust prover
Browse files Browse the repository at this point in the history
  • Loading branch information
nickdrozd committed Jul 6, 2024
1 parent 29306a9 commit 5af528d
Show file tree
Hide file tree
Showing 10 changed files with 656 additions and 56 deletions.
4 changes: 2 additions & 2 deletions src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,8 @@ mod rust_stuff {
use crate::{
blocks::opt_block,
machine::{
quick_term_or_rec_py, run_quick_machine, MachineResult,
TermRes,
quick_term_or_rec_py, run_prover, run_quick_machine,
MachineResult, TermRes,
},
parse::{
init_prog, parse_to_vec, read_slot, show_comp_py,
Expand Down
205 changes: 203 additions & 2 deletions src/machine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@ use pyo3::{pyclass, pyfunction, pymethods};
use crate::{
instrs::{CompProg, Slot, State},
parse::tcompile,
prover::{Prover, ProverResult},
rules::apply_rule,
tape::{BasicTape as Tape, Count, HeadTape},
};

Expand All @@ -16,23 +18,27 @@ type Blanks = Dict<State, Step>;

#[expect(non_camel_case_types)]
#[pyclass(eq, eq_int)]
#[derive(Clone, PartialEq, Eq)]
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum TermRes {
xlimit,
cfglim,
infrul,
spnout,
undfnd,
mulrul,
}

/**************************************/

#[pyclass]
#[derive(Debug, PartialEq, Eq)]
pub struct MachineResult {
result: TermRes,

steps: Step,
cycles: Step,
marks: Count,
rulapp: Count,

blanks: Blanks,

Expand All @@ -42,12 +48,13 @@ pub struct MachineResult {
#[pymethods]
impl MachineResult {
#[new]
#[pyo3(signature = (result, steps, cycles, marks, blanks, last_slot))]
#[pyo3(signature = (result, steps, cycles, marks, rulapp, blanks, last_slot))]
const fn new(
result: TermRes,
steps: Step,
cycles: Step,
marks: Count,
rulapp: Count,
blanks: Blanks,
last_slot: Option<Slot>,
) -> Self {
Expand All @@ -56,6 +63,7 @@ impl MachineResult {
steps,
cycles,
marks,
rulapp,
blanks,
last_slot,
}
Expand All @@ -76,6 +84,11 @@ impl MachineResult {
self.marks
}

#[getter]
const fn rulapp(&self) -> Count {
self.rulapp
}

#[getter]
fn blanks(&self) -> Blanks {
self.blanks.clone()
Expand Down Expand Up @@ -134,8 +147,164 @@ impl MachineResult {
_ => None,
}
}

#[getter]
const fn cfglim(&self) -> Option<Step> {
match self.result {
TermRes::cfglim => Some(self.steps),
_ => None,
}
}
}

/**************************************/

#[cfg(test)]
pub fn run_for_infrul(comp: &CompProg, sim_lim: Step) -> bool {
let mut tape = Tape::init(0);

let mut prover = Prover::new(comp);

let mut state = 0;

for cycle in 0..sim_lim {
match prover.try_rule(cycle as i32, state, &tape) {
None => {},
Some(
ProverResult::ConfigLimit | ProverResult::MultRule,
) => {
return false;
},
Some(ProverResult::InfiniteRule) => {
return true;
},
Some(ProverResult::Got(rule)) => {
if apply_rule(&rule, &mut tape).is_some() {
// println!("--> applying rule: {:?}", rule);
continue;
}
},
}

let slot = (state, tape.scan);

let Some(&(color, shift, next_state)) = comp.get(&slot) else {
return false;
};

let same = state == next_state;

if same && tape.at_edge(shift) {
return false;
}

tape.step(shift, color, same);

state = next_state;
}

false
}

/**************************************/

#[pyfunction]
#[pyo3(signature = (prog, sim_lim=100_000_000))]
pub fn run_prover(prog: &str, sim_lim: Step) -> MachineResult {
let comp = tcompile(prog);

let mut tape = Tape::init(0);

let mut prover = Prover::new(&comp);

let mut blanks = Blanks::new();

let mut state = 0;
let mut steps = 0;
let mut cycles = 0;
let mut rulapp = 0;

let mut result: Option<TermRes> = None;
let mut last_slot: Option<Slot> = None;

for cycle in 0..sim_lim {
match prover.try_rule(cycle as i32, state, &tape) {
None => {},
Some(ProverResult::ConfigLimit) => {
cycles = cycle;
result = Some(TermRes::cfglim);
break;
},
Some(ProverResult::InfiniteRule) => {
cycles = cycle;
result = Some(TermRes::infrul);
break;
},
Some(ProverResult::MultRule) => {
cycles = cycle;
result = Some(TermRes::mulrul);
break;
},
Some(ProverResult::Got(rule)) => {
if let Some(times) = apply_rule(&rule, &mut tape) {
// println!("--> applying rule: {:?}", rule);
rulapp += times;
continue;
}
},
}

let slot = (state, tape.scan);

let Some(&(color, shift, next_state)) = comp.get(&slot) else {
cycles = cycle;
result = Some(TermRes::undfnd);
last_slot = Some(slot);
break;
};

let same = state == next_state;

if same && tape.at_edge(shift) {
cycles = cycle;
result = Some(TermRes::spnout);
break;
}

let stepped = tape.step(shift, color, same);

steps += stepped;

state = next_state;

if color == 0 && tape.blank() {
if blanks.contains_key(&state) {
result = Some(TermRes::infrul);
break;
}

blanks.insert(state, steps);

if state == 0 {
result = Some(TermRes::infrul);
break;
}
}
}

MachineResult {
result: result.unwrap_or(TermRes::xlimit),
steps,
cycles,
marks: tape.marks(),
rulapp,
last_slot,
blanks,
}
}

/**************************************/

#[pyfunction]
#[pyo3(signature = (prog, sim_lim=100_000_000))]
pub fn run_quick_machine(prog: &str, sim_lim: Step) -> MachineResult {
Expand Down Expand Up @@ -196,6 +365,7 @@ pub fn run_quick_machine(prog: &str, sim_lim: Step) -> MachineResult {
steps,
cycles,
marks: tape.marks(),
rulapp: 0,
last_slot,
blanks,
}
Expand Down Expand Up @@ -273,3 +443,34 @@ pub fn quick_term_or_rec(

false
}

/**************************************/

#[test]
fn test_prover() {
assert_eq!(
run_prover("1RB 2LA 1RA 1RA 1LB 1LA 3RB ...", 1000),
MachineResult {
result: TermRes::undfnd,
steps: 36686,
cycles: 397,
marks: 2050,
rulapp: 987,
blanks: Dict::from([]),
last_slot: Some((1, 3))
}
);

assert_eq!(
run_prover("1RB 1LC 1RD 1RB 0RD 0RC 1LD 1LA", 1000),
MachineResult {
result: TermRes::spnout,
steps: 56459,
cycles: 229,
marks: 0,
rulapp: 5073,
blanks: Dict::from([(2, 56458), (3, 56459)]),
last_slot: None
}
);
}
Loading

0 comments on commit 5af528d

Please sign in to comment.