fix(z3): preserve implies args, multi-level field access, len(), nil, distinct operator

Z3 expression translator fixes:
- implies(x, y) now preserves both arguments (was dropping both → (=> true true))
- Multi-level field access m.price.amount → m_price_amount (was m_price.(>= amount 0))
- len() now handled same as length() (was left as bare len())
- nil/null translated to speckl_nil sentinel constant
- != now properly converts to (distinct X Y) via convertToPrefix (was bare 'distinct')
- Added 'distinct' as binary operator in convertToPrefix
- speckl_nil declared as Int constant in output

All 8 product spec constraints now produce valid SMT-LIB2.
57/57 tests pass.

compiler/dist/parser.js

@@ -51,15 +51,13 @@ function parseSpeck(lines, startIndex) {
         return null;
     const name = headerMatch[1];
     const members = [];
-    // Cycle 61: clear static metadata fields at the start of each parse
-    // so per-speck directives don't leak between parse calls. This is the
-    // pre-existing static-field-hack pattern for proto_package / go_package
-    // (see spec-compiler-dogfood skill anti-pattern). Refactoring to a
-    // local-object approach is tracked as a separate cleanup; for now
-    // resetting the fields here is the minimal-touch fix.
-    parseSpeck._protoPackage = undefined;
-    parseSpeck._goPackage = undefined;
-    parseSpeck._eventSuffix = undefined;
+    // Cycle 73: refactored from static-field hack to local-object pattern.
+    // Previously, proto_package / go_package / event_suffix were stored
+    // on (parseSpeck as any)._protoPackage etc — static function fields
+    // that leaked between parse calls. Now collected in a local metadata
+    // object and spread into the return value. No reset needed because
+    // the object is local to this invocation.
+    const metadata = {};
     let i = startIndex + 1;
     let braceCount = 1;
     while (i < lines.length && braceCount > 0) {
@@ -80,13 +78,13 @@ function parseSpeck(lines, startIndex) {
             // Strip surrounding quotes if present
             const value = metaMatch[2].trim().replace(/^['"]|['"]$/g, '');
             if (metaMatch[1] === 'proto_package') {
-                parseSpeck._protoPackage = value;
+                metadata.protoPackage = value;
             }
             else if (metaMatch[1] === 'go_package') {
-                parseSpeck._goPackage = value;
+                metadata.goPackage = value;
             }
             else if (metaMatch[1] === 'event_suffix') {
-                parseSpeck._eventSuffix = value;
+                metadata.eventSuffix = value;
             }
             i++;
             continue;
@@ -154,9 +152,9 @@ function parseSpeck(lines, startIndex) {
         i++;
     }
     return { type: 'speck', name, members,
-        protoPackage: parseSpeck._protoPackage,
-        goPackage: parseSpeck._goPackage,
-        eventSuffix: parseSpeck._eventSuffix };
+        protoPackage: metadata.protoPackage,
+        goPackage: metadata.goPackage,
+        eventSuffix: metadata.eventSuffix };
 }
 function findBlockEnd(lines, startIndex, startBraceCount) {
     let braceCount = startBraceCount;

compiler/node_modules/.vite/vitest/results.json

@@ -1 +1 @@
-{"version":"2.1.9","results":[[":__tests__/parser.test.ts",{"duration":31.455063999999993,"failed":false}],[":src/__tests__/compiler.test.ts",{"duration":12.627537000000018,"failed":false}]]}
+{"version":"2.1.9","results":[[":__tests__/parser.test.ts",{"duration":54.53141900000003,"failed":false}],[":src/__tests__/compiler.test.ts",{"duration":15.892710999999963,"failed":false}]]}

compiler/src/generators/z3.ts

@@ -91,6 +91,8 @@ function emitZ3(speck: SpeckNode, options: Z3Options): string {
   // Declare Speckl helper functions
   // speckl_len: length of Array-simulated sequences
   lines.push('(declare-fun speckl_len_Int ( (Array Int Int) ) Int)');
+  // speckl_nil: sentinel for nil/null comparisons (SpeckDL nil → Z3 constant)
+  lines.push('(declare-const speckl_nil Int)');
 
   // Step 1: Declare sorts for record types
   const recordTypes = collectRecordTypes(stateNode, actions);
@@ -428,35 +430,38 @@ function translateExpr(expr: string, stateVars: StateVar[], suffix: string): str
   // Handle prime notation for post-state: currentTerm' → currentTerm_post (invariant comparison)
   e = e.replace(/\b(\w+)'/g, '$1_post');
 
-  // Handle implies(x, y) function call pattern
-  e = e.replace(/implies\s*\(([^,)]+),\s*([^)]+)\)/g, '(=>  )');
-  // Handle bare implies keyword at top level
-  // Handle bare implies as SMT-LIB2 =>
-  // First, handle implies at top level of a line (no paren after second arg)
-  e = e.replace(/\bimplies\s+([^ ]+)\s+([^)]+)\)?/g, '(=>  )');
-  // Clean up (=> ) empty cases
-  e = e.replace(/(=>\s*)/g, '(=> true true)');
+  // Handle implies(x, y) function call pattern — preserve both arguments
+  e = e.replace(/implies\s*\(([^,)]+),\s*([^)]+)\)/g, '(=> $1 $2)');
+  // Handle bare implies keyword: implies A B → (=> A B)
+  e = e.replace(/\bimplies\s+([^\s]+)\s+(.+)$/g, '(=> $1 $2)');
 
   // Handle -> as implication (after field access cleanup to avoid false matches)// Handle -> as implication (after field access cleanup to avoid false matches)
   e = e.replace(/->/g, '=>');
 
