From b84fbe801d688b35a1cf3a6253268a17def73308 Mon Sep 17 00:00:00 2001 From: Yuhan Deng Date: Wed, 29 Jul 2026 11:28:06 -0700 Subject: [PATCH] feat: generate coupon.wat from fix-proof --- .gitignore | 1 + .gitmodules | 3 + fix/build.rs | 69 +++- fix/wasm/coupon.wat | 685 --------------------------------- fix/wasm/coupon/epilogue.wat | 98 +++++ fix/wasm/coupon/fix-proof | 1 + fix/wasm/coupon/prologue.wat | 26 ++ fix/wasm/coupon/rewrite-wat.sh | 62 +++ 8 files changed, 244 insertions(+), 701 deletions(-) delete mode 100644 fix/wasm/coupon.wat create mode 100644 fix/wasm/coupon/epilogue.wat create mode 160000 fix/wasm/coupon/fix-proof create mode 100644 fix/wasm/coupon/prologue.wat create mode 100755 fix/wasm/coupon/rewrite-wat.sh diff --git a/.gitignore b/.gitignore index e7aa5ba8..a9c97b2f 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ /target .build .fix +fix/wasm/coupon.wat diff --git a/.gitmodules b/.gitmodules index 068a7e52..2f65385b 100644 --- a/.gitmodules +++ b/.gitmodules @@ -4,3 +4,6 @@ [submodule "fix/wabt"] path = fix/wabt url = https://github.com/WebAssembly/wabt.git +[submodule "fix/wasm/fix-proof"] + path = fix/wasm/coupon/fix-proof + url = https://github.com/fix-project/fix-proof.git diff --git a/fix/build.rs b/fix/build.rs index c6067989..0e5cc791 100644 --- a/fix/build.rs +++ b/fix/build.rs @@ -130,6 +130,37 @@ fn c2elf(c: &[u8], h: &[u8]) -> Result> { Ok(o) } +fn generate_coupon() -> Result<()> { + let coupon_dir = Path::new("wasm/coupon"); + + let script = coupon_dir.join("rewrite-wat.sh"); + let coupon = coupon_dir.join("fix-proof/coupon.wat"); + let prologue = coupon_dir.join("prologue.wat"); + let epilogue = coupon_dir.join("epilogue.wat"); + + println!("cargo::rerun-if-changed={}", script.display()); + println!("cargo::rerun-if-changed={}", coupon.display()); + println!("cargo::rerun-if-changed={}", prologue.display()); + println!("cargo::rerun-if-changed={}", epilogue.display()); + + let output = Path::new("wasm/coupon.wat"); + + let status = Command::new("bash") + .arg(&script) + .arg(&coupon) + .arg(&prologue) + .arg(&epilogue) + .arg(output) + .status() + .unwrap_or_else(|error| panic!("failed to run {}: {error}", script.display())); + + if !status.success() { + panic!("{} failed with status {status}", script.display()); + } + + Ok(()) +} + fn main() -> Result<()> { let out_dir = env::var_os("OUT_DIR").unwrap(); @@ -157,24 +188,30 @@ fn main() -> Result<()> { WASM2C.set(dst.join("bin/wasm2c")).unwrap(); WAT2WASM.set(dst.join("bin/wat2wasm")).unwrap(); + generate_coupon()?; + for f in std::fs::read_dir("wasm")? { let f = f?; - let path = f.path(); - let base = path.file_stem().unwrap(); - let dst = Path::new(&out_dir).join(base); - println!( - "cargo::rerun-if-changed=wasm/{}", - f.file_name().to_str().unwrap() - ); - let wat = std::fs::read(f.path())?; - let wasm = wat2wasm(&wat)?; - let (c, h) = wasm2c(&wasm)?; - let elf = c2elf(&c, &h)?; - std::fs::write(&dst, elf)?; - - let link = Path::new(&out_dir).ancestors().nth(4).unwrap().join(base); - let _ = fs::remove_file(&link); - symlink(dst, link)?; + if f.file_type()?.is_file() { + let path = f.path(); + let base = path.file_stem().unwrap(); + let dst = Path::new(&out_dir).join(base); + if base != "coupon" { + println!( + "cargo::rerun-if-changed=wasm/{}", + f.file_name().to_str().unwrap() + ); + } + let wat = std::fs::read(f.path())?; + let wasm = wat2wasm(&wat)?; + let (c, h) = wasm2c(&wasm)?; + let elf = c2elf(&c, &h)?; + std::fs::write(&dst, elf)?; + + let link = Path::new(&out_dir).ancestors().nth(4).unwrap().join(base); + let _ = fs::remove_file(&link); + symlink(dst, link)?; + } } let cwd = std::env::var("CARGO_MANIFEST_DIR").unwrap(); diff --git a/fix/wasm/coupon.wat b/fix/wasm/coupon.wat deleted file mode 100644 index f7b36c35..00000000 --- a/fix/wasm/coupon.wat +++ /dev/null @@ -1,685 +0,0 @@ -(module - (import "fixpoint" "is_equal" (func $is_equal (param externref) (param externref) (result i32))) - (import "fixpoint" "is_tag" (func $is_tag (param externref) (result i32))) - (import "fixpoint" "attach_blob" (func $attach_blob (param i32) (param externref))) - (import "fixpoint" "attach_tree" (func $attach_tree (param i32) (param externref))) - (import "fixpoint" "create_blob_i32" (func $create_blob_i32 (param i32) (result externref))) - (import "fixpoint" "create_tag" (func $create_tag (param i32) (result externref))) - (import "fixpoint" "create_application_thunk" (func $create_application_thunk (param externref) (result externref))) - (import "fixpoint" "create_strict_encode" (func $create_strict_encode (param externref) (result externref))) - (import "fixpoint" "create_shallow_encode" (func $create_shallow_encode (param externref) (result externref))) - (import "fixpoint" "is_blob_obj" (func $is_blob_obj (param externref) (result i32))) - (import "fixpoint" "is_data" (func $is_data (param externref) (result i32))) - (import "fixpoint" "is_object" (func $is_object (param externref) (result i32))) - (table $encode 0 externref) - (table $coupon_scratch 0 externref) - (table $coupons 0 externref) - (table $lhstree 0 externref) - (table $rhstree 0 externref) - (table $output_coupon_scratch 4 externref) - (memory $mem_0 0) - (memory $mem_1 0) - (global $Eq i32 (i32.const 0)) - (global $Eval i32 (i32.const 1)) - (global $Apply i32 (i32.const 2)) - (global $Force i32 (i32.const 3)) - (global $Think i32 (i32.const 4)) - (global $Storage i32 (i32.const 5)) - (type $make_coupon_t (func (param externref externref) (result externref))) - (func $is_coupon (param $tag externref) (param $type i32) (result i32) - (call $is_tag (local.get $tag)) - (if (result i32) - (then - ;; Attach the tag - (call $attach_tree (i32.const 1) (local.get $tag)) - ;; Check if the tag was authored by us - (call $is_equal (table.get $encode (i32.const 0)) (table.get $coupon_scratch (i32.const 0))) - (if (result i32) - (then - ;; Check if the coupon type matches the input type - (call $attach_blob (i32.const 1) (table.get $coupon_scratch (i32.const 1))) - (i32.load (memory $mem_1) (i32.const 0)) - (local.get $type) - i32.eq - (if (result i32) - (then (i32.const 1)) - (else (i32.const 0)) - ) - ) - (else (i32.const 0)) - ) - ) - (else (i32.const 0)) - ) - ) - (func $is_eq_coupon (param $tag externref) (result i32) - (call $is_coupon (local.get $tag) (global.get $Eq)) - ) - (func $is_eval_coupon (param $tag externref) (result i32) - (call $is_coupon (local.get $tag) (global.get $Eval)) - ) - (func $is_apply_coupon (param $tag externref) (result i32) - (call $is_coupon (local.get $tag) (global.get $Apply)) - ) - (func $is_force_coupon (param $tag externref) (result i32) - (call $is_coupon (local.get $tag) (global.get $Force)) - ) - (func $is_think_coupon (param $tag externref) (result i32) - (call $is_coupon (local.get $tag) (global.get $Think)) - ) - (func $is_storage_coupon (param $tag externref) (result i32) - (call $is_coupon (local.get $tag) (global.get $Storage)) - ) - (func $create_coupon (param $type i32) (param $lhs externref) (param $rhs externref) (result externref) - (table.set $output_coupon_scratch (i32.const 0) (table.get $encode (i32.const 0))) - (table.set $output_coupon_scratch (i32.const 1) (call $create_blob_i32 (local.get $type))) - (table.set $output_coupon_scratch (i32.const 2) (local.get $lhs)) - (table.set $output_coupon_scratch (i32.const 3) (local.get $rhs)) - (call $create_tag (i32.const 5)) - ) - (func $create_eq_coupon (param $lhs externref) (param $rhs externref) (result externref) - (call $create_coupon (global.get $Eq) (local.get $lhs) (local.get $rhs)) - ) - (func $create_eval_coupon (param $lhs externref) (param $rhs externref) (result externref) - (call $create_coupon (global.get $Eval) (local.get $lhs) (local.get $rhs)) - ) - (func $create_force_coupon (param $lhs externref) (param $rhs externref) (result externref) - (call $create_coupon (global.get $Force) (local.get $lhs) (local.get $rhs)) - ) - (func $create_think_coupon (param $lhs externref) (param $rhs externref) (result externref) - (call $create_coupon (global.get $Think) (local.get $lhs) (local.get $rhs)) - ) - (func $get_coupon_lhs (param $coupon externref) (result externref) - (call $attach_tree (i32.const 1) (local.get $coupon)) - (table.get $coupon_scratch (i32.const 2)) - ) - (func $get_coupon_rhs (param $coupon externref) (result externref) - (call $attach_tree (i32.const 1) (local.get $coupon)) - (table.get $coupon_scratch (i32.const 3)) - ) - (func $attach_lhs_tree (param $lhs externref) - (call $attach_tree (i32.const 3) (local.get $lhs)) - ) - (func $attach_rhs_tree (param $rhs externref) - (call $attach_tree (i32.const 4) (local.get $rhs)) - ) - (func $get_tree_size_lhs (result i32) - table.size $lhstree - ) - (func $get_tree_size_rhs (result i32) - table.size $rhstree - ) - (func $get_tree_data_lhs (param $i i32) (result externref) - (table.get $lhstree (local.get $i)) - ) - (func $get_tree_data_rhs (param $i i32) (result externref) - (table.get $rhstree (local.get $i)) - ) - (func $make_eq_tree_coupon (export "make_eq_tree_coupon") (param $lhs externref) (param $rhs externref) (result externref) (local $c externref) (local $size i32) (local $i i32) - (local.set $size (table.size $coupons)) - ;; Check that all coupons are eq coupons - (local.set $i (i32.const 0)) - (block $exit - (loop $loop - (local.get $i) - (local.get $size) - i32.ge_s - br_if $exit - - (call $is_eq_coupon (table.get $coupons (local.get $i))) - (if - (then nop) - (else unreachable) - ) - - (local.set $i (i32.add (local.get $i) (i32.const 1))) - br $loop - ) - ) - - ;; Attach lhs tree and rhs tree - (call $attach_lhs_tree (local.get $lhs)) - (call $attach_rhs_tree (local.get $rhs)) - - ;; Check tree size of lhs and rhs - (i32.eq (call $get_tree_size_lhs) (local.get $size)) - (if (result externref) - (then - (i32.eq (call $get_tree_size_rhs) (local.get $size)) - (if (result externref) - (then - ;; Check that each coupon corresponds to one pair of tree entries - (local.set $i (i32.const 0)) - (block $exit - (loop $loop - (local.get $i) - (local.get $size) - i32.ge_s - br_if $exit - - (local.set $c (table.get $coupons (local.get $i))) - (call $is_equal (call $get_tree_data_lhs (local.get $i)) (call $get_coupon_lhs (local.get $c))) - (if - (then - (call $is_equal (call $get_tree_data_rhs (local.get $i)) (call $get_coupon_rhs (local.get $c))) - (if - (then nop) - (else unreachable) - ) - ) - (else - unreachable - ) - ) - - (local.set $i (i32.add (local.get $i) (i32.const 1))) - br $loop - ) - ) - (call $create_eq_coupon (local.get $lhs) (local.get $rhs)) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - )) - (func $make_eval_tree_coupon (export "make_eval_tree_coupon") (param $lhs externref) (param $rhs externref) (result externref) (local $c externref) (local $size i32) (local $i i32) - (local.set $size (table.size $coupons)) - ;; Check that all coupons are eval coupons - (local.set $i (i32.const 0)) - (block $exit - (loop $loop - (local.get $i) - (local.get $size) - i32.ge_s - br_if $exit - - (call $is_eval_coupon (table.get $coupons (local.get $i))) - (if - (then nop) - (else unreachable) - ) - - (local.set $i (i32.add (local.get $i) (i32.const 1))) - br $loop - ) - ) - - ;; Attach lhs tree and rhs tree - (call $attach_lhs_tree (local.get $lhs)) - (call $attach_rhs_tree (local.get $rhs)) - - ;; Check tree size of lhs and rhs - (i32.eq (call $get_tree_size_lhs) (local.get $size)) - (if (result externref) - (then - (i32.eq (call $get_tree_size_rhs) (local.get $size)) - (if (result externref) - (then - ;; Check that each coupon corresponds to one pair of tree entries - (local.set $i (i32.const 0)) - (block $exit - (loop $loop - (local.get $i) - (local.get $size) - i32.ge_s - br_if $exit - - (local.set $c (table.get $coupons (local.get $i))) - (call $is_equal (call $get_tree_data_lhs (local.get $i)) (call $get_coupon_lhs (local.get $c))) - (if - (then - (call $is_equal (call $get_tree_data_rhs (local.get $i)) (call $get_coupon_rhs (local.get $c))) - (if - (then nop) - (else unreachable) - ) - ) - (else - unreachable - ) - ) - - (local.set $i (i32.add (local.get $i) (i32.const 1))) - br $loop - ) - ) - (call $create_eval_coupon (local.get $lhs) (local.get $rhs)) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - )) - (func $make_force_result_eq_coupon (export "make_force_result_eq_coupon") (param $lhs externref) (param $rhs externref) (result externref) (local $f1 externref) (local $f2 externref) (local $e externref) - (local.set $f1 (table.get $coupons (i32.const 0))) - (local.set $f2 (table.get $coupons (i32.const 1))) - (local.set $e (table.get $coupons (i32.const 2))) - (call $is_force_coupon (local.get $f1)) - (if (result externref) - (then - (call $is_force_coupon (local.get $f2)) - (if (result externref) - (then - (call $is_eq_coupon (local.get $e)) - (if (result externref) - (then - (call $is_equal (call $get_coupon_rhs (local.get $f1)) (call $get_coupon_lhs (local.get $e))) - (if (result externref) - (then - (call $is_equal (call $get_coupon_rhs (local.get $f2)) (call $get_coupon_rhs (local.get $e))) - (if (result externref) - (then - (call $is_equal (call $get_coupon_lhs (local.get $f1)) (local.get $lhs)) - (if (result externref) - (then - (call $is_equal (call $get_coupon_lhs (local.get $f2)) (local.get $rhs)) - (if (result externref) - (then - (call $create_eq_coupon (local.get $lhs) (local.get $rhs)) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - )) - (func $make_eval_eq_coupon (export "make_eval_eq_coupon") (param $lhs externref) (param $rhs externref) (result externref) (local $c1 externref) (local $c2 externref) - (local.set $c1 (table.get $coupons (i32.const 0))) - (local.set $c2 (table.get $coupons (i32.const 1))) - (call $is_eval_coupon (local.get $c1)) - (if (result externref) - (then - (call $is_eq_coupon (local.get $c2)) - (if (result externref) - (then - (call $is_equal (call $get_coupon_lhs (local.get $c1)) (call $get_coupon_lhs (local.get $c2))) - (if (result externref) - (then - (call $is_equal (call $get_coupon_rhs (local.get $c2)) (local.get $lhs)) - (if (result externref) - (then - (call $is_equal (call $get_coupon_rhs (local.get $c1)) (local.get $rhs)) - (if (result externref) - (then - (call $create_eval_coupon (local.get $lhs) (local.get $rhs)) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (func $make_think_application_coupon (export "make_think_application_coupon") (param $lhs externref) (param $rhs externref) (result externref) (local $c1 externref) (local $c2 externref) - (local.set $c1 (table.get $coupons (i32.const 0))) - (local.set $c2 (table.get $coupons (i32.const 1))) - (call $is_eval_coupon (local.get $c1)) - (if (result externref) - (then - (call $is_apply_coupon (local.get $c2)) - (if (result externref) - (then - (call $is_equal (call $get_coupon_rhs (local.get $c1)) (call $get_coupon_lhs (local.get $c2))) - (if (result externref) - (then - (call $is_equal (call $create_application_thunk (call $get_coupon_lhs (local.get $c1))) (local.get $lhs)) - (if (result externref) - (then - (call $is_equal (call $get_coupon_rhs (local.get $c2)) (local.get $rhs)) - (if (result externref) - (then - (call $create_think_coupon (local.get $lhs) (local.get $rhs)) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - )) - (func $make_think_to_force_coupon (export "make_think_to_force_coupon") (param $lhs externref) (param $rhs externref) (result externref) (local $t externref) - (local.set $t (table.get $coupons (i32.const 0))) - (call $is_think_coupon (local.get $t)) - (if (result externref) - (then - (call $is_data (call $get_coupon_rhs (local.get $t))) - (if (result externref) - (then - (call $is_equal (call $get_coupon_lhs (local.get $t)) (local.get $lhs)) - (if (result externref) - (then - (call $is_equal (call $get_coupon_rhs (local.get $t)) (local.get $rhs)) - (if (result externref) - (then - (call $create_force_coupon (local.get $lhs) (local.get $rhs)) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - )) - (func $make_force_to_encode_strict_coupon (export "make_force_to_encode_strict_coupon") (param $lhs externref) (param $rhs externref) (result externref) (local $t externref) - (local.set $t (table.get $coupons (i32.const 0))) - (call $is_force_coupon (local.get $t)) - (if (result externref) - (then - (call $is_object (call $get_coupon_rhs (local.get $t))) - (if (result externref) - (then - (call $is_equal (call $get_coupon_rhs (local.get $t)) (local.get $rhs)) - (if (result externref) - (then - (call $is_equal (call $create_strict_encode (call $get_coupon_lhs (local.get $t))) (local.get $lhs)) - (if (result externref) - (then - (call $create_eq_coupon (local.get $lhs) (local.get $rhs)) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - )) -(func $make_eval_blobobj_coupon (export "make_eval_blobobj_coupon") (param $lhs externref) (param $rhs externref) (result externref) - (call $is_blob_obj (local.get $lhs)) - (if (result externref) - (then - (call $is_equal (local.get $lhs) (local.get $rhs)) - (if (result externref) - (then - (call $create_eval_coupon (local.get $lhs) (local.get $rhs)) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - )) - (func $make_eq_application_coupon (export "make_eq_application_coupon") (param $lhs externref) (param $rhs externref) (result externref) (local $e externref) - (local.set $e (table.get $coupons (i32.const 0))) - (call $is_eq_coupon (local.get $e)) - (if (result externref) - (then - (local.get $lhs) - (call $create_application_thunk (call $get_coupon_lhs (local.get $e))) - (call $is_equal) - (if (result externref) - (then - (local.get $rhs) - (call $create_application_thunk (call $get_coupon_rhs (local.get $e))) - (call $is_equal) - (if (result externref) - (then - (call $create_eq_coupon (local.get $lhs) (local.get $rhs)) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - )) - (func $make_eq_encode_strict_coupon (export "make_eq_encode_strict_coupon") (param $lhs externref) (param $rhs externref) (result externref) (local $e externref) - (local.set $e (table.get $coupons (i32.const 0))) - (call $is_eq_coupon (local.get $e)) - (if (result externref) - (then - (call $is_equal (call $create_strict_encode (call $get_coupon_lhs (local.get $e))) (local.get $lhs)) - (if (result externref) - (then - (call $is_equal (call $create_strict_encode (call $get_coupon_rhs (local.get $e))) (local.get $rhs)) - (if (result externref) - (then - (call $create_eq_coupon (local.get $lhs) (local.get $rhs)) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - )) - (func $make_sym_coupon (export "make_sym_coupon") (param $lhs externref) (param $rhs externref) (result externref) (local $e externref) - (local.set $e (table.get $coupons (i32.const 0))) - (call $is_eq_coupon (local.get $e)) - (if (result externref) - (then - (call $is_equal (call $get_coupon_rhs (local.get $e)) (local.get $lhs)) - (if (result externref) - (then - (call $is_equal (call $get_coupon_lhs (local.get $e)) (local.get $rhs)) - (if (result externref) - (then - (call $create_eq_coupon (local.get $lhs) (local.get $rhs)) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - )) - (func $make_trans_coupon (export "make_trans_coupon") (param $lhs externref) (param $rhs externref) (result externref) (local $e1 externref) (local $e2 externref) - (local.set $e1 (table.get $coupons (i32.const 0))) - (local.set $e2 (table.get $coupons (i32.const 1))) - (call $is_eq_coupon (local.get $e1)) - (if (result externref) - (then - (call $is_eq_coupon (local.get $e2)) - (if (result externref) - (then - (call $is_equal (call $get_coupon_rhs (local.get $e1)) (call $get_coupon_lhs (local.get $e2))) - (if (result externref) - (then - (call $is_equal (local.get $lhs) (call $get_coupon_lhs (local.get $e1))) - (if (result externref) - (then - (call $is_equal (local.get $rhs) (call $get_coupon_rhs (local.get $e2))) - (if (result externref) - (then - (call $create_eq_coupon (local.get $lhs) (local.get $rhs)) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - ) - ) - (else - unreachable - ) - )) - (func $make_self_coupon (export "make_self_coupon") (param $lhs externref) (param $rhs externref) (result externref) - (call $is_equal (local.get $lhs) (local.get $rhs)) - (if (result externref) - (then - (call $create_eq_coupon (local.get $lhs) (local.get $rhs)) - ) - (else - unreachable - ) - )) - (table $dispatch_table funcref (elem (ref.func $make_eq_tree_coupon) - (ref.func $make_eq_application_coupon) - (ref.func $make_force_result_eq_coupon) - (ref.func $make_eq_encode_strict_coupon) - (ref.func $make_think_application_coupon) - (ref.func $make_think_to_force_coupon) - (ref.func $make_force_to_encode_strict_coupon) - (ref.func $make_eval_eq_coupon) - (ref.func $make_eval_blobobj_coupon) - (ref.func $make_eval_tree_coupon) - (ref.func $make_sym_coupon) - (ref.func $make_trans_coupon) - (ref.func $make_self_coupon))) - (func $make_coupon (export "make_coupon") (param $request i32) (param $lhs externref) (param $rhs externref) (result externref) - local.get $request - table.size $dispatch_table - i32.lt_u - if (result externref) - local.get $lhs - local.get $rhs - local.get $request - (call_indirect $dispatch_table (type $make_coupon_t)) - else - unreachable - end - ) - (func (export "_fixpoint_apply") (param $combination externref) (result externref) - ;; attach combination tree - (call $attach_tree - (i32.const 0) - (local.get $combination)) - ;; attach coupons - (call $attach_tree - (i32.const 2) - (table.get $encode (i32.const 2))) - ;; attach request field - (call $attach_blob - (i32.const 1) - (table.get $encode (i32.const 1))) - (call $make_coupon - (i32.load $mem_1 (i32.const 0)) - (table.get $encode (i32.const 3)) - (table.get $encode (i32.const 4)) - ) - ) - (export "coupons" (table $coupons)) -) diff --git a/fix/wasm/coupon/epilogue.wat b/fix/wasm/coupon/epilogue.wat new file mode 100644 index 00000000..4423ec41 --- /dev/null +++ b/fix/wasm/coupon/epilogue.wat @@ -0,0 +1,98 @@ + (func $is_coupon (param $tag externref) (param $type i32) (result i32) + (call $is_tag (local.get $tag)) + (if (result i32) + (then + ;; Attach the tag + (call $attach_tree (i32.const 1) (local.get $tag)) + ;; Check if the tag was authored by us + (call $is_equal (table.get $encode (i32.const 0)) (table.get $coupon_scratch (i32.const 0))) + (if (result i32) + (then + ;; Check if the coupon type matches the input type + (call $attach_blob (i32.const 1) (table.get $coupon_scratch (i32.const 1))) + (i32.load (memory $mem_1) (i32.const 0)) + (local.get $type) + i32.eq + (if (result i32) + (then (i32.const 1)) + (else (i32.const 0)) + ) + ) + (else (i32.const 0)) + ) + ) + (else (i32.const 0)) + ) + ) + (func $is_eq_coupon (param $tag externref) (result i32) + (call $is_coupon (local.get $tag) (global.get $Eq)) + ) + (func $is_eval_coupon (param $tag externref) (result i32) + (call $is_coupon (local.get $tag) (global.get $Eval)) + ) + (func $is_apply_coupon (param $tag externref) (result i32) + (call $is_coupon (local.get $tag) (global.get $Apply)) + ) + (func $is_force_coupon (param $tag externref) (result i32) + (call $is_coupon (local.get $tag) (global.get $Force)) + ) + (func $is_think_coupon (param $tag externref) (result i32) + (call $is_coupon (local.get $tag) (global.get $Think)) + ) + (func $is_storage_coupon (param $tag externref) (result i32) + (call $is_coupon (local.get $tag) (global.get $Storage)) + ) + (func $create_coupon (param $type i32) (param $lhs externref) (param $rhs externref) (result externref) + (table.set $output_coupon_scratch (i32.const 0) (table.get $encode (i32.const 0))) + (table.set $output_coupon_scratch (i32.const 1) (call $create_blob_i32 (local.get $type))) + (table.set $output_coupon_scratch (i32.const 2) (local.get $lhs)) + (table.set $output_coupon_scratch (i32.const 3) (local.get $rhs)) + (call $create_tag (i32.const 5)) + ) + (func $create_eq_coupon (param $lhs externref) (param $rhs externref) (result externref) + (call $create_coupon (global.get $Eq) (local.get $lhs) (local.get $rhs)) + ) + (func $create_eval_coupon (param $lhs externref) (param $rhs externref) (result externref) + (call $create_coupon (global.get $Eval) (local.get $lhs) (local.get $rhs)) + ) + (func $create_force_coupon (param $lhs externref) (param $rhs externref) (result externref) + (call $create_coupon (global.get $Force) (local.get $lhs) (local.get $rhs)) + ) + (func $create_think_coupon (param $lhs externref) (param $rhs externref) (result externref) + (call $create_coupon (global.get $Think) (local.get $lhs) (local.get $rhs)) + ) + (func $get_coupon_lhs (param $coupon externref) (result externref) + (call $attach_tree (i32.const 1) (local.get $coupon)) + (table.get $coupon_scratch (i32.const 2)) + ) + (func $get_coupon_rhs (param $coupon externref) (result externref) + (call $attach_tree (i32.const 1) (local.get $coupon)) + (table.get $coupon_scratch (i32.const 3)) + ) + (func $get_tree_size (param $t externref) (result i32) + (call $attach_tree (i32.const 3) (local.get $t)) + table.size $tree_scratch + ) + (func $get_tree_data (param $t externref) (param $i i32) (result externref) + (call $attach_tree (i32.const 3) (local.get $t)) + (table.get $tree_scratch (local.get $i)) + ) + (func (export "_fixpoint_apply") (param $combination externref) (result externref) + ;; attach combination tree + (call $attach_tree + (i32.const 0) + (local.get $combination)) + ;; attach coupons + (call $attach_tree + (i32.const 2) + (table.get $encode (i32.const 2))) + ;; attach request field + (call $attach_blob + (i32.const 1) + (table.get $encode (i32.const 1))) + (call $make_coupon + (i32.load $mem_1 (i32.const 0)) + (table.get $encode (i32.const 3)) + (table.get $encode (i32.const 4)) + ) + ) diff --git a/fix/wasm/coupon/fix-proof b/fix/wasm/coupon/fix-proof new file mode 160000 index 00000000..2f87b7f8 --- /dev/null +++ b/fix/wasm/coupon/fix-proof @@ -0,0 +1 @@ +Subproject commit 2f87b7f81d42037df7b570f156772aaced0af58d diff --git a/fix/wasm/coupon/prologue.wat b/fix/wasm/coupon/prologue.wat new file mode 100644 index 00000000..0c5cbe90 --- /dev/null +++ b/fix/wasm/coupon/prologue.wat @@ -0,0 +1,26 @@ +(module + (import "fixpoint" "is_equal" (func $is_equal (param externref) (param externref) (result i32))) + (import "fixpoint" "is_tag" (func $is_tag (param externref) (result i32))) + (import "fixpoint" "attach_blob" (func $attach_blob (param i32) (param externref))) + (import "fixpoint" "attach_tree" (func $attach_tree (param i32) (param externref))) + (import "fixpoint" "create_blob_i32" (func $create_blob_i32 (param i32) (result externref))) + (import "fixpoint" "create_tag" (func $create_tag (param i32) (result externref))) + (import "fixpoint" "create_application_thunk" (func $create_application_thunk (param externref) (result externref))) + (import "fixpoint" "create_strict_encode" (func $create_strict_encode (param externref) (result externref))) + (import "fixpoint" "create_shallow_encode" (func $create_shallow_encode (param externref) (result externref))) + (import "fixpoint" "is_blob_obj" (func $is_blob_obj (param externref) (result i32))) + (import "fixpoint" "is_data" (func $is_data (param externref) (result i32))) + (import "fixpoint" "is_object" (func $is_object (param externref) (result i32))) + (table $encode 0 externref) + (table $coupon_scratch 0 externref) + (table $coupons 0 externref) + (table $tree_scratch 0 externref) + (table $output_coupon_scratch 4 externref) + (memory $mem_0 0) + (memory $mem_1 0) + (global $Eq i32 (i32.const 0)) + (global $Eval i32 (i32.const 1)) + (global $Apply i32 (i32.const 2)) + (global $Force i32 (i32.const 3)) + (global $Think i32 (i32.const 4)) + (global $Storage i32 (i32.const 5)) diff --git a/fix/wasm/coupon/rewrite-wat.sh b/fix/wasm/coupon/rewrite-wat.sh new file mode 100755 index 00000000..09184a3f --- /dev/null +++ b/fix/wasm/coupon/rewrite-wat.sh @@ -0,0 +1,62 @@ +#!/usr/bin/bash + +if [[ $# -ne 4 ]]; then + echo "Usage: $0 ORIGINAL.wat PREAMBLE.wat EXTRA_FUNCS.wat OUTPUT.wat" >&2 + exit 1 +fi + +original=$1 +preamble=$2 +extra_funcs=$3 +output=$4 + +for file in "$original" "$preamble" "$extra_funcs"; do + if [[ ! -f "$file" ]]; then + echo "Error: file not found: $file" >&2 + exit 1 + fi +done + +tmp=$(mktemp) +trap 'rm -f "$tmp"' EXIT + +cat "$preamble" > "$tmp" + +awk ' + /^[[:space:]]*\(type([[:space:](]|$)/ { + found = 1 + } + + found { + lines[++count] = $0 + } + + END { + if (!found) { + print "Error: no type declaration found" > "/dev/stderr" + exit 1 + } + + # Find the last nonblank line, which should close the module. + last = count + while (last > 0 && lines[last] ~ /^[[:space:]]*$/) { + last-- + } + + if (last == 0 || lines[last] !~ /^[[:space:]]*\)[[:space:]]*$/) { + print "Error: module does not end with a standalone closing parenthesis" \ + > "/dev/stderr" + exit 1 + } + + # Print everything except the module closing parenthesis. + for (i = 1; i < last; i++) { + print lines[i] + } + } +' "$original" >> "$tmp" + +cat "$extra_funcs" >> "$tmp" +printf ')\n' >> "$tmp" + +mv "$tmp" "$output"