feat: finalize generation

Author: andrii-a8c

crates/move-prover-boogie-backend/src/boogie_backend/lib.rs

@@ -4,7 +4,7 @@
 
 #![forbid(unsafe_code)]
 
-use std::{collections::BTreeSet, fs};
+use std::{cmp::Ordering, collections::BTreeSet, fs};
 
 use itertools::Itertools;
 #[allow(unused_imports)]
@@ -45,12 +45,14 @@ const TABLE_ARRAY_THEORY: &[u8] = include_bytes!("prelude/table-array-theory.bpl
 const BCS_MODULE: &str = "0x1::bcs";
 const EVENT_MODULE: &str = "0x1::event";
 
-#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize, Default)]
+#[derive(Debug, Clone, Serialize, Deserialize, Default)]
 struct TypeInfo {
     name: String,
     suffix: String,
     has_native_equality: bool,
     is_bv: bool,
+    is_number: bool,
+    bit_width: String,
 }
 
 #[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize, Default)]
@@ -455,10 +457,38 @@ impl TypeInfo {
             suffix: boogie_type_suffix_bv(env, ty, bv_flag),
             has_native_equality: has_native_equality(env, options, ty),
             is_bv: bv_flag,
+            bit_width: ty.get_bit_width().unwrap_or(8).to_string(),
+            is_number: ty.is_number(),
         }
     }
 }
 
+impl PartialEq for TypeInfo {
+    fn eq(&self, other: &Self) -> bool {
+        self.name == other.name && self.suffix == other.suffix && self.has_native_equality == other.has_native_equality
+    }
+}
+
+impl PartialOrd for TypeInfo {
+    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
+        Some(self.cmp(other))
+    }
+}
+
+impl Ord for TypeInfo {
+    fn cmp(&self, other: &Self) -> Ordering {
+        match self.name.cmp(&other.name) {
+            Ordering::Equal => match self.suffix.cmp(&other.suffix) {
+                Ordering::Equal => self.has_native_equality.cmp(&other.has_native_equality),
+                other => other,
+            },
+            other => other,
+        }
+    }
+}
+
+impl Eq for TypeInfo {}
+
 impl TableImpl {
     fn table(
         env: &GlobalEnv,

crates/move-prover-boogie-backend/src/boogie_backend/prelude/native.bpl

@@ -372,6 +372,7 @@ function {:inline} $1_vector_$skip{{S}}(v: Vec ({{T}}), n: int): Vec ({{T}}) {
     (if n >= LenVec(v) then EmptyVec() else SliceVec(v, n, LenVec(v)))
 }
 
+{%- if instance.is_number -%}
 function $0_vec_$sum{{S}}(v: Vec ({{T}}), start: int, end: int): {{T}};
 
 {%- if instance.is_bv -%}
@@ -386,13 +387,13 @@ axiom (forall v: Vec ({{T}}), start1: int, end1: int, start2: int, end2: int ::
 // the sum over an empty range is zero
 axiom (forall v: Vec ({{T}}), start: int, end: int ::
       { $0_vec_$sum{{S}}(v, start, end)}
-   (start >= end ==> $0_vec_$sum{{S}}(v, start, end) == 0bv8));
+   (start >= end ==> $0_vec_$sum{{S}}(v, start, end) == 0bv{{instance.bit_width}}));
 
 // the sum of a range can be split in two
 axiom (forall v: Vec ({{T}}), a: int, b: int, c: int, d: int ::
   { $0_vec_$sum{{S}}(v, a, b), $0_vec_$sum{{S}}(v, c, d) }
   0 <= a && a <= b && b == c && c <= d && d <= LenVec(v)  ==>
-    $Add'Bv8'($0_vec_$sum{{S}}(v, a, b), $0_vec_$sum{{S}}(v, c, d)) == $0_vec_$sum{{S}}(v, a, d)) ;
+    $Add'Bv{{instance.bit_width}}'($0_vec_$sum{{S}}(v, a, b), $0_vec_$sum{{S}}(v, c, d)) == $0_vec_$sum{{S}}(v, a, d)) ;
 
 // the sum over a singleton range is the vector element there
 axiom (forall v: Vec ({{T}}), a: int, x: int, y: int ::
@@ -403,7 +404,7 @@ axiom (forall v: Vec ({{T}}), a: int, x: int, y: int ::
 axiom (forall v: Vec ({{T}}), a: int, b: int, c: int, d: int ::
   { $0_vec_$sum{{S}}(v, a, d), $0_vec_$sum{{S}}(v, b, c) }
   $IsValid'vec{{S}}'(v) && 0 <= a && a <= b && b <= c && c <= d && d <= LenVec(v)  ==>
-    $Le'Bv8'($0_vec_$sum{{S}}(v, b, c), $0_vec_$sum{{S}}(v, a, d)));
+    $Le'Bv{{instance.bit_width}}'($0_vec_$sum{{S}}(v, b, c), $0_vec_$sum{{S}}(v, a, d)));
 
 {%- else -%}
 
@@ -437,11 +438,13 @@ axiom (forall v: Vec ({{T}}), a: int, b: int, c: int, d: int ::
 
 {%- endif %}
 
-procedure {:inline 1} $0_vec_sum{{S}}(v: Vec ({{T}})) returns (res: {{T}}) {
+procedure {:inline 1} $0_vector_iter_sum{{S}}(v: Vec ({{T}})) returns (res: {{T}}) {
     res := $0_vec_$sum{{S}}(v, 0, LenVec(v));
 }
 
-procedure {:inline 1} $0_vec_slice{{S}}(v: Vec ({{T}}), start: int, end: int) returns (res: Vec ({{T}})) {
+{%- endif %}
+
+procedure {:inline 1} $0_vector_iter_slice{{S}}(v: Vec ({{T}}), start: int, end: int) returns (res: Vec ({{T}})) {
     var len: int;
     len := LenVec(v);
     if (start >= len || end <= start) {

crates/sui-prover/tests/inputs/sum_slice.ok.move

@@ -1,7 +1,7 @@
 module 0x42::foo;
 
 use prover::prover::ensures;
-use prover::vec::{slice, sum};
+use prover::vector_iter::{slice, sum};
 
 #[spec(prove)]
 fun test_slice_and_sum() {