#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.
114 lines
5.5 KiB
TypeScript
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;
|
|
}
|
|
}
|