Fix refactor crypto performance

.github/workflows/continuousIntegration.yml

@@ -64,6 +64,10 @@ jobs:
             test-dir: tests/smt
           - name: other
             test-dir: tests/error tests/froglet tests/srclocs tests/temporal
+          - name: custom-solver
+            test-dir: tests/forge/custom-solver
+            custom-run: true
+
     name: test-${{ matrix.name }}
     steps:
     - name: Checkout repo
@@ -106,7 +110,83 @@ jobs:
     - name: Run tests
       run: |
         cd forge/
-        chmod +x run-tests.sh
-        for dir in ${{ matrix.test-dir }}; do
-          ./run-tests.sh "$dir"
-        done
+        if [ "${{ matrix.custom-run }}" = "true" ]; then
+          cd ${{ matrix.test-dir }}
+          chmod +x run.sh subdir/run.sh
+          exitCode=0
+          for f in *.frg; do
+            echo "Running $f..."
+            if ! racket "$f" -O run_sterling 'off'; then
+              echo "FAILED: $f"
+              exitCode=1
+            fi
+          done
+          exit $exitCode
+        else
+          chmod +x run-tests.sh
+          for dir in ${{ matrix.test-dir }}; do
+            ./run-tests.sh "$dir"
+          done
+        fi
+
+  test-custom-solver-win:
+    needs: check-test-coverage
+    runs-on: windows-latest
+    name: test-custom-solver-win
+    steps:
+    - name: Checkout repo
+      uses: actions/checkout@v4
+
+    - name: Setup Racket
+      uses: Bogdanp/setup-racket@v1.14
+      with:
+        version: '8.15'
+
+    - name: Setup Java
+      uses: actions/setup-java@v4
+      with:
+        distribution: 'temurin'
+        java-version: '17'
+
+    - name: Cache Racket packages
+      uses: actions/cache@v4
+      with:
+        path: ~/AppData/Roaming/Racket
+        key: racket-pkgs-win-${{ hashFiles('forge/info.rkt') }}
+        restore-keys: racket-pkgs-win-
+
+    - name: Install Forge
+      run: |
+        raco pkg update --auto --no-docs --batch ./forge 2>$null; if ($LASTEXITCODE -ne 0) { raco pkg install --auto --no-docs ./forge }
+
+    - name: Run custom solver tests
+      shell: cmd
+      run: |
+        cd forge\tests\forge\custom-solver\win
+        set exitCode=0
+        for %%f in (*.frg) do (
+          echo Running %%f...
+          racket "%%f" -O run_sterling 'off'
+          if errorlevel 1 (
+            echo FAILED: %%f
+            set exitCode=1
+          )
+        )
+        exit /b %exitCode%
+
+    - name: Run custom solver tests (path with spaces)
+      shell: cmd
+      run: |
+        mkdir "forge\tests\forge\custom-solver\win space test"
+        xcopy /s /e /i "forge\tests\forge\custom-solver\win" "forge\tests\forge\custom-solver\win space test"
+        cd "forge\tests\forge\custom-solver\win space test"
+        set exitCode=0
+        for %%f in (*.frg) do (
+          echo Running %%f [space path]...
+          racket "%%f" -O run_sterling 'off'
+          if errorlevel 1 (
+            echo FAILED: %%f
+            set exitCode=1
+          )
+        )
+        exit /b %exitCode%

forge/domains/crypto/README.md

@@ -84,6 +84,14 @@ Forge does _bounded_ model finding; that is, it renders the search problem decid
 
 E.g., we might say that there are no more than `3` names in an execution of the reflection protocol: the initiator's name, the responder's name, and the attacker's name. (The attacker must be present, as the model follows Dolev-Yao is making them the medium by which principles communicate.)
 
