Add a CI and some proof fixes

Author: dc-mak

.github/workflows/ci.yml

@@ -0,0 +1,93 @@
+name: Proof
+
+on:
+  # Run this action every day
+  schedule:
+    - cron: '30 18 * * *'
+  pull_request:
+  push:
+
+# cancel in-progress job when a new push is performed
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  build:
+    strategy:
+      matrix:
+        version: [5.2.0]
+
+    runs-on: ubuntu-22.04
+
+    steps:
+    - uses: actions/checkout@v4
+      with:
+        repository: rems-project/cerberus
+
+    - name: System dependencies (ubuntu)
+      run: |
+        sudo apt install build-essential libgmp-dev z3 opam
+
+    - name: Restore cached opam
+      id: cache-opam-restore
+      uses: actions/cache/restore@v4
+      with:
+        path: ~/.opam
+        key: ${{ matrix.version }}
+
+    - name: Setup opam
+      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
+      run: |
+        opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
+        opam switch ${{ matrix.version }}
+        eval $(opam env --switch=${{ matrix.version }})
+        opam install --deps-only --yes ./cerberus.opam ./cerberus-lib.opam ./cn.opam
+        opam install --yes z3
+
+    - name: Save cached opam
+      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
+      id: cache-opam-save
+      uses: actions/cache/save@v4
+      with:
+        path: ~/.opam
+        key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }}
+
+    - name: Install Cerberus
+      run: |
+        opam switch ${{ matrix.version }}
+        eval $(opam env --switch=${{ matrix.version }})
+        opam pin --yes --no-action add cerberus-lib .
+        opam pin --yes --no-action add cerberus .
+        opam install --yes cerberus
+
+    - name: Install CN
+      run: |
+        opam switch ${{ matrix.version }}
+        eval $(opam env --switch=${{ matrix.version }})
+        opam pin --yes --no-action add cn .
+        opam install --yes cn
+
+#   - name: Download cvc5 release
+#     uses: robinraju/release-downloader@v1
+#     with:
+#       repository: cvc5/cvc5
+#       tag: cvc5-1.1.2
+#       fileName: cvc5-Linux-static.zip
+
+#    - name: Unzip and install cvc5
+#      run: |
+#        unzip cvc5-Linux-static.zip
+#        chmod +x cvc5-Linux-static/bin/cvc5
+#        sudo cp cvc5-Linux-static/bin/cvc5 /usr/local/bin/
+
+    - name: Checkout this repo
+      uses: actions/checkout@v4
+      with:
+        path: buddy-alloc
+
+    - name: Run CN Proof
+      run: |
+        opam switch ${{ matrix.version }}
+        eval $(opam env --switch=${{ matrix.version }})
+        cd buddy-alloc && ./proof.sh

defs.h

@@ -176,6 +176,10 @@ function (boolean) vmemmap_wf (u64 page_index,
     && (page_group_ok(page_index, vmemmap, pool))
 }
 
+function (boolean) eq_t(pointer x, pointer y) {
+    ptr_eq(x,y) || !addr_eq(x,y)
+}
+
 function (boolean) vmemmap_l_wf (u64 page_index, i64 physvirt_offset,
         pointer virt_ptr,
         map <u64, struct hyp_page> vmemmap, map <u64, struct list_head> APs,
@@ -212,7 +216,11 @@ function (boolean) vmemmap_l_wf (u64 page_index, i64 physvirt_offset,
   // there is no self-loop case for this node type, as it is cleared unless it is
   // present in the per-order free list - TODO delete?
   let nonempty_clause = (prev != self_node_pointer) && (next != self_node_pointer);
-  (prev_clause && next_clause)
+  let eq_testable = eq_t(prev, self_node_pointer)
+                    && eq_t(prev, pool_free_area_pointer)
+                    && eq_t(next, prev)
+                    && eq_t(next, pool_free_area_pointer);
+  (prev_clause && next_clause && eq_testable)
 }
 
 
@@ -265,7 +273,7 @@ function (boolean) hyp_pool_wf (pointer pool_pointer, struct hyp_pool pool,
     (range_start < range_end)
     && (range_end < shift_left(1u64, 52u64))
     && (physvirt_offset < (i64) range_start) // use '<='
-    && (mod((u64) physvirt_offset, (page_size ())) == 0u64)
+    && mod((u64) physvirt_offset, page_size ()) == 0u64
     && (((range_start / (page_size ())) * (page_size ())) == range_start)
     && (((range_end / (page_size ())) * (page_size ())) == range_end)
     && (pool.max_order <= (max_order ()))
@@ -305,9 +313,7 @@ predicate void Page (pointer vbase, boolean guard, u8 order)
   }
   else {
     let length = page_size_of_order(order);
-    let vbaseI = (u64) vbase;
-    take Bytes = each (u64 i; (vbaseI <= i) && (i < (vbaseI + length)))
-         {Byte(array_shift<char>(NULL, i))};
+    take Bytes = each (u64 i; 0u64 <= i && i < length) {Byte(array_shift<char>(vbase, i))};
     return;
   }
 }
