Content for HACS 2026, plus some other changes

Author: dstebila

Gemfile

@@ -1,10 +1,7 @@
 source 'https://rubygems.org'
 
-gem "jekyll", "~> 4.3.3" # installed by `gem jekyll`
-# gem "webrick"        # required when using Ruby >= 3 and Jekyll <= 4.2.2
-
-gem "just-the-docs", "0.8.1" # pinned to the current release
-# gem "just-the-docs"        # always download the latest release
+gem "jekyll", "~> 4.4"
+gem "just-the-docs", "0.12.0"
 
 group :jekyll_plugins do
   gem 'jekyll-katex'

Gemfile.lock

@@ -1,33 +1,56 @@
 GEM
   remote: https://rubygems.org/
   specs:
-    addressable (2.8.6)
-      public_suffix (>= 2.0.2, < 6.0)
+    addressable (2.8.9)
+      public_suffix (>= 2.0.2, < 8.0)
+    base64 (0.3.0)
+    bigdecimal (4.0.1)
     colorator (1.1.0)
-    concurrent-ruby (1.2.3)
+    concurrent-ruby (1.3.6)
+    csv (3.3.5)
     em-websocket (0.5.3)
       eventmachine (>= 0.12.9)
       http_parser.rb (~> 0)
     eventmachine (1.2.7)
-    execjs (2.9.1)
-    ffi (1.16.3)
+    execjs (2.10.0)
+    ffi (1.17.3)
+    ffi (1.17.3-arm64-darwin)
+    ffi (1.17.3-x86-linux-gnu)
+    ffi (1.17.3-x86-linux-musl)
+    ffi (1.17.3-x86_64-darwin)
     forwardable-extended (2.6.0)
-    google-protobuf (3.25.3-arm64-darwin)
-    google-protobuf (3.25.3-x86_64-linux)
-    http_parser.rb (0.8.0)
-    i18n (1.14.4)
+    google-protobuf (4.34.0)
+      bigdecimal
+      rake (~> 13.3)
+    google-protobuf (4.34.0-arm64-darwin)
+      bigdecimal
+      rake (~> 13.3)
+    google-protobuf (4.34.0-x86-linux-gnu)
+      bigdecimal
+      rake (~> 13.3)
+    google-protobuf (4.34.0-x86-linux-musl)
+      bigdecimal
+      rake (~> 13.3)
+    google-protobuf (4.34.0-x86_64-darwin)
+      bigdecimal
+      rake (~> 13.3)
+    http_parser.rb (0.8.1)
+    i18n (1.14.8)
       concurrent-ruby (~> 1.0)
-    jekyll (4.3.3)
+    jekyll (4.4.1)
       addressable (~> 2.4)
+      base64 (~> 0.2)
       colorator (~> 1.0)
+      csv (~> 3.0)
       em-websocket (~> 0.5)
       i18n (~> 1.0)
       jekyll-sass-converter (>= 2.0, < 4.0)
       jekyll-watch (~> 2.0)
+      json (~> 2.6)
       kramdown (~> 2.3, >= 2.3.1)
       kramdown-parser-gfm (~> 1.0)
       liquid (~> 4.0)
-      mercenary (>= 0.3.6, < 0.5)
+      mercenary (~> 0.3, >= 0.3.6)
       pathutil (~> 0.9)
       rouge (>= 3.0, < 5.0)
       safe_yaml (~> 1.0)
@@ -38,52 +61,62 @@ GEM
     jekyll-katex (1.0.0)
       execjs (~> 2.7)
       jekyll (>= 3.6, < 5.0)
-    jekyll-sass-converter (3.0.0)
-      sass-embedded (~> 1.54)
+    jekyll-sass-converter (3.1.0)
+      sass-embedded (~> 1.75)
     jekyll-seo-tag (2.8.0)
       jekyll (>= 3.8, < 5.0)
     jekyll-watch (2.2.1)
       listen (~> 3.0)
-    just-the-docs (0.8.1)
+    json (2.18.1)
+    just-the-docs (0.12.0)
       jekyll (>= 3.8.5)
       jekyll-include-cache
       jekyll-seo-tag (>= 2.0)
       rake (>= 12.3.1)
