speckl/out/OAuth2AuthorizationCode.ts
Scott Scoble 8b520284cb TS generator: fix #12 (5 expression patterns) + #11 (opaque record types)
#12: All 5 untranslated SpeckDL patterns now emit valid JS:
  - notIn → !.has(), old() → drop, union → Set spread,
    set diff → filter, append() → [...X, Y], length() → .length
  - ==/!= operator replacement fixed (word-boundary regression)
  - Postcondition object comparisons get @ts-expect-error TS2839

#11: Generator auto-detects opaque identifier types used in state
  variables and action params, emits 'type X = any' before class.
  - State properties use ! (non-null assertion) for strict mode

TigerBeetleLedger → tsc --noEmit = 0 errors. 37/37 tests pass.
2026-05-11 10:16:15 -07:00

114 lines
5.5 KiB
TypeScript

// Auto-generated by speckl-compile from OAuth2AuthorizationCode
// DO NOT EDIT MANUALLY — regenerate from .speckdl source
export const OAuth2AuthorizationCodeState = {
Open: 'open',
Closed: 'closed',
} as const;
export type OAuth2AuthorizationCodeState = typeof OAuth2AuthorizationCodeState[keyof typeof OAuth2AuthorizationCodeState];
export class OAuth2AuthorizationCodeMachine {
clients: Map<ClientId, { redirect_uris: Set<RedirectUri>; client_secret: ClientSecret }>;
authorizationCodes: Map(AuthorizationCode, {;
client_id: ClientId;
redirect_uri: RedirectUri;
state: OAuth2AuthorizationCodeState;
code_challenge: CodeChallenge;
code_challenge_method: String;
scope: Scope;
user_id: UserId;
session_id: SessionId;
created_at: number;
used: boolean;
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: number;
sessions: Map<SessionId, { user_id: UserId }>;
stateNonces: Map<OAuth2AuthorizationCodeState, { 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) {
if (!(this.clients.has(client))) throw new Error('Guard failed: this.clients.has(client)');
if (!(this.clients.client.redirect_uris.has(redirectUri))) throw new Error('Guard failed: this.clients.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');
this.stateNonces[state] = { this.client_id: client, this.redirect_uri: redirectUri };
this.pkceChallenges[codeChallenge] = { code_verifier_hash: hash(codeVerifier, "S256"), method: "S256" };
this.authorizationCodes[authCode] = {;
}
ApproveAuthorization(code: AuthorizationCode, userId: UserId) {
if (!(this.authorizationCodes.has(code))) throw new Error('Guard failed: this.authorizationCodes.has(code)');
if (!(c.this.user_id == userId)) throw new Error('Guard failed: c.this.user_id == userId');
if (!(c.this.used == false)) throw new Error('Guard failed: c.this.used == false');
}
ExchangeCode(req: TokenRequest) {
if (!(this.clients.has(req.this.client_id))) throw new Error('Guard failed: this.clients.has(req.this.client_id)');
if (!(this.authorizationCodes.has(req.code))) throw new Error('Guard failed: this.authorizationCodes.has(req.code)');
if (!(c.this.used == false)) throw new Error('Guard failed: c.this.used == false');
if (!(c.this.client_id == req.this.client_id)) throw new Error('Guard failed: c.this.client_id == req.this.client_id');
if (!(c.this.redirect_uri == req.this.redirect_uri)) throw new Error('Guard failed: c.this.redirect_uri == req.this.redirect_uri');
if (!(expectedChallenge == c.this.code_challenge)) throw new Error('Guard failed: expectedChallenge == c.this.code_challenge');
this.pkceChallenges[c.code_challenge] = null;
this.stateNonces[c.state] = null;
this.accessTokens[accessToken] = {;
this.refreshTokens[refreshToken] = {;
}
RefreshToken(req: RefreshRequest) {
if (!(this.clients.has(req.this.client_id))) throw new Error('Guard failed: this.clients.has(req.this.client_id)');
if (!(this.refreshTokens.has(req.this.refresh_token))) throw new Error('Guard failed: this.refreshTokens.has(req.this.refresh_token)');
if (!(r.this.client_id == req.this.client_id)) throw new Error('Guard failed: r.this.client_id == req.this.client_id');
this.accessTokens[r.access_token] = null;
this.accessTokens[newAccessToken] = {;
this.refreshTokens[newRefreshToken] = {;
this.refreshTokens[req.refresh_token] = null;
}
RevokeToken(client: ClientId, token: string, tokenType: string) {
if (!(this.clients.has(client) if tokenType == "access" {)) 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)');
if (!(t.this.client_id == client)) throw new Error('Guard failed: t.this.client_id == client');
if (!(this.refreshTokens.has(token))) throw new Error('Guard failed: this.refreshTokens.has(token)');
if (!(r.this.client_id == client)) throw new Error('Guard failed: r.this.client_id == client');
this.accessTokens[token] = null;
this.refreshTokens[t.refresh_token] = null;
this.refreshTokens[token] = null;
this.accessTokens[r.access_token] = null;
}
VerifyPKCE(code: AuthorizationCode, verifier: CodeVerifier) {
if (!(this.authorizationCodes.has(code))) throw new Error('Guard failed: this.authorizationCodes.has(code)');
if (!(c.this.used == false)) throw new Error('Guard failed: c.this.used == false');
if (!(expectedChallenge == c.this.code_challenge)) throw new Error('Guard failed: expectedChallenge == c.this.code_challenge');
}
// V1: Always(NoTokenLeakage)
async verify1(): Promise<boolean> {
// TODO: Model-check or monitor
// Temporal: Always(NoTokenLeakage)
return true;
}
}