start filling in builtin cost model
Co-authored-by: rvcas <x@rvcas.dev>
This commit is contained in:
parent
a5140513de
commit
84df3be139
|
@ -4,7 +4,7 @@ use crate::{
|
||||||
builtins::DefaultFunction,
|
builtins::DefaultFunction,
|
||||||
debruijn::{self, Converter},
|
debruijn::{self, Converter},
|
||||||
machine::{
|
machine::{
|
||||||
cost_model::{ExBudget, MachineCosts},
|
cost_model::{ExBudget, CostModel},
|
||||||
Machine,
|
Machine,
|
||||||
},
|
},
|
||||||
};
|
};
|
||||||
|
@ -407,7 +407,7 @@ impl From<Term<FakeNamedDeBruijn>> for Term<NamedDeBruijn> {
|
||||||
|
|
||||||
impl Program<NamedDeBruijn> {
|
impl Program<NamedDeBruijn> {
|
||||||
pub fn eval(&self) -> Result<Term<NamedDeBruijn>, crate::machine::Error> {
|
pub fn eval(&self) -> Result<Term<NamedDeBruijn>, crate::machine::Error> {
|
||||||
let mut machine = Machine::new(MachineCosts::default(), ExBudget::default(), 200);
|
let mut machine = Machine::new(CostModel::default(), ExBudget::default(), 200);
|
||||||
|
|
||||||
let (term, _, _) = machine.run(&self.term)?;
|
let (term, _, _) = machine.run(&self.term)?;
|
||||||
|
|
||||||
|
|
|
@ -7,13 +7,13 @@ pub mod cost_model;
|
||||||
mod error;
|
mod error;
|
||||||
mod runtime;
|
mod runtime;
|
||||||
|
|
||||||
use cost_model::{ExBudget, MachineCosts, StepKind};
|
use cost_model::{ExBudget, StepKind};
|
||||||
pub use error::Error;
|
pub use error::Error;
|
||||||
|
|
||||||
use self::runtime::BuiltinRuntime;
|
use self::{cost_model::CostModel, runtime::BuiltinRuntime};
|
||||||
|
|
||||||
pub struct Machine {
|
pub struct Machine {
|
||||||
costs: MachineCosts,
|
costs: CostModel,
|
||||||
ex_budget: ExBudget,
|
ex_budget: ExBudget,
|
||||||
frames: Vec<Context>,
|
frames: Vec<Context>,
|
||||||
slippage: u32,
|
slippage: u32,
|
||||||
|
@ -22,7 +22,7 @@ pub struct Machine {
|
||||||
}
|
}
|
||||||
|
|
||||||
impl Machine {
|
impl Machine {
|
||||||
pub fn new(costs: MachineCosts, initial_budget: ExBudget, slippage: u32) -> Machine {
|
pub fn new(costs: CostModel, initial_budget: ExBudget, slippage: u32) -> Machine {
|
||||||
Machine {
|
Machine {
|
||||||
costs,
|
costs,
|
||||||
ex_budget: initial_budget,
|
ex_budget: initial_budget,
|
||||||
|
@ -37,7 +37,7 @@ impl Machine {
|
||||||
&mut self,
|
&mut self,
|
||||||
term: &Term<NamedDeBruijn>,
|
term: &Term<NamedDeBruijn>,
|
||||||
) -> Result<(Term<NamedDeBruijn>, usize, Vec<String>), Error> {
|
) -> Result<(Term<NamedDeBruijn>, usize, Vec<String>), Error> {
|
||||||
let startup_budget = self.costs.get(StepKind::StartUp);
|
let startup_budget = self.costs.machine_costs.get(StepKind::StartUp);
|
||||||
|
|
||||||
self.spend_budget(startup_budget)?;
|
self.spend_budget(startup_budget)?;
|
||||||
|
|
||||||
|
@ -244,7 +244,7 @@ impl Machine {
|
||||||
runtime: BuiltinRuntime,
|
runtime: BuiltinRuntime,
|
||||||
) -> Result<Value, Error> {
|
) -> Result<Value, Error> {
|
||||||
if runtime.is_ready() {
|
if runtime.is_ready() {
|
||||||
self.spend_budget(ExBudget::default())?;
|
self.spend_budget(todo!())?;
|
||||||
|
|
||||||
runtime.call()
|
runtime.call()
|
||||||
} else {
|
} else {
|
||||||
|
@ -281,7 +281,8 @@ impl Machine {
|
||||||
|
|
||||||
fn spend_unbudgeted_steps(&mut self) -> Result<(), Error> {
|
fn spend_unbudgeted_steps(&mut self) -> Result<(), Error> {
|
||||||
for i in 0..self.unbudgeted_steps.len() - 1 {
|
for i in 0..self.unbudgeted_steps.len() - 1 {
|
||||||
let mut unspent_step_budget = self.costs.get(StepKind::try_from(i as u8)?);
|
let mut unspent_step_budget =
|
||||||
|
self.costs.machine_costs.get(StepKind::try_from(i as u8)?);
|
||||||
|
|
||||||
unspent_step_budget.occurences(self.unbudgeted_steps[i] as i32);
|
unspent_step_budget.occurences(self.unbudgeted_steps[i] as i32);
|
||||||
|
|
||||||
|
|
|
@ -11,14 +11,14 @@ impl ExBudget {
|
||||||
self.cpu *= n;
|
self.cpu *= n;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
#[derive(Default)]
|
||||||
pub struct CostModel {
|
pub struct CostModel {
|
||||||
pub machine_costs: MachineCosts,
|
pub machine_costs: MachineCosts,
|
||||||
|
pub builtin_costs: BuiltinCosts,
|
||||||
}
|
}
|
||||||
|
|
||||||
/// There's no entry for Error since we'll be exiting anyway; also, what would
|
/// There's no entry for Error since we'll be exiting anyway; also, what would
|
||||||
/// happen if calling 'Error' caused the budget to be exceeded?
|
/// happen if calling 'Error' caused the budget to be exceeded?
|
||||||
#[derive(Default)]
|
|
||||||
pub struct MachineCosts {
|
pub struct MachineCosts {
|
||||||
startup: ExBudget,
|
startup: ExBudget,
|
||||||
var: ExBudget,
|
var: ExBudget,
|
||||||
|
@ -47,6 +47,42 @@ impl MachineCosts {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
impl Default for MachineCosts {
|
||||||
|
fn default() -> Self {
|
||||||
|
Self {
|
||||||
|
startup: ExBudget { mem: 100, cpu: 100 },
|
||||||
|
var: ExBudget {
|
||||||
|
mem: 100,
|
||||||
|
cpu: 23000,
|
||||||
|
},
|
||||||
|
constant: ExBudget {
|
||||||
|
mem: 100,
|
||||||
|
cpu: 23000,
|
||||||
|
},
|
||||||
|
lambda: ExBudget {
|
||||||
|
mem: 100,
|
||||||
|
cpu: 23000,
|
||||||
|
},
|
||||||
|
delay: ExBudget {
|
||||||
|
mem: 100,
|
||||||
|
cpu: 23000,
|
||||||
|
},
|
||||||
|
force: ExBudget {
|
||||||
|
mem: 100,
|
||||||
|
cpu: 23000,
|
||||||
|
},
|
||||||
|
apply: ExBudget {
|
||||||
|
mem: 100,
|
||||||
|
cpu: 23000,
|
||||||
|
},
|
||||||
|
builtin: ExBudget {
|
||||||
|
mem: 100,
|
||||||
|
cpu: 23000,
|
||||||
|
},
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
pub struct BuiltinCosts {
|
pub struct BuiltinCosts {
|
||||||
pub add_integer: CostingFun<TwoArguments>,
|
pub add_integer: CostingFun<TwoArguments>,
|
||||||
pub subtract_integer: CostingFun<TwoArguments>,
|
pub subtract_integer: CostingFun<TwoArguments>,
|
||||||
|
@ -114,6 +150,322 @@ pub struct BuiltinCosts {
|
||||||
pub serialise_data: CostingFun<OneArgument>,
|
pub serialise_data: CostingFun<OneArgument>,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
impl Default for BuiltinCosts {
|
||||||
|
fn default() -> Self {
|
||||||
|
Self {
|
||||||
|
add_integer: CostingFun {
|
||||||
|
memory: TwoArguments::MaxSize(MaxSize {
|
||||||
|
intercept: 1,
|
||||||
|
slope: 1,
|
||||||
|
}),
|
||||||
|
cpu: TwoArguments::MaxSize(MaxSize {
|
||||||
|
intercept: 205665,
|
||||||
|
slope: 812,
|
||||||
|
}),
|
||||||
|
},
|
||||||
|
subtract_integer: CostingFun {
|
||||||
|
memory: TwoArguments::MaxSize(MaxSize {
|
||||||
|
intercept: 1,
|
||||||
|
slope: 1,
|
||||||
|
}),
|
||||||
|
cpu: TwoArguments::MaxSize(MaxSize {
|
||||||
|
intercept: 205665,
|
||||||
|
slope: 812,
|
||||||
|
}),
|
||||||
|
},
|
||||||
|
multiply_integer: CostingFun {
|
||||||
|
memory: TwoArguments::AddedSizes(AddedSizes {
|
||||||
|
intercept: 0,
|
||||||
|
slope: 1,
|
||||||
|
}),
|
||||||
|
|
||||||
|
cpu: TwoArguments::AddedSizes(AddedSizes {
|
||||||
|
intercept: 69522,
|
||||||
|
slope: 11687,
|
||||||
|
}),
|
||||||
|
},
|
||||||
|
divide_integer: CostingFun {
|
||||||
|
memory: TwoArguments::SubtractedSizes(SubtractedSizes {
|
||||||
|
intercept: 0,
|
||||||
|
slope: 1,
|
||||||
|
minimum: 1,
|
||||||
|
}),
|
||||||
|
cpu: TwoArguments::ConstAboveDiagonal(ConstantOrTwoArguments {
|
||||||
|
constant: 196500,
|
||||||
|
model: Box::new(TwoArguments::MultipliedSizes(MultipliedSizes {
|
||||||
|
intercept: 453240,
|
||||||
|
slope: 220,
|
||||||
|
})),
|
||||||
|
}),
|
||||||
|
},
|
||||||
|
quotient_integer: CostingFun {
|
||||||
|
memory: TwoArguments::SubtractedSizes(SubtractedSizes {
|
||||||
|
intercept: 0,
|
||||||
|
slope: 1,
|
||||||
|
minimum: 1,
|
||||||
|
}),
|
||||||
|
cpu: TwoArguments::ConstAboveDiagonal(ConstantOrTwoArguments {
|
||||||
|
constant: 196500,
|
||||||
|
model: Box::new(TwoArguments::MultipliedSizes(MultipliedSizes {
|
||||||
|
intercept: 453240,
|
||||||
|
slope: 220,
|
||||||
|
})),
|
||||||
|
}),
|
||||||
|
},
|
||||||
|
remainder_integer: CostingFun {
|
||||||
|
memory: TwoArguments::SubtractedSizes(SubtractedSizes {
|
||||||
|
intercept: 0,
|
||||||
|
slope: 1,
|
||||||
|
minimum: 1,
|
||||||
|
}),
|
||||||
|
cpu: TwoArguments::ConstAboveDiagonal(ConstantOrTwoArguments {
|
||||||
|
constant: 196500,
|
||||||
|
model: Box::new(TwoArguments::MultipliedSizes(MultipliedSizes {
|
||||||
|
intercept: 453240,
|
||||||
|
slope: 220,
|
||||||
|
})),
|
||||||
|
}),
|
||||||
|
},
|
||||||
|
mod_integer: CostingFun {
|
||||||
|
memory: TwoArguments::SubtractedSizes(SubtractedSizes {
|
||||||
|
intercept: 0,
|
||||||
|
slope: 1,
|
||||||
|
minimum: 1,
|
||||||
|
}),
|
||||||
|
cpu: TwoArguments::ConstAboveDiagonal(ConstantOrTwoArguments {
|
||||||
|
constant: 196500,
|
||||||
|
model: Box::new(TwoArguments::MultipliedSizes(MultipliedSizes {
|
||||||
|
intercept: 453240,
|
||||||
|
slope: 220,
|
||||||
|
})),
|
||||||
|
}),
|
||||||
|
},
|
||||||
|
equals_integer: CostingFun {
|
||||||
|
memory: TwoArguments::ConstantCost(1),
|
||||||
|
cpu: TwoArguments::MinSize(MinSize {
|
||||||
|
intercept: 208512,
|
||||||
|
slope: 421,
|
||||||
|
}),
|
||||||
|
},
|
||||||
|
less_than_integer: CostingFun {
|
||||||
|
memory: TwoArguments::ConstantCost(1),
|
||||||
|
cpu: TwoArguments::MinSize(MinSize {
|
||||||
|
intercept: 208896,
|
||||||
|
slope: 511,
|
||||||
|
}),
|
||||||
|
},
|
||||||
|
less_than_equals_integer: CostingFun {
|
||||||
|
memory: TwoArguments::ConstantCost(1),
|
||||||
|
cpu: TwoArguments::MinSize(MinSize {
|
||||||
|
intercept: 204924,
|
||||||
|
slope: 473,
|
||||||
|
}),
|
||||||
|
},
|
||||||
|
append_byte_string: CostingFun {
|
||||||
|
memory: TwoArguments::AddedSizes(AddedSizes {
|
||||||
|
intercept: 1000,
|
||||||
|
slope: 571,
|
||||||
|
}),
|
||||||
|
cpu: TwoArguments::AddedSizes(AddedSizes {
|
||||||
|
intercept: 0,
|
||||||
|
slope: 1,
|
||||||
|
}),
|
||||||
|
},
|
||||||
|
cons_byte_string: CostingFun {
|
||||||
|
memory: TwoArguments::AddedSizes(AddedSizes {
|
||||||
|
intercept: 0,
|
||||||
|
slope: 1,
|
||||||
|
}),
|
||||||
|
cpu: TwoArguments::LinearInY(LinearSize {
|
||||||
|
intercept: 221973,
|
||||||
|
slope: 511,
|
||||||
|
}),
|
||||||
|
},
|
||||||
|
slice_byte_string: CostingFun {
|
||||||
|
memory: ThreeArguments::LinearInZ(LinearSize {
|
||||||
|
intercept: 4,
|
||||||
|
slope: 0,
|
||||||
|
}),
|
||||||
|
cpu: ThreeArguments::LinearInZ(LinearSize {
|
||||||
|
intercept: 265318,
|
||||||
|
slope: 0,
|
||||||
|
}),
|
||||||
|
},
|
||||||
|
length_of_byte_string: CostingFun {
|
||||||
|
memory: OneArgument::ConstantCost(10),
|
||||||
|
cpu: OneArgument::ConstantCost(1000),
|
||||||
|
},
|
||||||
|
index_byte_string: CostingFun {
|
||||||
|
memory: TwoArguments::ConstantCost(4),
|
||||||
|
cpu: TwoArguments::ConstantCost(57667),
|
||||||
|
},
|
||||||
|
equals_byte_string: CostingFun {
|
||||||
|
memory: TwoArguments::ConstantCost(1),
|
||||||
|
cpu: TwoArguments::LinearOnDiagonal(ConstantOrLinear {
|
||||||
|
constant: 245000,
|
||||||
|
intercept: 216773,
|
||||||
|
slope: 62,
|
||||||
|
}),
|
||||||
|
},
|
||||||
|
less_than_byte_string: CostingFun {
|
||||||
|
memory: TwoArguments::ConstantCost(1),
|
||||||
|
cpu: TwoArguments::MinSize(MinSize {
|
||||||
|
intercept: 197145,
|
||||||
|
slope: 156,
|
||||||
|
}),
|
||||||
|
},
|
||||||
|
less_than_equals_byte_string: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
sha2_256: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
sha3_256: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
blake2b_256: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
verify_ed25519_signature: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
verify_ecdsa_secp256k1_signature: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
verify_schnorr_secp256k1_signature: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
append_string: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
equals_string: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
encode_utf8: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
decode_utf8: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
if_then_else: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
choose_unit: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
trace: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
fst_pair: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
snd_pair: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
choose_list: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
mk_cons: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
head_list: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
tail_list: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
null_list: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
choose_data: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
constr_data: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
map_data: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
list_data: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
i_data: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
b_data: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
un_constr_data: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
un_map_data: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
un_list_data: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
un_i_data: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
un_b_data: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
equals_data: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
mk_pair_data: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
mk_nil_data: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
mk_nil_pair_data: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
serialise_data: CostingFun {
|
||||||
|
memory: todo!(),
|
||||||
|
cpu: todo!(),
|
||||||
|
},
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
pub struct CostingFun<T> {
|
pub struct CostingFun<T> {
|
||||||
pub memory: T,
|
pub memory: T,
|
||||||
pub cpu: T,
|
pub cpu: T,
|
||||||
|
|
Loading…
Reference in New Issue