Vector: Remove now unnecessary uses of undefined

Sail 0.18 contains the vector_init primitive, to make initialising
vectors with defined values easier. We can use this in some places
where the vector code was creating an uninitalised vector, only to
then initialize it later.

Second, we can remove some uses of undefined by refactoring slightly
how init_masked_result is used, which has the added benefit of making
mask immutable.

Some additional constraints need to be added to use the vector_init
primitive.

Sail's pattern completeness checker is now smarter than before, so
some wildcard cases can also be safely removed.

8 files changed, 196 insertions, 270 deletions

diff --git a/model/prelude.sail b/model/prelude.sail
index 34ff30e..67855c5 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -47,6 +47,8 @@ val sub_vec_int = pure {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits(
 
 overload operator - = {sub_vec, sub_vec_int}
 
+val quot_positive_round_zero = pure {interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int", coq: "Z.quot"} : forall 'n 'm, 'n >= 0 & 'm > 0. (int('n), int('m)) -> int(div('n, 'm))
+
 val quot_round_zero = pure {interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int
 val rem_round_zero = pure {interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int
 
@@ -196,7 +198,7 @@ function reverse_bits_in_byte (xs : bits(8)) -> bits(8) = {
 
 overload reverse = {reverse_bits_in_byte}
 
-overload operator / = {quot_round_zero}
+overload operator / = {quot_positive_round_zero, quot_round_zero}
 overload operator * = {mult_atom, mult_int}
 
 /* helper for vector extension
diff --git a/model/riscv_insts_vext_arith.sail b/model/riscv_insts_vext_arith.sail
index b832dcf..1654f65 100644
--- a/model/riscv_insts_vext_arith.sail
+++ b/model/riscv_insts_vext_arith.sail
@@ -59,10 +59,9 @@ function clause execute(VVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -196,10 +195,9 @@ function clause execute(NVSTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   assert(SEW_widen <= 64);
   foreach (i from 0 to (num_elem - 1)) {
@@ -263,10 +261,9 @@ function clause execute(NVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   assert(SEW_widen <= 64);
   foreach (i from 0 to (num_elem - 1)) {
@@ -323,7 +320,7 @@ function clause execute(MASKTYPEV(vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
+  var result  : vector('n, dec, bits('m)) = vector_init(zeros());
 
   let tail_ag : agtype = get_vtype_vta();
   foreach (i from 0 to (num_elem - 1)) {
@@ -367,10 +364,9 @@ function clause execute(MOVETYPEV(vs1, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b1, 0b00000);
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then result[i] = vs1_val[i]
@@ -427,10 +423,9 @@ function clause execute(VXTYPE(funct6, vm, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -548,10 +543,9 @@ function clause execute(NXSTYPE(funct6, vm, vs2, rs1, vd)) = {
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   assert(SEW_widen <= 64);
   foreach (i from 0 to (num_elem - 1)) {
@@ -615,10 +609,9 @@ function clause execute(NXTYPE(funct6, vm, vs2, rs1, vd)) = {
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   assert(SEW_widen <= 64);
   foreach (i from 0 to (num_elem - 1)) {
@@ -681,10 +674,9 @@ function clause execute(VXSG(funct6, vm, vs2, rs1, vd)) = {
   let rs1_val : nat                       = unsigned(X(rs1));
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -745,7 +737,7 @@ function clause execute(MASKTYPEX(vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
+  var result  : vector('n, dec, bits('m)) = vector_init(zeros());
 
   let tail_ag : agtype = get_vtype_vta();
   foreach (i from 0 to (num_elem - 1)) {
@@ -789,10 +781,9 @@ function clause execute(MOVETYPEX(rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar(rs1, 'm);
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b1, 0b00000);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then result[i] = rs1_val
@@ -841,10 +832,9 @@ function clause execute(VITYPE(funct6, vm, vs2, simm, vd)) = {
   let imm_val : bits('m)                  = sign_extend(simm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -938,10 +928,9 @@ function clause execute(NISTYPE(funct6, vm, vs2, simm, vd)) = {
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
   let imm_val : bits('m)                  = sign_extend(simm);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   assert(SEW_widen <= 64);
   foreach (i from 0 to (num_elem - 1)) {
@@ -1005,10 +994,9 @@ function clause execute(NITYPE(funct6, vm, vs2, simm, vd)) = {
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
   let imm_val : bits('m)                  = sign_extend(simm);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   assert(SEW_widen <= 64);
   foreach (i from 0 to (num_elem - 1)) {
@@ -1071,10 +1059,9 @@ function clause execute(VISG(funct6, vm, vs2, simm, vd)) = {
   let imm_val : nat                       = unsigned(zero_extend(sizeof(xlen), simm));
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -1135,7 +1122,7 @@ function clause execute(MASKTYPEI(vs2, simm, vd)) = {
   let imm_val : bits('m)                  = sign_extend(simm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
+  var result  : vector('n, dec, bits('m)) = vector_init(zeros());
 
   let tail_ag : agtype = get_vtype_vta();
   foreach (i from 0 to (num_elem - 1)) {
@@ -1179,10 +1166,9 @@ function clause execute(MOVETYPEI(vd, simm)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b1, 0b00000);
   let imm_val : bits('m)                  = sign_extend(simm);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then result[i] = imm_val
@@ -1218,7 +1204,7 @@ function clause execute(VMVRTYPE(vs2, simm, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b1, 0b00000);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, EMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, EMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
+  var result  : vector('n, dec, bits('m)) = vector_init(zeros());
 
   foreach (i from 0 to (num_elem - 1)) {
     result[i] = if i < start_element then vd_val[i] else vs2_val[i]
@@ -1274,10 +1260,9 @@ function clause execute(MVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -1383,10 +1368,9 @@ function clause execute(MVVMATYPE(funct6, vm, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -1449,10 +1433,9 @@ function clause execute(WVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
-  var result  : vector('n, dec, bits('o)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -1518,10 +1501,9 @@ function clause execute(WVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  var result  : vector('n, dec, bits('o)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -1582,10 +1564,9 @@ function clause execute(WMVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
-  var result  : vector('n, dec, bits('o)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -1641,12 +1622,10 @@ function clause execute(VEXT2TYPE(funct6, vm, vs2, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, 0b00000);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_half, LMUL_pow_half, vs2);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
-  assert(SEW > SEW_half);
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
       result[i] = match funct6 {
@@ -1699,12 +1678,10 @@ function clause execute(VEXT4TYPE(funct6, vm, vs2, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, 0b00000);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_quart, LMUL_pow_quart, vs2);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
-  assert(SEW > SEW_quart);
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
       result[i] = match funct6 {
@@ -1757,10 +1734,9 @@ function clause execute(VEXT8TYPE(funct6, vm, vs2, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, 0b00000);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_eighth, LMUL_pow_eighth, vs2);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   assert(SEW > SEW_eighth);
   foreach (i from 0 to (num_elem - 1)) {
@@ -1836,7 +1812,7 @@ function clause execute(MVVCOMPRESS(vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
+  var result  : vector('n, dec, bits('m)) = vector_init(zeros());
 
   /* body elements */
   var vd_idx : nat = 0;
@@ -1907,10 +1883,9 @@ function clause execute(MVXTYPE(funct6, vm, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -2027,10 +2002,9 @@ function clause execute(MVXMATYPE(funct6, vm, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -2093,10 +2067,9 @@ function clause execute(WVXTYPE(funct6, vm, vs2, rs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
-  var result  : vector('n, dec, bits('o)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -2161,10 +2134,9 @@ function clause execute(WXTYPE(funct6, vm, vs2, rs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  var result  : vector('n, dec, bits('o)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -2225,10 +2197,9 @@ function clause execute(WMVXTYPE(funct6, vm, vs2, rs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
-  var result  : vector('n, dec, bits('o)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -2275,10 +2246,9 @@ function clause execute(VMVSX(rs1, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b1, 0b00000);
   let rs1_val : bits('m)                  = get_scalar(rs1, 'm);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, 0, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, 0, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, 0, vd_val, vm_val);
+  var result = initial_result;
 
   /* one body element */
   if mask[0] then result[0] = rs1_val;
diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail
index 83006d1..72bdca2 100755
--- a/model/riscv_insts_vext_fp.sail
+++ b/model/riscv_insts_vext_fp.sail
@@ -46,10 +46,9 @@ function clause execute(FVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -121,10 +120,9 @@ function clause execute(FVVMATYPE(funct6, vm, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -194,10 +192,9 @@ function clause execute(FWVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
-  var result  : vector('n, dec, bits('o)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -259,10 +256,9 @@ function clause execute(FWVVMATYPE(funct6, vm, vs1, vs2, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
-  var result  : vector('n, dec, bits('o)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -322,10 +318,9 @@ function clause execute(FWVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  var result  : vector('n, dec, bits('o)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -379,10 +374,9 @@ function clause execute(VFUNARY0(vm, vs2, vfunary0, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -498,10 +492,9 @@ function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
-  var result  : vector('n, dec, bits('o)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -628,10 +621,9 @@ function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -759,10 +751,9 @@ function clause execute(VFUNARY1(vm, vs2, vfunary1, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -884,10 +875,9 @@ function clause execute(FVFTYPE(funct6, vm, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar_fp(rs1, 'm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -974,10 +964,9 @@ function clause execute(FVFMATYPE(funct6, vm, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar_fp(rs1, 'm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -1046,10 +1035,9 @@ function clause execute(FWVFTYPE(funct6, vm, vs2, rs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let rs1_val : bits('m)                  = get_scalar_fp(rs1, 'm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
-  var result  : vector('n, dec, bits('o)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -1110,10 +1098,9 @@ function clause execute(FWVFMATYPE(funct6, vm, rs1, vs2, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let rs1_val : bits('m)                  = get_scalar_fp(rs1, 'm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
-  var result  : vector('n, dec, bits('o)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -1172,10 +1159,9 @@ function clause execute(FWFTYPE(funct6, vm, vs2, rs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let rs1_val : bits('m)                  = get_scalar_fp(rs1, 'm);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  var result  : vector('n, dec, bits('o)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -1225,7 +1211,7 @@ function clause execute(VFMERGE(vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar_fp(rs1, 'm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
+  var result  : vector('n, dec, bits('m)) = vector_init(zeros());
 
   let tail_ag : agtype = get_vtype_vta();
   foreach (i from 0 to (num_elem - 1)) {
@@ -1272,10 +1258,9 @@ function clause execute(VFMV(rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar_fp(rs1, 'm);
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b1, 0b00000);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then result[i] = rs1_val
@@ -1309,10 +1294,9 @@ function clause execute(VFMVSF(rs1, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b1, 0b00000);
   let rs1_val : bits('m)                  = get_scalar_fp(rs1, 'm);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, 0, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, 0, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, 0, vd_val, vm_val);
+  var result = initial_result;
 
   /* one body element */
   if mask[0] then result[0] = rs1_val;
diff --git a/model/riscv_insts_vext_fp_vm.sail b/model/riscv_insts_vext_fp_vm.sail
index 1914ed7..6d578fa 100755
--- a/model/riscv_insts_vext_fp_vm.sail
+++ b/model/riscv_insts_vext_fp_vm.sail
@@ -41,10 +41,9 @@ function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  var result  : vector('n, dec, bool)     = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -105,10 +104,9 @@ function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar_fp(rs1, 'm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  var result  : vector('n, dec, bool)     = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
diff --git a/model/riscv_insts_vext_mask.sail b/model/riscv_insts_vext_mask.sail
index 9c536bb..432ac81 100755
--- a/model/riscv_insts_vext_mask.sail
+++ b/model/riscv_insts_vext_mask.sail
@@ -41,10 +41,9 @@ function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs1);
   let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
   let vd_val  : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd);
-  var result  : vector('n, dec, bool) = undefined;
-  var mask    : vector('n, dec, bool) = undefined;
 
-  (result, mask) = init_masked_result_carry(num_elem, SEW, 0, vd_val);
+  let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, 0, vd_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -98,10 +97,9 @@ function clause execute(VCPOP_M(vm, vs2, rd)) = {
 
   let vm_val  : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
-  var result  : vector('n, dec, bool) = undefined;
-  var mask    : vector('n, dec, bool) = undefined;
 
-  (result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val);
+  let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val);
+  var result = initial_result;
 
   var count : nat = 0;
   foreach (i from 0 to (num_elem - 1)) {
@@ -134,10 +132,9 @@ function clause execute(VFIRST_M(vm, vs2, rd)) = {
 
   let vm_val  : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
-  var result  : vector('n, dec, bool) = undefined;
-  var mask    : vector('n, dec, bool) = undefined;
 
-  (result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val);
+  let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val);
+  var result = initial_result;
 
   var index : int = -1;
   foreach (i from 0 to (num_elem - 1)) {
@@ -174,10 +171,9 @@ function clause execute(VMSBF_M(vm, vs2, vd)) = {
   let vm_val  : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
   let vd_val  : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd);
-  var result  : vector('n, dec, bool) = undefined;
-  var mask    : vector('n, dec, bool) = undefined;
 
-  (result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val);
+  var result = initial_result;
 
   var found_elem : bool = false;
   foreach (i from 0 to (num_elem - 1)) {
@@ -215,10 +211,9 @@ function clause execute(VMSIF_M(vm, vs2, vd)) = {
   let vm_val  : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
   let vd_val  : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd);
-  var result  : vector('n, dec, bool) = undefined;
-  var mask    : vector('n, dec, bool) = undefined;
 
-  (result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val);
+  var result = initial_result;
 
   var found_elem : bool = false;
   foreach (i from 0 to (num_elem - 1)) {
@@ -256,10 +251,9 @@ function clause execute(VMSOF_M(vm, vs2, vd)) = {
   let vm_val  : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
   let vd_val  : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd);
-  var result  : vector('n, dec, bool) = undefined;
-  var mask    : vector('n, dec, bool) = undefined;
 
-  (result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val);
+  var result = initial_result;
 
   var found_elem : bool = false;
   foreach (i from 0 to (num_elem - 1)) {
@@ -301,10 +295,9 @@ function clause execute(VIOTA_M(vm, vs2, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   var sum : int = 0;
   foreach (i from 0 to (num_elem - 1)) {
@@ -340,10 +333,9 @@ function clause execute(VID_V(vm, vd)) = {
 
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, 0b00000);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then result[i] = to_bits(SEW, i)
diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail
index 87cb386..eeec681 100755
--- a/model/riscv_insts_vext_utils.sail
+++ b/model/riscv_insts_vext_utils.sail
@@ -199,7 +199,7 @@ function get_end_element() = unsigned(vl) - 1
  *   vector2 is a "mask" vector that is true for an element if the corresponding element
  *     in the result vector should be updated by the calling instruction
  */
-val init_masked_result : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), vector('n, dec, bits('m)), vector('n, dec, bool)) -> (vector('n, dec, bits('m)), vector('n, dec, bool))
+val init_masked_result : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), vector('n, dec, bits('m)), vector('n, dec, bool)) -> (vector('n, dec, bits('m)), vector('n, dec, bool))
 function init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) = {
   let start_element = get_start_element();
   let end_element   = get_end_element();
diff --git a/model/riscv_insts_vext_vm.sail b/model/riscv_insts_vext_vm.sail
index e524b75..93ad7e7 100755
--- a/model/riscv_insts_vext_vm.sail
+++ b/model/riscv_insts_vext_vm.sail
@@ -39,10 +39,9 @@ function clause execute(VVMTYPE(funct6, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  var result  : vector('n, dec, bool)     = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
+  let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -94,10 +93,9 @@ function clause execute(VVMCTYPE(funct6, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  var result  : vector('n, dec, bool)     = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
+  let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -156,10 +154,9 @@ function clause execute(VVMSTYPE(funct6, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -213,10 +210,9 @@ function clause execute(VVCMPTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  var result  : vector('n, dec, bool)     = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -277,10 +273,9 @@ function clause execute(VXMTYPE(funct6, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  var result  : vector('n, dec, bool)     = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
+  let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -332,10 +327,9 @@ function clause execute(VXMCTYPE(funct6, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  var result  : vector('n, dec, bool)     = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
+  let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -394,10 +388,9 @@ function clause execute(VXMSTYPE(funct6, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -453,10 +446,9 @@ function clause execute(VXCMPTYPE(funct6, vm, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  var result  : vector('n, dec, bool)     = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -520,10 +512,9 @@ function clause execute(VIMTYPE(funct6, vs2, simm, vd)) = {
   let imm_val : bits('m)                  = sign_extend(simm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  var result  : vector('n, dec, bool)     = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
+  let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -572,10 +563,9 @@ function clause execute(VIMCTYPE(funct6, vs2, simm, vd)) = {
   let imm_val : bits('m)                  = sign_extend(simm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  var result  : vector('n, dec, bool)     = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
+  let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -631,10 +621,9 @@ function clause execute(VIMSTYPE(funct6, vs2, simm, vd)) = {
   let imm_val : bits('m)                  = sign_extend(simm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  var result  : vector('n, dec, bits('m)) = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues);
+  let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
@@ -686,10 +675,9 @@ function clause execute(VICMPTYPE(funct6, vm, vs2, simm, vd)) = {
   let imm_val : bits('m)                  = sign_extend(simm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  var result  : vector('n, dec, bool)     = undefined;
-  var mask    : vector('n, dec, bool)     = undefined;
 
-  (result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+  var result = initial_result;
 
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail
index 377d92d..f823155 100644
--- a/model/riscv_vext_regs.sail
+++ b/model/riscv_vext_regs.sail
@@ -87,48 +87,43 @@ function dirty_v_context_if_present() -> unit = {
 }
 
 function rV (r : regno) -> vregtype = {
-  let zero_vreg : vregtype = zeros();
-  let v : vregtype =
-    match r {
-      0 => vr0,
-      1 => vr1,
-      2 => vr2,
-      3 => vr3,
-      4 => vr4,
-      5 => vr5,
-      6 => vr6,
-      7 => vr7,
-      8 => vr8,
-      9 => vr9,
-      10 => vr10,
-      11 => vr11,
-      12 => vr12,
-      13 => vr13,
-      14 => vr14,
-      15 => vr15,
-      16 => vr16,
-      17 => vr17,
-      18 => vr18,
-      19 => vr19,
-      20 => vr20,
-      21 => vr21,
-      22 => vr22,
-      23 => vr23,
-      24 => vr24,
-      25 => vr25,
-      26 => vr26,
-      27 => vr27,
-      28 => vr28,
-      29 => vr29,
-      30 => vr30,
-      31 => vr31,
-      _  => {assert(false, "invalid vector register number"); zero_vreg}
-    };
-    v
+  match r {
+    0 => vr0,
+    1 => vr1,
+    2 => vr2,
+    3 => vr3,
+    4 => vr4,
+    5 => vr5,
+    6 => vr6,
+    7 => vr7,
+    8 => vr8,
+    9 => vr9,
+    10 => vr10,
+    11 => vr11,
+    12 => vr12,
+    13 => vr13,
+    14 => vr14,
+    15 => vr15,
+    16 => vr16,
+    17 => vr17,
+    18 => vr18,
+    19 => vr19,
+    20 => vr20,
+    21 => vr21,
+    22 => vr22,
+    23 => vr23,
+    24 => vr24,
+    25 => vr25,
+    26 => vr26,
+    27 => vr27,
+    28 => vr28,
+    29 => vr29,
+    30 => vr30,
+    31 => vr31,
+  }
 }
 
-function wV (r : regno, in_v : vregtype) -> unit = {
-  let v = in_v;
+function wV (r : regno, v : vregtype) -> unit = {
   match r {
     0 => vr0 = v,
     1 => vr1 = v,
@@ -162,7 +157,6 @@ function wV (r : regno, in_v : vregtype) -> unit = {
     29 => vr29 = v,
     30 => vr30 = v,
     31 => vr31 = v,
-    _ => assert(false, "invalid vector register number")
   };
 
   dirty_v_context();
@@ -245,10 +239,10 @@ function get_num_elem(LMUL_pow, SEW) = {
 }
 
 /* Reads a single vreg into multiple elements */
-val read_single_vreg : forall 'n 'm, 'n >= 0. (int('n), int('m), regidx) -> vector('n, dec, bits('m))
+val read_single_vreg : forall 'n 'm, 'n >= 0 & 'm >= 0. (int('n), int('m), regidx) -> vector('n, dec, bits('m))
 function read_single_vreg(num_elem, SEW, vrid) = {
   let bv     : vregtype                  = V(vrid);
-  var result : vector('n, dec, bits('m)) = undefined;
+  var result : vector('n, dec, bits('m)) = vector_init(zeros());
 
   assert(8 <= SEW & SEW <= 64);
   foreach (i from 0 to (num_elem - 1)) {
@@ -274,9 +268,9 @@ function write_single_vreg(num_elem, SEW, vrid, v) = {
 }
 
 /* The general vreg reading operation with num_elem as max(VLMAX,VLEN/SEW)) */
-val read_vreg : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), regidx) -> vector('n, dec, bits('m))
+val read_vreg : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), regidx) -> vector('n, dec, bits('m))
 function read_vreg(num_elem, SEW, LMUL_pow, vrid) = {
-  var result : vector('n, dec, bits('m)) = undefined;
+  var result : vector('n, dec, bits('m)) = vector_init(zeros());
   let VLEN = unsigned(vlenb) * 8;
   let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow;
 
@@ -326,7 +320,7 @@ function read_single_element(EEW, index, vrid) = {
 }
 
 /* The general vreg writing operation with num_elem as max(VLMAX,VLEN/SEW)) */
-val write_vreg : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), regidx, vector('n, dec, bits('m))) -> unit
+val write_vreg : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), regidx, vector('n, dec, bits('m))) -> unit
 function write_vreg(num_elem, SEW, LMUL_pow, vrid, vec) = {
   let VLEN = unsigned(vlenb) * 8;
   let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow;
@@ -334,7 +328,7 @@ function write_vreg(num_elem, SEW, LMUL_pow, vrid, vec) = {
   let 'num_elem_single  : int = VLEN / SEW;
   assert('num_elem_single >= 0);
   foreach (i_lmul from 0 to (2 ^ LMUL_pow_reg - 1)) {
-    var single_vec : vector('num_elem_single, dec, bits('m)) = undefined;
+    var single_vec : vector('num_elem_single, dec, bits('m)) = vector_init(zeros());
     let vrid_lmul  : regidx = vrid + to_bits(5, i_lmul);
     let r_start_i  : int = i_lmul * 'num_elem_single;
     let r_end_i    : int = r_start_i + 'num_elem_single - 1;
@@ -373,17 +367,16 @@ function write_single_element(EEW, index, vrid, value) = {
 /* Mask register reading operation with num_elem as max(VLMAX,VLEN/SEW)) */
 val read_vmask : forall 'n, 'n >= 0. (int('n), bits(1), regidx) -> vector('n, dec, bool)
 function read_vmask(num_elem, vm, vrid) = {
-  let VLEN = unsigned(vlenb) * 8;
   assert(num_elem <= sizeof(vlenmax));
   let vreg_val : vregtype = V(vrid);
-  var result   : vector('n, dec, bool) = undefined;
+  var result   : vector('n, dec, bool) = vector_init(true);
+
+  if vm == 0b1 then {
+    return result
+  };
 
   foreach (i from 0 to (num_elem - 1)) {
-    if vm == 0b1 then {
-      result[i] = true
-    } else {
-      result[i] = bit_to_bool(vreg_val[i])
-    }
+    result[i] = bit_to_bool(vreg_val[i])
   };
 
   result
@@ -392,17 +385,16 @@ function read_vmask(num_elem, vm, vrid) = {
 /* This is a special version of read_vmask for carry/borrow instructions, where vm=1 means no carry */
 val read_vmask_carry : forall 'n, 'n >= 0. (int('n), bits(1), regidx) -> vector('n, dec, bool)
 function read_vmask_carry(num_elem, vm, vrid) = {
-  let VLEN = unsigned(vlenb) * 8;
-  assert(0 < num_elem & num_elem <= sizeof(vlenmax));
+  assert(num_elem <= sizeof(vlenmax));
   let vreg_val : vregtype = V(vrid);
-  var result   : vector('n, dec, bool) = undefined;
+  var result   : vector('n, dec, bool) = vector_init(false);
+
+  if vm == 0b1 then {
+    return result
+  };
 
   foreach (i from 0 to (num_elem - 1)) {
-    if vm == 0b1 then {
-      result[i] = false
-    } else {
-      result[i] = bit_to_bool(vreg_val[i])
-    }
+    result[i] = bit_to_bool(vreg_val[i])
   };
 
   result