From 6c0c94d688a2c1cbec7c5ea2f226d7c80d932d1b Mon Sep 17 00:00:00 2001
From: Tobias Reiher <reiher@adacore.com>
Date: Wed, 21 Aug 2024 14:04:22 +0200
Subject: [PATCH] Enable SPARK proofs for SPDM responder example

Ref. eng/recordflux/RecordFlux#1704
---
 .gitlab-ci.yml                                     | 14 +++++++-------
 examples/apps/spdm_responder/Makefile              |  7 +++++--
 examples/apps/spdm_responder/build_lib.gpr         |  1 +
 .../src/lib/rflx-spdm_responder-session.adb        |  2 +-
 4 files changed, 14 insertions(+), 10 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b9da0c70c..0a393e249 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -504,15 +504,15 @@ verification_apps:
   services:
     - image:recordflux
     - cpu:4
-    - mem:30
+    - mem:32
     - security_group:GitLabRunnerTasksExecDefaultSG
   parallel:
     matrix:
-      - APP:
-        - "ping"
-        - "dhcp_client"
-        - "spdm_responder"
-        - "dccp"
+      - APP: "ping"
+      - APP: "dhcp_client"
+      - APP: "spdm_responder"
+        PROOF_PROCS: 2
+      - APP: "dccp"
   script:
     - *show_gnatprove_cache_stats
     - *update_timestamps_of_generated_code
@@ -520,7 +520,7 @@ verification_apps:
     - *setup_spark
     - *setup_gnat_cross
     - *setup_python
-    - timeout -k 60 27600 make -C examples/apps/${APP} prove
+    - timeout -k 60 20000 make -C examples/apps/${APP} prove
   cache:
     - *spark-cache-main
     - *spark-cache
diff --git a/examples/apps/spdm_responder/Makefile b/examples/apps/spdm_responder/Makefile
index e7eeb3558..271577696 100644
--- a/examples/apps/spdm_responder/Makefile
+++ b/examples/apps/spdm_responder/Makefile
@@ -1,5 +1,7 @@
 include ../../../Makefile.common
 
+PROOF_PROCS ?= $(shell nproc)
+
 GENERATED = generated/rflx-spdm.ads
 
 SOURCE_SPECIFICATIONS = \
@@ -71,9 +73,10 @@ libriscv64: $(BUILD_DIR)/riscv64/lib/libspdm.a
 
 .PHONY: prove
 
+# TODO(eng/recordflux/RecordFlux#1390): Prove SPDM messages
 prove: $(GNATPROVE_CACHE_DIR) $(GENERATED)
-	gnatprove -P build_lib.gpr -j0 -XTARGET=riscv64 -u responder
-	gnatprove -P build.gpr -j0 -XTARGET=riscv64 -u main
+	gnatprove -P build_lib.gpr -j$(PROOF_PROCS) -XTARGET=riscv64 -u responder -u rflx.spdm_responder.session -u rflx.spdm_responder.session.fsm -u rflx.spdm_responder.session.fsm_allocator -u rflx.spdm_responder.session_environment
+	gnatprove -P build.gpr -j$(PROOF_PROCS) -XTARGET=riscv64 -u main
 
 .PHONY: generate
 
diff --git a/examples/apps/spdm_responder/build_lib.gpr b/examples/apps/spdm_responder/build_lib.gpr
index aa4c918cc..22ba30e9d 100644
--- a/examples/apps/spdm_responder/build_lib.gpr
+++ b/examples/apps/spdm_responder/build_lib.gpr
@@ -107,6 +107,7 @@ project Build_Lib is
    package Prove is
       for Proof_Switches ("Ada") use Defaults.Proof_Switches;
       for Proof_Switches ("responder.adb") use ("--prover=z3,cvc5", "--steps=64000", "--memlimit=6000", "--timeout=600");
+      for Proof_Switches ("rflx-spdm_responder-session-fsm.adb") use ("--timeout=120");
    end Prove;
 
 end Build_Lib;
diff --git a/examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session.adb b/examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session.adb
index e78b76348..8bf47890c 100644
--- a/examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session.adb
+++ b/examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session.adb
@@ -15,7 +15,7 @@ with RFLX.SPDM_Responder.Session_Environment;
 --  SPARK mode is disabled for this package body because the C binding requires
 --  Ada features that are not part of the SPARK language.
 package body RFLX.SPDM_Responder.Session with
-   SPARK_Mode
+   SPARK_Mode => Off
 is
    --  Return CT exponent (DSP0274_1.1.0 [178]).
    --