-    kramdown (2.4.0)
-      rexml
+    kramdown (2.5.2)
+      rexml (>= 3.4.4)
     kramdown-parser-gfm (1.1.0)
       kramdown (~> 2.0)
     liquid (4.0.4)
-    listen (3.9.0)
+    listen (3.10.0)
+      logger
       rb-fsevent (~> 0.10, >= 0.10.3)
       rb-inotify (~> 0.9, >= 0.9.10)
+    logger (1.7.0)
     mercenary (0.4.0)
     pathutil (0.16.2)
       forwardable-extended (~> 2.6)
-    public_suffix (5.0.4)
-    rake (13.1.0)
+    public_suffix (6.0.2)
+    rake (13.3.1)
     rb-fsevent (0.11.2)
-    rb-inotify (0.10.1)
+    rb-inotify (0.11.1)
       ffi (~> 1.0)
-    rexml (3.2.6)
-    rouge (4.2.0)
+    rexml (3.4.4)
+    rouge (4.7.0)
     safe_yaml (1.0.5)
-    sass-embedded (1.69.5)
-      google-protobuf (~> 3.23)
-      rake (>= 13.0.0)
+    sass-embedded (1.97.3)
+      google-protobuf (~> 4.31)
+      rake (>= 13)
+    sass-embedded (1.97.3-arm64-darwin)
+      google-protobuf (~> 4.31)
+    sass-embedded (1.97.3-x86_64-darwin)
+      google-protobuf (~> 4.31)
     terminal-table (3.0.2)
       unicode-display_width (>= 1.1.1, < 3)
-    unicode-display_width (2.5.0)
-    webrick (1.8.1)
+    unicode-display_width (2.6.0)
+    webrick (1.9.2)
 
 PLATFORMS
-  arm64-darwin-23
-  x86_64-linux
+  arm64-darwin
+  ruby
+  x86-linux-gnu
+  x86-linux-musl
+  x86_64-darwin
 
 DEPENDENCIES
-  jekyll (~> 4.3.3)
+  jekyll (~> 4.4)
   jekyll-katex
-  just-the-docs (= 0.8.1)
+  just-the-docs (= 0.12.0)
 
 BUNDLED WITH
-   2.3.26
+   2.5.18

_config.yml

@@ -2,10 +2,26 @@ title: ProofFrog
 description: A tool for verifying game-hopping proofs
 theme: just-the-docs
 
-url: https://just-the-docs.github.io
+url: https://prooffrog.github.io
 
 aux_links:
-  ProofFrog Hub: https://github.com/ProofFrog
+  ProofFrog GitHub: https://github.com/ProofFrog
 
 plugins:
   - jekyll-katex
+
+callouts:
+  highlight:
+    color: yellow
+  important:
+    title: Important
+    color: blue
+  new:
+    title: New
+    color: green
+  note:
+    title: Note
+    color: purple
+  warning:
+    title: Warning
+    color: red

_includes/head_custom.html

@@ -1 +1,3 @@
 <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.11.1/dist/katex.min.css" integrity="sha384-zB1R0rpPzHqg7Kpt0Aljp8JPLqbXI3bhnPWROx27a9N0Ll6ZP/+DiW/UqRcLbRjq" crossorigin="anonymous">
+<script src="https://cdn.jsdelivr.net/npm/prismjs@1.29.0/prism.min.js"></script>
+<script src="{{ '/assets/js/prism-prooffrog.js' | relative_url }}"></script>

_sass/custom/custom.scss