-  // Handle function calls: length(expr), min(a,b), etc.
+  // Handle function calls: length(expr), len(expr), min(a,b), etc.
   e = e.replace(/\blength\(([^)]+)\)/g, 'len__$1__xx');  // marker, fix later
+  e = e.replace(/\blen\(([^)]+)\)/g, 'len__$1__xx');  // marker, fix later
   e = e.replace(/\bmin\(([^,)]+),\s*([^)]+)\)/g, 'min__$1__$2__xx');
 
-  // Field access: a.balance → balance (drop qualifier for bound forall vars)
-  // For record fields accessed via dot, translate to Z3-safe names
-  e = e.replace(/(\w+)\.([\w_]+)/g, (_, obj, field) => {
-    // If the object is a state variable (map), .field is an accessor we can't resolve
-    // For bound forall variables, just use the field name
-    if (stateVarNames.has(obj)) {
-      // Accessing field on opaque sort — use a compound name
-      return `${obj}_${field}`;
+  // Field access: a.b.c → a_b_c (flatten all dot levels in one pass)
+  // For record fields accessed via dot, translate to Z3-safe compound names.
+  // Multi-level: m.price.amount → m_price_amount
+  e = e.replace(/(\w+)\.(\w+)(\.(\w+))*/g, (match, obj, field1, rest, field2) => {
+    if (rest) {
+      // Multi-level: m.price.amount → m_price_amount
+      return `${obj}_${field1}_${field2}`;
     }
-    // For bound variables in forall, just emit the field
-    return `${obj}_${field}`;
+    return `${obj}_${field1}`;
   });
 
+  // Handle nil → Z3 doesn't have nil/null. Translate to a sentinel:
+  // x != nil → (distinct x nil_sentinel) — but for Z3 we'll use a special value.
+  // For record types (opaque sorts), nil means "no value". We'll use a declared
+  // constant `nil` of a generic sort. For Int fields, nil = -1 sentinel.
+  // Simplest approach: translate nil to a Z3 declared constant `speckl_nil`.
+  e = e.replace(/\bnil\b/g, 'speckl_nil');
+  e = e.replace(/\bnull\b/g, 'speckl_nil');
+
   // Handle notIn BEFORE general patterns
   e = e.replace(/(\S+)\s+notIn\s+(\S+)\.keys/g, '(not (select $2 $1))');
 
@@ -540,8 +545,9 @@ function translateExpr(expr: string, stateVars: StateVar[], suffix: string): str
   e = e.replace(/__GE__/g, '>=');
   e = e.replace(/__LE__/g, '<=');
 
-  // Wrap distinct
-  e = e.replace(/\bdistinct\s+(\S+)\s+(\S+)/g, '(distinct $1 $2)');
+  // Wrap distinct: X distinct Y → (distinct X Y)
+  // Handle both simple identifiers and parenthesized expressions
+  e = e.replace(/(\b\w+|\([^()]+\))\s+distinct\s+(\b\w+|\([^()]+\))/g, '(distinct $1 $2)');
 
   // Fix remaining infix operators that escaped convertToPrefix
   // word = word/val: convert to (= word val)
@@ -568,6 +574,7 @@ function restoreStrings(expr: string, strings: string[]): string {
  */
 function convertToPrefix(expr: string): string {
   expr = convertOp(expr, '=>', '=>');
+  expr = convertOp(expr, 'distinct', 'distinct');
   expr = convertOp(expr, 'and', 'and');
   expr = convertOp(expr, 'or', 'or');
   expr = convertOp(expr, '=', '=');

compiler/test-ast.mjs

@@ -0,0 +1,16 @@
+import { parseSpeckFile } from './dist/parser.js';
+import fs from 'fs';
+
+const ast = parseSpeckFile('/home/sscoble/speckl/examples/Raft.speck');
+for (const speck of ast.specks) {
+  for (const m of speck.members) {
+    if (m.type === 'action') {
+      for (const s of (m.statements || [])) {
+        if (s.type === 'ifblock') {
+          console.log('--- ifblock in', m.name, '---');
+          console.log('raw:', s.raw.substring(0, 200));
+        }
+      }
+    }
+  }
+}

compiler/test-output/RetryHandler.prov.jsonld

@@ -12,7 +12,7 @@
         "@type": "prov:Generation",
         "prov:activity": {
           "@type": "prov:Activity",
-          "prov:startTime": "2026-05-11T17:13:39.546Z"
+          "prov:startTime": "2026-06-30T00:31:19.971Z"
         }
       },
       "rdfs:label": "RetryHandler",

compiler/test-output/RetryHandler.specbom.cdx.json

@@ -38,7 +38,7 @@
         "name": "Scott Scoble",
         "email": "scott@scoble.me"
       },
-      "timestamp": "2026-05-11T17:13:39.549Z"
+      "timestamp": "2026-06-30T00:31:19.973Z"
     },
     {
       "subject": "speck:RetryHandler",
@@ -53,7 +53,7 @@
         "name": "Speckl Compiler",
         "email": "compiler@speckl.scoble.me"
       },
-      "timestamp": "2026-05-11T17:13:39.549Z"
+      "timestamp": "2026-06-30T00:31:19.974Z"
     },
     {
       "subject": "speck:RetryHandler",
@@ -68,7 +68,7 @@
         "name": "Speckl Compiler",
         "email": "compiler@speckl.scoble.me"
       },
-      "timestamp": "2026-05-11T17:13:39.549Z"
+      "timestamp": "2026-06-30T00:31:19.974Z"
     }
   ]
 }