@@ -318,21 +324,18 @@ predicate void ZeroPage (pointer vbase, boolean guard, u8 order)
     return;
   }
   else {
-    let length = page_size_of_order(order);
-    let vbaseI = ((u64) vbase);
-    take Bytes = each (u64 i; (vbaseI <= i) && (i < (vbaseI + length)))
-         {ByteV(array_shift<char>(NULL, i), 0u8)};
+    let length = sizeof<struct list_head>;
+    take B1 = each (u64 i; 0u64 <= i && i < length) {ByteV(array_shift<char>(vbase, i), 0u8)};
+    take B2 = each (u64 i; length <= i && i < page_size_of_order(order)) {ByteV(array_shift<char>(vbase, i), 0u8)};
     return;
   }
 }
 
-predicate void AllocatorPageZeroPart (pointer zero_start, u8 order)
+predicate void AllocatorPageZeroPart (pointer vbase, u8 order)
 {
-  let start = (u64) zero_start;
   let region_length = page_size_of_order(order);
-  let length = region_length - sizeof<struct list_head>;
-  take Bytes = each (u64 i; (start <= i) && (i < (start + length)))
-       {ByteV(array_shift<char>(NULL, i), 0u8)};
+  take Bytes = each (u64 i; sizeof<struct list_head> <= i && i < region_length)
+      {ByteV(array_shift<char>(vbase, i), 0u8)};
   return;
 }
 
@@ -347,9 +350,8 @@ predicate struct list_head AllocatorPage
     return (todo_default_list_head ());
   }
   else {
-    let zero_start = array_shift<struct list_head>(vbase, 1u8);
-    take ZeroPart = AllocatorPageZeroPart (zero_start, order);
     take Node = Owned<struct list_head>(vbase);
+    take ZeroPart = AllocatorPageZeroPart (vbase, order);
     return Node;
   }
 }

lemmas.h

@@ -160,15 +160,12 @@ lemma page_size_of_order2(u8 order) // unsigned int
 
 lemma struct_list_head_to_bytes(pointer node) // struct list_head * 
   requires take Node = Owned<struct list_head>(node);
-  ensures take B = each (u64 i; ((u64) node) <= i && i < (((u64) node) + (sizeof<struct list_head>))){Byte(array_shift<char>(NULL, i))};
+  ensures take B = each (u64 i; 0u64 <= i && i < sizeof<struct list_head>){Byte(array_shift<char>(node, i))};
 
 
 lemma bytes_to_struct_list_head(pointer node, // struct list_head *
                                 u8 order)
-  requires let length = page_size_of_order(order) ;
-           let nodeI = ((u64) node) ;
-           take B = each (u64 i; (nodeI <= i) && (i < (nodeI + length))) {ByteV(array_shift<char>(NULL, i), 0u8)};
-  ensures take Node = Owned<struct list_head>(node) ;
-          take BR = each (u64 i; (nodeI + (sizeof<struct list_head>)) <= i && i < (nodeI + length)){ByteV(array_shift<char>(NULL, i), 0u8)};
+  requires take B = each (u64 i; 0u64 <= i && i < sizeof<struct list_head>) {ByteV(array_shift<char>(node, i), 0u8)};
+  ensures take Node = Owned<struct list_head>(node);
 
 @*/

memory.h

@@ -35,9 +35,11 @@ extern struct hyp_page *__hyp_vmemmap;
 
 static inline void *hyp_phys_to_virt(phys_addr_t phys)
 /*@ accesses hyp_physvirt_offset; cn_virt_base; @*/
-/*@ requires let virt = phys - (u64) hyp_physvirt_offset; @*/
+/*@ requires has_alloc_id(cn_virt_base); @*/
+/*@ requires let virt = cn__hyp_va(cn_virt_base, hyp_physvirt_offset, phys); @*/
 /*@ ensures {hyp_physvirt_offset} unchanged; @*/
-/*@ ensures (u64) return == virt; @*/
+/*@ ensures {cn_virt_base} unchanged; @*/
+/*@ ensures ptr_eq(return, virt); @*/
 {
     return CN_COPY_ALLOC_ID(__hyp_va(phys), cn_virt_base);
 }
@@ -73,9 +75,13 @@ function (u64) max_pfn ()
 
 static inline u64 hyp_page_to_pfn(struct hyp_page *page)
 /*@ accesses __hyp_vmemmap; @*/
+/*@ requires has_alloc_id(page); @*/
+/*@ requires has_alloc_id(__hyp_vmemmap); @*/
+/*@ requires (alloc_id) page == (alloc_id) __hyp_vmemmap; @*/
+/*@ requires mod((u64)__hyp_vmemmap, sizeof<struct hyp_page>) == 0u64; @*/
 /*@ requires let offs = ((u64) page) - ((u64) __hyp_vmemmap); @*/
 /*@ requires offs <= max_pfn () * (sizeof<struct hyp_page>); @*/
-/*@ requires mod(offs, sizeof<struct hyp_page>) == 0u64; @*/
+/*@ requires mod((u64)page, sizeof<struct hyp_page>) == 0u64; @*/
 /*@ ensures return == offs / (sizeof<struct hyp_page>); @*/
 /*@ ensures {__hyp_vmemmap} unchanged; @*/
 {