Update types of indices to be u64

src/examples/add_two_array.c

@@ -1,10 +1,10 @@
-unsigned int array_read_two (unsigned int *p, int n, int i, int j)
+unsigned int array_read_two (unsigned int *p, unsigned long n, unsigned long i, unsigned long j)
 /* --BEGIN-- */
-/*@ requires take a1 = each(i32 k; 0i32 <= k && k < n) { Owned<unsigned int>(array_shift<unsigned int>(p,k)) };
-             0i32 <= i && i < n;
-             0i32 <= j && j < n;
+/*@ requires take a1 = each(u64 k; 0u64 <= k && k < n) { Owned<unsigned int>(array_shift<unsigned int>(p,k)) };
+             0u64 <= i && i < n;
+             0u64 <= j && j < n;
              j != i;
-    ensures take a2 = each(i32 k; 0i32 <= k && k < n) { Owned<unsigned int>(array_shift<unsigned int>(p,k)) };
+    ensures take a2 = each(u64 k; 0u64 <= k && k < n) { Owned<unsigned int>(array_shift<unsigned int>(p,k)) };
             a1 == a2;
             return == a1[i] + a1[j];
 @*/

src/examples/array_load.broken.c

@@ -1,7 +1,7 @@
-int read (int *p, int n, int i)
-/*@ requires take a1 = each(i32 j; 0i32 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) };
-             0i32 <= i && i < n; 
-    ensures take a2 = each(i32 j; 0i32 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) }; @*/
+int read (int *p, unsigned long n, unsigned long i)
+/*@ requires take a1 = each(u64 j; 0u64 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) };
+             0u64 <= i && i < n;
+    ensures take a2 = each(u64 j; 0u64 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) }; @*/
 {
   return p[i];
 }

src/examples/array_load.c

@@ -1,10 +1,11 @@
-int read (int *p, int n, int i)
-/*@ requires take a1 = each(i32 j; 0i32 <= j && j < n) { 
+int read (int *p, unsigned long n, unsigned long i)
+/*@ requires take a1 = each(u64 j; 0u64 <= j && j < n) {
                           Owned<int>(array_shift<int>(p,j)) };
-             0i32 <= i && i < n;
-    ensures take a2 = each(i32 j; 0i32 <= j && j < n) { 
+             0u64 <= i && i < n;
+             n > 0u64;
+    ensures take a2 = each(u64 j; 0u64 <= j && j < n) {
                             Owned<int>(array_shift<int>(p,j)) }; @*/
 {
-  /*@ extract Owned<int>, i; @*/
-  return p[i];
+  /*@ extract Owned<int>, 0u64; @*/
+  return p[0];
 }

src/examples/array_load2.c

@@ -1,7 +1,7 @@
-int read (int *p, int n, int i)
-/*@ requires take a1 = each(i32 j; 0i32 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) };
-             0i32 <= i && i < n;
-    ensures take a2 = each(i32 j; 0i32 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) };
+int read (int *p, unsigned long n, unsigned long i)
+/*@ requires take a1 = each(u64 j; 0u64 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) };
+             0u64 <= i && i < n;
+    ensures take a2 = each(u64 j; 0u64 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) };
             a1 == a2;
             return == a1[i];
 @*/

src/examples/init_array.c