compiler/test-output/RetryHandler.specbom.spdx.json

@@ -13,7 +13,7 @@
     "spdxVersion": "3.0.1",
     "dataLicense": "CC0-1.0",
     "creationInfo": {
-      "created": "2026-05-11T17:13:39.551Z",
+      "created": "2026-06-30T00:31:19.976Z",
       "createdBy": [
         "Organization: Speckl",
         "tool: speckl-compile-0.2.0"
@@ -27,7 +27,7 @@
           "@type": "spdx:Tool",
           "name": "speckl-compile"
         },
-        "timestamp": "2026-05-11T17:13:39.551Z",
+        "timestamp": "2026-06-30T00:31:19.976Z",
         "comment": "Review type: manual"
       }
     ]

compiler/test-parser.mjs

@@ -0,0 +1,22 @@
+import { parseActionStatements } from './dist/expr/stmt-parser.js';
+
+const tests = [
+  ['serverState[voter].currentTerm := req.term'],
+  ['let newTerm := 5', 'newTerm := 6'],
+  ['require foo == bar'],
+  ['return 5'],
+  ['emit VoteGranted { voter: voter, candidate: 1, term: 2 }'],
+  ['if foo { x := 1 } else { y := 2 }'],
+  ['x := 1', 'y := 2', 'return 5'],
+];
+
+for (const lines of tests) {
+  console.log('---');
+  console.log('input:', lines);
+  try {
+    const out = parseActionStatements(lines);
+    console.log('output:', JSON.stringify(out, null, 2).substring(0, 700));
+  } catch (e) {
+    console.log('error:', e.message);
+  }
+}

out_fresh/OAuth2AuthorizationCode.prov.jsonld

@@ -0,0 +1,21 @@
+{
+  "@context": {
+    "prov": "http://www.w3.org/ns/prov#",
+    "speckl": "https://speckl.scoble.me/ns/v0.2#",
+    "rdfs": "http://www.w3.org/2000/01/rdf-schema#"
+  },
+  "@graph": [
+    {
+      "@type": "prov:Entity",
+      "@id": "speck:OAuth2AuthorizationCode",
+      "prov:qualifiedGeneration": {
+        "@type": "prov:Generation",
+        "prov:activity": {
+          "@type": "prov:Activity",
+          "prov:startTime": "2026-06-08T14:27:09.658Z"
+        }
+      },
+      "rdfs:label": "OAuth2AuthorizationCode"
+    }
+  ]
+}

