<div align="center">
    <h1><code>finite-wasm</code></h1>
    <strong>Cheating a little to solve the halting problem at scale</strong>
</div>

Guarantee deterministic limits on execution time and space resources made available to the
WebAssembly programs in a runtime-agnostic way.

# Contents

This projects provides a couple things:

* Ammendments to the WebAssembly core module specification describing the changes to the execution
  model such that the resource use is kept track of and limits are enforced;
* Analyses that inspect a given WebAssembly module and produce the information necessary to enforce
  the limits based on the amended execution model;
* A test suite validating the implementation of analyses against a modified reference WebAssembly
  interpreter.

The results of the provided analyses can be utilized quite flexibly: to instrument the WASM code;
to augment the machine code generated during compilation of the WASM code; to enforce the
resource limits at the interpreter runtime; or some other way, thus achieving the portability
properties of this project.

# Using `finite-wasm`

The test suite implements a rudimentary WebAssembly module transformation pass. The intent is for
it to be just enough to validate the properties of the analyses against the reference interpreter,
but it can definitely be taken as a base and adapted into a full production-grade transformation.
This is probably the best way to start with.

However this approach may prove to be less than satisfactory performance wise. Transforming a WASM
module will require parsing it, modifying it and then serializing it again. While parsing the WASM
module at least twice may be be unavoidable, the analyses are constructed such that modification
and re-serialization of the modules is not required.

## Examples

```rust
use finite_wasm::{wasmparser as wp, prefix_sum_vec};

struct MySizeConfig;
impl finite_wasm::max_stack::SizeConfig for MySizeConfig {
    fn size_of_value(&self, ty: wp::ValType) -> u8 {
        use wp::ValType::*;
        match ty {
            I32 => 4,
            I64 => 8,
            F32 => 4,
            F64 => 8,
            V128 => 16,
            FuncRef => 32,
            ExternRef => 32,
        }
    }

    fn size_of_function_activation(
        &self,
        locals: &prefix_sum_vec::PrefixSumVec<wp::ValType, u32>,
    ) -> u64 {
        u64::from(locals.max_index().map(|&v| v + 1).unwrap_or(0))
    }
}

macro_rules! define_fee {
    ($(@$proposal:ident $op:ident $({ $($arg:ident: $argty:ty),* })? => $visit:ident)*) => {
        $(
            fn $visit(&mut self $($(,$arg: $argty)*)?) -> Self::Output { 1 }
        )*
    }
}

struct MyGasConfig;
impl<'a> wp::VisitOperator<'a> for MyGasConfig {
    type Output = u64;
    wp::for_each_operator!(define_fee);
}

fn analyze_module(wasm_code: &[u8]) -> finite_wasm::AnalysisOutcome {
    finite_wasm::Analysis::new()
        .with_stack(MySizeConfig)
        .with_gas(MyGasConfig)
        .analyze(wasm_code)
        .expect("something went wrong!")
}
```

# License

This project is licensed under the MIT or Apache-2.0 license.
