wip

kernel/.gitignore

@@ -0,0 +1,3 @@
+owi-out
+*.wat
+proofs

kernel/Cargo.toml

@@ -7,6 +7,7 @@ edition = "2021"
 
 [dev-dependencies]
 wasm-bindgen-test = "0.3.39"
+owi = {git = "https://github.com/dylibso/owi-rs"}
 
 [features]
 default = ["bounds-checking"]
@@ -15,4 +16,4 @@ bounds-checking = []
 [workspace]
 members = [
   "."
-]
+]

kernel/build.sh

@@ -1,5 +1,7 @@
 #!/usr/bin/env bash
 
+set -e
+
 export CARGO_FLAGS=""
 
 while getopts d flag

kernel/examples/alloc_length.rs

@@ -0,0 +1,21 @@
+#![no_main]
+#![no_std]
+use extism_runtime_kernel::*;
+use owi::*;
+
+main!({
+    let n = alloc(1024);
+
+    let x = u64();
+    assume(x > 0);
+
+    let m = alloc(x);
+
+    // 1. Length should equal `x` while active
+    assert(length(m) == x);
+
+    // 2. Length should equal `0` after free
+    free(m); // Free the block
+    assert(length(m) == 0);
+    free(n);
+});

kernel/examples/error.rs

@@ -0,0 +1,24 @@
+#![no_main]
+#![no_std]
+use extism_runtime_kernel::*;
+use owi::*;
+
+main!({
+    let x = u64();
+    let n = u64();
+    let m = u64();
+    assume(x > 0);
+    assume(n > 0);
+    assume(m > 0);
+
+    alloc(n);
+    alloc(m);
+    let n = alloc(x);
+    assert(error_get() == 0);
+
+    error_set(n);
+    assert(error_get() == n);
+    alloc(m);
+    error_set(0);
+    assert(error_get() == 0);
+});

kernel/examples/load_store.rs

@@ -0,0 +1,17 @@
+#![no_main]
+#![no_std]
+use extism_runtime_kernel::*;
+use owi::*;
+
+main!({
+    let x = u64();
+    assume(x > 0);
+
+    let m = alloc(x);
+    assert(length(m) == x);
+    for i in 0..x {
+        store_u8(m + i, i as u8);
+        assert(load_u8(m + i) == i as u8);
+    }
+    free(m);
+});

kernel/examples/reuse.rs

@@ -0,0 +1,39 @@
+#![no_main]
+#![no_std]
+use extism_runtime_kernel::*;
+use owi::*;
+
+main!({
+    let x = u64();
+    assume(x > 0);
+
+    let y = u64();
+    assume(y > 0);
+
+    let mut tmp = 0;
+
+    for _ in 0..y {
+        let m = alloc(x);
+        if tmp == 0 {
+            tmp = m;
+        } else {
+            // Check that the existing block is being re-used
+            assert(m == tmp);
+        }
+
+        assert(length(m) == x);
+        free(m); // Free the block
+    }
+
+    let y = u64();
+    assume(y == x + 1);
+    let n = alloc(y);
+    assert(n > tmp);
+
+    let z = u64();
+    assume(z <= x);
+    assume(x - z < 32);
+    assume(z > 0);
+    let p = alloc(z);
+    assert(p == tmp);
+});

kernel/src/bin/extism-runtime.rs

@@ -1,5 +1,5 @@
-#![no_main]
 #![no_std]
+#![no_main]
 
 pub use extism_runtime_kernel::*;
 

kernel/src/lib.rs

@@ -175,7 +175,7 @@ impl MemoryRoot {
         core::ptr::write_bytes(
             self.blocks.as_mut_ptr() as *mut u8,
             MemoryStatus::Unused as u8,
-            self_position as usize,
+            self_position as usize - core::mem::size_of::<MemoryRoot>(),
         );
 
         // Clear extism runtime metadata
@@ -638,4 +638,15 @@ mod test {
 
         assert_eq!(last, 0);
     }
+
+    #[wasm_bindgen_test]
+    fn test_sym() {
+        unsafe {
+            reset();
+            let a = alloc(47);
+            let b = alloc(20);
+            assert_eq!(length(a), 47);
+            assert_eq!(length(b), 20);
+        }
+    }
 }

kernel/verify.sh

@@ -0,0 +1,23 @@
+#!/usr/bin/env bash
+
+set -e
+
+OUT_DIR=./target/wasm32-unknown-unknown/release/examples/
+get_proof() {
+   cp "$OUT_DIR/$1.wasm" "./proofs/$1.wasm"
+}
+
+cargo build --examples --release --target wasm32-unknown-unknown --no-default-features
+
+mkdir -p proofs
+get_proof alloc_length
+get_proof load_store
+get_proof reuse
+get_proof error
+
+for proof in $(ls proofs/*.wasm); do
+  echo "Checking $proof"
+  owi  conc "$proof" $@
+  echo
+  echo "---"
+done