+#### Time
+
+The model has two different notions of time:
+  - The `Timeslot` sig, which represents the handling of a single message. This should always be either sent or received by the `Attacker`, who is synonymous with the medium of communication.
+  - The `Microtick` sig, which is used to properly order how agents learn values within nested encrypted terms. The scope for `Microtick` should never be lower than `2`, representing the pre-state where nothing has yet been learned and the post-state where a single layer of encryption has been removed. If a protocol requires deeper nesting, increment the scope on `Microtick` to one more than the nesting depth.
+
+Note that the `Microtick` sig was not present in the original paper, which used the `Timeslot` sig for both kinds of "time", resulting in poor performance.
+
 ### Visualizing Executions 
 
 When Sterling opens, the solver will (perhaps after some delay) produce an instance. The default visualization will appear as a dense cluster of boxes and lines. To switch to the sequence diagram version, click on the 'Script' tab and paste in the contents of the [visualization script](./vis/crypto_viz.js). Then click 'Run'. 

forge/domains/crypto/base.frg

@@ -20,6 +20,12 @@
       as the protocol role execution.
     - This model embraces Dolev-Yao in a very concrete way: there is an explicit 
       attacker, who is also the medium of communication between participants.
+
+  Fall 2025 update:
+    - This model had previously used the `Timeslot` sig for both states between 
+      messages _and_ microticks (which allow "learning" within nested encrypted terms).
+      Instead, the model now uses a subset of the available time slots according to 
+      the user-provided scope on the `Microtick` sig.
 */
 
 -- NOTE WELL: `mesg` is what CPSA calls terms; we echo that here, do not confuse 
@@ -36,6 +42,7 @@ sig PublicKey extends akey {}
 one sig KeyPairs {
   pairs: set PrivateKey -> PublicKey,
   owners: func PrivateKey -> name,
+  -- There may be LTKs that aren't pre-assigned to a pair of agents. E.g., session keys.
   ltks: set name -> name -> skey
 }
 
@@ -54,8 +61,9 @@ fun getInv[k: Key]: one Key {
 }
 
 
