From d96f77f05021f0b2e1fb700891f4185d7c326885 Mon Sep 17 00:00:00 2001
From: Arne Keller <arne.keller@posteo.de>
Date: Thu, 18 Jan 2024 11:16:41 +0100
Subject: [PATCH 1/2] Revert "Remove dev section on proof caching"

This reverts commit 76ef4dd48190090700d5915890b47e7877c86931.
---
 docs/devel/ProofCaching.md | 168 +++++++++++++++++++++++++++++++++++++
 mkdocs.yml                 |   1 +
 2 files changed, 169 insertions(+)
 create mode 100644 docs/devel/ProofCaching.md

diff --git a/docs/devel/ProofCaching.md b/docs/devel/ProofCaching.md
new file mode 100644
index 0000000..1076644
--- /dev/null
+++ b/docs/devel/ProofCaching.md
@@ -0,0 +1,168 @@
+# Proof Caching
+
+See also the [end-user documentation](../../user/ProofCaching/).
+
+## On-disk database
+
+### Proofs
+
+When adding a proof to the database, the following is done:
+
+- a copy is saved in ~/.key/cachedProofs/
+- the Java source file(s) are saved
+- included `.key` files are saved
+- metadata is updated (see below)
+
+### Java source files, .key files
+
+When these are referenced in a proof, they will be copied into `~/.key/cachedProofs/` using a simple content-addressing scheme.
+
+The proof header is modified to refer to a new `~/.key/cachedProofs/javaSource123456` directory containing hardlinked copies of the source files.
+
+### Metadata
+
+Filename: `~/.key/cachedProofs.json`.
+
+Planned format: JSON.
+
+Schema: ([schema playground](https://dashjoin.github.io/#/schema))
+```
+{
+  "type": "object",
+  "properties": {
+    "proofs": {
+      "type": "array",
+      "items": {
+        "type": "object",
+        "properties": {
+          "name": {
+            "type": "string"
+          },
+          "file": {
+            "type": "string"
+          },
+          "keyVersion": {
+            "type": "string"
+          },
+          "choiceSettings": {
+            "type": "string"
+          },
+          "referencedFiles": {
+            "type": "array",
+            "items": {
+              "type": "string"
+            }
+          },
+          "cachedSequents": {
+            "type": "array",
+            "items": {
+              "type": "string"
+            }
+          },
+          "cachedGraph": {
+            "type": "object",
+            "properties": {
+              "nodes": {
+                "type": "array",
+                "items": {
+                  "type": "string"
+                }
+              },
+              "edges": {
+                "type": "array",
+                "items": {
+                  "type": "object",
+                  "properties": {
+                    "in": {
+                      "type": "array",
+                      "items": {
+                        "type": "string"
+                      }
+                    },
+                    "out": {
+                      "type": "array",
+                      "items": {
+                        "type": "string"
+                      }
+                    }
+                  }
+                }
+              }
+            }
+          },
+          "classpathHash": {
+            "type": "string"
+          },
+          "bootclasspathHash": {
+            "type": "string"
+          }
+        }
+      }
+    },
+    "files": {
+      "type": "array",
+      "items": {
+        "type": "object",
+        "properties": {
+          "file": {
+            "type": "string"
+          },
+          "hash": {
+            "type": "string"
+          }
+        }
+      }
+    }
+  }
+}
+```
+
+proof.choiceSettings should encode taclet options and other relevant properties (e.g. OSS use).
+
+proof.classpathHash should encode the entire classpath if it is explicitly set. Otherwise it should identify the classpath provided by the used KeY version.
+
+proof.keyVersion should help filter out proofs that are unlikely to load.
+
+Example:
+```
+{
+  "proofs": [
+    {
+      "name": "sumAndMax",
+      "file": "proof12345.proof",
+      "keyVersion": "2.13.0",
+      "choiceSettings": "xxxx",
+      "referencedFiles": [
+        "java123456.java"
+      ],
+      "cachedSequents": [
+        "a==>b"
+      ],
+      "cachedGraph": {
+        "nodes": [
+          "false ==>",
+          "Closed goal 1"
+        ],
+        "edges": [
+          {
+            "in": [
+              "false ==>"
+            ],
+            "out": [
+              "Closed goal 1"
+            ]
+          }
+        ]
+      },
+      "classpathHash": null,
+      "bootclasspathHash": null
+    }
+  ],
+  "files": [
+    {
+      "file": "java123456.java",
+      "hash": "41847972b9c92994502c60c58b406f098ef0afae"
+    }
+  ]
+}
+```
\ No newline at end of file
diff --git a/mkdocs.yml b/mkdocs.yml
index deea199..31c9162 100644
--- a/mkdocs.yml
+++ b/mkdocs.yml
@@ -160,6 +160,7 @@ nav:
           - devel/Testing/deterministicTestOrder.md
           - devel/Testing/parserMessageTest.md
       - Write Documentation: "devel/howtodoc/index.md"
+      - devel/ProofCaching.md
 
 repo_name: key-docs
 repo_url: https://github.com/KeYProject/key-docs/

From 6a37b5b319b3a5080ff85e658dee45cbbc01d51a Mon Sep 17 00:00:00 2001
From: Arne Keller <arne.keller@posteo.de>
Date: Thu, 18 Jan 2024 15:59:13 +0100
Subject: [PATCH 2/2] Change DB schema

---
 docs/devel/ProofCaching.md | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/docs/devel/ProofCaching.md b/docs/devel/ProofCaching.md
index 1076644..7ce6387 100644
--- a/docs/devel/ProofCaching.md
+++ b/docs/devel/ProofCaching.md
@@ -56,7 +56,15 @@ Schema: ([schema playground](https://dashjoin.github.io/#/schema))
           "cachedSequents": {
             "type": "array",
             "items": {
-              "type": "string"
+              "type": "object",
+              "properties": {
+                "stepIndex": {
+                  "type": "number"
+                },
+                "sequent": {
+                  "type": "string"
+                }
+              }
             }
           },
           "cachedGraph": {
@@ -136,7 +144,10 @@ Example:
         "java123456.java"
       ],
       "cachedSequents": [
-        "a==>b"
+        {
+          "stepIndex": 15,
+          "sequent": "a==>b"
+        }
       ],
       "cachedGraph": {
         "nodes": [