fix(compiler): translate Map/Set expression patterns to JavaScript (#18)
- 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)
This commit is contained in:
Scott Scoble
parent
03de892259
commit
1cbad9d756
20 changed files with 908 additions and 17 deletions
21
out/OAuth2AuthorizationCode.prov.jsonld
Normal file
21
out/OAuth2AuthorizationCode.prov.jsonld
Normal file
|
|
@ -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-05-10T04:51:39.510Z"
|
||||
}
|
||||
},
|
||||
"rdfs:label": "OAuth2AuthorizationCode"
|
||||
}
|
||||
]
|
||||
}
|
||||
15
out/OAuth2AuthorizationCode.specbom.cdx.json
Normal file
15
out/OAuth2AuthorizationCode.specbom.cdx.json
Normal file
|
|
@ -0,0 +1,15 @@
|
|||
{
|
||||
"bomFormat": "CycloneDX",
|
||||
"specVersion": "1.6",
|
||||
"components": [],
|
||||
"metadata": {
|
||||
"tools": [],
|
||||
"component": {
|
||||
"type": "application",
|
||||
"name": "OAuth2AuthorizationCode",
|
||||
"version": "0.2.0",
|
||||
"properties": []
|
||||
}
|
||||
},
|
||||
"annotations": []
|
||||
}
|
||||
26
out/OAuth2AuthorizationCode.specbom.spdx.json
Normal file
26
out/OAuth2AuthorizationCode.specbom.spdx.json
Normal file
|
|
@ -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-05-10T04:51:39.520Z",
|
||||
"createdBy": [
|
||||
"Organization: Speckl",
|
||||
"tool: speckl-compile-0.2.0"
|
||||
]
|
||||
}
|
||||
},
|
||||
"builtBy": [],
|
||||
"relationships": [],
|
||||
"elements": []
|
||||
}
|
||||
120
out/OAuth2AuthorizationCode.ts
Normal file
120
out/OAuth2AuthorizationCode.ts
Normal file
|
|
@ -0,0 +1,120 @@
|
|||
// 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;
|
||||
}
|
||||
}
|
||||
211
out/OAuth2AuthorizationCode.wat
Normal file
211
out/OAuth2AuthorizationCode.wat
Normal file
|
|
@ -0,0 +1,211 @@
|
|||
;; Auto-generated by speckl-compile from OAuth2AuthorizationCode
|
||||
;; Compile: wat2wasm OAuth2AuthorizationCode.wat -o OAuth2AuthorizationCode.wasm
|
||||
|
||||
(module
|
||||
;; Host imports for Map/Set/alloc
|
||||
(import "speckl" "map_create" (func $map_create (result i32)))
|
||||
(import "speckl" "map_set" (func $map_set (param i32 i32 i32)))
|
||||
(import "speckl" "map_get" (func $map_get (param i32 i32) (result i32)))
|
||||
(import "speckl" "map_has" (func $map_has (param i32 i32) (result i32)))
|
||||
(import "speckl" "map_remove" (func $map_remove (param i32 i32)))
|
||||
(import "speckl" "set_create" (func $set_create (result i32)))
|
||||
(import "speckl" "set_add" (func $set_add (param i32 i32)))
|
||||
(import "speckl" "set_has" (func $set_has (param i32 i32) (result i32)))
|
||||
(import "speckl" "set_size" (func $set_size (param i32) (result i32)))
|
||||
(import "speckl" "alloc" (func $alloc (param i32) (result i32)))
|
||||
(import "speckl" "write_i32" (func $write_i32 (param i32 i32)))
|
||||
(import "speckl" "write_f64" (func $write_f64 (param i32 f64)))
|
||||
|
||||
;; Linear memory (exported so host can read state)
|
||||
(memory (export "memory") 1)
|
||||
|
||||
;; State globals
|
||||
|
||||
|
||||
;; ---- init ----
|
||||
(func $init (export "init")
|
||||
|
||||
)
|
||||
|
||||
;; ---- Actions ----
|
||||
;; action: Authorize
|
||||
(func $Authorize (export "Authorize") (param $client i32) (param $redirectUri i32) (param $scope i32) (param $userId i32) (param $sessionId i32) (result i32)
|
||||
|
||||
(local $state i32)
|
||||
(local $codeVerifier i32)
|
||||
(local $codeChallenge i32)
|
||||
(local $authCode i32)
|
||||
;; require: client in clients.keys
|
||||
;; Complex guard not compiled: client in clients.keys
|
||||
;; require: redirectUri in clients.client.redirect_uris
|
||||
;; Complex guard not compiled: redirectUri in clients.client.redirect_uris
|
||||
;; require: sessionId in sessions.keys
|
||||
;; Complex guard not compiled: sessionId in sessions.keys
|
||||
;; require: sessions[sessionId].user_id == userId
|
||||
;; Complex guard not compiled: sessions[sessionId].user_id == userId
|
||||
(i32.const 0) ;; uncompiled expr: "state_" + hash(client + redirectUri + currentTime)
|
||||
(local.set $state)
|
||||
(i32.const 0) ;; uncompiled expr: "verifier_" + hash(client + userId + currentTime)
|
||||
(local.set $codeVerifier)
|
||||
(i32.const 0) ;; uncompiled expr: hash(codeVerifier, "S256")
|
||||
(local.set $codeChallenge)
|
||||
;; stateNonces[state] := { client_id: client, redirect_uri: redirectUri }
|
||||
;; Unrecognized assignment target: stateNonces[state]
|
||||
;; pkceChallenges[codeChallenge] := { code_verifier_hash: hash(codeVerifier, "S256"), method: "S256" }
|
||||
;; Unrecognized assignment target: pkceChallenges[codeChallenge]
|
||||
(i32.const 0) ;; uncompiled expr: "code_" + hash(client + userId + currentTime)
|
||||
(local.set $authCode)
|
||||
;; authorizationCodes[authCode] := {
|
||||
;; Unrecognized assignment target: authorizationCodes[authCode]
|
||||
(i32.const 1)
|
||||
)
|
||||
|
||||
;; action: ApproveAuthorization
|
||||
(func $ApproveAuthorization (export "ApproveAuthorization") (param $code i32) (param $userId i32) (result i32)
|
||||
|
||||
(local $c i32)
|
||||
;; require: code in authorizationCodes.keys
|
||||
;; Complex guard not compiled: code in authorizationCodes.keys
|
||||
(i32.const 0) ;; uncompiled expr: authorizationCodes[code]
|
||||
(local.set $c)
|
||||
;; require: c.user_id == userId
|
||||
;; Complex guard not compiled: c.user_id == userId
|
||||
;; require: c.used == false
|
||||
;; Complex guard not compiled: c.used == false
|
||||
(i32.const 1)
|
||||
)
|
||||
|
||||
;; action: ExchangeCode
|
||||
(func $ExchangeCode (export "ExchangeCode") (param $req i32) (result i32)
|
||||
|
||||
(local $c i32)
|
||||
(local $expectedChallenge i32)
|
||||
(local $accessToken i32)
|
||||
(local $refreshToken i32)
|
||||
(local $expiresAt i32)
|
||||
;; require: req.client_id in clients.keys
|
||||
;; Complex guard not compiled: req.client_id in clients.keys
|
||||
;; require: req.code in authorizationCodes.keys
|
||||
;; Complex guard not compiled: req.code in authorizationCodes.keys
|
||||
(i32.const 0) ;; uncompiled expr: authorizationCodes[req.code]
|
||||
(local.set $c)
|
||||
;; require: c.used == false
|
||||
;; Complex guard not compiled: c.used == false
|
||||
;; require: c.client_id == req.client_id
|
||||
;; Complex guard not compiled: c.client_id == req.client_id
|
||||
;; require: c.redirect_uri == req.redirect_uri
|
||||
;; Complex guard not compiled: c.redirect_uri == req.redirect_uri
|
||||
(i32.const 0) ;; uncompiled expr: hash(req.code_verifier, c.code_challenge_method)
|
||||
(local.set $expectedChallenge)
|
||||
;; require: expectedChallenge == c.code_challenge
|
||||
;; Guard on non-scalar not compiled: expectedChallenge == c.code_challenge
|
||||
;; pkceChallenges[c.code_challenge] := null
|
||||
;; Unrecognized assignment target: pkceChallenges[c.code_challenge]
|
||||
;; stateNonces[c.state] := null
|
||||
;; Unrecognized assignment target: stateNonces[c.state]
|
||||
(i32.const 0) ;; uncompiled expr: "access_" + hash(req.client_id + c.user_id + currentTime)
|
||||
(local.set $accessToken)
|
||||
(i32.const 0) ;; uncompiled expr: "refresh_" + hash(req.client_id + c.user_id + currentTime)
|
||||
(local.set $refreshToken)
|
||||
(i32.add (i32.const NaN) (i32.const 3600))
|
||||
(local.set $expiresAt)
|
||||
;; accessTokens[accessToken] := {
|
||||
;; Unrecognized assignment target: accessTokens[accessToken]
|
||||
;; refreshTokens[refreshToken] := {
|
||||
;; Unrecognized assignment target: refreshTokens[refreshToken]
|
||||
(i32.const 1)
|
||||
)
|
||||
|
||||
;; action: RefreshToken
|
||||
(func $RefreshToken (export "RefreshToken") (param $req i32) (result i32)
|
||||
|
||||
(local $r i32)
|
||||
(local $newAccessToken i32)
|
||||
(local $newRefreshToken i32)
|
||||
(local $expiresAt i32)
|
||||
;; require: req.client_id in clients.keys
|
||||
;; Complex guard not compiled: req.client_id in clients.keys
|
||||
;; require: req.refresh_token in refreshTokens.keys
|
||||
;; Complex guard not compiled: req.refresh_token in refreshTokens.keys
|
||||
(i32.const 0) ;; uncompiled expr: refreshTokens[req.refresh_token]
|
||||
(local.set $r)
|
||||
;; require: r.client_id == req.client_id
|
||||
;; Complex guard not compiled: r.client_id == req.client_id
|
||||
;; accessTokens[r.access_token] := null
|
||||
;; Unrecognized assignment target: accessTokens[r.access_token]
|
||||
(i32.const 0) ;; uncompiled expr: "access_" + hash(req.client_id + r.user_id + currentTime)
|
||||
(local.set $newAccessToken)
|
||||
(i32.const 0) ;; uncompiled expr: "refresh_" + hash(req.client_id + r.user_id + currentTime)
|
||||
(local.set $newRefreshToken)
|
||||
(i32.add (i32.const NaN) (i32.const 3600))
|
||||
(local.set $expiresAt)
|
||||
;; accessTokens[newAccessToken] := {
|
||||
;; Unrecognized assignment target: accessTokens[newAccessToken]
|
||||
;; refreshTokens[newRefreshToken] := {
|
||||
;; Unrecognized assignment target: refreshTokens[newRefreshToken]
|
||||
;; refreshTokens[req.refresh_token] := null
|
||||
;; Unrecognized assignment target: refreshTokens[req.refresh_token]
|
||||
(i32.const 1)
|
||||
)
|
||||
|
||||
;; action: RevokeToken
|
||||
(func $RevokeToken (export "RevokeToken") (param $client i32) (param $token i32) (param $tokenType i32) (result i32)
|
||||
|
||||
(local $t i32)
|
||||
(local $r i32)
|
||||
;; require: client in clients.keys
|
||||
;; Complex guard not compiled: client in clients.keys
|
||||
;; require: token in accessTokens.keys
|
||||
;; Complex guard not compiled: token in accessTokens.keys
|
||||
(i32.const 0) ;; uncompiled expr: accessTokens[token]
|
||||
(local.set $t)
|
||||
;; require: t.client_id == client
|
||||
;; Complex guard not compiled: t.client_id == client
|
||||
;; accessTokens[token] := null
|
||||
;; Unrecognized assignment target: accessTokens[token]
|
||||
;; refreshTokens[t.refresh_token] := null
|
||||
;; Unrecognized assignment target: refreshTokens[t.refresh_token]
|
||||
;; require: token in refreshTokens.keys
|
||||
;; Complex guard not compiled: token in refreshTokens.keys
|
||||
(i32.const 0) ;; uncompiled expr: refreshTokens[token]
|
||||
(local.set $r)
|
||||
;; require: r.client_id == client
|
||||
;; Complex guard not compiled: r.client_id == client
|
||||
;; refreshTokens[token] := null
|
||||
;; Unrecognized assignment target: refreshTokens[token]
|
||||
;; accessTokens[r.access_token] := null
|
||||
;; Unrecognized assignment target: accessTokens[r.access_token]
|
||||
(i32.const 1)
|
||||
)
|
||||
|
||||
;; action: VerifyPKCE
|
||||
(func $VerifyPKCE (export "VerifyPKCE") (param $code i32) (param $verifier i32) (result i32)
|
||||
|
||||
(local $c i32)
|
||||
(local $expectedChallenge i32)
|
||||
;; require: code in authorizationCodes.keys
|
||||
;; Complex guard not compiled: code in authorizationCodes.keys
|
||||
(i32.const 0) ;; uncompiled expr: authorizationCodes[code]
|
||||
(local.set $c)
|
||||
;; require: c.used == false
|
||||
;; Complex guard not compiled: c.used == false
|
||||
(i32.const 0) ;; uncompiled expr: hash(verifier, c.code_challenge_method)
|
||||
(local.set $expectedChallenge)
|
||||
;; require: expectedChallenge == c.code_challenge
|
||||
;; Guard on non-scalar not compiled: expectedChallenge == c.code_challenge
|
||||
(i32.const 1)
|
||||
)
|
||||
|
||||
;; ---- getState ----
|
||||
(func $getState (export "getState") (result i32 i32)
|
||||
(i32.const 0)
|
||||
(i32.const 0)
|
||||
)
|
||||
|
||||
|
||||
;; checkConstraints — runtime constraint evaluation stub
|
||||
(func $checkConstraints (export "checkConstraints") (result i32)
|
||||
;; TODO: evaluate constraint expressions at runtime
|
||||
(i32.const 1)
|
||||
)
|
||||
)
|
||||
21
out/TigerBeetleLedger.prov.jsonld
Normal file
21
out/TigerBeetleLedger.prov.jsonld
Normal file
|
|
@ -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:TigerBeetleLedger",
|
||||
"prov:qualifiedGeneration": {
|
||||
"@type": "prov:Generation",
|
||||
"prov:activity": {
|
||||
"@type": "prov:Activity",
|
||||
"prov:startTime": "2026-05-10T05:07:04.778Z"
|
||||
}
|
||||
},
|
||||
"rdfs:label": "TigerBeetleLedger"
|
||||
}
|
||||
]
|
||||
}
|
||||
15
out/TigerBeetleLedger.specbom.cdx.json
Normal file
15
out/TigerBeetleLedger.specbom.cdx.json
Normal file
|
|
@ -0,0 +1,15 @@
|
|||
{
|
||||
"bomFormat": "CycloneDX",
|
||||
"specVersion": "1.6",
|
||||
"components": [],
|
||||
"metadata": {
|
||||
"tools": [],
|
||||
"component": {
|
||||
"type": "application",
|
||||
"name": "TigerBeetleLedger",
|
||||
"version": "0.2.0",
|
||||
"properties": []
|
||||
}
|
||||
},
|
||||
"annotations": []
|
||||
}
|
||||
26
out/TigerBeetleLedger.specbom.spdx.json
Normal file
26
out/TigerBeetleLedger.specbom.spdx.json
Normal file
|
|
@ -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:TigerBeetleLedger",
|
||||
"@type": "spdx:Snippet",
|
||||
"name": "TigerBeetleLedger",
|
||||
"spdxVersion": "3.0.1",
|
||||
"dataLicense": "CC0-1.0",
|
||||
"creationInfo": {
|
||||
"created": "2026-05-10T05:07:04.787Z",
|
||||
"createdBy": [
|
||||
"Organization: Speckl",
|
||||
"tool: speckl-compile-0.2.0"
|
||||
]
|
||||
}
|
||||
},
|
||||
"builtBy": [],
|
||||
"relationships": [],
|
||||
"elements": []
|
||||
}
|
||||
143
out/TigerBeetleLedger.ts
Normal file
143
out/TigerBeetleLedger.ts
Normal file
|
|
@ -0,0 +1,143 @@
|
|||
// Auto-generated by speckl-compile from TigerBeetleLedger
|
||||
// DO NOT EDIT MANUALLY — regenerate from .speckdl source
|
||||
|
||||
export const TigerBeetleLedgerState = {
|
||||
Open: 'open',
|
||||
Closed: 'closed',
|
||||
} as const;
|
||||
export type TigerBeetleLedgerState = typeof TigerBeetleLedgerState[keyof typeof TigerBeetleLedgerState];
|
||||
|
||||
|
||||
|
||||
|
||||
export class TigerBeetleLedgerMachine {
|
||||
accounts: Map<number, Account>;
|
||||
transfers: Map<number, Transfer>;
|
||||
pending: Set<number>;
|
||||
replicaState: Map<number, Replica>;
|
||||
log: LogEntry[];
|
||||
commitIndex: number;
|
||||
leader: number;
|
||||
decisionLog: any[] = [];
|
||||
|
||||
constructor() {
|
||||
// No init block defined
|
||||
}
|
||||
|
||||
CreateTransfer(t: Transfer) {
|
||||
// precondition: !this.transfers.has(t.id)
|
||||
if (!(!this.transfers.has(t.id))) throw new Error('Precondition failed: !this.transfers.has(t.id)');
|
||||
// precondition: this.accounts.has(t.from)
|
||||
if (!(this.accounts.has(t.from))) throw new Error('Precondition failed: this.accounts.has(t.from)');
|
||||
// precondition: this.accounts.has(t.to)
|
||||
if (!(this.accounts.has(t.to))) throw new Error('Precondition failed: this.accounts.has(t.to)');
|
||||
// precondition: t.from != t.to
|
||||
if (!(t.from != t.to)) throw new Error('Precondition failed: t.from != t.to');
|
||||
// precondition: this.accounts.get(t.from).balance >= t.amount || this.accounts.get(t.from).flags.allows_overdraft
|
||||
if (!(this.accounts.get(t.from).balance >= t.amount || this.accounts.get(t.from).flags.allows_overdraft)) throw new Error('Precondition failed: this.accounts.get(t.from).balance >= t.amount || this.accounts.get(t.from).flags.allows_overdraft');
|
||||
// postcondition: this.transfers.get(t.id) == t
|
||||
if (!(this.transfers.get(t.id) == t)) throw new Error('Postcondition failed: this.transfers.get(t.id) == t');
|
||||
// postcondition: this.pending == new Set([...this.pending, t.id])
|
||||
if (!(this.pending == new Set([...this.pending, t.id]))) throw new Error('Postcondition failed: this.pending == new Set([...this.pending, t.id])');
|
||||
// postcondition: this.accounts.get(t.from).debits_pending == this.accounts.get(t.from).debits_pending + t.amount
|
||||
if (!(this.accounts.get(t.from).debits_pending == this.accounts.get(t.from).debits_pending + t.amount)) throw new Error('Postcondition failed: this.accounts.get(t.from).debits_pending == this.accounts.get(t.from).debits_pending + t.amount');
|
||||
// postcondition: this.accounts.get(t.to).credits_pending == this.accounts.get(t.to).credits_pending + t.amount
|
||||
if (!(this.accounts.get(t.to).credits_pending == this.accounts.get(t.to).credits_pending + t.amount)) throw new Error('Postcondition failed: this.accounts.get(t.to).credits_pending == this.accounts.get(t.to).credits_pending + t.amount');
|
||||
}
|
||||
|
||||
CommitTransfer(id: number) {
|
||||
// precondition: this.pending.has(id)
|
||||
if (!(this.pending.has(id))) throw new Error('Precondition failed: this.pending.has(id)');
|
||||
// precondition: this.transfers.has(id)
|
||||
if (!(this.transfers.has(id))) throw new Error('Precondition failed: this.transfers.has(id)');
|
||||
// precondition: this.transfers.get(id).pending == true
|
||||
if (!(this.transfers.get(id).pending == true)) throw new Error('Precondition failed: this.transfers.get(id).pending == true');
|
||||
// postcondition: this.pending == new Set([...this.pending].filter(x => x !== id))
|
||||
if (!(this.pending == new Set([...this.pending].filter(x => x !== id)))) throw new Error('Postcondition failed: this.pending == new Set([...this.pending].filter(x => x !== id))');
|
||||
// postcondition: this.transfers.get(id).pending == false
|
||||
if (!(this.transfers.get(id).pending == false)) throw new Error('Postcondition failed: this.transfers.get(id).pending == false');
|
||||
// postcondition: this.transfers.get(id).posted == true
|
||||
if (!(this.transfers.get(id).posted == true)) throw new Error('Postcondition failed: this.transfers.get(id).posted == true');
|
||||
// postcondition: this.accounts.get(this.transfers.get(id).from).debits_posted === this.accounts.get(this.transfers.get(id).from).debits_posted
|
||||
if (!(this.accounts.get(this.transfers.get(id).from).debits_posted === this.accounts.get(this.transfers.get(id).from).debits_posted)) throw new Error('Postcondition failed: this.accounts.get(this.transfers.get(id).from).debits_posted === this.accounts.get(this.transfers.get(id).from).debits_posted');
|
||||
// postcondition: this.accounts.get(this.transfers.get(id).to).credits_posted === this.accounts.get(this.transfers.get(id).to).credits_posted
|
||||
if (!(this.accounts.get(this.transfers.get(id).to).credits_posted === this.accounts.get(this.transfers.get(id).to).credits_posted)) throw new Error('Postcondition failed: this.accounts.get(this.transfers.get(id).to).credits_posted === this.accounts.get(this.transfers.get(id).to).credits_posted');
|
||||
// postcondition: this.accounts.get(this.transfers.get(id).from).debits_pending === this.accounts.get(this.transfers.get(id).from).debits_pending
|
||||
if (!(this.accounts.get(this.transfers.get(id).from).debits_pending === this.accounts.get(this.transfers.get(id).from).debits_pending)) throw new Error('Postcondition failed: this.accounts.get(this.transfers.get(id).from).debits_pending === this.accounts.get(this.transfers.get(id).from).debits_pending');
|
||||
// postcondition: this.accounts.get(this.transfers.get(id).to).credits_pending === this.accounts.get(this.transfers.get(id).to).credits_pending
|
||||
if (!(this.accounts.get(this.transfers.get(id).to).credits_pending === this.accounts.get(this.transfers.get(id).to).credits_pending)) throw new Error('Postcondition failed: this.accounts.get(this.transfers.get(id).to).credits_pending === this.accounts.get(this.transfers.get(id).to).credits_pending');
|
||||
}
|
||||
|
||||
VoidTransfer(id: number) {
|
||||
// precondition: this.pending.has(id)
|
||||
if (!(this.pending.has(id))) throw new Error('Precondition failed: this.pending.has(id)');
|
||||
// precondition: this.transfers.has(id)
|
||||
if (!(this.transfers.has(id))) throw new Error('Precondition failed: this.transfers.has(id)');
|
||||
// precondition: this.transfers.get(id).pending == true
|
||||
if (!(this.transfers.get(id).pending == true)) throw new Error('Precondition failed: this.transfers.get(id).pending == true');
|
||||
// postcondition: this.pending == new Set([...this.pending].filter(x => x !== id))
|
||||
if (!(this.pending == new Set([...this.pending].filter(x => x !== id)))) throw new Error('Postcondition failed: this.pending == new Set([...this.pending].filter(x => x !== id))');
|
||||
// postcondition: this.transfers.get(id).pending == false
|
||||
if (!(this.transfers.get(id).pending == false)) throw new Error('Postcondition failed: this.transfers.get(id).pending == false');
|
||||
// postcondition: this.transfers.get(id).voided == true
|
||||
if (!(this.transfers.get(id).voided == true)) throw new Error('Postcondition failed: this.transfers.get(id).voided == true');
|
||||
// postcondition: this.accounts.get(this.transfers.get(id).from).debits_pending === this.accounts.get(this.transfers.get(id).from).debits_pending
|
||||
if (!(this.accounts.get(this.transfers.get(id).from).debits_pending === this.accounts.get(this.transfers.get(id).from).debits_pending)) throw new Error('Postcondition failed: this.accounts.get(this.transfers.get(id).from).debits_pending === this.accounts.get(this.transfers.get(id).from).debits_pending');
|
||||
// postcondition: this.accounts.get(this.transfers.get(id).to).credits_pending === this.accounts.get(this.transfers.get(id).to).credits_pending
|
||||
if (!(this.accounts.get(this.transfers.get(id).to).credits_pending === this.accounts.get(this.transfers.get(id).to).credits_pending)) throw new Error('Postcondition failed: this.accounts.get(this.transfers.get(id).to).credits_pending === this.accounts.get(this.transfers.get(id).to).credits_pending');
|
||||
}
|
||||
|
||||
PostTransfer(t: Transfer) {
|
||||
// precondition: !this.transfers.has(t.id)
|
||||
if (!(!this.transfers.has(t.id))) throw new Error('Precondition failed: !this.transfers.has(t.id)');
|
||||
// precondition: this.accounts.has(t.from)
|
||||
if (!(this.accounts.has(t.from))) throw new Error('Precondition failed: this.accounts.has(t.from)');
|
||||
// precondition: this.accounts.has(t.to)
|
||||
if (!(this.accounts.has(t.to))) throw new Error('Precondition failed: this.accounts.has(t.to)');
|
||||
// precondition: t.from != t.to
|
||||
if (!(t.from != t.to)) throw new Error('Precondition failed: t.from != t.to');
|
||||
// precondition: this.accounts.get(t.from).balance >= t.amount || this.accounts.get(t.from).flags.allows_overdraft
|
||||
if (!(this.accounts.get(t.from).balance >= t.amount || this.accounts.get(t.from).flags.allows_overdraft)) throw new Error('Precondition failed: this.accounts.get(t.from).balance >= t.amount || this.accounts.get(t.from).flags.allows_overdraft');
|
||||
// postcondition: this.transfers.get(t.id) == { ...t, pending: false, posted: true, voided: false }
|
||||
if (!(this.transfers.get(t.id) == { ...t, pending: false, posted: true, voided: false })) throw new Error('Postcondition failed: this.transfers.get(t.id) == { ...t, pending: false, posted: true, voided: false }');
|
||||
// postcondition: this.accounts.get(t.from).debits_posted == this.accounts.get(t.from).debits_posted + t.amount
|
||||
if (!(this.accounts.get(t.from).debits_posted == this.accounts.get(t.from).debits_posted + t.amount)) throw new Error('Postcondition failed: this.accounts.get(t.from).debits_posted == this.accounts.get(t.from).debits_posted + t.amount');
|
||||
// postcondition: this.accounts.get(t.to).credits_posted == this.accounts.get(t.to).credits_posted + t.amount
|
||||
if (!(this.accounts.get(t.to).credits_posted == this.accounts.get(t.to).credits_posted + t.amount)) throw new Error('Postcondition failed: this.accounts.get(t.to).credits_posted == this.accounts.get(t.to).credits_posted + t.amount');
|
||||
}
|
||||
|
||||
BecomeLeader(replica: number, term: number) {
|
||||
// precondition: this.replicaState.has(replica)
|
||||
if (!(this.replicaState.has(replica))) throw new Error('Precondition failed: this.replicaState.has(replica)');
|
||||
// precondition: this.replicaState.get(replica).role == "candidate"
|
||||
if (!(this.replicaState.get(replica).role == "candidate")) throw new Error('Precondition failed: this.replicaState.get(replica).role == "candidate"');
|
||||
// precondition: this.replicaState.get(replica).currentTerm < term
|
||||
if (!(this.replicaState.get(replica).currentTerm < term)) throw new Error('Precondition failed: this.replicaState.get(replica).currentTerm < term');
|
||||
// postcondition: this.leader == replica
|
||||
if (!(this.leader == replica)) throw new Error('Postcondition failed: this.leader == replica');
|
||||
// postcondition: this.replicaState.get(replica).role == "this.leader"
|
||||
if (!(this.replicaState.get(replica).role == "this.leader")) throw new Error('Postcondition failed: this.replicaState.get(replica).role == "this.leader"');
|
||||
// postcondition: this.replicaState.get(replica).currentTerm == term
|
||||
if (!(this.replicaState.get(replica).currentTerm == term)) throw new Error('Postcondition failed: this.replicaState.get(replica).currentTerm == term');
|
||||
}
|
||||
|
||||
AppendEntry(entry: LogEntry, term: number) {
|
||||
// precondition: entry.index == length(this.log) + 1
|
||||
if (!(entry.index == length(this.log) + 1)) throw new Error('Precondition failed: entry.index == length(this.log) + 1');
|
||||
// precondition: term >= this.commitIndex
|
||||
if (!(term >= this.commitIndex)) throw new Error('Precondition failed: term >= this.commitIndex');
|
||||
// postcondition: this.log == append(this.log, entry)
|
||||
if (!(this.log == append(this.log, entry))) throw new Error('Postcondition failed: this.log == append(this.log, entry)');
|
||||
// postcondition: this.commitIndex == entry.index
|
||||
if (!(this.commitIndex == entry.index)) throw new Error('Postcondition failed: this.commitIndex == entry.index');
|
||||
}
|
||||
|
||||
|
||||
|
||||
// V1: Always(AccountBalanceInvariant)
|
||||
async verify1(): Promise<boolean> {
|
||||
// TODO: Model-check or monitor
|
||||
// Temporal: Always(AccountBalanceInvariant)
|
||||
return true;
|
||||
}
|
||||
}
|
||||
102
out/TigerBeetleLedger.wat
Normal file
102
out/TigerBeetleLedger.wat
Normal file
|
|
@ -0,0 +1,102 @@
|
|||
;; Auto-generated by speckl-compile from TigerBeetleLedger
|
||||
;; Compile: wat2wasm TigerBeetleLedger.wat -o TigerBeetleLedger.wasm
|
||||
|
||||
(module
|
||||
;; Host imports for Map/Set/alloc
|
||||
(import "speckl" "map_create" (func $map_create (result i32)))
|
||||
(import "speckl" "map_set" (func $map_set (param i32 i32 i32)))
|
||||
(import "speckl" "map_get" (func $map_get (param i32 i32) (result i32)))
|
||||
(import "speckl" "map_has" (func $map_has (param i32 i32) (result i32)))
|
||||
(import "speckl" "map_remove" (func $map_remove (param i32 i32)))
|
||||
(import "speckl" "set_create" (func $set_create (result i32)))
|
||||
(import "speckl" "set_add" (func $set_add (param i32 i32)))
|
||||
(import "speckl" "set_has" (func $set_has (param i32 i32) (result i32)))
|
||||
(import "speckl" "set_size" (func $set_size (param i32) (result i32)))
|
||||
(import "speckl" "alloc" (func $alloc (param i32) (result i32)))
|
||||
(import "speckl" "write_i32" (func $write_i32 (param i32 i32)))
|
||||
(import "speckl" "write_f64" (func $write_f64 (param i32 f64)))
|
||||
|
||||
;; Linear memory (exported so host can read state)
|
||||
(memory (export "memory") 1)
|
||||
|
||||
;; State globals
|
||||
(global $accounts (mut i32) (i32.const 0))
|
||||
(global $transfers (mut i32) (i32.const 0))
|
||||
(global $pending (mut i32) (i32.const 0))
|
||||
(global $replicaState (mut i32) (i32.const 0))
|
||||
(global $log (mut i32) (i32.const 0))
|
||||
(global $commitIndex (mut i32) (i32.const 0))
|
||||
(global $leader (mut i32) (i32.const 0))
|
||||
|
||||
;; ---- init ----
|
||||
(func $init (export "init")
|
||||
(call $map_create)
|
||||
(global.set $accounts)
|
||||
(call $map_create)
|
||||
(global.set $transfers)
|
||||
(call $set_create)
|
||||
(global.set $pending)
|
||||
(call $map_create)
|
||||
(global.set $replicaState)
|
||||
(i32.const 0)
|
||||
(global.set $commitIndex)
|
||||
(i32.const 0)
|
||||
(global.set $leader)
|
||||
)
|
||||
|
||||
;; ---- Actions ----
|
||||
;; action: CreateTransfer
|
||||
(func $CreateTransfer (export "CreateTransfer") (param $t i32) (result i32)
|
||||
|
||||
(i32.const 1)
|
||||
)
|
||||
|
||||
;; action: CommitTransfer
|
||||
(func $CommitTransfer (export "CommitTransfer") (param $id i32) (result i32)
|
||||
|
||||
(i32.const 1)
|
||||
)
|
||||
|
||||
;; action: VoidTransfer
|
||||
(func $VoidTransfer (export "VoidTransfer") (param $id i32) (result i32)
|
||||
|
||||
(i32.const 1)
|
||||
)
|
||||
|
||||
;; action: PostTransfer
|
||||
(func $PostTransfer (export "PostTransfer") (param $t i32) (result i32)
|
||||
|
||||
(i32.const 1)
|
||||
)
|
||||
|
||||
;; action: BecomeLeader
|
||||
(func $BecomeLeader (export "BecomeLeader") (param $replica i32) (param $term i32) (result i32)
|
||||
|
||||
(i32.const 1)
|
||||
)
|
||||
|
||||
;; action: AppendEntry
|
||||
(func $AppendEntry (export "AppendEntry") (param $entry i32) (param $term i32) (result i32)
|
||||
|
||||
(i32.const 1)
|
||||
)
|
||||
|
||||
;; ---- getState ----
|
||||
(func $getState (export "getState") (result i32 i32)
|
||||
(i32.const 0)
|
||||
(global.get $commitIndex)
|
||||
(i32.store)
|
||||
(i32.const 4)
|
||||
(global.get $leader)
|
||||
(i32.store)
|
||||
(i32.const 0)
|
||||
(i32.const 8)
|
||||
)
|
||||
|
||||
|
||||
;; checkConstraints — runtime constraint evaluation stub
|
||||
(func $checkConstraints (export "checkConstraints") (result i32)
|
||||
;; TODO: evaluate constraint expressions at runtime
|
||||
(i32.const 1)
|
||||
)
|
||||
)
|
||||
21
out/ToggleSwitch.prov.jsonld
Normal file
21
out/ToggleSwitch.prov.jsonld
Normal file
|
|
@ -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:ToggleSwitch",
|
||||
"prov:qualifiedGeneration": {
|
||||
"@type": "prov:Generation",
|
||||
"prov:activity": {
|
||||
"@type": "prov:Activity",
|
||||
"prov:startTime": "2026-05-10T05:04:07.209Z"
|
||||
}
|
||||
},
|
||||
"rdfs:label": "ToggleSwitch"
|
||||
}
|
||||
]
|
||||
}
|
||||
15
out/ToggleSwitch.specbom.cdx.json
Normal file
15
out/ToggleSwitch.specbom.cdx.json
Normal file
|
|
@ -0,0 +1,15 @@
|
|||
{
|
||||
"bomFormat": "CycloneDX",
|
||||
"specVersion": "1.6",
|
||||
"components": [],
|
||||
"metadata": {
|
||||
"tools": [],
|
||||
"component": {
|
||||
"type": "application",
|
||||
"name": "ToggleSwitch",
|
||||
"version": "0.2.0",
|
||||
"properties": []
|
||||
}
|
||||
},
|
||||
"annotations": []
|
||||
}
|
||||
26
out/ToggleSwitch.specbom.spdx.json
Normal file
26
out/ToggleSwitch.specbom.spdx.json
Normal file
|
|
@ -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:ToggleSwitch",
|
||||
"@type": "spdx:Snippet",
|
||||
"name": "ToggleSwitch",
|
||||
"spdxVersion": "3.0.1",
|
||||
"dataLicense": "CC0-1.0",
|
||||
"creationInfo": {
|
||||
"created": "2026-05-10T05:04:07.215Z",
|
||||
"createdBy": [
|
||||
"Organization: Speckl",
|
||||
"tool: speckl-compile-0.2.0"
|
||||
]
|
||||
}
|
||||
},
|
||||
"builtBy": [],
|
||||
"relationships": [],
|
||||
"elements": []
|
||||
}
|
||||
34
out/ToggleSwitch.ts
Normal file
34
out/ToggleSwitch.ts
Normal file
|
|
@ -0,0 +1,34 @@
|
|||
// Auto-generated by speckl-compile from ToggleSwitch
|
||||
// DO NOT EDIT MANUALLY — regenerate from .speckdl source
|
||||
|
||||
export const ToggleSwitchState = {
|
||||
Open: 'open',
|
||||
Closed: 'closed',
|
||||
} as const;
|
||||
export type ToggleSwitchState = typeof ToggleSwitchState[keyof typeof ToggleSwitchState];
|
||||
|
||||
|
||||
|
||||
|
||||
export class ToggleSwitchMachine {
|
||||
isOn: boolean;
|
||||
decisionLog: any[] = [];
|
||||
|
||||
constructor() {
|
||||
// No init block defined
|
||||
}
|
||||
|
||||
TurnOn() {
|
||||
if (!(not this.isOn)) throw new Error('Guard failed: not this.isOn');
|
||||
this.isOn = true;
|
||||
}
|
||||
|
||||
TurnOff() {
|
||||
if (!(this.isOn)) throw new Error('Guard failed: this.isOn');
|
||||
this.isOn = false;
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
}
|
||||
71
out/ToggleSwitch.wat
Normal file
71
out/ToggleSwitch.wat
Normal file
|
|
@ -0,0 +1,71 @@
|
|||
;; Auto-generated by speckl-compile from ToggleSwitch
|
||||
;; Compile: wat2wasm ToggleSwitch.wat -o ToggleSwitch.wasm
|
||||
|
||||
(module
|
||||
;; Host imports for Map/Set/alloc
|
||||
(import "speckl" "map_create" (func $map_create (result i32)))
|
||||
(import "speckl" "map_set" (func $map_set (param i32 i32 i32)))
|
||||
(import "speckl" "map_get" (func $map_get (param i32 i32) (result i32)))
|
||||
(import "speckl" "map_has" (func $map_has (param i32 i32) (result i32)))
|
||||
(import "speckl" "map_remove" (func $map_remove (param i32 i32)))
|
||||
(import "speckl" "set_create" (func $set_create (result i32)))
|
||||
(import "speckl" "set_add" (func $set_add (param i32 i32)))
|
||||
(import "speckl" "set_has" (func $set_has (param i32 i32) (result i32)))
|
||||
(import "speckl" "set_size" (func $set_size (param i32) (result i32)))
|
||||
(import "speckl" "alloc" (func $alloc (param i32) (result i32)))
|
||||
(import "speckl" "write_i32" (func $write_i32 (param i32 i32)))
|
||||
(import "speckl" "write_f64" (func $write_f64 (param i32 f64)))
|
||||
|
||||
;; Linear memory (exported so host can read state)
|
||||
(memory (export "memory") 1)
|
||||
|
||||
;; State globals
|
||||
(global $isOn (mut i32) (i32.const 0))
|
||||
|
||||
;; ---- init ----
|
||||
(func $init (export "init")
|
||||
(i32.const 0)
|
||||
(global.set $isOn)
|
||||
)
|
||||
|
||||
;; ---- Actions ----
|
||||
;; action: TurnOn
|
||||
(func $TurnOn (export "TurnOn") (result i32)
|
||||
|
||||
;; require: not isOn
|
||||
;; Complex guard not compiled: not isOn
|
||||
;; isOn := true
|
||||
(i32.const 0) ;; uncompiled expr: true
|
||||
(global.set $isOn)
|
||||
(global.get $isOn)
|
||||
(return)
|
||||
)
|
||||
|
||||
;; action: TurnOff
|
||||
(func $TurnOff (export "TurnOff") (result i32)
|
||||
|
||||
;; require: isOn
|
||||
;; Complex guard not compiled: isOn
|
||||
;; isOn := false
|
||||
(i32.const 0) ;; uncompiled expr: false
|
||||
(global.set $isOn)
|
||||
(global.get $isOn)
|
||||
(return)
|
||||
)
|
||||
|
||||
;; ---- getState ----
|
||||
(func $getState (export "getState") (result i32 i32)
|
||||
(i32.const 0)
|
||||
(global.get $isOn)
|
||||
(i32.store)
|
||||
(i32.const 0)
|
||||
(i32.const 4)
|
||||
)
|
||||
|
||||
|
||||
;; checkConstraints — runtime constraint evaluation stub
|
||||
(func $checkConstraints (export "checkConstraints") (result i32)
|
||||
;; TODO: evaluate constraint expressions at runtime
|
||||
(i32.const 1)
|
||||
)
|
||||
)
|
||||
Loading…
Add table
Add a link
Reference in a new issue