restructures repository to have top-level directories for DH and SSM-Agent

Author: ArquintL

.github/workflows/artifact.yml

@@ -78,27 +78,65 @@ jobs:
         run: echo "IMAGE_TAG=${{ env.IMAGE_TAG }}" >> $GITHUB_OUTPUT
 
 
-  Test:
+  Test-DH:
     name: ${{ matrix.name }}
     runs-on: ubuntu-latest
     needs: Build
     strategy:
       # tests should not be stopped when they fail on one of the OSes:
       fail-fast: false
       matrix:
-        name: ["Verify protocol model", "Verify core"]
+        # name: ["Verify DH protocol model", "Verify DH core", "Verify DH I/O independence", "Verify DH core assumptions"]
+        name: ["Verify DH protocol model", "Verify DH core"]
         include:
-          - name: "Verify protocol model"
-            command: "/gobra/verify-model.sh"
+          - name: "Verify DH protocol model"
+            command: "/gobra/dh/verify-model.sh"
+            timeout-minutes: 1
+          - name: "Verify DH core"
+            command: "/gobra/dh/verify-core.sh"
+            timeout-minutes: 5
+          # - name: "Verify DH I/O independence"
+          #   command: "/gobra/dh/verify-io-independence.sh"
+          #   timeout-minutes: 3
+          # - name: "Verify DH core assumptions"
+          #   command: "/gobra/dh/verify-core-assumptions.sh"
+          #   timeout-minutes: 3
+    timeout-minutes: ${{ matrix.timeout-minutes }}
+    steps:
+      - name: Download artifact
+        uses: actions/download-artifact@v4
+        with:
+          name: ${{ env.IMAGE_WORKFLOW_ARTIFACT_NAME }}
+          path: /tmp
+
+      - name: Load image
+        run: docker load --input /tmp/image.tar
+
+      - name: ${{ matrix.name }}
+        run: docker run --entrypoint "/bin/bash" ${{ needs.Build.outputs.IMAGE_TAG }} -c "cp -r model-orig/. model/; cp -r implementation-orig/. implementation/; ${{ matrix.command }}"
+
+
+  Test-SSM-Agent:
+    name: ${{ matrix.name }}
+    runs-on: ubuntu-latest
+    needs: Build
+    strategy:
+      # tests should not be stopped when they fail on one of the OSes:
+      fail-fast: false
+      matrix:
+        name: ["Verify SSM Agent protocol model", "Verify SSM Agent core", "Verify SSM Agent I/O independence", "Verify SSM Agent core assumptions"]
+        include:
+          - name: "Verify SSM Agent protocol model"
+            command: "/gobra/ssm-agent/verify-model.sh"
             timeout-minutes: 15
-          - name: "Verify core"
-            command: "/gobra/verify-core.sh"
+          - name: "Verify SSM Agent core"
+            command: "/gobra/ssm-agent/verify-core.sh"
             timeout-minutes: 15
-          - name: "Verify I/O independence"
-            command: "/gobra/verify-io-independence.sh"
+          - name: "Verify SSM Agent I/O independence"
+            command: "/gobra/ssm-agent/verify-io-independence.sh"
             timeout-minutes: 10
-          - name: "Verify core assumptions"
-            command: "/gobra/verify-core-assumptions.sh"
+          - name: "Verify SSM Agent core assumptions"
+            command: "/gobra/ssm-agent/verify-core-assumptions.sh"
             timeout-minutes: 10
     timeout-minutes: ${{ matrix.timeout-minutes }}
     steps:
@@ -117,7 +155,7 @@ jobs:
 
   Publish:
     runs-on: ubuntu-latest
-    needs: [Build, Test]
+    needs: [Build, Test-DH, Test-SSM-Agent]
     timeout-minutes: 5
     # set per-job GITHUB_TOKEN permissions such that pushing the Docker image will be possible:
     permissions:

.gitignore

@@ -2,5 +2,6 @@
 .idea
 *.log
 tmp/
-
+dh-sync/
+ssm-agent-sync/
 argot-proofs/reports/

.gitmodules

@@ -1,5 +1,5 @@
 [submodule "implementation"]
-	path = implementation
+	path = ssm-agent/implementation
 	url = https://github.com/ArquintL/amazon-ssm-agent
 	branch = diodon
 [submodule "ar-go-tools"]

README.md

@@ -24,13 +24,13 @@ We require an installation of Docker. The following steps have been tested on ma
 - We recommend to adapt the Docker settings to provide sufficient resources to Docker. We have tested our artifact on a 2019 16-inch MacBook Pro with 2.3 GHz 8-Core Intel Core i9 running macOS Sonoma 14.0 and configured Docker to allocate up 16 cores (which includes 8 virtual cores), 6 GB of memory, and 1 GB of swap memory. In case you are using an ARM-based Mac, enable the option "Use Rosetta for x86/amd64 emulation on Apple Silicon" in the Docker Desktop Settings, which is available on macOS 13 or newer. Measurements on an Apple M1 Pro Silicon have shown that performing this additional emulation results in 20-25\% longer verification times compared to those reported in the remainder of this artifact appendix.
 - Navigate to a convenient folder, in which directories can be created for the purpose of running this artifact.
 - Open a shell at this folder location.
-- Create two new folders named `model-sync` and `implementation-sync` by executing:
+- Create two new folders named `dh-sync` and `ssm-agent-sync` by executing:
 	```
-    mkdir model-sync && mkdir implementation-sync
+    mkdir dh-sync && mkdir ssm-agent-sync
     ```
 - Download and start the Docker image containing our artifact by executing the following command:
     ```
-    docker run -it --platform linux/amd64 --volume $PWD/model-sync:/gobra/model --volume $PWD/implementation-sync:/gobra/implementation ghcr.io/arquintl/diodon-artifact:latest
+    docker run -it --platform linux/amd64 --volume $PWD/dh-sync:/gobra/dh --volume $PWD/ssm-agent-sync:/gobra/ssm-agent ghcr.io/arquintl/diodon-artifact:latest
     ```
     > ⚠️
     > Note that this command results in the Docker container writing files to the two folders `model-sync` and `implementation-sync` on your host machine.

dh/implementation/.gitignore

@@ -0,0 +1,3 @@
+.gobra/
+local-verify.sh
+dh-gobra

dh/implementation/responder/.gitignore

@@ -0,0 +1,3 @@
+.gradle/
+build/
+dh-gobra.jar

dh/implementation/verify.sh

@@ -0,0 +1 @@
+client_session_key.aes

dh/model/.gitignore

@@ -1,6 +1,6 @@
 
 
-input_file /Users/arquintlinard/ETH/PhD/gh-artifact/arquintl-diodon-artifact/dh/model/dh.spthy
+input_file /Users/arquintlinard/ETH/PhD/gh-artifact/arquintl-diodon-artifact/dh/model/protocol-model.spthy
 
 base_dir /Users/arquintlinard/ETH/PhD/gh-artifact/arquintl-diodon-artifact/dh/model/generated_iospecs
 module dh-gobra/verification