From bfc2bb5582ebe397b9da827d69c040221210a971 Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Tue, 28 Jul 2026 11:30:02 +0200 Subject: [PATCH] Changes --- specification/wasm-1.0/8-reduction.spectec | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/specification/wasm-1.0/8-reduction.spectec b/specification/wasm-1.0/8-reduction.spectec index 24ea82b09a..6b160730aa 100644 --- a/specification/wasm-1.0/8-reduction.spectec +++ b/specification/wasm-1.0/8-reduction.spectec @@ -8,12 +8,12 @@ relation Step_read: config ~> admininstr* hint(show "E") hint(tabular) relation Steps: config ~>* config hint(show "E") hint(tabular) rule Step/pure: - z; instr* ~> z; instr'* - -- Step_pure: instr* ~> instr'* + z; admininstr* ~> z; admininstr'* + -- Step_pure: admininstr* ~> admininstr'* rule Step/read: - z; instr* ~> z; instr'* - -- Step_read: z; instr* ~> instr'* + z; admininstr* ~> z; admininstr'* + -- Step_read: z; admininstr* ~> admininstr'* rule Steps/refl: z; admininstr* ~>* z; admininstr* @@ -155,13 +155,17 @@ rule Step_pure/trap-frame: ;; Context rule Step/ctxt-label: - z; (LABEL_ n `{instr_0*} instr*) ~> z'; (LABEL_ n `{instr_0*} instr'*) - -- Step: z; instr* ~> z'; instr'* + z; (LABEL_ n `{instr_0*} admininstr*) ~> z'; (LABEL_ n `{instr_0*} admininstr'*) + -- Step: z; admininstr* ~> z'; admininstr'* rule Step/ctxt-frame: - s; f; (FRAME_ n `{f'} instr*) ~> s'; f; (FRAME_ n `{f'} instr'*) - -- Step: s; f'; instr* ~> s'; f'; instr'* + s; f; (FRAME_ n `{f'} admininstr*) ~> s'; f; (FRAME_ n `{f''} admininstr'*) + -- Step: s; f'; admininstr* ~> s'; f''; admininstr'* +rule Step/ctxt-instrs: + z; val* admininstr* admininstr_1* ~> z'; val* admininstr'* admininstr_1* + -- Step: z; admininstr* ~> z'; admininstr'* + -- if val* =/= eps \/ admininstr_1* =/= eps ;; Numeric instructions