Create a common structure for verifiable state transition function

This commit is contained in:
Soowon Jeong
2023-09-19 20:19:32 +09:00
committed by GitHub
parent 0b1a29fe7b
commit 773c1bd1bb
8 changed files with 127 additions and 0 deletions

6
.gitignore vendored
View File

@@ -12,3 +12,9 @@ Cargo.lock
# MSVC Windows builds of rustc generate these, which store debugging information
*.pdb
# Added by cargo
/target
/Cargo.lock

8
Cargo.toml Normal file
View File

@@ -0,0 +1,8 @@
[package]
name = "vstf"
version = "0.1.0"
edition = "2021"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[dependencies]

53
src/execution/isa/mod.rs Normal file
View File

@@ -0,0 +1,53 @@
use crate::state::cpu::CpuState;
use crate::state_transition::Executable;
#[derive(Debug, Clone)]
pub enum Instruction {
Nop,
BinOp { op: BinaryOperation },
Branch(Branch),
Jump(usize),
Load,
Save,
}
impl Executable for Instruction {
type State = CpuState;
fn execute(&self, state: Self::State) -> Self::State {
match self {
Self::Nop => state,
_ => todo!(),
}
}
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum BinaryOperation {
Add,
Minus,
Multiply,
Divide,
Equal,
NotEqual,
LessThan,
GreaterThan,
And,
Or,
Xor,
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Branch {
Beq,
Bne,
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Operand {
Register(Register),
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Register {
Temp(usize),
}

1
src/execution/mod.rs Normal file
View File

@@ -0,0 +1 @@
pub mod isa;

10
src/lib.rs Normal file
View File

@@ -0,0 +1,10 @@
pub mod execution;
pub mod state;
pub mod state_transition;
pub mod benches;
#[derive(Debug, Clone)]
pub enum Error {
Misc,
}

14
src/state/cpu.rs Normal file
View File

@@ -0,0 +1,14 @@
use crate::state_transition::State;
#[derive(Clone, Debug, Copy)]
pub struct CpuState {
pub pc: usize,
}
impl CpuState {
pub fn init() -> Self {
CpuState { pc: 0 }
}
}
impl State for CpuState {}

1
src/state/mod.rs Normal file
View File

@@ -0,0 +1 @@
pub mod cpu;

View File

@@ -0,0 +1,34 @@
use std::fmt::Debug;
pub trait State: Clone + Debug {}
pub trait Executable: Clone + Debug {
type State: State;
fn execute(&self, state: Self::State) -> Self::State;
}
pub trait Instance: Clone + Debug {
type ProvableObject: Clone + Debug;
type ProvedObject: Clone + Debug;
type Error: Clone + Debug;
type State: Clone + Debug;
fn prove(&self) -> Result<Self::ProvedObject, Self::Error>;
fn verify(&self) -> bool;
}
pub trait StateTransition: Clone + Debug {
type Provable: Instance;
type Executable: Clone + Debug;
type Error: Clone + Debug;
// if it uses folding or recursive method,
// then the number of element of each parameter should be 1
// And run this vstf for all steps
fn vstf(
input_instance: Vec<Self::Provable>,
result_instance: Self::Provable,
execution: Vec<Self::Executable>,
) -> bool;
}