out_fresh/OAuth2AuthorizationCode.specbom.cdx.json

@@ -0,0 +1,15 @@
+{
+  "bomFormat": "CycloneDX",
+  "specVersion": "1.6",
+  "components": [],
+  "metadata": {
+    "tools": [],
+    "component": {
+      "type": "application",
+      "name": "OAuth2AuthorizationCode",
+      "version": "0.2.0",
+      "properties": []
+    }
+  },
+  "annotations": []
+}

out_fresh/OAuth2AuthorizationCode.specbom.spdx.json

@@ -0,0 +1,26 @@
+{
+  "@context": [
+    "https://spdx.github.io/spdx-v3/spdx-context.jsonld",
+    {
+      "speckl": "https://speckl.scoble.me/ns/v0.2#"
+    }
+  ],
+  "@type": "spdx:Document",
+  "spdx": {
+    "@id": "spdx:OAuth2AuthorizationCode",
+    "@type": "spdx:Snippet",
+    "name": "OAuth2AuthorizationCode",
+    "spdxVersion": "3.0.1",
+    "dataLicense": "CC0-1.0",
+    "creationInfo": {
+      "created": "2026-06-08T14:27:09.674Z",
+      "createdBy": [
+        "Organization: Speckl",
+        "tool: speckl-compile-0.2.0"
+      ]
+    }
+  },
+  "builtBy": [],
+  "relationships": [],
+  "elements": []
+}

out_fresh/OAuth2AuthorizationCode.ts

