From 37f943d7f78603a4612e27926c1524141fc4ad78 Mon Sep 17 00:00:00 2001 From: Yoshihiro Imai Date: Tue, 24 Mar 2026 12:47:19 +0900 Subject: [PATCH 1/3] feat: :sparkles: :memo: Generate the Theorems for the Verification of Target WASM code --- core/wasm-to-v/src/translator.rs | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/core/wasm-to-v/src/translator.rs b/core/wasm-to-v/src/translator.rs index e242eef0..d4cd0b5f 100644 --- a/core/wasm-to-v/src/translator.rs +++ b/core/wasm-to-v/src/translator.rs @@ -308,7 +308,7 @@ impl WasmParseData<'_> { res.push_str("Require Import ZArith.\n"); res.push_str("From Wasm Require Import bytes.\n"); res.push_str("From Wasm Require Import numerics.\n"); - res.push_str("From Wasm Require Import datatypes.\n"); + res.push_str("From Wasm Require Import datatypes verifier.\n"); res.push('\n'); res.push_str("Definition Vi32 i := VAL_int32 (Wasm_int.int_of_Z i32m i).\n"); res.push_str("Definition Vi64 i := VAL_int64 (Wasm_int.int_of_Z i64m i).\n"); @@ -500,6 +500,14 @@ impl WasmParseData<'_> { res.push_str(format!(" mod_imports :=\n{translated_imports};\n").as_str()); res.push_str(format!(" mod_exports :=\n{created_exports};\n").as_str()); res.push_str(RCB_DOT); + + // Generate Theorems + res.push('\n'); + res.push_str("(* Theorems *)\n"); + res.push_str(format!"Theorem valid_{module_name} : ValidModule {module_name}.\n").as_str()); + res.push_str("Proof.\n"); + res.push_str(" (* TODO: fill the proof *)\n"); + res.push_str("Qed.\n"); Ok(res) } From 85c1067f426f359ab691cd25ac9161e4c782842b Mon Sep 17 00:00:00 2001 From: Georgii Plotnikov Date: Tue, 24 Mar 2026 11:08:27 +0500 Subject: [PATCH 2/3] Update core/wasm-to-v/src/translator.rs Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> Signed-off-by: Georgii Plotnikov --- core/wasm-to-v/src/translator.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/core/wasm-to-v/src/translator.rs b/core/wasm-to-v/src/translator.rs index d4cd0b5f..8ef3b591 100644 --- a/core/wasm-to-v/src/translator.rs +++ b/core/wasm-to-v/src/translator.rs @@ -504,7 +504,7 @@ impl WasmParseData<'_> { // Generate Theorems res.push('\n'); res.push_str("(* Theorems *)\n"); - res.push_str(format!"Theorem valid_{module_name} : ValidModule {module_name}.\n").as_str()); + res.push_str(format!("Theorem valid_{module_name} : ValidModule {module_name}.\n").as_str()); res.push_str("Proof.\n"); res.push_str(" (* TODO: fill the proof *)\n"); res.push_str("Qed.\n"); From 9f452bec291d83472570a80fed62e1472f5f332e Mon Sep 17 00:00:00 2001 From: Yoshihiro Imai Date: Mon, 11 May 2026 21:31:22 +0900 Subject: [PATCH 3/3] feat: introduce a section --- core/wasm-to-v/src/translator.rs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/core/wasm-to-v/src/translator.rs b/core/wasm-to-v/src/translator.rs index 8ef3b591..b4f9510e 100644 --- a/core/wasm-to-v/src/translator.rs +++ b/core/wasm-to-v/src/translator.rs @@ -503,11 +503,16 @@ impl WasmParseData<'_> { // Generate Theorems res.push('\n'); + res.push_str("Section Host.\n"); + res.push_str("Context `{ho: host}.\n"); + res.push('\n'); res.push_str("(* Theorems *)\n"); res.push_str(format!("Theorem valid_{module_name} : ValidModule {module_name}.\n").as_str()); res.push_str("Proof.\n"); res.push_str(" (* TODO: fill the proof *)\n"); res.push_str("Qed.\n"); + res.push('\n'); + res.push_str("End Host.\n"); Ok(res) }