Add some missing explicit var declarations

Implicit `var` declarations will eventually be an error. This makes some implicit `var` declarations explicit.

model/riscv_insts_zbb.sail

@@ -184,7 +184,7 @@ mapping clause assembly = RISCV_REV8(rs1, rd)
 
 function clause execute (RISCV_REV8(rs1, rd)) = {
   let rs1_val = X(rs1);
-  result : xlenbits = zeros();
+  var result : xlenbits = zeros();
   foreach (i from 0 to (sizeof(xlen) - 8) by 8)
     result[(i + 7) .. i] = rs1_val[(sizeof(xlen) - i - 1) .. (sizeof(xlen) - i - 8)];
   X(rd) = result;
@@ -202,7 +202,7 @@ mapping clause assembly = RISCV_ORCB(rs1, rd)
 
 function clause execute (RISCV_ORCB(rs1, rd)) = {
   let rs1_val = X(rs1);
-  result : xlenbits = zeros();
+  var result : xlenbits = zeros();
   foreach (i from 0 to (sizeof(xlen) - 8) by 8)
     result[(i + 7) .. i] = if rs1_val[(i + 7) .. i] == zeros()
                            then 0x00
@@ -222,7 +222,7 @@ mapping clause assembly = RISCV_CPOP(rs1, rd)
 
 function clause execute (RISCV_CPOP(rs1, rd)) = {
   let rs1_val = X(rs1);
-  result : nat = 0;
+  var result : nat = 0;
   foreach (i from 0 to (xlen_val - 1))
     if rs1_val[i] == bitone then result = result + 1;
   X(rd) = to_bits(sizeof(xlen), result);
@@ -240,7 +240,7 @@ mapping clause assembly = RISCV_CPOPW(rs1, rd)
 
 function clause execute (RISCV_CPOPW(rs1, rd)) = {
   let rs1_val = X(rs1);
-  result : nat = 0;
+  var result : nat = 0;
   foreach (i from 0 to 31)
     if rs1_val[i] == bitone then result = result + 1;
   X(rd) = to_bits(sizeof(xlen), result);
@@ -258,8 +258,8 @@ mapping clause assembly = RISCV_CLZ(rs1, rd)
 
 function clause execute (RISCV_CLZ(rs1, rd)) = {
   let rs1_val = X(rs1);
-  result : nat = 0;
-  done : bool = false;
+  var result : nat = 0;
+  var done : bool = false;
   foreach (i from (sizeof(xlen) - 1) downto 0)
     if not(done) then if rs1_val[i] == bitzero
                     then result = result + 1
@@ -279,8 +279,8 @@ mapping clause assembly = RISCV_CLZW(rs1, rd)
 
 function clause execute (RISCV_CLZW(rs1, rd)) = {
   let rs1_val = X(rs1);
-  result : nat = 0;
-  done : bool = false;
+  var result : nat = 0;
+  var done : bool = false;
   foreach (i from 31 downto 0)
     if not(done) then if rs1_val[i] == bitzero
                     then result = result + 1
@@ -300,8 +300,8 @@ mapping clause assembly = RISCV_CTZ(rs1, rd)
 
 function clause execute (RISCV_CTZ(rs1, rd)) = {
   let rs1_val = X(rs1);
-  result : nat = 0;
-  done : bool = false;
+  var result : nat = 0;
+  var done : bool = false;
   foreach (i from 0 to (sizeof(xlen) - 1))
     if not(done) then if rs1_val[i] == bitzero
                     then result = result + 1
@@ -321,8 +321,8 @@ mapping clause assembly = RISCV_CTZW(rs1, rd)
 
 function clause execute (RISCV_CTZW(rs1, rd)) = {
   let rs1_val = X(rs1);
-  result : nat = 0;
-  done : bool = false;
+  var result : nat = 0;
+  var done : bool = false;
   foreach (i from 0 to 31)
     if not(done) then if rs1_val[i] == bitzero
                     then result = result + 1

model/riscv_insts_zbc.sail

@@ -18,7 +18,7 @@ mapping clause assembly = RISCV_CLMUL(rs2, rs1, rd)
 function clause execute (RISCV_CLMUL(rs2, rs1, rd)) = {
   let rs1_val = X(rs1);
   let rs2_val = X(rs2);
-  result : xlenbits = zeros();
+  var result : xlenbits = zeros();
   foreach (i from 0 to (xlen_val - 1))
     if rs2_val[i] == bitone then result = result ^ (rs1_val << i);
   X(rd) = result;
@@ -37,7 +37,7 @@ mapping clause assembly = RISCV_CLMULH(rs2, rs1, rd)
 function clause execute (RISCV_CLMULH(rs2, rs1, rd)) = {
   let rs1_val = X(rs1);
   let rs2_val = X(rs2);
-  result : xlenbits = zeros();
+  var result : xlenbits = zeros();
   foreach (i from 0 to (xlen_val - 1))
     if rs2_val[i] == bitone then result = result ^ (rs1_val >> (xlen_val - i));
   X(rd) = result;
@@ -56,7 +56,7 @@ mapping clause assembly = RISCV_CLMULR(rs2, rs1, rd)
 function clause execute (RISCV_CLMULR(rs2, rs1, rd)) = {
   let rs1_val = X(rs1);
   let rs2_val = X(rs2);
-  result : xlenbits = zeros();
+  var result : xlenbits = zeros();
   foreach (i from 0 to (xlen_val - 1))
     if rs2_val[i] == bitone then result = result ^ (rs1_val >> (xlen_val - i - 1));
   X(rd) = result;

model/riscv_insts_zbkb.sail

@@ -64,7 +64,7 @@ mapping clause assembly = RISCV_ZIP(rs1, rd)
 function clause execute (RISCV_ZIP(rs1, rd)) = {
   assert(sizeof(xlen) == 32);
   let rs1_val = X(rs1);
-  result : xlenbits = zeros();
+  var result : xlenbits = zeros();
   foreach (i from 0 to (sizeof(xlen_bytes)*4 - 1)) {
     result[i*2] = rs1_val[i];
     result[i*2 + 1] = rs1_val[i + sizeof(xlen_bytes)*4];
@@ -85,7 +85,7 @@ mapping clause assembly = RISCV_UNZIP(rs1, rd)
 function clause execute (RISCV_UNZIP(rs1, rd)) = {
   assert(sizeof(xlen) == 32);
   let rs1_val = X(rs1);
-  result : xlenbits = zeros();
+  var result : xlenbits = zeros();
   foreach (i from 0 to (sizeof(xlen_bytes)*4 - 1)) {
     result[i] = rs1_val[i*2];
     result[i + sizeof(xlen_bytes)*4] = rs1_val[i*2 + 1];
@@ -105,7 +105,7 @@ mapping clause assembly = RISCV_BREV8(rs1, rd)
 
 function clause execute (RISCV_BREV8(rs1, rd)) = {
   let rs1_val = X(rs1);
-  result : xlenbits = zeros();
+  var result : xlenbits = zeros();
   foreach (i from 0 to (sizeof(xlen) - 8) by 8)
     result[i+7..i] = reverse(rs1_val[i+7..i]);
   X(rd) = result;

model/riscv_insts_zbkx.sail

@@ -18,7 +18,7 @@ mapping clause assembly = RISCV_XPERM8(rs2, rs1, rd)
 function clause execute (RISCV_XPERM8(rs2, rs1, rd)) = {
   let rs1_val = X(rs1);
   let rs2_val = X(rs2);
-  result : xlenbits = zeros();
+  var result : xlenbits = zeros();
   foreach (i from 0 to (sizeof(xlen) - 8) by 8) {
     let index = unsigned(rs2_val[i+7..i]);
     result[i+7..i] = if 8*index < sizeof(xlen)
@@ -41,7 +41,7 @@ mapping clause assembly = RISCV_XPERM4(rs2, rs1, rd)
 function clause execute (RISCV_XPERM4(rs2, rs1, rd)) = {
   let rs1_val = X(rs1);
   let rs2_val = X(rs2);
-  result : xlenbits = zeros();
+  var result : xlenbits = zeros();
   foreach (i from 0 to (sizeof(xlen) - 4) by 4) {
     let index = unsigned(rs2_val[i+3..i]);
     result[i+3..i] = if 4*index < sizeof(xlen)