ci: add missing Rust examples

Author: clarus

examples/custom/loops.rs

@@ -0,0 +1,56 @@
+#![no_std]
+
+pub fn sum_checked(xs: &[u32]) -> Option<u32> {
+    let mut acc: u32 = 0;
+    let mut i: usize = 0;
+    // Invariant idea (Coq):
+    //  - 0 <= i <= xs.len()
+    //  - acc = sum(xs[0..i]) and never overflowed
+    while i < xs.len() {
+        match acc.checked_add(xs[i]) {
+            Some(v) => acc = v,
+            None => return None,
+        }
+        i += 1;
+    }
+    Some(acc)
+}
+
+pub fn reverse_in_place(xs: &mut [i32]) {
+  if xs.len() == 0 { return; }
+  let mut l: usize = 0;
+  let mut r: usize = xs.len() - 1;
+  // Invariant idea:
+  //  - xs[0..l] and xs[r+1..] are already reversed wrt original
+  //  - l <= r + 1
+  while l < r {
+      let tmp = xs[l];
+      xs[l] = xs[r];
+      xs[r] = tmp;
+      l += 1;
+      r -= 1;
+  }
+}
+
+pub fn is_sorted(xs: &[i32]) -> bool {
+  let mut i: usize = 1;
+  // Invariant idea:
+  //  - prefix xs[0..i] is sorted (pairwise non-decreasing)
+  while i < xs.len() {
+      if xs[i - 1] > xs[i] { return false; }
+      i += 1;
+  }
+  true
+}
+
+pub fn max_array<const N: usize>(a: &[i32; N]) -> i32 {
+  let mut m = a[0];
+  let mut i: usize = 1;
+  // Invariant idea:
+  //  - m = max(a[0..i])
+  while i < N {
+      if a[i] > m { m = a[i]; }
+      i += 1;
+  }
+  m
+}

examples/custom/loops_free.rs

@@ -0,0 +1,42 @@
+#![no_std]
+
+// max2(a,b) = a or max2(a,b) = b
+// max2(a,b) >= a and >= b
+pub fn max2(a: u32, b: u32) -> u32 {
+    if a < b { b } else { a }
+}
+
+// result ≥ 0
+pub fn abs_i32(x: i32) -> i32 {
+  if x < 0 { -x } else { x }
+}
+
+// Truth table correctness
+pub fn bool_and(a: bool, b: bool) -> bool {
+  if a {
+      if b { true } else { false }
+  } else {
+      false
+  }
+}
+
+pub fn get_or_zero(xs: &[u32; 4], i: usize) -> u32 {
+  if i < 4 { xs[i] } else { 0 }
+}
+
+pub fn eq2(a: &[u32; 2], b: &[u32; 2]) -> bool {
+  if a[0] == b[0] && a[1] == b[1] {
+      true
+  } else {
+      false
+  }
+}
+
+pub fn eq_pair(x: (u32, u32), y: (u32, u32)) -> bool {
+  if x.0 == y.0 && x.1 == y.1 { true } else { false }
+}
+
+pub fn min3(a: u32, b: u32, c: u32) -> u32 {
+  let m = if a < b { a } else { b };
+  if m < c { m } else { c }
+}