- x in someSet → someSet.has(x) - x in someMap.keys → someMap.has(x) - x notIn someMap.keys → !someMap.has(x) - m[k] → m.get(k) for Map state variables - s.size() → s.size (property, not method) - Track Map-typed state variables via mapVarNames for accurate .get() translation - Thread mapVarNames through emitAction and rewriteExpr All 41 tests passing. TigerBeetleLedger now generates correct TypeScript with .get() for Map access and .has() for Set membership. Part of M0.1: Fix TS generator bugs (speckl#18)
120 lines
5.6 KiB
TypeScript
120 lines
5.6 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() {
|
|
this.clients = new Map();
|
|
this.used = false;
|
|
this.created_at = 0;
|
|
this.sessions = new Map();
|
|
this.stateNonces = new Map();
|
|
this.pkceChallenges = new Map();
|
|
this.currentTime = 0;
|
|
}
|
|
|
|
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.has(redirectUri).client.redirect_uris)) throw new Error('Guard failed: this.clients.has(redirectUri).client.redirect_uris');
|
|
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))) throw new Error('Guard failed: this.clients.has(client)');
|
|
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;
|
|
}
|
|
}
|