@@ -0,0 +1,192 @@
+// Auto-generated by speckl-compile from OAuth2AuthorizationCode
+// DO NOT EDIT MANUALLY — regenerate from .speckdl source
+
+export const OAuth2AuthorizationCodeOAuth2AuthorizationCodeState = {
+  Open: 'open',
+  Closed: 'closed',
+} as const;
+export type OAuth2AuthorizationCodeOAuth2AuthorizationCodeState = typeof OAuth2AuthorizationCodeOAuth2AuthorizationCodeState[keyof typeof OAuth2AuthorizationCodeOAuth2AuthorizationCodeState];
+
+
+
+// Simple hash utility for SpeckDL hash() function
+// In production, replace with a real crypto hash
+function simpleHash(s: string, method?: string): string {
+  let h = 0;
+  for (let i = 0; i < s.length; i++) {
+    h = ((h << 5) - h + s.charCodeAt(i)) | 0;
+  }
+  return 'h_' + Math.abs(h).toString(16);
+}
+
+
+// Runtime type placeholders (opaque record types)
+type AccessToken = any;
+type AuthorizationCode = any;
+type Bool }) = any;
+type ClientId = any;
+type ClientSecret = any;
+type CodeChallenge = any;
+type CodeVerifier = any;
+type Map(AccessToken, { client_id: ClientId = any;
+type Map(AuthorizationCode, { client_id: ClientId = any;
+type Map(RefreshToken, { client_id: ClientId = any;
+type Nat }) = any;
+type RedirectUri = any;
+type RefreshRequest = any;
+type RefreshToken }) = any;
+type Scope = any;
+type SessionId = any;
+type State = any;
+type TokenRequest = any;
+type UserId = any;
+
+export class OAuth2AuthorizationCodeMachine {
+  clients!: Map<ClientId, { redirect_uris: Set<RedirectUri>; client_secret: ClientSecret }>;
+  authorizationCodes!: Map(AuthorizationCode, { client_id: ClientId;
+  redirect_uri!: RedirectUri;
+  state!: State;
+  code_challenge!: CodeChallenge;
+  code_challenge_method!: string;
+  scope!: Scope;
+  user_id!: UserId;
+  session_id!: SessionId;
+  created_at!: number;
+  used!: Bool });
+  accessTokens!: Map(AccessToken, { client_id: ClientId;
+  user_id!: UserId;
+  scope!: Scope;
+  expires_at!: number;
+  session_id!: SessionId;
+  refresh_token!: RefreshToken });
+  refreshTokens!: Map(RefreshToken, { client_id: ClientId;
+  user_id!: UserId;
+  scope!: Scope;
+  access_token!: AccessToken;
+  created_at!: Nat });
+  sessions!: Map<SessionId, { user_id: UserId }>;
+  stateNonces!: Map<State, { client_id: ClientId; redirect_uri: RedirectUri }>;
+  pkceChallenges!: Map<CodeChallenge, { code_verifier_hash: string; method: string }>;
+  currentTime!: number;
+  decisionLog: any[] = [];
+
+  constructor() {
+    // No init block defined
+  }
+
+  Authorize(client: ClientId, redirectUri: RedirectUri, scope: Scope, userId: UserId, sessionId: SessionId) {
+    const xxx: any = {} as any;  // FIXME: parser dropped let/forall
+    const client_id: any = {} as any;  // FIXME: parser dropped let/forall
+    const code_verifier_hash: any = {} as any;  // FIXME: parser dropped let/forall
+    const __STR_LIT_0__: any = {} as any;  // FIXME: parser dropped let/forall
+    const method: any = {} as any;  // FIXME: parser dropped let/forall
+    const __STR_LIT_1__: any = {} as any;  // FIXME: parser dropped let/forall
+    if (!(this.clients.has(client))) throw new Error('Guard failed: this.clients.has(client)');
+    if (!(this.clients.get(client)!.redirect_uris.has(redirectUri))) throw new Error('Guard failed: this.clients.get(client)!.redirect_uris.has(redirectUri)');
+    if (!(this.sessions.has(sessionId))) throw new Error('Guard failed: this.sessions.has(sessionId)');
+    if (!(this.sessions.get(sessionId)!.user_id === userId)) throw new Error('Guard failed: this.sessions.get(sessionId)!.user_id === userId');
+    const state = "state_" + simpleHash(client + redirectUri + this.currentTime);
+    const codeVerifier = "verifier_" + simpleHash(client + userId + this.currentTime);
+    const codeChallenge = simpleHash(codeVerifier, "S256");
+    this.stateNonces.set(state, { client_id: client, redirect_uri: redirectUri });
+    this.pkceChallenges.set(codeChallenge, { code_verifier_hash: simpleHash(codeVerifier, __STR_LIT_0__), method: __STR_LIT_1__ });
+    const authCode = "code_" + simpleHash(client + userId + this.currentTime);
+    this.authorizationCodes.set(authCode, { client_id: client, redirect_uri: redirectUri, state: state, code_challenge: codeChallenge, code_challenge_method: __STR_LIT_0__, scope: scope, user_id: userId, session_id: sessionId, created_at: this.currentTime, used: false });
+  }
+
+  ApproveAuthorization(code: AuthorizationCode, userId: UserId) {
+    const xxx: any = {} as any;  // FIXME: parser dropped let/forall
+    if (!(this.authorizationCodes.has(code))) throw new Error('Guard failed: this.authorizationCodes.has(code)');
+    const c = this.authorizationCodes.get(code)!;
+    if (!(c.user_id === userId)) throw new Error('Guard failed: c.user_id === userId');
+    if (!(c.used === false)) throw new Error('Guard failed: c.used === false');
+  }
+
+  ExchangeCode(req: TokenRequest) {
+    const xxx: any = {} as any;  // FIXME: parser dropped let/forall
+    const client_id: any = {} as any;  // FIXME: parser dropped let/forall
+    if (!(this.clients.has(req.client_id))) throw new Error('Guard failed: this.clients.has(req.client_id)');
+    if (!(this.authorizationCodes.has(req.code))) throw new Error('Guard failed: this.authorizationCodes.has(req.code)');
+    const c = this.authorizationCodes.get(req.code)!;
+    if (!(c.used === false)) throw new Error('Guard failed: c.used === false');
+    if (!(c.client_id === req.client_id)) throw new Error('Guard failed: c.client_id === req.client_id');
+    if (!(c.redirect_uri === req.redirect_uri)) throw new Error('Guard failed: c.redirect_uri === req.redirect_uri');
+    const expectedChallenge = simpleHash(req.code_verifier, c.code_challenge_method);
+    if (!(expectedChallenge === c.code_challenge)) throw new Error('Guard failed: expectedChallenge === c.code_challenge');
+    this.pkceChallenges.delete(c.code_challenge);
+    this.stateNonces.delete(c.state);
+    const accessToken = "access_" + simpleHash(req.client_id + c.user_id + this.currentTime);
+    const refreshToken = "refresh_" + simpleHash(req.client_id + c.user_id + this.currentTime);
+    const expiresAt = this.currentTime + 3600;
+    this.accessTokens.set(accessToken, { client_id: req.client_id, user_id: c.user_id, scope: c.scope, expires_at: expiresAt, session_id: c.session_id, refresh_token: refreshToken });
+    this.refreshTokens.set(refreshToken, { client_id: req.client_id, user_id: c.user_id, scope: c.scope, access_token: accessToken, created_at: this.currentTime });
+  }
+
+  RefreshToken(req: RefreshRequest) {
+    const xxx: any = {} as any;  // FIXME: parser dropped let/forall
+    const client_id: any = {} as any;  // FIXME: parser dropped let/forall
+    if (!(this.clients.has(req.client_id))) throw new Error('Guard failed: this.clients.has(req.client_id)');
+    if (!(this.refreshTokens.has(req.refresh_token))) throw new Error('Guard failed: this.refreshTokens.has(req.refresh_token)');
+    const r = this.refreshTokens.get(req.refresh_token)!;
+    if (!(r.client_id === req.client_id)) throw new Error('Guard failed: r.client_id === req.client_id');
+    this.accessTokens.delete(r.access_token);
+    const newAccessToken = "access_" + simpleHash(req.client_id + r.user_id + this.currentTime);
+    const newRefreshToken = "refresh_" + simpleHash(req.client_id + r.user_id + this.currentTime);
+    const expiresAt = this.currentTime + 3600;
+    this.accessTokens.set(newAccessToken, { client_id: req.client_id, user_id: r.user_id, scope: req.scope.or(r.scope), expires_at: expiresAt, session_id: r.access_token.session_id, refresh_token: newRefreshToken });
+    this.refreshTokens.set(newRefreshToken, { client_id: req.client_id, user_id: r.user_id, scope: req.scope.or(r.scope), access_token: newAccessToken, created_at: this.currentTime });
+    this.refreshTokens.delete(req.refresh_token);
+  }
+
+  RevokeToken(client: ClientId, token: string, tokenType: string) {
+    const xxx: any = {} as any;  // FIXME: parser dropped let/forall
+    const t: any = {} as any;  // FIXME: parser dropped let/forall
+    const r: any = {} as any;  // FIXME: parser dropped let/forall
+    if (!(this.clients.has(client))) throw new Error('Guard failed: this.clients.has(client)');
+    if (tokenType === "access") {
+      if (!(this.accessTokens.has(token))) throw new Error('Guard failed: this.accessTokens.has(token)');
+      this.t = this.accessTokens.get(token)!;
+      if (!(t.client_id === client)) throw new Error('Guard failed: t.client_id === client');
+      this.s[token] = null;
+      this.s[t.refresh_token] = null;
+    } else {
+      if (tokenType === "refresh") {
+        if (!(this.refreshTokens.has(token))) throw new Error('Guard failed: this.refreshTokens.has(token)');
+        this.r = this.refreshTokens.get(token)!;
+        if (!(r.client_id === client)) throw new Error('Guard failed: r.client_id === client');
+        this.s[token] = null;
+        this.s[r.access_token] = null;
+      }
+    }
+  }
+
+  VerifyPKCE(code: AuthorizationCode, verifier: CodeVerifier) {
+    const xxx: any = {} as any;  // FIXME: parser dropped let/forall
+    if (!(this.authorizationCodes.has(code))) throw new Error('Guard failed: this.authorizationCodes.has(code)');
+    const c = this.authorizationCodes.get(code)!;
+    if (!(c.used === false)) throw new Error('Guard failed: c.used === false');
+    const expectedChallenge = simpleHash(verifier, c.code_challenge_method);
+    if (!(expectedChallenge === c.code_challenge)) throw new Error('Guard failed: expectedChallenge === c.code_challenge');
+  }
+
+
+
+  // V1: Always(NoTokenLeakage)
+  // Z3 call-out: Bounded Model Checking (BMC) with depth = decisionLog.length+1.
+  // Mirrors the SMT-LIB BMC emitted by compiler/src/generators/z3.ts (emitBMC).
+  // The inner expression is SpeckDL; we translate it to a TS boolean
+  // check that reads the current class state via this.<stateVar>.
+  async verify1(): Promise<boolean> {
+    // Temporal: Always(NoTokenLeakage)
+    // LTL: always(p). Bounded check — p must hold at every step in the
+    // bounded trace (decision log + current state). The first step
+    // where p is false violates the always-quantified property.
+    if (!(NoTokenLeakage)) return false;
+    for (const _evt of this.decisionLog) {
+      // Each emit() entry is a step boundary; p is re-evaluated
+      // against the live state (BMC "safety-at-horizon" view).
+      if (!(NoTokenLeakage)) return false;
+    }
+    return true;
+  }
+}