@@ -1,12 +1,12 @@
-void init_array (char *p, unsigned int n)
-/*@ requires take a1 = each(u32 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
-    ensures  take a2 = each(u32 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
+void init_array (char *p, unsigned long n)
+/*@ requires take a1 = each(u64 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
+    ensures  take a2 = each(u64 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
 @*/
 {
-  unsigned int j = 0;
+  unsigned long j = 0;
   while (j < n)
 /* --BEGIN-- */
-  /*@ inv take ai = each(u32 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
+  /*@ inv take ai = each(u64 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
           {p} unchanged; {n} unchanged;
   @*/
 /* --END-- */

src/examples/init_array2.c

@@ -1,13 +1,13 @@
-void init_array2 (char *p, unsigned int n)
-/*@ requires take a1 = each(u32 i; i < n) { Block<char>( array_shift<char>(p, i)) };
-    ensures  take a2 = each(u32 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
+void init_array2 (char *p, unsigned long n)
+/*@ requires take a1 = each(u64 i; i < n) { Block<char>( array_shift<char>(p, i)) };
+    ensures  take a2 = each(u64 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
 @*/
 {
-  unsigned int j = 0;
+  unsigned long j = 0;
   while (j < n)
 /* --BEGIN-- */
-  /*@ inv take al = each(u32 i; i < j) { Owned<char>( array_shift<char>(p, i)) };
-          take ar = each(u32 i; j <= i && i < n) { Block<char>( array_shift<char>(p, i)) };
+  /*@ inv take al = each(u64 i; i < j) { Owned<char>( array_shift<char>(p, i)) };
+          take ar = each(u64 i; j <= i && i < n) { Block<char>( array_shift<char>(p, i)) };
           {p} unchanged; {n} unchanged;
           j <= n;
   @*/

src/examples/init_array_rev.c

@@ -1,22 +1,22 @@
-void init_array2 (char *p, unsigned int n)
-/*@ requires take a1 = each(u32 i; i < n) { Block<char>( array_shift<char>(p, i)) };
-    n > 0u32;
-    ensures  take a2 = each(u32 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
+void init_array2 (char *p, unsigned long n)
+/*@ requires take a1 = each(u64 i; i < n) { Block<char>( array_shift<char>(p, i)) };
+    n > 0u64;
+    ensures  take a2 = each(u64 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
 @*/
 {
-  unsigned int j = 0;
+  unsigned long j = 0;
   while (j < n)
 /* --BEGIN-- */
-  /*@ inv take al = each(u32 i; i < n-j) { Block<char>( array_shift<char>(p, i)) };
-          take ar = each(u32 i; n-j <= i && i < n) { Owned<char>( array_shift<char>(p, i)) };
+  /*@ inv take al = each(u64 i; i < n-j) { Block<char>( array_shift<char>(p, i)) };
+          take ar = each(u64 i; n-j <= i && i < n) { Owned<char>( array_shift<char>(p, i)) };
           {p} unchanged; {n} unchanged;
-          0u32 <= j && j <= n;
+          0u64 <= j && j <= n;
   @*/
 /* --END-- */
   {
 /* --BEGIN-- */
-    /*@ extract Block<char>, n-(j+1u32); @*/
-    /*@ extract Owned<char>, n-(j+1u32); @*/
+    /*@ extract Block<char>, n-(j+1u64); @*/
+    /*@ extract Owned<char>, n-(j+1u64); @*/
 /* --END-- */
     p[n-(j+1)] = 0;
     j++;

src/examples/swap_array.c

@@ -1,10 +1,10 @@
-void swap_array (int *p, int n, int i, int j)
+void swap_array (int *p, unsigned long n, unsigned long i, unsigned long j)
 /* --BEGIN-- */
-/*@ requires take a1 = each(i32 k; 0i32 <= k && k < n) { Owned<int>(array_shift<int>(p,k)) };
-             0i32 <= i && i < n;
-             0i32 <= j && j < n;
+/*@ requires take a1 = each(u64 k; 0u64 <= k && k < n) { Owned<int>(array_shift<int>(p,k)) };
+             0u64 <= i && i < n;
+             0u64 <= j && j < n;
              j != i;
-    ensures take a2 = each(i32 k; 0i32 <= k && k < n) { Owned<int>(array_shift<int>(p,k)) };
+    ensures take a2 = each(u64 k; 0u64 <= k && k < n) { Owned<int>(array_shift<int>(p,k)) };
             a2 == a1[i: a1[j], j: a1[i]];
 @*/
 /* --END-- */

src/tutorial.adoc

@@ -443,13 +443,13 @@ To support reasoning about code manipulating arrays and computed pointers, CN ha
 
 [source,c]
 ----
-each (i32 i; 0i32 <= i && i < 10i32)
+each (u64 i; 0u64 <= i && i < 10u64)
      { Owned<int>(array_shift<int>(p,i)) }
 ----
 
 In detail, this can be read as follows:
 
-* for each integer `+i+` of CN type `+i32+`, …
+* for each integer `+i+` of CN type `+u64+`, …
 
 * if `+i+` is between `+0+` and `+10+`, …
 
@@ -508,7 +508,7 @@ Here the CN comment `+/*@ extract Owned<int>, i; @*/+` is a CN "`ghost statement
 
 [source,c]
 ----
-each(i32 j; 0i32 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) }
+each(u64 j; 0u64 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) }
 ----
 
 is split into
@@ -523,15 +523,15 @@ Owned<int>(array_shift<int>(p,i))
 +
 [source,c]
 ----
-each(i32 j; 0i32 <= j && j < n && j != i)
+each(u64 j; 0u64 <= j && j < n && j != i)
     { Owned<int>(array_shift<int>(p,j)) }
 ----
 
 After this extraction step, CN can use the (former) extracted resource to justify the access `+p[i]+`.
 
 Following an `+extract+` statement, CN moreover remembers the extracted index and can automatically "`reverse`" the extraction when needed: after type checking the access `+p[i]+` CN must ensure the function’s postcondition holds, which needs the full array ownership again (including the extracted index `+i+`); remembering the index `+i+`, CN then automatically merges resources (1) and (2) again to obtain the required full array ownership, and completes the verification of the function.
 
-So far the specification only guarantees safe execution but does not specify the behaviour of `+read+`. To address this, let’s return to the iterated resources in the function specification. When we specify `+take a1 = each ...+` here, what is `+a1+`? In CN, the output of an iterated resource is a _map_ from indices to resource outputs. In this example, where index `+j+` has CN type `+i32+` and the iterated resource is `+Owned<int>+`, the output `+a1+` is a map from `+i32+` indices to `+i32+` values — CN type `+map<i32,i32>+`. (If the type of `+j+` was `+i64+` and the resource `+Owned<char>+`, `+a1+` would have type `+map<i64,u8>+`.)
+So far the specification only guarantees safe execution but does not specify the behaviour of `+read+`. To address this, let’s return to the iterated resources in the function specification. When we specify `+take a1 = each ...+` here, what is `+a1+`? In CN, the output of an iterated resource is a _map_ from indices to resource outputs. In this example, where index `+j+` has CN type `+u64+` and the iterated resource is `+Owned<int>+`, the output `+a1+` is a map from `+u64+` indices to `+i32+` values — CN type `+map<u64,i32>+`.
 
 We can use this to refine our specification with information about the functional behaviour of `+read+`.
 
@@ -557,14 +557,14 @@ include_example(exercises/swap_array.c)
 ////
 TODO: BCP: I wrote this, which seemed natural but did not work -- I still don't fully understand why.  I think this section will need some more examples / exercises to be fully digestible, or perhaps this is just yet another symptom of my imperfecdt understanding of how the numeric stuff works.
 
-    void swap_array (int *p, int n, int i, int j)
-    /*@ requires take a1 = each(i32 k; 0i32 <= k && k < n) { Owned<unsigned int>(array_shift<unsigned int>(p,k)) };
-                 0i32 <= i && i < n;
-                 0i32 <= j && j < n;
+    void swap_array (int *p, unsigned long n, unsigned long i, unsigned long j)
+    /*@ requires take a1 = each(u64 k; 0u64 <= k && k < n) { Owned<unsigned int>(array_shift<unsigned int>(p,k)) };
+                 0u64 <= i && i < n;
+                 0u64 <= j && j < n;
                  j != i;
                  take xi = Owned<unsigned int>(array_shift(p,i));
                  take xj = Owned<unsigned int>(array_shift(p,j))
-        ensures take a2 = each(i32 k; 0i32 <= k && k < n) { Owned<unsigned int>(array_shift<unsigned int>(p,k)) };
+        ensures take a2 = each(u64 k; 0u64 <= k && k < n) { Owned<unsigned int>(array_shift<unsigned int>(p,k)) };
                 a1[i:xj][j:xi] == a2
     @*/
     {