@@ -1,3 +1,16 @@
+// Prism.js token colors (no theme CSS loaded — just-the-docs controls layout)
+.token.comment { color: #6a737d; font-style: italic; }
+.token.string { color: #032f62; }
+.token.keyword { color: #d73a49; }
+.token.class-name { color: #6f42c1; font-weight: bold; }
+.token.builtin { color: #005cc5; }
+.token.boolean,
+.token.constant { color: #005cc5; }
+.token.number { color: #005cc5; }
+.token.operator { color: #d73a49; }
+.token.punctuation { color: #24292e; }
+pre:has(> code[class*="language-"]) { background: #f6f8fa; padding: 1em; }
+
 .site-title::after {
 	background-image: url("../../prooffrog.png");
 	width: 46px;

assets/js/prism-prooffrog.js

@@ -0,0 +1,43 @@
+// ── Prism.js language grammar for ProofFrog's FrogLang ──────────────────────
+// Defines Prism.languages.prooffrog for syntax highlighting FrogLang files
+// (.primitive, .scheme, .game, .proof).
+
+(function (Prism) {
+    Prism.languages.prooffrog = {
+        // Line comments: // to end of line
+        "comment": /\/\/.*/,
+
+        // Import path strings: single-quoted
+        "string": /'[^']*'/,
+
+        // Numbers: binary (0b...) and decimal
+        "number": /\b0b[01]+\b|\b\d+\b/,
+
+        // Built-in type names
+        "builtin": /\b(?:Bool|Void|Int|BitString|Set|Map|Array)\b/,
+
+        // Boolean literals
+        "boolean": /\b(?:true|false)\b/,
+
+        // None literal
+        "constant": /\bNone\b/,
+
+        // Declaration keywords (top-level construct introducers)
+        "class-name": /\b(?:Primitive|Scheme|Game|Reduction|Phase)\b/,
+
+        // Keywords
+        "keyword": /\b(?:import|export|as|extends|compose|against|requires|if|else|for|return|in|to|union|subsets|induction|from|calls|Adversary|oracles|proof|let|assume|theorem|games)\b/,
+
+        // Operators (longest match first via alternation order)
+        "operator": /<-|[=!<>]=|&&|\|\||[+\-*\/\\|!<>=]/,
+
+        // Punctuation
+        "punctuation": /[{}[\]();:,.?]/,
+    };
+
+    // Register for all FrogLang file extensions
+    Prism.languages.primitive = Prism.languages.prooffrog;
+    Prism.languages.scheme = Prism.languages.prooffrog;
+    Prism.languages.game = Prism.languages.prooffrog;
+    Prism.languages.proof = Prism.languages.prooffrog;
+})(Prism);

files/game.md

@@ -14,8 +14,8 @@ Finally, each game has the option to specify an `Initialize` method which is ass
 `Initialize` also has the ability to return information to the adversary that they may use during the attack (for example, adversaries should be provided the public key when attacking public key encryption).
 An example of a game file defining CPA security for symmetric encryption schemes is provided below.
 
-```
-import 'examples/Primitives/SymEnc.primitive';
+```prooffrog
+import 'Primitives/SymEnc.primitive';
 
 Game Left(SymEnc E) {
     E.Key k;

files/primitive.md

@@ -12,7 +12,7 @@ A primitive file allows a user to describe the sets and functions that are assoc
 A primitive contains constant fields and method signatures.
 An example of a primitive for an abstract symmetric encryption scheme is shown below.
 
-```
+```prooffrog
 Primitive SymEnc(Set MessageSpace, Set CiphertextSpace, Set KeySpace) {
     Set Message = MessageSpace;
     Set Ciphertext = CiphertextSpace;

files/proof.md

@@ -16,10 +16,10 @@ Each game in the sequence is checked to be either interchangeable with the next
 Indistinguishability only occurs if the author writes a reduction to utilize a previously specified indistinguishability assumption.
 An example proof file is shown below, which ProofFrog can verify to show that CPA$ security for a symmetric encryption scheme implies CPA security.
 
-```
-import 'examples/Primitives/SymEnc.primitive';
-import 'examples/Games/SymEnc/CPA.game';
-import 'examples/Games/SymEnc/CPA$.game';
+```prooffrog
+import 'Primitives/SymEnc.primitive';
+import 'Games/SymEnc/CPA.game';
+import 'Games/SymEnc/CPA$.game';
 
 Reduction R1(SymEnc E) compose CPA$(E) against CPA(E).Adversary {
     E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {

files/scheme.md

@@ -12,8 +12,8 @@ Each scheme file provides one scheme which "extends" from a primitive.
 A scheme must define the same fields as the primitive it extends, and provide definitions for each primitive method signature.
 An example of a scheme for a symmetric encryption scheme composed from two other symmeteric encryption schemes is shown below.
 
-```
-import 'examples/Primitives/SymEnc.primitive';
+```prooffrog
+import 'Primitives/SymEnc.primitive';
 
 Scheme DoubleSymEnc(SymEnc S, SymEnc T) extends SymEnc {
     requires S.Ciphertext == T.Message;