feat(use): run a contract's execution plan with the vLLM backend

README.md

@@ -81,7 +81,7 @@ Python workers do the heavy computation: vLLM generates and Hugging Face trains
 | `invar compare numerical`, `invar score` | take the measurements above |
 | `invar use prepare` | build a use contract from the owner's declaration |
 | `invar use plan` | estimate the sample size a contract needs under stated assumptions |
-| `invar use run` | run a contract's finite execution plan on Apple Silicon and keep every record |
+| `invar use run` | run a contract's finite execution plan with the MLX or vLLM backend and keep every record |
 | `invar use admit` | decide admission under a use contract |
 | `invar compare histories` | check that two runs which scheduled their work differently published the same policies |
 

app/UseExecution.hs

@@ -29,7 +29,7 @@ decode document =
     top = L.root "execution"
     text fields name = L.field "invalid-value" top fields name `andThen` L.text "invalid-value" (L.child top name)
     formatted fields = text fields "format" `andThen` \found -> if found == "invar-use-execution-v1" then value () else problem "invalid-value" (L.render (L.child top "format")) "Expected invar-use-execution-v1"
-    supported found = if found == "mlx" then value found else problem "unsupported" (L.render (L.child top "backend")) "Only the mlx backend can run a contract"
+    supported found = if found `elem` ["mlx", "vllm"] then value found else problem "unsupported" (L.render (L.child top "backend")) "Only the mlx and vllm backends can run a contract"
     side fields name =
         let sides = L.child top "sides"
             path = L.child sides name

docs/guides/walkthrough.md

@@ -75,6 +75,8 @@ EOF
 
 Relative paths in `execution.json` resolve from its own directory.
 
+On a CUDA host the plan names the `vllm` backend, `entries/vllmbatch.py` as each side's worker and the vLLM launch file as its configuration; the remaining steps are the same.
+
 ## Prepare
 
 ```sh