--- Time indexes (t=0, t=1, ...). These are also used as micro-tick indexes, so the 
--- bound on `Timeslot` will also affect how many microticks are available between ticks.
+/** Time indexes corresponding to one message being sent and received.
+    Dropped messages are modeled as the medium receiving the message but 
+    not forwarding it. */
 sig Timeslot {
   -- structure of time (must be rendered linear in every run via `next is linear`)
   next: lone Timeslot,
@@ -67,7 +75,16 @@ sig Timeslot {
 
   -- relation is: Tick x Microtick x learned-mesg
   -- Only one agent per tick is receiving, so always know which agent's workspace it is
-  workspace: set Timeslot -> mesg
+  workspace: set Microtick -> mesg
+}
+
+/** A Microtick represents a step of _learning_ that is part of processing a single 
+    message reception. */
+sig Microtick {
+  -- structure of microticks. (must be rendered linear in every run via `next is linear`)
+  -- The `wellformed` predicate below contains constraints that enforce this, in case 
+  -- a user forgets the add the linear annotation, but doing so would harm performance. 
+  mt_next: lone Microtick
 }
 
 -- As names process received messages, they learn pieces of data
@@ -89,7 +106,7 @@ one sig Attacker extends name {}
 sig Ciphertext extends mesg {
    -- encrypted with this key
    encryptionKey: one Key,
-   -- result in concating plaintexts
+   -- concatenated plaintexts (order not currently modeled)
    plaintext: set mesg
 }
 
@@ -111,11 +128,29 @@ fun baseKnown[a: name]: set mesg {
     a
 }
 
+/** Time and micro-time are ordered. 
+    (This constraint should be tautologous if the user has given an `is linear` 
+    for `next` and `mt_next`.) */
+pred timeSafety {
+  some firstTimeslot: Timeslot | {
+    all ts: Timeslot | ts in firstTimeslot.*next
+    no firstTimeslot.~next
+    -- field declaration ensures at most one successor
+  }
+  some firstMicro: Microtick | {
+    all ts: Microtick  | ts in firstMicro.*mt_next
+    no firstMicro.~mt_next
+    -- field declaration ensures at most one successor
+  }
+}
+
 /** This (large) predicate contains the vast majority of domain axioms */
 pred wellformed {
   -- Design choice: only one message event per timeslot;
   --   assume we have a shared notion of time
-
+
+  timeSafety
+
   -- You cannot send a message with no data
   all m: Timeslot | some m.data
 
@@ -124,10 +159,10 @@ pred wellformed {
 
   -- workspace: workaround to avoid cyclic justification within just deconstructions
   -- AGENT -> TICK -> MICRO-TICK LEARNED_SUBTERM
-  all d: mesg | all t, microt: Timeslot | let a = t.receiver.agent | d in (workspace[t])[microt] iff {
+  all d: mesg | all t: Timeslot, microt: Microtick | let a = t.receiver.agent | d in (workspace[t])[microt] iff {
     -- Base case:
-    -- received the data in the clear just now 
-    {d in t.data and no microt.~next}
+    -- received the data in the clear just now (first microtick)
+    {d in t.data and no microt.~mt_next}
     or
     -- Inductive case:
     -- breaking down a ciphertext we learned *previously*, or that we've produced from 
@@ -139,11 +174,20 @@ pred wellformed {
     { 
       --d not in ((a.workspace)[t])[Timeslot - microt.^next] and -- first time appearing
       {some superterm : Ciphertext | {      
-      d in superterm.plaintext and     
-      superterm in (a.learned_times).(Timeslot - t.*next) + workspace[t][Timeslot - microt.*next] + baseKnown[a] and
-      getInv[superterm.encryptionKey] in (a.learned_times).(Timeslot - t.*next) + workspace[t][Timeslot - microt.*next] + baseKnown[a]
+           -- the term in question is contained within superterm
+           d in superterm.plaintext 
+           and     
+           -- we had learned the superterm in a previous timeslot or previous microtick in this timeslot
+           superterm in (a.learned_times).(Timeslot - t.*next) + 
+                        workspace[t][Microtick - microt.*mt_next] + 
+                        baseKnown[a] 
+           and
+           -- we had also learned how to decrypt the superterm previously
+           getInv[superterm.encryptionKey] in (a.learned_times).(Timeslot - t.*next) + 
+                                              workspace[t][Microtick - microt.*mt_next] + 
+                                              baseKnown[a]
     }}}
-  }
+  } -- end block for workspace 
 
   -- names only learn information that associated strands are explicitly sent 
   -- (start big disjunction for learned_times)
@@ -166,7 +210,7 @@ pred wellformed {
     -- consider: (k1, enc(k2, enc(n1, invk(k2)), invk(k1)))
     -- or, worse: (k1, enc(x, invk(k3)), enc(k2, enc(k3, invk(k2)), invk(k1)))
     { t.receiver.agent = a
-      d in workspace[t][Timeslot] -- derived in any micro-tick in this (reception) timeslot
+      d in workspace[t][Microtick] -- derived in any micro-tick in this (reception) timeslot
     }   
     or 
     -- construct encrypted terms (only allow at NON-reception time; see above)
@@ -190,7 +234,8 @@ pred wellformed {
 
   -- Messages comprise only values known by the sender
   all m: Timeslot | m.data in (((m.sender).agent).learned_times).(Timeslot - m.^next) 
-  -- Always send or receive to the adversary
+
+  -- Always send or receive to the adversary (who is the "medium of communication")
   all m: Timeslot | m.sender = AttackerStrand or m.receiver = AttackerStrand 
 
   -- plaintext relation is acyclic  

forge/domains/crypto/examples/blanchet-corrected.frg

@@ -0,0 +1,122 @@
+#lang forge
+
+// Protocol definitions in CPSA DSL
+open "blanchet-corrected.rkt" 
+// Domain-specific visualizer script
+option run_sterling "../vis/crypto_viz.js"
+
+pred blanchet_corrected_run {
+    exec_blanchet_corrected_init
+    exec_blanchet_corrected_resp
+
+    -- Do not run more than one skeleton at a time.
+    -- constrain_skeleton_blanchet_0  -- init strand perspective 
+    -- constrain_skeleton_blanchet_1  -- sat by self
+
+    -- This contains a "listener strand", which the expander turns into 
+    -- #`(in (join #,this-strand-or-skeleton #,(id-converter pname strand-role-or-skeleton-idx v))
+    --           (join Attacker learned_times Timeslot)))
+    -- That is: the attacker learns the value of this strand variable at some point in time.
+    --  (It does NOT create a separate listener strand, it just checks the attacker's knowledge base.)
+    constrain_skeleton_blanchet_corrected_2 -- responder strand perspective (with 1 commented out skeleton)
+
+    wellformed
+}
+
+/** The attacker has no long-term keys. */
+pred atk_no_ltks {
+   // KeyPairs.ltks:  set name -> name -> skey
+
+    no Attacker.(KeyPairs.ltks)
+    // Simplified from:
+    //(no (+ (join Attacker (join name     (join KeyPairs ltks)))
+    //       (join name     (join Attacker (join KeyPairs ltks)))))
+}
+
+
+// Bounds can be quite troublesome. Count carefully.
+run {
+    blanchet_corrected_run
+    atk_no_ltks
+
+    // The attacker is not playing a game by themselves
+    // It's unclear if this should just be a base assumption. But we do want the attacker to
+    // be able to own multiple strands. 
+    blanchet_corrected_init.agent != Attacker
+    blanchet_corrected_resp.agent != Attacker
+
+    // The keys used by the initiator are of the proper types. The CPSA definition just says they are 
+    // asymmetric keys, not that (e.g.) the outermost encryption key was a public key.
+    blanchet_corrected_init.blanchet_corrected_init_a in PublicKey
+    blanchet_corrected_init.blanchet_corrected_init_b in PublicKey
+
+    // The symmetric key sent is not pre-assigned to any agent pair. 
+    no KeyPairs.ltks.(blanchet_corrected_init.blanchet_corrected_init_s)
+
+
+} for exactly 1 KeyPairs, exactly 4 Timeslot,  20 mesg, 9 Key, 6 akey, 3 PrivateKey, 3 PublicKey, 
+              3 skey, 3 name, 1 Attacker, 3 text, exactly 5 Ciphertext, exactly 1 AttackerStrand, 
+              exactly 1 blanchet_corrected_init, exactly 1 blanchet_corrected_resp, exactly 3 strand, 
+              //exactly 1 skeleton_blanchet_0, 
+              //exactly 1 skeleton_blanchet_1, 
+              exactly 1 skeleton_blanchet_corrected_2
+
+              , 5 Int
+
+              , 3 Microtick
+
+  for {next is linear
+       mt_next is linear}
+
+    //   #:scope [(KeyPairs 1 1)
+    //            (Timeslot 4 4) 
+    //            (Message 4 4)
+
+    //            (mesg 20) ; 9 + 3 + 3 + 5
+
+    //            (Key 9)
+    //            (akey 6)               
+    //            (PrivateKey 3)
+    //            (PublicKey 3)
+    //            (skey 3)
+
+    //            (name 3)
+    //            (Attacker 1 1)
+
+    //            (text 3) ; includes data
+
+    //            (Ciphertext 5 5)               
+
+    //            (AttackerStrand 1 1)               
+    //            (blanchet_init 1 1)
+    //            (blanchet_resp 1 1)               
+    //            (strand 3 3)
+
+    //            (skeleton_blanchet_0 1 1)
+    //            (skeleton_blanchet_1 1 1)
+    //            (skeleton_blanchet_2 1 1)               
+    //            (Int 5)
+    //            ]
+    //   ;#:expect sat
+    //   )
+
+
+
+/*
+
+(defprotocol blanchet basic             OS-EPL term count, if all distinct (recall inv denotes counterpart keys)
+  (defrole init                         ------------------------
+    (vars (a b akey) (s skey) (d data)) + 4 akey, 1 skey, 1 data
+    (trace
+     (send (enc (enc s (invk a)) b))    + 2 ciphertext
+     (recv (enc d s)))                  + 1 ciphertext
+    (uniq-orig s))
+  (defrole resp
+    (vars (a b akey) (s skey) (d data)) + 4 akey, 1 skey, 1 data
+    (trace
+     (recv (enc (enc s (invk a)) b))    + 2 ciphertext
+     (send (enc d s)))                  + 1 ciphertext
+    (uniq-orig d))                      ------------------------
+  (comment "Blanchet's protocol"))        8 akey, 2 skey, 2 data, 6 ciphertext
+
+*/