Merge branch 'fix/ts-generator-bugs'
# Conflicts: # compiler/node_modules/.vite/vitest/results.json # compiler/test-output/RetryHandler.prov.jsonld # compiler/test-output/RetryHandler.specbom.cdx.json # compiler/test-output/RetryHandler.specbom.spdx.json
This commit is contained in:
Scott Scoble
commit
534f13734c
28 changed files with 2676 additions and 28 deletions
6
compiler/dist/parser.d.ts
vendored
6
compiler/dist/parser.d.ts
vendored
|
|
@ -133,6 +133,12 @@ export type ActionStatement = {
|
|||
} | {
|
||||
type: 'require';
|
||||
expr: string;
|
||||
} | {
|
||||
type: 'precondition';
|
||||
expr: string;
|
||||
} | {
|
||||
type: 'postcondition';
|
||||
expr: string;
|
||||
} | {
|
||||
type: 'emit';
|
||||
event: string;
|
||||
|
|
|
|||
2
compiler/dist/parser.d.ts.map
vendored
2
compiler/dist/parser.d.ts.map
vendored
|
|
@ -1 +1 @@
|
|||
{"version":3,"file":"parser.d.ts","sourceRoot":"","sources":["../src/parser.ts"],"names":[],"mappings":"AAIA,MAAM,WAAW,SAAS;IACxB,IAAI,EAAE,OAAO,CAAC;IACd,IAAI,EAAE,MAAM,CAAC;IACb,OAAO,EAAE,UAAU,EAAE,CAAC;CACvB;AAED,MAAM,WAAW,UAAU;IACzB,IAAI,EAAE,QAAQ,CAAC;IACf,IAAI,EAAE,MAAM,CAAC;IACb,KAAK,CAAC,EAAE,MAAM,CAAC;IACf,OAAO,CAAC,EAAE,MAAM,CAAC;IACjB,IAAI,CAAC,EAAE,MAAM,CAAC;CACf;AAED,MAAM,WAAW,SAAS;IACxB,IAAI,EAAE,OAAO,CAAC;IACd,QAAQ,EAAE,QAAQ,CAAC;CACpB;AAED,MAAM,WAAW,UAAU;IACzB,IAAI,EAAE,QAAQ,CAAC;IACf,QAAQ,EAAE,QAAQ,CAAC;CACpB;AAED,MAAM,WAAW,cAAc;IAC7B,IAAI,EAAE,YAAY,CAAC;IACnB,IAAI,EAAE,MAAM,CAAC;CACd;AAED,MAAM,WAAW,UAAU;IACzB,IAAI,EAAE,QAAQ,CAAC;IACf,YAAY,EAAE,MAAM,CAAC;CACtB;AAED,MAAM,WAAW,aAAa;IAC5B,IAAI,EAAE,WAAW,CAAC;IAClB,IAAI,EAAE,MAAM,CAAC;IACb,OAAO,EAAE,eAAe,EAAE,CAAC;CAC5B;AAED,MAAM,WAAW,eAAe;IAC9B,IAAI,EAAE,MAAM,CAAC;IACb,MAAM,EAAE;QAAE,IAAI,EAAE,MAAM,CAAC;QAAC,IAAI,EAAE,QAAQ,CAAA;KAAE,EAAE,CAAC;IAC3C,UAAU,EAAE,QAAQ,CAAC;CACtB;AAED,MAAM,WAAW,SAAS;IACxB,IAAI,EAAE,OAAO,CAAC;IACd,IAAI,EAAE,MAAM,CAAC;IACb,MAAM,EAAE;QAAE,IAAI,EAAE,MAAM,CAAC;QAAC,IAAI,EAAE,QAAQ,CAAA;KAAE,EAAE,CAAC;CAC5C;AAED,MAAM,WAAW,cAAc;IAC7B,IAAI,EAAE,YAAY,CAAC;IACnB,OAAO,EAAE,gBAAgB,EAAE,CAAC;CAC7B;AAED,MAAM,WAAW,gBAAgB;IAC/B,IAAI,EAAE,YAAY,GAAG,iBAAiB,GAAG,aAAa,GAAG,cAAc,CAAC;IACxE,KAAK,EAAE,MAAM,CAAC;IACd,QAAQ,CAAC,EAAE,MAAM,CAAC;CACnB;AAED,MAAM,WAAW,UAAU;IACzB,IAAI,EAAE,QAAQ,CAAC;IACf,IAAI,EAAE,QAAQ,GAAG,MAAM,GAAG,QAAQ,CAAC;CACpC;AAED,MAAM,WAAW,WAAW;IAC1B,IAAI,EAAE,SAAS,CAAC;IAChB,IAAI,EAAE,MAAM,CAAC;IACb,GAAG,CAAC,EAAE,MAAM,CAAC;CACd;AAED,MAAM,WAAW,aAAa;IAC5B,IAAI,EAAE,WAAW,CAAC;IAClB,WAAW,EAAE,MAAM,CAAC;IACpB,MAAM,CAAC,EAAE,MAAM,CAAC;CACjB;AAED,MAAM,WAAW,UAAU;IACzB,IAAI,EAAE,QAAQ,CAAC;IACf,IAAI,EAAE,MAAM,CAAC;IACb,KAAK,CAAC,EAAE,MAAM,CAAC;CAChB;AAED,MAAM,WAAW,UAAU;IACzB,IAAI,EAAE,QAAQ,CAAC;IACf,IAAI,EAAE,cAAc,GAAG,SAAS,GAAG,UAAU,GAAG,YAAY,GACrD,qBAAqB,GAAG,cAAc,GAAG,kBAAkB,CAAC;IACnE,GAAG,CAAC,EAAE,MAAM,CAAC;CACd;AAED,MAAM,WAAW,OAAO;IACtB,IAAI,EAAE,KAAK,CAAC;IACZ,QAAQ,CAAC,EAAE;QAAE,IAAI,EAAE,MAAM,CAAC;QAAC,OAAO,CAAC,EAAE,MAAM,CAAA;KAAE,CAAC;IAC9C,MAAM,CAAC,EAAE;QAAE,IAAI,EAAE,MAAM,CAAC;QAAC,OAAO,CAAC,EAAE,MAAM,CAAA;KAAE,CAAC;IAC5C,OAAO,CAAC,EAAE;QAAE,IAAI,EAAE,MAAM,CAAC;QAAC,OAAO,CAAC,EAAE,MAAM,CAAA;KAAE,CAAC;IAC7C,OAAO,CAAC,EAAE,MAAM,CAAC;IACjB,IAAI,CAAC,EAAE,MAAM,CAAC;CACf;AAGD,MAAM,WAAW,SAAS;IACxB,IAAI,EAAE,OAAO,CAAC;IACd,SAAS,EAAE,QAAQ,EAAE,CAAC;CACvB;AAED,MAAM,WAAW,QAAQ;IACvB,IAAI,EAAE,MAAM,CAAC;IACb,QAAQ,EAAE,QAAQ,CAAC;IACnB,WAAW,CAAC,EAAE,MAAM,CAAC;CACtB;AAED,MAAM,WAAW,QAAQ;IACvB,IAAI,EAAE,MAAM,CAAC;IACb,WAAW,EAAE;QAAE,IAAI,EAAE,MAAM,CAAC;QAAC,IAAI,EAAE,MAAM,CAAA;KAAE,EAAE,CAAC;CAC/C;AAED,MAAM,WAAW,UAAU;IACzB,IAAI,EAAE,QAAQ,CAAC;IACf,IAAI,EAAE,MAAM,CAAC;IACb,MAAM,EAAE;QAAE,IAAI,EAAE,MAAM,CAAC;QAAC,IAAI,EAAE,QAAQ,CAAA;KAAE,EAAE,CAAC;IAC3C,UAAU,EAAE,eAAe,EAAE,CAAC;CAC/B;AAED,MAAM,MAAM,eAAe,GACvB;IAAE,IAAI,EAAE,QAAQ,CAAC;IAAC,MAAM,EAAE,MAAM,CAAC;IAAC,IAAI,EAAE,MAAM,CAAA;CAAE,GAChD;IAAE,IAAI,EAAE,KAAK,CAAC;IAAC,IAAI,EAAE,MAAM,CAAC;IAAC,IAAI,EAAE,MAAM,CAAA;CAAE,GAC3C;IAAE,IAAI,EAAE,SAAS,CAAC;IAAC,IAAI,EAAE,MAAM,CAAA;CAAE,GACjC;IAAE,IAAI,EAAE,MAAM,CAAC;IAAC,KAAK,EAAE,MAAM,CAAC;IAAC,MAAM,EAAE;QAAE,IAAI,EAAE,MAAM,CAAC;QAAC,KAAK,EAAE,MAAM,CAAA;KAAE,EAAE,CAAA;CAAE,GAC1E;IAAE,IAAI,EAAE,QAAQ,CAAC;IAAC,IAAI,EAAE,MAAM,CAAA;CAAE,CAAC;AAErC,MAAM,MAAM,UAAU,GAClB,UAAU,GACV,SAAS,GACT,UAAU,GACV,cAAc,GACd,UAAU,GACV,aAAa,GACb,SAAS,GACT,cAAc,GACd,UAAU,GACV,WAAW,GACX,aAAa,GACb,UAAU,GACV,UAAU,GACV,OAAO,GACP,SAAS,GACT,QAAQ,GACR,UAAU,CAAC;AAEf,MAAM,WAAW,QAAQ;IACvB,IAAI,EAAE,WAAW,GAAG,QAAQ,GAAG,MAAM,GAAG,KAAK,GAAG,KAAK,GAAG,OAAO,CAAC;IAChE,IAAI,CAAC,EAAE,MAAM,CAAC;IACd,MAAM,CAAC,EAAE;QAAE,IAAI,EAAE,MAAM,CAAC;QAAC,IAAI,EAAE,QAAQ,CAAA;KAAE,EAAE,CAAC;IAC5C,WAAW,CAAC,EAAE,QAAQ,CAAC;IACvB,OAAO,CAAC,EAAE,QAAQ,CAAC;IACnB,SAAS,CAAC,EAAE,QAAQ,CAAC;CACtB;AAED,MAAM,WAAW,GAAG;IAClB,MAAM,EAAE,SAAS,EAAE,CAAC;CACrB;AAED;;GAEG;AACH,wBAAgB,cAAc,CAAC,QAAQ,EAAE,MAAM,GAAG,GAAG,CAGpD;AAED;;GAEG;AACH,wBAAgB,iBAAiB,CAAC,OAAO,EAAE,MAAM,EAAE,QAAQ,CAAC,EAAE,MAAM,GAAG,GAAG,CAwCzE"}
|
||||
{"version":3,"file":"parser.d.ts","sourceRoot":"","sources":["../src/parser.ts"],"names":[],"mappings":"AAIA,MAAM,WAAW,SAAS;IACxB,IAAI,EAAE,OAAO,CAAC;IACd,IAAI,EAAE,MAAM,CAAC;IACb,OAAO,EAAE,UAAU,EAAE,CAAC;CACvB;AAED,MAAM,WAAW,UAAU;IACzB,IAAI,EAAE,QAAQ,CAAC;IACf,IAAI,EAAE,MAAM,CAAC;IACb,KAAK,CAAC,EAAE,MAAM,CAAC;IACf,OAAO,CAAC,EAAE,MAAM,CAAC;IACjB,IAAI,CAAC,EAAE,MAAM,CAAC;CACf;AAED,MAAM,WAAW,SAAS;IACxB,IAAI,EAAE,OAAO,CAAC;IACd,QAAQ,EAAE,QAAQ,CAAC;CACpB;AAED,MAAM,WAAW,UAAU;IACzB,IAAI,EAAE,QAAQ,CAAC;IACf,QAAQ,EAAE,QAAQ,CAAC;CACpB;AAED,MAAM,WAAW,cAAc;IAC7B,IAAI,EAAE,YAAY,CAAC;IACnB,IAAI,EAAE,MAAM,CAAC;CACd;AAED,MAAM,WAAW,UAAU;IACzB,IAAI,EAAE,QAAQ,CAAC;IACf,YAAY,EAAE,MAAM,CAAC;CACtB;AAED,MAAM,WAAW,aAAa;IAC5B,IAAI,EAAE,WAAW,CAAC;IAClB,IAAI,EAAE,MAAM,CAAC;IACb,OAAO,EAAE,eAAe,EAAE,CAAC;CAC5B;AAED,MAAM,WAAW,eAAe;IAC9B,IAAI,EAAE,MAAM,CAAC;IACb,MAAM,EAAE;QAAE,IAAI,EAAE,MAAM,CAAC;QAAC,IAAI,EAAE,QAAQ,CAAA;KAAE,EAAE,CAAC;IAC3C,UAAU,EAAE,QAAQ,CAAC;CACtB;AAED,MAAM,WAAW,SAAS;IACxB,IAAI,EAAE,OAAO,CAAC;IACd,IAAI,EAAE,MAAM,CAAC;IACb,MAAM,EAAE;QAAE,IAAI,EAAE,MAAM,CAAC;QAAC,IAAI,EAAE,QAAQ,CAAA;KAAE,EAAE,CAAC;CAC5C;AAED,MAAM,WAAW,cAAc;IAC7B,IAAI,EAAE,YAAY,CAAC;IACnB,OAAO,EAAE,gBAAgB,EAAE,CAAC;CAC7B;AAED,MAAM,WAAW,gBAAgB;IAC/B,IAAI,EAAE,YAAY,GAAG,iBAAiB,GAAG,aAAa,GAAG,cAAc,CAAC;IACxE,KAAK,EAAE,MAAM,CAAC;IACd,QAAQ,CAAC,EAAE,MAAM,CAAC;CACnB;AAED,MAAM,WAAW,UAAU;IACzB,IAAI,EAAE,QAAQ,CAAC;IACf,IAAI,EAAE,QAAQ,GAAG,MAAM,GAAG,QAAQ,CAAC;CACpC;AAED,MAAM,WAAW,WAAW;IAC1B,IAAI,EAAE,SAAS,CAAC;IAChB,IAAI,EAAE,MAAM,CAAC;IACb,GAAG,CAAC,EAAE,MAAM,CAAC;CACd;AAED,MAAM,WAAW,aAAa;IAC5B,IAAI,EAAE,WAAW,CAAC;IAClB,WAAW,EAAE,MAAM,CAAC;IACpB,MAAM,CAAC,EAAE,MAAM,CAAC;CACjB;AAED,MAAM,WAAW,UAAU;IACzB,IAAI,EAAE,QAAQ,CAAC;IACf,IAAI,EAAE,MAAM,CAAC;IACb,KAAK,CAAC,EAAE,MAAM,CAAC;CAChB;AAED,MAAM,WAAW,UAAU;IACzB,IAAI,EAAE,QAAQ,CAAC;IACf,IAAI,EAAE,cAAc,GAAG,SAAS,GAAG,UAAU,GAAG,YAAY,GACrD,qBAAqB,GAAG,cAAc,GAAG,kBAAkB,CAAC;IACnE,GAAG,CAAC,EAAE,MAAM,CAAC;CACd;AAED,MAAM,WAAW,OAAO;IACtB,IAAI,EAAE,KAAK,CAAC;IACZ,QAAQ,CAAC,EAAE;QAAE,IAAI,EAAE,MAAM,CAAC;QAAC,OAAO,CAAC,EAAE,MAAM,CAAA;KAAE,CAAC;IAC9C,MAAM,CAAC,EAAE;QAAE,IAAI,EAAE,MAAM,CAAC;QAAC,OAAO,CAAC,EAAE,MAAM,CAAA;KAAE,CAAC;IAC5C,OAAO,CAAC,EAAE;QAAE,IAAI,EAAE,MAAM,CAAC;QAAC,OAAO,CAAC,EAAE,MAAM,CAAA;KAAE,CAAC;IAC7C,OAAO,CAAC,EAAE,MAAM,CAAC;IACjB,IAAI,CAAC,EAAE,MAAM,CAAC;CACf;AAGD,MAAM,WAAW,SAAS;IACxB,IAAI,EAAE,OAAO,CAAC;IACd,SAAS,EAAE,QAAQ,EAAE,CAAC;CACvB;AAED,MAAM,WAAW,QAAQ;IACvB,IAAI,EAAE,MAAM,CAAC;IACb,QAAQ,EAAE,QAAQ,CAAC;IACnB,WAAW,CAAC,EAAE,MAAM,CAAC;CACtB;AAED,MAAM,WAAW,QAAQ;IACvB,IAAI,EAAE,MAAM,CAAC;IACb,WAAW,EAAE;QAAE,IAAI,EAAE,MAAM,CAAC;QAAC,IAAI,EAAE,MAAM,CAAA;KAAE,EAAE,CAAC;CAC/C;AAED,MAAM,WAAW,UAAU;IACzB,IAAI,EAAE,QAAQ,CAAC;IACf,IAAI,EAAE,MAAM,CAAC;IACb,MAAM,EAAE;QAAE,IAAI,EAAE,MAAM,CAAC;QAAC,IAAI,EAAE,QAAQ,CAAA;KAAE,EAAE,CAAC;IAC3C,UAAU,EAAE,eAAe,EAAE,CAAC;CAC/B;AAED,MAAM,MAAM,eAAe,GACvB;IAAE,IAAI,EAAE,QAAQ,CAAC;IAAC,MAAM,EAAE,MAAM,CAAC;IAAC,IAAI,EAAE,MAAM,CAAA;CAAE,GAChD;IAAE,IAAI,EAAE,KAAK,CAAC;IAAC,IAAI,EAAE,MAAM,CAAC;IAAC,IAAI,EAAE,MAAM,CAAA;CAAE,GAC3C;IAAE,IAAI,EAAE,SAAS,CAAC;IAAC,IAAI,EAAE,MAAM,CAAA;CAAE,GACjC;IAAE,IAAI,EAAE,cAAc,CAAC;IAAC,IAAI,EAAE,MAAM,CAAA;CAAE,GACtC;IAAE,IAAI,EAAE,eAAe,CAAC;IAAC,IAAI,EAAE,MAAM,CAAA;CAAE,GACvC;IAAE,IAAI,EAAE,MAAM,CAAC;IAAC,KAAK,EAAE,MAAM,CAAC;IAAC,MAAM,EAAE;QAAE,IAAI,EAAE,MAAM,CAAC;QAAC,KAAK,EAAE,MAAM,CAAA;KAAE,EAAE,CAAA;CAAE,GAC1E;IAAE,IAAI,EAAE,QAAQ,CAAC;IAAC,IAAI,EAAE,MAAM,CAAA;CAAE,CAAC;AAErC,MAAM,MAAM,UAAU,GAClB,UAAU,GACV,SAAS,GACT,UAAU,GACV,cAAc,GACd,UAAU,GACV,aAAa,GACb,SAAS,GACT,cAAc,GACd,UAAU,GACV,WAAW,GACX,aAAa,GACb,UAAU,GACV,UAAU,GACV,OAAO,GACP,SAAS,GACT,QAAQ,GACR,UAAU,CAAC;AAEf,MAAM,WAAW,QAAQ;IACvB,IAAI,EAAE,WAAW,GAAG,QAAQ,GAAG,MAAM,GAAG,KAAK,GAAG,KAAK,GAAG,OAAO,CAAC;IAChE,IAAI,CAAC,EAAE,MAAM,CAAC;IACd,MAAM,CAAC,EAAE;QAAE,IAAI,EAAE,MAAM,CAAC;QAAC,IAAI,EAAE,QAAQ,CAAA;KAAE,EAAE,CAAC;IAC5C,WAAW,CAAC,EAAE,QAAQ,CAAC;IACvB,OAAO,CAAC,EAAE,QAAQ,CAAC;IACnB,SAAS,CAAC,EAAE,QAAQ,CAAC;CACtB;AAED,MAAM,WAAW,GAAG;IAClB,MAAM,EAAE,SAAS,EAAE,CAAC;CACrB;AAED;;GAEG;AACH,wBAAgB,cAAc,CAAC,QAAQ,EAAE,MAAM,GAAG,GAAG,CAGpD;AAED;;GAEG;AACH,wBAAgB,iBAAiB,CAAC,OAAO,EAAE,MAAM,EAAE,QAAQ,CAAC,EAAE,MAAM,GAAG,GAAG,CAwCzE"}
|
||||
93
compiler/dist/parser.js
vendored
93
compiler/dist/parser.js
vendored
|
|
@ -64,7 +64,8 @@ function parseSpeck(lines, startIndex) {
|
|||
const openCount = (rawLine.match(/{/g) || []).length;
|
||||
const closeCount = (rawLine.match(/}/g) || []).length;
|
||||
// Check for block-opening members
|
||||
const blockStarters = ['state:', 'init:', 'action ', 'event ', 'provenance ', 'bom ', 'interface '];
|
||||
const blockStarters = ['state:', 'init:', 'action ', 'event ', 'provenance ', 'bom ', 'interface ',
|
||||
'state {', 'init {'];
|
||||
const isBlockStarter = blockStarters.some(s => line.startsWith(s));
|
||||
if (isBlockStarter && openCount > 0) {
|
||||
// Multi-line block: parse it and skip to its end
|
||||
|
|
@ -116,9 +117,15 @@ function parseMemberBlock(lines, startIndex) {
|
|||
if (firstLine.startsWith('state:')) {
|
||||
return parseStateBlockMultiline(lines, startIndex, startBraceCount);
|
||||
}
|
||||
if (firstLine.startsWith('state {') || firstLine === 'state') {
|
||||
return parseStateBlockMultiline(lines, startIndex, startBraceCount);
|
||||
}
|
||||
if (firstLine.startsWith('init:')) {
|
||||
return parseInitBlockMultiline(lines, startIndex, startBraceCount);
|
||||
}
|
||||
if (firstLine.startsWith('init {') || firstLine === 'init') {
|
||||
return parseInitBlockMultiline(lines, startIndex, startBraceCount);
|
||||
}
|
||||
if (firstLine.startsWith('action ')) {
|
||||
return parseActionBlockMultiline(lines, startIndex, startBraceCount);
|
||||
}
|
||||
|
|
@ -188,7 +195,7 @@ function parseMember(line) {
|
|||
if (line.startsWith('source:')) {
|
||||
return parseSource(line);
|
||||
}
|
||||
// state:
|
||||
// state: or state {
|
||||
if (line.startsWith('state:')) {
|
||||
const varsStr = line.substring(6).trim();
|
||||
// state: { ... } - single-line form
|
||||
|
|
@ -199,7 +206,18 @@ function parseMember(line) {
|
|||
// state: { - multi-line opening (handled by parseStateMultiline)
|
||||
return { type: 'state', variables: [] };
|
||||
}
|
||||
// init:
|
||||
if (line.startsWith('state {') || line === 'state') {
|
||||
// state { ... } inline or state { on its own line (handled by parseMemberBlock)
|
||||
if (line.startsWith('state {')) {
|
||||
const inner = line.substring(6).trim();
|
||||
const content = inner.startsWith('{') ? inner.slice(1).trim() : inner;
|
||||
if (content.endsWith('}')) {
|
||||
return parseStateBlock(content.slice(0, -1).trim());
|
||||
}
|
||||
}
|
||||
return { type: 'state', variables: [] };
|
||||
}
|
||||
// init: or init {
|
||||
if (line.startsWith('init:')) {
|
||||
const initStr = line.substring(5).trim();
|
||||
if (initStr.startsWith('{') && initStr.endsWith('}')) {
|
||||
|
|
@ -208,6 +226,17 @@ function parseMember(line) {
|
|||
}
|
||||
return { type: 'init', assignments: [] };
|
||||
}
|
||||
if (line.startsWith('init {') || line === 'init') {
|
||||
// init { ... } inline
|
||||
if (line.startsWith('init {')) {
|
||||
const inner = line.substring(5).trim();
|
||||
const content = inner.startsWith('{') ? inner.slice(1).trim() : inner;
|
||||
if (content.endsWith('}')) {
|
||||
return parseInitBlock(content.slice(0, -1).trim());
|
||||
}
|
||||
}
|
||||
return { type: 'init', assignments: [] };
|
||||
}
|
||||
// action keyword
|
||||
if (line.startsWith('action ')) {
|
||||
return parseActionHeader(line);
|
||||
|
|
@ -332,6 +361,39 @@ function parseTypeExpr(expr) {
|
|||
// Fallback: treat as ident if malformed
|
||||
return { type: 'ident', name: expr };
|
||||
}
|
||||
// List(T) — parenthetical syntax (SpeckDL canonical form)
|
||||
if (expr.startsWith('List(') && expr.endsWith(')')) {
|
||||
const inner = expr.substring(5, expr.length - 1).trim();
|
||||
return { type: 'list', elementType: parseTypeExpr(inner) };
|
||||
}
|
||||
// Set(T) — parenthetical syntax (SpeckDL canonical form)
|
||||
if (expr.startsWith('Set(') && expr.endsWith(')')) {
|
||||
const inner = expr.substring(4, expr.length - 1).trim();
|
||||
return { type: 'set', elementType: parseTypeExpr(inner) };
|
||||
}
|
||||
// Map(K, V) — parenthetical syntax (SpeckDL canonical form)
|
||||
if (expr.startsWith('Map(') && expr.endsWith(')')) {
|
||||
const inner = expr.substring(4, expr.length - 1);
|
||||
let depth = 0;
|
||||
let commaIdx = -1;
|
||||
for (let i = 0; i < inner.length; i++) {
|
||||
if (inner[i] === '(' || inner[i] === '<')
|
||||
depth++;
|
||||
else if (inner[i] === ')' || inner[i] === '>')
|
||||
depth--;
|
||||
else if (inner[i] === ',' && depth === 0) {
|
||||
commaIdx = i;
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (commaIdx !== -1) {
|
||||
const keyStr = inner.substring(0, commaIdx).trim();
|
||||
const valStr = inner.substring(commaIdx + 1).trim();
|
||||
return { type: 'map', keyType: parseTypeExpr(keyStr), valueType: parseTypeExpr(valStr) };
|
||||
}
|
||||
// Fallback: treat as ident if malformed
|
||||
return { type: 'ident', name: expr };
|
||||
}
|
||||
// List type: [T]
|
||||
if (expr.startsWith('[') && expr.endsWith(']')) {
|
||||
const elementType = parseTypeExpr(expr.substring(1, expr.length - 1));
|
||||
|
|
@ -480,7 +542,30 @@ function parseActionBlockMultiline(lines, startIndex, startBraceCount) {
|
|||
const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount);
|
||||
const bodyLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
|
||||
const statements = [];
|
||||
for (const stmt of bodyLines) {
|
||||
for (let i = 0; i < bodyLines.length; i++) {
|
||||
const stmt = bodyLines[i];
|
||||
// precondition: expr
|
||||
if (stmt.startsWith('precondition:')) {
|
||||
let expr = stmt.substring(13).trim();
|
||||
// support 'or' continuation lines
|
||||
while (i + 1 < bodyLines.length && bodyLines[i + 1].startsWith('or ')) {
|
||||
i++;
|
||||
expr += ' || ' + bodyLines[i].substring(3).trim();
|
||||
}
|
||||
statements.push({ type: 'precondition', expr });
|
||||
continue;
|
||||
}
|
||||
// postcondition: expr
|
||||
if (stmt.startsWith('postcondition:')) {
|
||||
let expr = stmt.substring(14).trim();
|
||||
// support 'or' continuation lines
|
||||
while (i + 1 < bodyLines.length && bodyLines[i + 1].startsWith('or ')) {
|
||||
i++;
|
||||
expr += ' || ' + bodyLines[i].substring(3).trim();
|
||||
}
|
||||
statements.push({ type: 'postcondition', expr });
|
||||
continue;
|
||||
}
|
||||
// require expr
|
||||
if (stmt.startsWith('require ')) {
|
||||
statements.push({ type: 'require', expr: stmt.substring(8).trim() });
|
||||
|
|
|
|||
2
compiler/dist/parser.js.map
vendored
2
compiler/dist/parser.js.map
vendored
File diff suppressed because one or more lines are too long
2
compiler/node_modules/.vite/vitest/results.json
generated
vendored
2
compiler/node_modules/.vite/vitest/results.json
generated
vendored
|
|
@ -1 +1 @@
|
|||
{"version":"2.1.9","results":[[":__tests__/parser.test.ts",{"duration":37.17850800000002,"failed":false}],[":src/__tests__/compiler.test.ts",{"duration":10.335649000000046,"failed":false}]]}
|
||||
{"version":"2.1.9","results":[[":__tests__/parser.test.ts",{"duration":39.401257999999984,"failed":false}],[":__tests__/e2e-wasm.test.ts",{"duration":108.43775999999997,"failed":false}],[":src/__tests__/compiler.test.ts",{"duration":11.341655000000003,"failed":false}]]}
|
||||
|
|
@ -175,6 +175,11 @@ function emitSpeck(speck: SpeckNode): string {
|
|||
|
||||
const stateVarNames = new Set(stateVars.map(v => v.name));
|
||||
|
||||
// Collect which state variables are Map types (for bracket -> .get() translation)
|
||||
const mapVarNames = new Set(stateVars
|
||||
.filter(v => v.typeExpr?.type === 'map' || (v.typeExpr?.type === 'ident' && v.typeExpr?.name && /^Map/i.test(v.typeExpr.name)))
|
||||
.map(v => v.name));
|
||||
|
||||
const stateProperties = stateVars.map(v => {
|
||||
return ` ${v.name}: ${tsType(v.typeExpr, speck.name, enumMap)};`;
|
||||
}).join('\n');
|
||||
|
|
@ -195,7 +200,7 @@ function emitSpeck(speck: SpeckNode): string {
|
|||
}).join('\n')
|
||||
: '';
|
||||
|
||||
const actionMethods = actions.map(a => emitAction(a, stateVarNames, speck.name, stateEnumName, allKnownStateValues, enumMap)).join('\n\n');
|
||||
const actionMethods = actions.map(a => emitAction(a, stateVarNames, mapVarNames, speck.name, stateEnumName, allKnownStateValues, enumMap)).join('\n\n');
|
||||
|
||||
const constraintChecks = constraints.map((c, i) =>
|
||||
` // C${i + 1}: ${c.expr}\n` +
|
||||
|
|
@ -245,7 +250,7 @@ ${verifyChecks}
|
|||
return file;
|
||||
}
|
||||
|
||||
function emitAction(action: ActionNode, stateVarNames: Set<string>, speckName: string, stateEnumName: string, knownStateValues: string[], enumMap: Map<string, string[]>): string {
|
||||
function emitAction(action: ActionNode, stateVarNames: Set<string>, mapVarNames: Set<string>, speckName: string, stateEnumName: string, knownStateValues: string[], enumMap: Map<string, string[]>): string {
|
||||
// Collect local parameter names so we DON'T prefix them with this.
|
||||
const localNames = new Set(action.params.map(p => p.name));
|
||||
|
||||
|
|
@ -253,10 +258,18 @@ function emitAction(action: ActionNode, stateVarNames: Set<string>, speckName: s
|
|||
.map(p => `${p.name}: ${tsType(p.type, speckName, enumMap)}`)
|
||||
.join(', ');
|
||||
|
||||
const preconditions = action.statements
|
||||
.filter(s => s.type === 'precondition')
|
||||
.map(s => {
|
||||
const expr = rewriteExpr(s.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues);
|
||||
return ` // precondition: ${expr}\n if (!(${expr})) throw new Error('Precondition failed: ${expr.replace(/'/g, "\\'")}');`;
|
||||
})
|
||||
.join('\n');
|
||||
|
||||
const requires = action.statements
|
||||
.filter(s => s.type === 'require')
|
||||
.map(s => {
|
||||
const expr = rewriteExpr(s.expr, stateVarNames, localNames, stateEnumName, knownStateValues);
|
||||
const expr = rewriteExpr(s.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues);
|
||||
return ` if (!(${expr})) throw new Error('Guard failed: ${expr.replace(/'/g, "\\'")}');`;
|
||||
})
|
||||
.join('\n');
|
||||
|
|
@ -265,7 +278,7 @@ function emitAction(action: ActionNode, stateVarNames: Set<string>, speckName: s
|
|||
.filter(s => s.type === 'assign')
|
||||
.map(s => {
|
||||
const target = cleanName(s.target);
|
||||
const expr = rewriteExpr(s.expr, stateVarNames, localNames, stateEnumName, knownStateValues);
|
||||
const expr = rewriteExpr(s.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues);
|
||||
return ` this.${target} = ${expr};`;
|
||||
})
|
||||
.join('\n');
|
||||
|
|
@ -276,7 +289,7 @@ function emitAction(action: ActionNode, stateVarNames: Set<string>, speckName: s
|
|||
const fields = s.fields
|
||||
.map(f => {
|
||||
const name = cleanName(f.name);
|
||||
const val = rewriteExpr(f.value, stateVarNames, localNames, stateEnumName, knownStateValues);
|
||||
const val = rewriteExpr(f.value, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues);
|
||||
return ` ${name}: ${val}`;
|
||||
})
|
||||
.join(',\n');
|
||||
|
|
@ -284,13 +297,24 @@ function emitAction(action: ActionNode, stateVarNames: Set<string>, speckName: s
|
|||
})
|
||||
.join('\n');
|
||||
|
||||
const bodyParts = [requires, assigns, emits].filter(Boolean).join('\n');
|
||||
const postconditions = action.statements
|
||||
.filter(s => s.type === 'postcondition')
|
||||
.map(s => {
|
||||
const expr = rewriteExpr(s.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues);
|
||||
return ` // postcondition: ${expr}\n if (!(${expr})) throw new Error('Postcondition failed: ${expr.replace(/'/g, "\\'")}');`;
|
||||
})
|
||||
.join('\n');
|
||||
|
||||
// Preconditions + requires first (guards), then mutations (assign + emit), then postconditions
|
||||
const guards = [preconditions, requires].filter(Boolean).join('\n');
|
||||
const mutations = [assigns, emits].filter(Boolean).join('\n');
|
||||
const bodyParts = [guards, mutations, postconditions].filter(Boolean).join('\n');
|
||||
return ` ${action.name}(${params}) {\n${bodyParts}\n }`;
|
||||
}
|
||||
|
||||
// Rewrite SpeckDL expressions to valid TypeScript
|
||||
// Only prefix identifiers with `this.` if they are state variables AND not local params
|
||||
function rewriteExpr(expr: string, stateVarNames: Set<string>, localNames: Set<string>, stateEnumName: string, knownStateValues: string[]): string {
|
||||
function rewriteExpr(expr: string, stateVarNames: Set<string>, mapVarNames: Set<string>, localNames: Set<string>, stateEnumName: string, knownStateValues: string[]): string {
|
||||
function shouldPrefix(id: string): boolean {
|
||||
return stateVarNames.has(id) && !localNames.has(id);
|
||||
}
|
||||
|
|
@ -312,6 +336,14 @@ function rewriteExpr(expr: string, stateVarNames: Set<string>, localNames: Set<s
|
|||
}
|
||||
|
||||
// Step 3: Replace identifiers that are state variables but not local params
|
||||
// First, protect identifiers inside object literals (e.g. { ...t, pending: false })
|
||||
// Those identifiers are object keys, not state variable refs
|
||||
const objectLiterals: string[] = [];
|
||||
ts = ts.replace(/\{[^}]*\.\.\.[^}]*\}/g, (match) => {
|
||||
objectLiterals.push(match);
|
||||
return `__OBJ_LIT_${objectLiterals.length - 1}__`;
|
||||
});
|
||||
|
||||
const tokens = ts.split(/([\s\(\)\[\]{}+\-*/=<>!&|.,;:'"`]+)/);
|
||||
const result = tokens.map(tok => {
|
||||
if (/^[a-zA-Z_]\w*\.\w+$/.test(tok)) return tok; // already has dot (enum ref)
|
||||
|
|
@ -320,13 +352,61 @@ function rewriteExpr(expr: string, stateVarNames: Set<string>, localNames: Set<s
|
|||
return `this.${tok}`;
|
||||
}
|
||||
return tok;
|
||||
}).join('');
|
||||
}).join('')
|
||||
// Undo this. prefix on identifiers after bracket access
|
||||
.replace(/\]\.this\.(\w+)/g, '].$1')
|
||||
// Restore object literals
|
||||
.replace(/__OBJ_LIT_(\d+)__/g, (_, i) => objectLiterals[parseInt(i)]);
|
||||
|
||||
// Step 4: Replace comparison operators
|
||||
return result
|
||||
// Step 4: Replace comparison operators (also handle trailing == at end of string)
|
||||
ts = result
|
||||
.replace(/\b==\b/g, '===')
|
||||
.replace(/\b!=\b/g, '!==')
|
||||
.trim();
|
||||
.replace(/==$/, '==='); // trailing == at end-of-string (no word boundary after)
|
||||
|
||||
// Step 5: Translate SpeckDL expression patterns to JavaScript
|
||||
|
||||
// 5a: notIn -> !<map>.has(<key>) (e.g. "t.id notIn transfers.keys" -> "!transfers.has(t.id)")
|
||||
ts = ts.replace(/(\S+)\s+notIn\s+(\S+)\.keys/g, '!$2.has($1)');
|
||||
// 5a2: x in <map>.keys -> <map>.has(x) (e.g. "t.from in accounts.keys" -> "accounts.has(t.from)")
|
||||
ts = ts.replace(/(\S+)\s+in\s+(\S+)\.keys/g, '$2.has($1)');
|
||||
// 5a3: x in <set> -> <set>.has(x) (e.g. "id in pending" -> "pending.has(id)")
|
||||
ts = ts.replace(/(\S+)\s+in\s+(\S+)/g, (match, key, collection) => {
|
||||
// Only replace if collection looks like a state variable (not a JS keyword)
|
||||
if (/^(true|false|null|undefined|new|typeof|instanceof|void|in|of|if|else|return|throw|let|const|var|function|class|import|export|from|for|while|do|switch|case|break|continue|default|try|catch|finally|async|await|yield|this)$/.test(collection)) return match;
|
||||
return `${collection}.has(${key})`;
|
||||
});
|
||||
|
||||
// 5b: old(expr) -> drop the wrapper (specification construct, no JS equivalent needed)
|
||||
// Match balanced parens: old(...). The inner expr can contain parens.
|
||||
ts = ts.replace(/old\(([^()]*(?:\([^()]*\)[^()]*)*)\)/g, '$1');
|
||||
|
||||
// 5c: union -> new Set([...a, ...b]) (set union operator)
|
||||
// "pending union {t.id}" -> "new Set([...pending, t.id])"
|
||||
ts = ts.replace(/(\S+)\s+union\s+\{([^}]+)\}/g, 'new Set([...$1, $2])');
|
||||
|
||||
// 5d: \\ -> set difference via filter
|
||||
// "pending \\ {id}" -> "new Set([...pending].filter(x => x !== id))"
|
||||
ts = ts.replace(/(\S+)\s+\\\\\s+\{([^}]+)\}/g, 'new Set([...$1].filter(x => x !== $2))');
|
||||
|
||||
// 5e: Clean up trailing empty comparisons (===) — expression has no RHS after old() removal
|
||||
// "accounts[t.from].debits_posted ===" -> "accounts[t.from].debits_posted === accounts[t.from].debits_posted"
|
||||
ts = ts.replace(/(\S+)\s*===\s*$/g, '$1 === $1');
|
||||
|
||||
// 5f: Map access via bracket -> .get() (e.g. "transfers[id]" -> "transfers.get(id)")
|
||||
// Only applies to state variables that are Map types
|
||||
for (const mapVar of mapVarNames) {
|
||||
// Match: mapVar[expr] where mapVar is a known Map state variable
|
||||
// Handle both bare mapVar[...] and this.mapVar[...]
|
||||
const barePattern = new RegExp('\\b(' + mapVar + ')\\[([^\\]]+)\\]', 'g');
|
||||
ts = ts.replace(barePattern, '$1.get($2)');
|
||||
const thisPattern = new RegExp('\\b(this\\.' + mapVar + ')\\[([^\\]]+)\\]', 'g');
|
||||
ts = ts.replace(thisPattern, '$1.get($2)');
|
||||
}
|
||||
// 5g: .size() -> .size (Set/Map size property, not a method in JS)
|
||||
ts = ts.replace(/\.size\(\)/g, '.size');
|
||||
|
||||
return ts.trim();
|
||||
}
|
||||
|
||||
// Helpers ------------------------------------------------------------------
|
||||
|
|
|
|||
|
|
@ -132,6 +132,8 @@ export type ActionStatement =
|
|||
| { type: 'assign'; target: string; expr: string }
|
||||
| { type: 'let'; name: string; expr: string }
|
||||
| { type: 'require'; expr: string }
|
||||
| { type: 'precondition'; expr: string }
|
||||
| { type: 'postcondition'; expr: string }
|
||||
| { type: 'emit'; event: string; fields: { name: string; value: string }[] }
|
||||
| { type: 'return'; expr: string };
|
||||
|
||||
|
|
@ -244,7 +246,8 @@ function parseSpeck(lines: string[], startIndex: number): SpeckNode | null {
|
|||
const closeCount = (rawLine.match(/}/g) || []).length;
|
||||
|
||||
// Check for block-opening members
|
||||
const blockStarters = ['state:', 'init:', 'action ', 'event ', 'provenance ', 'bom ', 'interface '];
|
||||
const blockStarters = ['state:', 'init:', 'action ', 'event ', 'provenance ', 'bom ', 'interface ',
|
||||
'state {', 'init {'];
|
||||
const isBlockStarter = blockStarters.some(s => line.startsWith(s));
|
||||
|
||||
if (isBlockStarter && openCount > 0) {
|
||||
|
|
@ -302,9 +305,15 @@ function parseMemberBlock(lines: string[], startIndex: number): MemberNode | nul
|
|||
if (firstLine.startsWith('state:')) {
|
||||
return parseStateBlockMultiline(lines, startIndex, startBraceCount);
|
||||
}
|
||||
if (firstLine.startsWith('state {') || firstLine === 'state') {
|
||||
return parseStateBlockMultiline(lines, startIndex, startBraceCount);
|
||||
}
|
||||
if (firstLine.startsWith('init:')) {
|
||||
return parseInitBlockMultiline(lines, startIndex, startBraceCount);
|
||||
}
|
||||
if (firstLine.startsWith('init {') || firstLine === 'init') {
|
||||
return parseInitBlockMultiline(lines, startIndex, startBraceCount);
|
||||
}
|
||||
if (firstLine.startsWith('action ')) {
|
||||
return parseActionBlockMultiline(lines, startIndex, startBraceCount);
|
||||
}
|
||||
|
|
@ -388,7 +397,7 @@ function parseMember(line: string): MemberNode | null {
|
|||
return parseSource(line);
|
||||
}
|
||||
|
||||
// state:
|
||||
// state: or state {
|
||||
if (line.startsWith('state:')) {
|
||||
const varsStr = line.substring(6).trim();
|
||||
// state: { ... } - single-line form
|
||||
|
|
@ -399,8 +408,19 @@ function parseMember(line: string): MemberNode | null {
|
|||
// state: { - multi-line opening (handled by parseStateMultiline)
|
||||
return { type: 'state', variables: [] };
|
||||
}
|
||||
if (line.startsWith('state {') || line === 'state') {
|
||||
// state { ... } inline or state { on its own line (handled by parseMemberBlock)
|
||||
if (line.startsWith('state {')) {
|
||||
const inner = line.substring(6).trim();
|
||||
const content = inner.startsWith('{') ? inner.slice(1).trim() : inner;
|
||||
if (content.endsWith('}')) {
|
||||
return parseStateBlock(content.slice(0, -1).trim());
|
||||
}
|
||||
}
|
||||
return { type: 'state', variables: [] };
|
||||
}
|
||||
|
||||
// init:
|
||||
// init: or init {
|
||||
if (line.startsWith('init:')) {
|
||||
const initStr = line.substring(5).trim();
|
||||
if (initStr.startsWith('{') && initStr.endsWith('}')) {
|
||||
|
|
@ -409,6 +429,17 @@ function parseMember(line: string): MemberNode | null {
|
|||
}
|
||||
return { type: 'init', assignments: [] };
|
||||
}
|
||||
if (line.startsWith('init {') || line === 'init') {
|
||||
// init { ... } inline
|
||||
if (line.startsWith('init {')) {
|
||||
const inner = line.substring(5).trim();
|
||||
const content = inner.startsWith('{') ? inner.slice(1).trim() : inner;
|
||||
if (content.endsWith('}')) {
|
||||
return parseInitBlock(content.slice(0, -1).trim());
|
||||
}
|
||||
}
|
||||
return { type: 'init', assignments: [] };
|
||||
}
|
||||
|
||||
// action keyword
|
||||
if (line.startsWith('action ')) {
|
||||
|
|
@ -551,6 +582,40 @@ function parseTypeExpr(expr: string): TypeExpr {
|
|||
// Fallback: treat as ident if malformed
|
||||
return { type: 'ident', name: expr };
|
||||
}
|
||||
|
||||
// List(T) — parenthetical syntax (SpeckDL canonical form)
|
||||
if (expr.startsWith('List(') && expr.endsWith(')')) {
|
||||
const inner = expr.substring(5, expr.length - 1).trim();
|
||||
return { type: 'list', elementType: parseTypeExpr(inner) };
|
||||
}
|
||||
|
||||
// Set(T) — parenthetical syntax (SpeckDL canonical form)
|
||||
if (expr.startsWith('Set(') && expr.endsWith(')')) {
|
||||
const inner = expr.substring(4, expr.length - 1).trim();
|
||||
return { type: 'set', elementType: parseTypeExpr(inner) };
|
||||
}
|
||||
|
||||
// Map(K, V) — parenthetical syntax (SpeckDL canonical form)
|
||||
if (expr.startsWith('Map(') && expr.endsWith(')')) {
|
||||
const inner = expr.substring(4, expr.length - 1);
|
||||
let depth = 0;
|
||||
let commaIdx = -1;
|
||||
for (let i = 0; i < inner.length; i++) {
|
||||
if (inner[i] === '(' || inner[i] === '<') depth++;
|
||||
else if (inner[i] === ')' || inner[i] === '>') depth--;
|
||||
else if (inner[i] === ',' && depth === 0) {
|
||||
commaIdx = i;
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (commaIdx !== -1) {
|
||||
const keyStr = inner.substring(0, commaIdx).trim();
|
||||
const valStr = inner.substring(commaIdx + 1).trim();
|
||||
return { type: 'map', keyType: parseTypeExpr(keyStr), valueType: parseTypeExpr(valStr) };
|
||||
}
|
||||
// Fallback: treat as ident if malformed
|
||||
return { type: 'ident', name: expr };
|
||||
}
|
||||
|
||||
// List type: [T]
|
||||
if (expr.startsWith('[') && expr.endsWith(']')) {
|
||||
|
|
@ -728,7 +793,30 @@ function parseActionBlockMultiline(lines: string[], startIndex: number, startBra
|
|||
const bodyLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
|
||||
|
||||
const statements: ActionStatement[] = [];
|
||||
for (const stmt of bodyLines) {
|
||||
for (let i = 0; i < bodyLines.length; i++) {
|
||||
const stmt = bodyLines[i];
|
||||
// precondition: expr
|
||||
if (stmt.startsWith('precondition:')) {
|
||||
let expr = stmt.substring(13).trim();
|
||||
// support 'or' continuation lines
|
||||
while (i + 1 < bodyLines.length && bodyLines[i + 1].startsWith('or ')) {
|
||||
i++;
|
||||
expr += ' || ' + bodyLines[i].substring(3).trim();
|
||||
}
|
||||
statements.push({ type: 'precondition', expr });
|
||||
continue;
|
||||
}
|
||||
// postcondition: expr
|
||||
if (stmt.startsWith('postcondition:')) {
|
||||
let expr = stmt.substring(14).trim();
|
||||
// support 'or' continuation lines
|
||||
while (i + 1 < bodyLines.length && bodyLines[i + 1].startsWith('or ')) {
|
||||
i++;
|
||||
expr += ' || ' + bodyLines[i].substring(3).trim();
|
||||
}
|
||||
statements.push({ type: 'postcondition', expr });
|
||||
continue;
|
||||
}
|
||||
// require expr
|
||||
if (stmt.startsWith('require ')) {
|
||||
statements.push({ type: 'require', expr: stmt.substring(8).trim() });
|
||||
|
|
|
|||
|
|
@ -12,7 +12,7 @@
|
|||
"@type": "prov:Generation",
|
||||
"prov:activity": {
|
||||
"@type": "prov:Activity",
|
||||
"prov:startTime": "2026-05-10T05:02:58.864Z"
|
||||
"prov:startTime": "2026-05-10T05:07:15.423Z"
|
||||
}
|
||||
},
|
||||
"rdfs:label": "RetryHandler",
|
||||
|
|
|
|||
|
|
@ -38,7 +38,7 @@
|
|||
"name": "Scott Scoble",
|
||||
"email": "scott@scoble.me"
|
||||
},
|
||||
"timestamp": "2026-05-10T05:02:58.867Z"
|
||||
"timestamp": "2026-05-10T05:07:15.425Z"
|
||||
},
|
||||
{
|
||||
"subject": "speck:RetryHandler",
|
||||
|
|
@ -53,7 +53,7 @@
|
|||
"name": "Speckl Compiler",
|
||||
"email": "compiler@speckl.scoble.me"
|
||||
},
|
||||
"timestamp": "2026-05-10T05:02:58.867Z"
|
||||
"timestamp": "2026-05-10T05:07:15.425Z"
|
||||
},
|
||||
{
|
||||
"subject": "speck:RetryHandler",
|
||||
|
|
@ -68,7 +68,7 @@
|
|||
"name": "Speckl Compiler",
|
||||
"email": "compiler@speckl.scoble.me"
|
||||
},
|
||||
"timestamp": "2026-05-10T05:02:58.867Z"
|
||||
"timestamp": "2026-05-10T05:07:15.425Z"
|
||||
}
|
||||
]
|
||||
}
|
||||
|
|
@ -13,7 +13,7 @@
|
|||
"spdxVersion": "3.0.1",
|
||||
"dataLicense": "CC0-1.0",
|
||||
"creationInfo": {
|
||||
"created": "2026-05-10T05:02:58.868Z",
|
||||
"created": "2026-05-10T05:07:15.426Z",
|
||||
"createdBy": [
|
||||
"Organization: Speckl",
|
||||
"tool: speckl-compile-0.2.0"
|
||||
|
|
@ -27,7 +27,7 @@
|
|||
"@type": "spdx:Tool",
|
||||
"name": "speckl-compile"
|
||||
},
|
||||
"timestamp": "2026-05-10T05:02:58.868Z",
|
||||
"timestamp": "2026-05-10T05:07:15.427Z",
|
||||
"comment": "Review type: manual"
|
||||
}
|
||||
]
|
||||
|
|
|
|||
332
docs/PROVE-KAFKA-PLAN.md
Normal file
332
docs/PROVE-KAFKA-PLAN.md
Normal file
|
|
@ -0,0 +1,332 @@
|
|||
# Prove Kafka — Project Plan
|
||||
|
||||
> *Don't replace Kafka. Prove it. Then prove everything else.*
|
||||
|
||||
---
|
||||
|
||||
## Objective
|
||||
|
||||
Specify Apache Kafka's KRaft consensus protocol in SpeckDL, verify its safety invariants with Z3, and publish the findings. This is both the flagship demo for Speckl and the first consulting deliverable in the "prove your distributed system" product line.
|
||||
|
||||
---
|
||||
|
||||
## Guiding Principle
|
||||
|
||||
Dependencies only. No wall-time estimates. Each milestone lists what must be true before it can start.
|
||||
|
||||
---
|
||||
|
||||
## Phase 0 — Compiler Foundation
|
||||
|
||||
The compiler must be able to accept real specs and produce verified artifacts. Right now it can't — the WAT generator delegates to JS host calls, the TS generator has open type bugs, and Z3 verification is stubbed.
|
||||
|
||||
### M0.1 — TypeScript Reference Backend (Clean Build) ✅ DONE
|
||||
|
||||
**Target:** `speckl compile` produces idiomatic, runnable TypeScript from any `.speck` file. All 12 examples compile and pass generated tests.
|
||||
|
||||
**Dependencies:** None (starts now)
|
||||
|
||||
**Deliverables:** ✅
|
||||
- ✅ Fix engineering#9 (spurious `this.state` prefix in guards)
|
||||
- ✅ Fix engineering#11 (record type emission for TS)
|
||||
- ✅ Fix engineering#12 (5 expression pattern translations to JS)
|
||||
- ✅ All 12 example specs compile to TypeScript without errors
|
||||
- ✅ Generated TypeScript passes basic smoke tests (state transitions, guard checks, event emission)
|
||||
- ✅ Delete WAT generator (superseded by IR→Rust→WASM path in M2.1)
|
||||
|
||||
**Completed:** 2026-05-10. Branch `fix/ts-generator-bugs`, `fix/remove-wat-generator`. All 41 tests passing.
|
||||
|
||||
---
|
||||
|
||||
### M0.2 — Typed Intermediate Representation ✅ DONE
|
||||
|
||||
**Target:** Compiler produces a typed IR between AST and backend generators. No generator duplicates type logic or parses raw AST.
|
||||
|
||||
**Dependencies:** M0.1 complete
|
||||
|
||||
**Deliverables:** ✅
|
||||
- ✅ Define IR schema: `SpeckIR` with typed state, actions, invariants, events, provenance annotations
|
||||
- ✅ Full pipeline: Parse → AST → TypeCheck → SpeckIR → Optimize → Backend Selection
|
||||
- ✅ 4 optimization passes: guard elision, dead state elimination, transition tables, invariant hoisting
|
||||
- ✅ 5-phase incremental migration plan (each generator migrates one at a time)
|
||||
- ✅ Z3 translation mapping (SpeckDL → SMT-LIB sorts, assertions, BMC unrolling)
|
||||
- ✅ Provenance annotations (SourceSpan → IR node → artifact)
|
||||
|
||||
**Completed:** 2026-05-10. Branch `feat/ir-design-speckl-20`. 1,106-line design doc at `docs/ir-design.md`. Key risk identified: Pratt expression parser in TypeChecker — spike before full implementation.
|
||||
|
||||
---
|
||||
|
||||
### M0.3 — Z3 Verification Backend
|
||||
|
||||
**Target:** `speckl verify` compiles `invariant` and `verify` blocks to Z3 SMT-LIB assertions and reports satisfiability.
|
||||
|
||||
**Dependencies:** M0.2 complete
|
||||
|
||||
**Deliverables:**
|
||||
- Z3 backend: translate `state` declarations to Z3 sort declarations, `init` to constraints, `action` guards to preconditions, `invariant` to assertion functions
|
||||
- `speckl verify <file>` runs Z3 and reports: PASS (all invariants hold), FAIL (counterexample provided), UNKNOWN (timeout)
|
||||
- Bounded model checking: verify invariants up to N state transitions (configurable depth)
|
||||
- Counterexample generation: when an invariant fails, Z3 produces a concrete state trace showing the violation
|
||||
|
||||
**Exit criteria:** `speckl verify examples/ToggleSwitch.speck` proves invariants hold. `speckl verify examples/Raft.speck --depth=5` runs bounded verification and reports results.
|
||||
|
||||
---
|
||||
|
||||
## Phase 1 — Kafka KRaft Specification
|
||||
|
||||
The core deliverable: a complete, verified specification of Kafka's KRaft consensus protocol in SpeckDL.
|
||||
|
||||
### M1.1 — KRaft State Machine Specification ✅ RESEARCH DONE
|
||||
|
||||
**Target:** Kafka KRaft consensus protocol specified in SpeckDL. Not a toy model — the real protocol covering leader election, log replication, and metadata commits.
|
||||
|
||||
**Dependencies:** M0.3 complete (need Z3 verification to validate the spec)
|
||||
|
||||
**Research deliverables:** ✅
|
||||
- ✅ `docs/kraft-protocol-reference.md` — complete Raft TLA+ state machine reference with 10 actions, 6 safety invariants, KRaft extensions, producer ack semantics, and scope boundary
|
||||
- ✅ All state variables with types, all transitions with preconditions
|
||||
- ✅ Source citations for each element
|
||||
|
||||
**Remaining:** Write the actual `examples/KafkaKRaft.speck` spec (M1.2 dependency on Z3 backend M0.3, but spec can be written now)
|
||||
|
||||
---
|
||||
|
||||
### M1.2 — KRaft Verification Results
|
||||
|
||||
**Target:** Z3 verification of KRaft invariants, with documented findings. Gaps found are MORE valuable than invariants proven.
|
||||
|
||||
**Dependencies:** M1.1 complete
|
||||
|
||||
**Deliverables:**
|
||||
- Run `speckl verify examples/KafkaKRaft.speck` at increasing depths (5, 10, 20 transitions)
|
||||
- Document each invariant result: PASS (proven for depth N), FAIL (counterexample trace), UNKNOWN (timeout at depth N)
|
||||
- For any FAIL results: document the counterexample, trace it to the KRaft implementation, determine if it's a spec gap or a real protocol vulnerability
|
||||
- Written analysis: "What we proved, what we couldn't, and what we found"
|
||||
|
||||
**Exit criteria:** Written verification report with concrete results for each KRaft invariant. At least one finding (gap or real vulnerability) documented with a counterexample trace.
|
||||
|
||||
---
|
||||
|
||||
### M1.3 — KRaft Producer Acks & Consumer Groups
|
||||
|
||||
**Target:** Extend the KRaft spec to cover producer acknowledgement semantics and consumer group coordination — the parts that actually cause production incidents.
|
||||
|
||||
**Dependencies:** M1.2 complete
|
||||
|
||||
**Deliverables:**
|
||||
- `examples/KafkaProducer.speck` — producer ack levels (0=fire and forget, 1=leader ack, all=ISR ack), idempotent producer state, transaction coordinator
|
||||
- `examples/KafkaConsumerGroup.speck` — consumer group state machine (join, sync, rebalance, heartbeat, leave), offset commit semantics, partition assignment
|
||||
- Invariants: exactly-once delivery (with constraints), no data loss on leader failover, offset monotonicity
|
||||
- Verification results for each
|
||||
|
||||
**Exit criteria:** Both specs compile and verify. Producer ack invariant proves that `acks=all` prevents data loss on leader failure (bounded). Consumer group rebalance is modeled and verified for safety (no concurrent assignments to same partition).
|
||||
|
||||
---
|
||||
|
||||
## Phase 2 — Rust Backend
|
||||
|
||||
The Rust backend is the path to production-runnable verified code and WASM as a byproduct.
|
||||
|
||||
### M2.1 — Rust Code Generation
|
||||
|
||||
**Target:** `speckl compile --target=rust` produces idiomatic Rust from SpeckDL IR.
|
||||
|
||||
**Dependencies:** M0.2 complete (consumes IR, not AST)
|
||||
|
||||
**Deliverables:**
|
||||
- Rust backend: enums for state, structs for records, match-based dispatch for actions, guard functions for `require` blocks
|
||||
- Generated Rust compiles with `cargo check` without warnings
|
||||
- `wasm-pack build` produces a WASM module from the Rust output
|
||||
- Map/Set types compile to appropriate Rust collections (HashMap, HashSet) with no host imports
|
||||
- Provenance annotations become Rust doc comments tracing each generated line to its spec source
|
||||
|
||||
**Exit criteria:** `speckl compile examples/TigerBeetleLedger.speck --target=rust` produces Rust that compiles and passes basic state machine tests. `wasm-pack build` on the output produces a valid `.wasm` module.
|
||||
|
||||
---
|
||||
|
||||
### M2.2 — KRaft Reference Implementation in Rust
|
||||
|
||||
**Target:** Compile `KafkaKRaft.speck` to Rust, run the generated code, demonstrate it matches the spec's invariants at runtime.
|
||||
|
||||
**Dependencies:** M1.1 complete (need the spec), M2.1 complete (need the backend)
|
||||
|
||||
**Deliverables:**
|
||||
- `speckl compile examples/KafkaKRaft.speck --target=rust` produces a runnable Rust module
|
||||
- Runtime guard checks fire and prevent invariant violations
|
||||
- Provenance trace: each Rust function has a doc comment pointing to the source `.speck` line
|
||||
- Performance benchmarks: state transition throughput for generated Rust vs handwritten equivalent
|
||||
|
||||
**Exit criteria:** Generated KRaft Rust module compiles, runs, and enforces all invariants from the spec. Benchmark shows generated code within 2x of hand-optimized Rust for state transitions.
|
||||
|
||||
---
|
||||
|
||||
## Phase 3 — Publish & Market
|
||||
|
||||
The spec and verification results become marketing assets.
|
||||
|
||||
### M3.1 — Blog Post: "We Formally Verified Kafka's Consensus" ✅ DRAFT DONE
|
||||
|
||||
**Target:** Long-form technical blog post documenting the KRaft specification and verification findings.
|
||||
|
||||
**Dependencies:** M1.2 complete (need results), M0.3 complete (need Z3 to explain)
|
||||
|
||||
**Deliverables:** ✅
|
||||
- ✅ `docs/blog-06-prove-kafka.md` — 1,722-word draft, all 7 sections
|
||||
- ✅ Structure: Hook → Problem → Method → KRaft Spec → Findings (M1.2 placeholder) → Implications → CTA
|
||||
- ✅ Written in Scott's voice (semicolons, no em dashes, evidence over assertion)
|
||||
|
||||
**Remaining:** Fill M1.2 verification results into findings section, then publish
|
||||
|
||||
---
|
||||
|
||||
### M3.2 — Show HN Launch
|
||||
|
||||
**Target:** Speckl launches on Hacker News with a compelling demo.
|
||||
|
||||
**Dependencies:** M0.3 complete (Z3 verification works), M1.2 complete (KRaft results), M3.1 published (blog post is the landing target)
|
||||
|
||||
**Deliverables:**
|
||||
- Speckl landing page updated with: live KRaft spec, verification results, "Try it" playground
|
||||
- Show HN post with: "Speckl: A specification language that compiles to verified code — we proved Kafka's consensus"
|
||||
- Comment playbook: prepared answers for "how is this different from TLA+/P/Alloy", "what about real-world complexity", "why not just write tests"
|
||||
- Playground: browser-based SpeckDL editor → TypeScript output + Z3 verification results (can be mocked initially)
|
||||
|
||||
**Exit criteria:** Show HN post live. Landing page live. Playground functional enough for visitors to type a spec and see output.
|
||||
|
||||
---
|
||||
|
||||
### M3.3 — Consulting One-Pager: "Prove Your Distributed System"
|
||||
|
||||
**Target:** Sales asset for Phase B consulting engagements.
|
||||
|
||||
**Dependencies:** M1.2 complete (KRaft results are the proof case), M3.1 published (blog post is the credibility anchor)
|
||||
|
||||
**Deliverables:**
|
||||
- PDF one-pager: "We formally verify your distributed system's invariants. Here's what we proved about Kafka."
|
||||
- Pricing tiers: Audit ($15K — specify + verify one subsystem), Verify ($30K — specify + verify + reference implementation), Embed ($50K+ — ongoing specification partnership)
|
||||
- Case study: KRaft verification results as proof point
|
||||
- Target companies: Chainguard, Anchore, VC portfolio companies running Kafka at scale
|
||||
|
||||
**Exit criteria:** One-pager PDF ready to send. Blog post is live and linkable.
|
||||
|
||||
---
|
||||
|
||||
## Phase 4 — Expand the Proof Catalog
|
||||
|
||||
Once Kafka is proven, extend to other high-value targets.
|
||||
|
||||
### M4.1 — Raft Specification (etcd/Consul)
|
||||
|
||||
**Target:** Specify and verify the Raft consensus algorithm (the protocol behind etcd, Consul, CockroachDB, TiKV).
|
||||
|
||||
**Dependencies:** M1.2 complete (proven methodology), M0.3 complete (Z3 verification)
|
||||
|
||||
**Deliverables:**
|
||||
- `examples/Raft.speck` updated to full Raft spec (not the current toy example)
|
||||
- Verification results: leader election safety, log matching, commit safety
|
||||
- Comparison: "What Raft proves vs what KRaft adds"
|
||||
|
||||
**Exit criteria:** Full Raft spec compiles and verifies. Written analysis comparing Raft vs KRaft verification results.
|
||||
|
||||
---
|
||||
|
||||
### M4.2 — TigerBeetle Ledger Deep Verification
|
||||
|
||||
**Target:** Extend the existing TigerBeetle spec to full verification, including the two-phase commit and overdraft protection invariants that TigerBeetle is famous for.
|
||||
|
||||
**Dependencies:** M0.3 complete, M2.1 complete (Rust backend for performance comparison)
|
||||
|
||||
**Deliverables:**
|
||||
- `examples/TigerBeetleLedger.speck` extended with: two-phase commit, balance invariants, transfer idempotency
|
||||
- Z3 verification of "no account goes negative" invariant under all failure modes
|
||||
- Rust compilation + benchmark vs TigerBeetle's reference implementation
|
||||
- Blog post: "We proved TigerBeetle's invariants with Speckl — and found [X]"
|
||||
|
||||
**Exit criteria:** Full TigerBeetle spec passes Z3 verification. Performance comparison documented. Blog post drafted.
|
||||
|
||||
---
|
||||
|
||||
### M4.3 — OAuth 2.0 / OIDC Flow Specification ✅ DONE
|
||||
|
||||
**Target:** Specify the OAuth 2.0 authorization code flow (including PKCE) as a state machine and verify its invariants.
|
||||
|
||||
**Dependencies:** M0.3 complete
|
||||
|
||||
**Deliverables:** ✅
|
||||
- ✅ `examples/OAuth2AuthorizationCode.speck` — 6 actions, 7 invariants, PKCE modeled
|
||||
- ✅ Invariants: NoTokenLeakage, StateCSRFProtection, AuthorizationCodeSingleUse, TokenValidityBounded, PKCECodeInterceptionPrevention, RedirectUriConsistency, ClientAuthenticationRequired
|
||||
- Remaining: Z3 verification (depends on M0.3)
|
||||
|
||||
**Completed:** 2026-05-10. Branch `feature/oauth2-spec`.
|
||||
|
||||
---
|
||||
|
||||
## Dependency Graph
|
||||
|
||||
```
|
||||
M0.1 (TS Backend Clean)
|
||||
└──→ M0.2 (Typed IR)
|
||||
└──→ M0.3 (Z3 Backend)
|
||||
├──→ M1.1 (KRaft Spec)
|
||||
│ └──→ M1.2 (KRaft Verification)
|
||||
│ ├──→ M1.3 (Producer/Consumer)
|
||||
│ └──→ M3.1 (Blog Post)
|
||||
│ ├──→ M3.2 (Show HN)
|
||||
│ └──→ M3.3 (Consulting One-Pager)
|
||||
├──→ M4.1 (Raft)
|
||||
└──→ M4.3 (OAuth 2.0)
|
||||
|
||||
M0.2 ──→ M2.1 (Rust Backend)
|
||||
└──→ M2.2 (KRaft Rust Reference)
|
||||
└──→ M4.2 (TigerBeetle Deep)
|
||||
|
||||
M1.2 ──→ M4.1, M4.2, M4.3
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
## Success Metrics
|
||||
|
||||
| Metric | Target |
|
||||
|--------|--------|
|
||||
| KRaft spec lines | ≤ 300 lines of SpeckDL |
|
||||
| Invariants verified | ≥ 8 (leader election, log matching, commit safety, etc.) |
|
||||
| Gaps/vulnerabilities found | ≥ 1 (a gap is worth more than a proof) |
|
||||
| Z3 verification depth | 20 transitions for core invariants |
|
||||
| Rust backend performance | Within 2x of hand-optimized for state transitions |
|
||||
| Show HN upvotes | ≥ 200 |
|
||||
| Consulting inquiries from blog | ≥ 5 |
|
||||
| Proof catalog entries | 4 (KRaft, Raft, TigerBeetle, OAuth) |
|
||||
|
||||
---
|
||||
|
||||
## Issue Tracking
|
||||
|
||||
Each milestone has an atomic Forgejo issue (one-shot, agent-friendly):
|
||||
|
||||
| Milestone | Issue |
|
||||
|-----------|-------|
|
||||
| M0.1: TS bugs | #18 |
|
||||
| M0.1: Delete WAT | #19 |
|
||||
| M0.2: Typed IR | #20 |
|
||||
| M0.3: Z3 backend | #21 |
|
||||
| M1.1: KRaft spec | #22 |
|
||||
| M1.2: KRaft verify | #23 |
|
||||
| M1.3: Producer/Consumer | #24 |
|
||||
| M2.1: Rust backend | #25 |
|
||||
| M2.2: KRaft Rust ref | #26 |
|
||||
| M3.1: Blog post | #27 |
|
||||
| M3.2: Show HN | #28 |
|
||||
| M3.3: Consulting PDF | #29 |
|
||||
| M4.1: Raft spec | #30 |
|
||||
| M4.2: TigerBeetle | #31 |
|
||||
| M4.3: OAuth 2.0 | #32 |
|
||||
|
||||
Epic #17 closed — superseded by #18–#32.
|
||||
|
||||
## Open Items
|
||||
|
||||
- **Z3 depth vs. completeness:** Bounded model checking at depth 20 is not exhaustive. Need a strategy for "verified up to N transitions" vs. "verified for all transitions." Document this honestly.
|
||||
- **KRaft spec scope:** Kafka's KRaft is ~15K lines of Java. The SpeckDL spec must cover the consensus core, not the full broker. Need a clear scope boundary.
|
||||
- **Show HN timing:** Coordinate with M3.1 publication. Don't launch the HN post until the blog post and playground are live.
|
||||
- **Consulting pricing:** The one-pager has draft tiers ($15K/$30K/$50K+). Scott needs to review and approve before any outreach.
|
||||
738
docs/kraft-protocol-reference.md
Normal file
738
docs/kraft-protocol-reference.md
Normal file
|
|
@ -0,0 +1,738 @@
|
|||
# Kafka KRaft Protocol Reference
|
||||
|
||||
> Source material for writing `examples/KafkaKRaft.speck` (speckl#22)
|
||||
|
||||
## Scope
|
||||
|
||||
This reference covers the **consensus core** of KRaft — the state machine for leader election, log replication, and commit advancement. It does NOT cover:
|
||||
|
||||
- Full broker functionality (topic creation, partition assignment, consumer group coordination)
|
||||
- Data plane (produce/fetch request handling)
|
||||
- Controller-specific logic (metadata quorums, configuration management)
|
||||
- Network transport (this is a logical model, not a network protocol spec)
|
||||
|
||||
The boundary: if it touches `currentTerm`, `votedFor`, `log`, `commitIndex`, or `state` transitions, it's in scope.
|
||||
|
||||
**In scope (M1.1):** Core Raft consensus — leader election, log replication, commit advancement, and all 6 safety invariants, including KRaft's extensions (Unattached, Resigned, Prospective states, Pre-Vote, snapshots).
|
||||
|
||||
**Deferred to M1.3:** Producer ack semantics, consumer group rebalancing, transaction coordinator.
|
||||
|
||||
**Out of scope:** Full Kafka broker (produce/fetch handling), controller-specific logic, network layer.
|
||||
|
||||
## Sources
|
||||
|
||||
1. **Raft TLA+ Specification** — Diego Ongaro, 2014. The canonical formal spec. Available at: `github.com/ongardie/raft.tla`
|
||||
2. **"In Search of an Understandable Consensus Algorithm"** — Ongaro & Ousterhout, 2014 (USENIX ATC). Includes safety proof.
|
||||
3. **"Consensus: Bridging Theory and Practice"** — Ongaro, 2014 (PhD dissertation). Extended TLA+ spec, implementation concerns.
|
||||
4. **KIP-595: A Raft Protocol for the Metadata Quorum** — The foundational KIP that introduced KRaft. `cwiki.apache.org/confluence/display/KAFKA/KIP-595`
|
||||
5. **KIP-630: Kafka Raft Snapshot** — Snapshot mechanism for KRaft metadata log. Status: Adopted.
|
||||
6. **KIP-996: Pre-Vote for KRaft** — Adds Pre-Vote phase to prevent disruptive servers. Status: Implementing.
|
||||
7. **KIP-853: KRaft Controller Membership Changes** — Dynamic quorum membership changes. Status: Implemented.
|
||||
8. **Apache Kafka source** — `kafka/raft/` package. Key files: `KafkaRaftClient.java`, `QuorumState.java`, `LeaderState.java`, `CandidateState.java`, `FollowerState.java`, `UnattachedState.java`, `ProspectiveState.java`, `ResignedState.java`, `EpochState.java`
|
||||
9. **Red Hat Deep Dive** — "A Deep Dive into Apache Kafka's KRaft Protocol" (developers.redhat.com, 2025). Covers KRaft v1 based on Kafka 4.1.0.
|
||||
|
||||
---
|
||||
|
||||
## 1. Raft State Machine (from TLA+ Spec)
|
||||
|
||||
*Reference: Source [1], [3]*
|
||||
|
||||
### 1.1 State Variables
|
||||
|
||||
Per server (`i ∈ Server`):
|
||||
|
||||
| Variable | Type | Description |
|
||||
|----------|------|-------------|
|
||||
| `currentTerm` | Nat | Current term number (monotonically increasing) |
|
||||
| `state` | {Follower, Candidate, Leader} | Server role |
|
||||
| `votedFor` | Server ∪ {Nil} | Candidate voted for in current term, or Nil |
|
||||
| `log` | Seq(LogEntry) | Sequence of log entries (index = position) |
|
||||
| `commitIndex` | Nat | Index of highest log entry known to be committed |
|
||||
| `nextIndex` | Server → Nat | (Leader only) Next log index to send to each follower |
|
||||
| `matchIndex` | Server → Nat | (Leader only) Highest log index replicated on each follower |
|
||||
| `votesResponded` | Set(Server) | (Candidate only) Servers that responded to RequestVote |
|
||||
| `votesGranted` | Set(Server) | (Candidate only) Servers that granted vote |
|
||||
|
||||
Global:
|
||||
|
||||
| Variable | Type | Description |
|
||||
|----------|------|-------------|
|
||||
| `messages` | Bag(Message) | In-flight messages (requests/responses) |
|
||||
|
||||
### 1.2 LogEntry Type
|
||||
|
||||
```
|
||||
LogEntry == { term: Nat, value: Value }
|
||||
```
|
||||
|
||||
### 1.3 Quorum
|
||||
|
||||
```
|
||||
Quorum == {i ∈ SUBSET(Server) : Cardinality(i) * 2 > Cardinality(Server)}
|
||||
```
|
||||
|
||||
Simple majority. The key property: any two quorums overlap.
|
||||
|
||||
### 1.4 Initial State
|
||||
|
||||
```
|
||||
currentTerm[i] = 1
|
||||
state[i] = Follower
|
||||
votedFor[i] = Nil
|
||||
log[i] = <<>> (empty sequence)
|
||||
commitIndex[i] = 0
|
||||
```
|
||||
|
||||
### 1.5 Actions (State Transitions)
|
||||
|
||||
#### Action 1: Timeout → Start Election
|
||||
|
||||
**Preconditions:**
|
||||
- `state[i] ∈ {Follower, Candidate}`
|
||||
|
||||
**Effects:**
|
||||
- `state[i] ← Candidate`
|
||||
- `currentTerm[i] ← currentTerm[i] + 1`
|
||||
- `votedFor[i] ← Nil`
|
||||
- `votesResponded[i] ← {}`
|
||||
- `votesGranted[i] ← {}`
|
||||
|
||||
#### Action 2: RequestVote Request (Candidate → Peer)
|
||||
|
||||
**Preconditions:**
|
||||
- `state[i] = Candidate`
|
||||
- `j ∉ votesResponded[i]`
|
||||
|
||||
**Effects:**
|
||||
- Send `RequestVoteRequest` with `{mterm: currentTerm[i], mlastLogTerm: LastTerm(log[i]), mlastLogIndex: Len(log[i]), msource: i, mdest: j}`
|
||||
|
||||
#### Action 3: HandleRequestVoteRequest (Peer → Candidate)
|
||||
|
||||
**Preconditions:**
|
||||
- `m.mterm ≤ currentTerm[i]`
|
||||
|
||||
**Log check (`logOk`):**
|
||||
```
|
||||
logOk ≡ m.mlastLogTerm > LastTerm(log[i])
|
||||
∨ (m.mlastLogTerm = LastTerm(log[i]) ∧ m.mlastLogIndex ≥ Len(log[i]))
|
||||
```
|
||||
|
||||
**Grant conditions:**
|
||||
```
|
||||
grant ≡ m.mterm = currentTerm[i] ∧ logOk ∧ votedFor[i] ∈ {Nil, j}
|
||||
```
|
||||
|
||||
**Effects (if grant):**
|
||||
- `votedFor[i] ← j`
|
||||
|
||||
**Effects (always):**
|
||||
- Reply with `RequestVoteResponse{mterm: currentTerm[i], mvoteGranted: grant}`
|
||||
|
||||
#### Action 4: HandleRequestVoteResponse (Candidate receives vote)
|
||||
|
||||
**Preconditions:**
|
||||
- `m.mterm = currentTerm[i]`
|
||||
|
||||
**Effects:**
|
||||
- `votesResponded[i] ← votesResponded[i] ∪ {j}`
|
||||
- If `m.mvoteGranted`: `votesGranted[i] ← votesGranted[i] ∪ {j}`
|
||||
|
||||
#### Action 5: BecomeLeader (Candidate → Leader)
|
||||
|
||||
**Preconditions:**
|
||||
- `state[i] = Candidate`
|
||||
- `votesGranted[i] ∈ Quorum`
|
||||
|
||||
**Effects:**
|
||||
- `state[i] ← Leader`
|
||||
- `nextIndex[i] ← [j ∈ Server → Len(log[i]) + 1]` for all j
|
||||
- `matchIndex[i] ← [j ∈ Server → 0]` for all j
|
||||
|
||||
#### Action 6: AppendEntries Request (Leader → Follower)
|
||||
|
||||
**Preconditions:**
|
||||
- `i ≠ j`
|
||||
- `state[i] = Leader`
|
||||
|
||||
**Effects:**
|
||||
- Send `AppendEntriesRequest` with entries from `nextIndex[i][j]` to `min(Len(log[i]), nextIndex[i][j])` (at most 1 entry per message in the spec)
|
||||
- Include `mprevLogIndex = nextIndex[i][j] - 1`, `mprevLogTerm`, `mcommitIndex`
|
||||
|
||||
#### Action 7: HandleAppendEntriesRequest (Follower receives entries)
|
||||
|
||||
**Preconditions:**
|
||||
- `m.mterm ≤ currentTerm[i]`
|
||||
|
||||
**Log consistency check (`logOk`):**
|
||||
```
|
||||
logOk ≡ m.mprevLogIndex = 0
|
||||
∨ (m.mprevLogIndex ≤ Len(log[i]) ∧ m.mprevLogTerm = log[i][m.mprevLogIndex].term)
|
||||
```
|
||||
|
||||
**Effects (if logOk AND m.mterm ≥ currentTerm[i]):**
|
||||
- Reset to Follower if Candidate
|
||||
- Update `currentTerm[i] ← m.mterm` if needed
|
||||
- Append/conflict resolution: if `mprevLogIndex > 0`, entries after `mprevLogIndex` that conflict are truncated
|
||||
- `commitIndex[i] ← min(m.mcommitIndex, Len(log[i]))`
|
||||
- Reply `AppendEntriesResponse{msuccess: TRUE, mmatchIndex: ...}`
|
||||
|
||||
**Effects (if !logOk OR m.mterm < currentTerm[i]):**
|
||||
- Reply `AppendEntriesResponse{msuccess: FALSE, mmatchIndex: 0}`
|
||||
|
||||
#### Action 8: AdvanceCommitIndex (Leader)
|
||||
|
||||
**Preconditions:**
|
||||
- `state[i] = Leader`
|
||||
|
||||
**Effects:**
|
||||
- Find highest `N` such that `N > commitIndex[i]` and a quorum of `matchIndex[i][k] ≥ N`
|
||||
- Only commit entries from current term: `log[i][N].term = currentTerm[i]`
|
||||
- `commitIndex[i] ← N`
|
||||
|
||||
#### Action 9: ClientRequest (Leader appends entry)
|
||||
|
||||
**Preconditions:**
|
||||
- `state[i] = Leader`
|
||||
|
||||
**Effects:**
|
||||
- Append `[term: currentTerm[i], value: v]` to `log[i]`
|
||||
|
||||
#### Action 10: Restart (Server crash recovery)
|
||||
|
||||
**Effects:**
|
||||
- `state[i] ← Follower`
|
||||
- Reset volatile state (`votesResponded`, `votesGranted`, `nextIndex`, `matchIndex`, `commitIndex`)
|
||||
- Preserve persistent state (`currentTerm`, `votedFor`, `log`)
|
||||
|
||||
---
|
||||
|
||||
## 2. KRaft Extensions Over Vanilla Raft
|
||||
|
||||
*References: Sources [4], [5], [6], [7], [8], [9]*
|
||||
|
||||
KRaft is Kafka's adaptation of Raft for metadata management. Key differences from vanilla Raft:
|
||||
|
||||
1. **No ZooKeeper:** KRaft replaces the ZooKeeper-based metadata quorum with a Raft-based one.
|
||||
2. **Metadata log:** The replicated log contains metadata records (topic configs, partition assignments), not user data.
|
||||
3. **Controller node:** KRaft has an "active controller" concept — the leader of the metadata quorum acts as the controller for the Kafka cluster.
|
||||
4. **Snapshotting:** KRaft supports snapshot-based log compaction (KIP-630).
|
||||
5. **Voters and observers:** Not all nodes are voters; some are observer nodes that replicate but don't vote.
|
||||
6. **Resignation:** A leader can voluntarily step down (immediate or graceful).
|
||||
7. **Pre-Vote:** KRaft implements Pre-Vote (KIP-996) to prevent disruptive servers from forcing unnecessary elections.
|
||||
8. **Epochs instead of terms:** KRaft uses "epoch" terminology instead of "term" (functionally equivalent).
|
||||
9. **Additional states:** KRaft adds Unattached, Prospective, Resigned, and Detached states beyond Follower/Candidate/Leader.
|
||||
|
||||
### 2.1 KRaft State Machine
|
||||
|
||||
The KRaft state machine is implemented in `QuorumState.java`. Unlike vanilla Raft's three-state model (Follower/Candidate/Leader), KRaft has a richer set of epoch-based states, all implementing the `EpochState` interface.
|
||||
|
||||
#### State Hierarchy
|
||||
|
||||
```
|
||||
EpochState (interface)
|
||||
├── UnattachedState — Known epoch, unknown leader (initial startup or learned higher epoch)
|
||||
├── ProspectiveState — Pre-Vote candidate; gathering pre-votes before becoming Candidate
|
||||
├── CandidateState — Standard Raft candidate; actively requesting votes
|
||||
├── FollowerState — Standard Raft follower; replicating from a leader
|
||||
├── LeaderState — Standard Raft leader; accepting client writes
|
||||
├── ResignedState — Gracefully stepped-down leader; still processing resignations
|
||||
└── DetachedState — Observer or non-voter; replicating but cannot vote
|
||||
```
|
||||
|
||||
#### Transition Diagram
|
||||
|
||||
```
|
||||
┌──────────────────────────────┐
|
||||
│ │
|
||||
▼ │
|
||||
┌──────────┐ Pre-Vote OK │
|
||||
│Unattached│────────────────┐ │
|
||||
└──────────┘ │ │
|
||||
│ ▼ │
|
||||
│ ┌────────────┐ │
|
||||
Discover │ │ Prospective│ │
|
||||
Leader │ │ (Pre-Vote)│ │
|
||||
│ └────────────┘ │
|
||||
│ │ │
|
||||
│ Pre-Vote │ │
|
||||
│ succeeded │ │
|
||||
│ ▼ │
|
||||
│ ┌────────────┐ │
|
||||
│ │ Candidate │───────┤ Won election
|
||||
│ └────────────┘ │
|
||||
│ │ │
|
||||
│ Lost │ Won election │
|
||||
│ election │ (quorum) │
|
||||
│ ▼ │
|
||||
│ ┌────────────┐ │
|
||||
└───────► │ Follower │◄────────┤
|
||||
└────────────┘ │
|
||||
│ │
|
||||
Become leader │
|
||||
│ │
|
||||
▼ │
|
||||
┌────────────┐ │
|
||||
│ Leader │───────────┘ Higher term
|
||||
└────────────┘
|
||||
│
|
||||
Resign (graceful)
|
||||
│
|
||||
▼
|
||||
┌────────────┐
|
||||
│ Resigned │
|
||||
└────────────┘
|
||||
```
|
||||
|
||||
Additionally, `DetachedState` is used for observers (non-voters) who track the leader but don't participate in elections.
|
||||
|
||||
---
|
||||
|
||||
## 3. KRaft State Variables (from Kafka Source)
|
||||
|
||||
*Reference: Source [8] — Apache Kafka `kafka/raft/` package*
|
||||
|
||||
### 3.1 Common State (QuorumState)
|
||||
|
||||
| Variable | Type | Description |
|
||||
|----------|------|-------------|
|
||||
| `localId` | Int | This node's replica ID |
|
||||
| `voters` | Set(Int) | Set of voter replica IDs |
|
||||
| `observers` | Set(Int) | Set of observer replica IDs |
|
||||
| `epochState` | EpochState | Current state object (one of the states below) |
|
||||
| `currentClaimedEpoch` | Int | Epoch this node last claimed (for persistence) |
|
||||
|
||||
### 3.2 UnattachedState
|
||||
|
||||
When a node knows about an epoch but hasn't discovered the leader yet, or is starting up.
|
||||
|
||||
| Variable | Type | Description |
|
||||
|----------|------|-------------|
|
||||
| `epoch` | Int | The epoch this node is in |
|
||||
| `votedId` | Int? | Replica ID voted for in this epoch, or -1 (unvoted) |
|
||||
|
||||
### 3.3 ProspectiveState (Pre-Vote, KIP-996)
|
||||
|
||||
A node that has started Pre-Vote but hasn't transitioned to Candidate yet. This prevents disruptive servers from forcing elections.
|
||||
|
||||
| Variable | Type | Description |
|
||||
|----------|------|-------------|
|
||||
| `epoch` | Int | The epoch for which Pre-Vote is being conducted |
|
||||
| `votedId` | Int? | Vote (always self during Pre-Vote) |
|
||||
| `hasSufficientVote` | Bool | Whether a quorum of pre-votes has been received |
|
||||
| `preVoteResponded` | Set(Int) | Voters that responded to Pre-Vote |
|
||||
| `preVoteGranted` | Set(Int) | Voters that granted Pre-Vote |
|
||||
| `gracePeriodExpired` | Bool | Whether the election timeout has expired |
|
||||
|
||||
**Transition to Candidate:** Only when `hasSufficientVote = true` AND `gracePeriodExpired = true`.
|
||||
|
||||
### 3.4 CandidateState
|
||||
|
||||
Standard Raft candidate with KRaft-specific additions.
|
||||
|
||||
| Variable | Type | Description |
|
||||
|----------|------|-------------|
|
||||
| `epoch` | Int | Current election epoch |
|
||||
| `votedId` | Int | Always `localId` (votes for self) |
|
||||
| `votes` | Set(Int) | Voter IDs that granted a vote |
|
||||
| `isVoteGranted` | Bool | Whether a quorum of votes has been received |
|
||||
| `isVoteRejected` | Bool | Whether the election is doomed (quorum impossible) |
|
||||
| `highWatermark` | Long | Last known high watermark at election start |
|
||||
| `retryVoteQuorumGracePeriod` | Bool | Whether to retry sending vote requests |
|
||||
|
||||
### 3.5 FollowerState
|
||||
|
||||
Standard Raft follower with KRaft-specific additions.
|
||||
|
||||
| Variable | Type | Description |
|
||||
|----------|------|-------------|
|
||||
| `epoch` | Int | Current epoch |
|
||||
| `leaderId` | Int | ID of the current leader |
|
||||
| `votedId` | Int? | Replica ID voted for (or -1) |
|
||||
| `highWatermark` | Long | Last known high watermark |
|
||||
| `lastCaughtUpTimeMs` | Long | Timestamp of last successful replication |
|
||||
| `lingerHighWatermark` | Long | High watermark at which we started lingering |
|
||||
| `isLingering` | Bool | Whether this follower is in linger mode (delaying transition) |
|
||||
|
||||
### 3.6 LeaderState
|
||||
|
||||
Standard Raft leader with KRaft-specific additions.
|
||||
|
||||
| Variable | Type | Description |
|
||||
|----------|------|-------------|
|
||||
| `epoch` | Int | Current epoch (same as currentTerm) |
|
||||
| `leaderId` | Int | This node's ID |
|
||||
| `highWatermark` | Long | Current high watermark (equivalent to commitIndex) |
|
||||
| `voterStates` | Map(Int, VoterState) | Per-voter tracking: nextOffset, matchOffset, lastCaughtUpTime |
|
||||
| `localId` | Int | This node's replica ID |
|
||||
| `retryForVoterEnabled` | Bool | Whether to retry AppendEntries to slow voters |
|
||||
|
||||
**VoterState sub-structure:**
|
||||
|
||||
| Variable | Type | Description |
|
||||
|----------|------|-------------|
|
||||
| `nextOffset` | Long | Next log offset to send to this voter (= nextIndex) |
|
||||
| `matchOffset` | Long | Highest offset known to be replicated on this voter (= matchIndex) |
|
||||
| `lastCaughtUpTimeMs` | Long | Timestamp of last successful catch-up |
|
||||
| `lastSentTimeMs` | Long | Timestamp of last AppendEntries sent |
|
||||
| `isVoter` | Bool | Whether this replica is a voter |
|
||||
|
||||
### 3.7 ResignedState
|
||||
|
||||
A leader that has gracefully stepped down. Not present in vanilla Raft.
|
||||
|
||||
| Variable | Type | Description |
|
||||
|----------|------|-------------|
|
||||
| `epoch` | Int | The epoch when the leader resigned |
|
||||
| `leaderId` | Int | Former leader's ID |
|
||||
|
||||
*Key behavior:* A resigned leader does not accept new client writes. It continues to process in-flight requests until they complete or time out. It then transitions to Unattached or Follower depending on what it learns about the new epoch.
|
||||
|
||||
### 3.8 DetachedState (Observer)
|
||||
|
||||
Used for observer (non-voter) nodes.
|
||||
|
||||
| Variable | Type | Description |
|
||||
|----------|------|-------------|
|
||||
| `epoch` | Int | Current epoch |
|
||||
| `leaderId` | Int | ID of the leader being followed |
|
||||
| `highWatermark` | Long | Last known high watermark |
|
||||
|
||||
*Key behavior:* Detached observers replicate the log but never vote or become candidates. They can transition to Follower or Unattached if they learn about a new epoch.
|
||||
|
||||
---
|
||||
|
||||
## 4. KRaft State Transitions (Detailed)
|
||||
|
||||
*Reference: Source [8], [9]*
|
||||
|
||||
### 4.1 Complete Transition Table
|
||||
|
||||
| From | To | Trigger | Preconditions |
|
||||
|------|----|---------|--------------|
|
||||
| Unattached | Prospective | Election timeout + Pre-Vote enabled | `votedId == -1`, `hasSufficientVote == false` |
|
||||
| Unattached | Follower | DiscoverLeader with valid leader | `leaderId` known, `epoch` matches |
|
||||
| Prospective | Candidate | Pre-Vote quorum reached + grace period expired | `hasSufficientVote ∧ gracePeriodExpired` |
|
||||
| Prospective | Follower | DiscoverLeader OR higher AppendEntries | `leaderId` known or higher term received |
|
||||
| Candidate | Leader | Election won (quorum of votes) | `isVoteGranted == true` |
|
||||
| Candidate | Follower | DiscoverLeader OR higher term AppendEntries | `leaderId` known or higher term received |
|
||||
| Follower | Prospective | Election timeout + no heartbeat | `votedId == -1`, Pre-Vote enabled |
|
||||
| Follower | Candidate | Election timeout + Pre-Vote disabled | `votedId == -1` |
|
||||
| Leader | Resigned | Graceful shutdown / Resign RPC | Leader decides to step down |
|
||||
| Leader | Follower | Higher term received | `m.epoch > currentEpoch` |
|
||||
| Resigned | Unattached | Resign processing complete + no leader known | All in-flight requests handled |
|
||||
| Resigned | Follower | Learn about new leader | `leaderId` known in new epoch |
|
||||
| Detached | Follower | Promoted to voter | Node gains voting right |
|
||||
| Any | Unattached | Higher epoch learned (no leader known) | `m.epoch > currentEpoch` |
|
||||
|
||||
### 4.2 Pre-Vote Protocol (KIP-996)
|
||||
|
||||
*Reference: Source [6]*
|
||||
|
||||
Pre-Vote prevents disruptive servers (those that are partitioned or have stale logs) from forcing unnecessary elections.
|
||||
|
||||
**Protocol:**
|
||||
|
||||
1. **Before becoming Candidate**, a server first enters Prospective state and sends Pre-Vote requests.
|
||||
2. **Pre-Vote Request:** `{lastOffset: Long, lastEpoch: Int}` — the prospective candidate advertises its log position.
|
||||
3. **Pre-Vote Response:** `{granted: Bool}` — a server grants Pre-Vote only if:
|
||||
- The prospective candidate's log is at least as up-to-date as the responder's
|
||||
- The responder has not heard from a valid leader recently (within election timeout)
|
||||
4. **Transition to Candidate:** Only after receiving a quorum of Pre-Vote grants AND the grace period expires.
|
||||
|
||||
**Why Pre-Vote matters for verification:**
|
||||
- Prevents a partitioned node with a stale term from disrupting the cluster
|
||||
- The invariant is: a node only enters Candidate state if it could potentially win an election
|
||||
- This eliminates a class of livelock scenarios where nodes continuously force elections they can't win
|
||||
|
||||
### 4.3 Resignation Protocol
|
||||
|
||||
*Reference: Source [8], [9]*
|
||||
|
||||
A KRaft leader can gracefully resign (step down) without crashing. This is not in vanilla Raft.
|
||||
|
||||
**Resign process:**
|
||||
1. Leader transitions to Resigned state
|
||||
2. Stops accepting new client writes
|
||||
3. Continues to serve in-flight AppendEntries responses
|
||||
4. Other nodes see an election timeout and start a new election
|
||||
5. Resigned leader may learn about the new leader and transition to Follower
|
||||
|
||||
**Verification concern:** During the resign window, the old leader's committed entries are still valid, but no new entries can be committed. This is a liveness property (eventually a new leader is elected), not a safety concern.
|
||||
|
||||
---
|
||||
|
||||
## 5. Safety Invariants
|
||||
|
||||
*References: Sources [1], [2], [3]*
|
||||
|
||||
These are the invariants we need to prove in SpeckDL/Z3.
|
||||
|
||||
### 5.1 Raft Paper Invariants (vanilla Raft)
|
||||
|
||||
**I1: Election Safety.** At most one leader per term.
|
||||
```
|
||||
∀ i, j ∈ Server:
|
||||
state[i] = Leader ∧ state[j] = Leader ∧ currentTerm[i] = currentTerm[j] → i = j
|
||||
```
|
||||
|
||||
**I2: Leader Completeness.** If a log entry is committed in term T, then all leaders for terms > T have that entry.
|
||||
```
|
||||
This is the core invariant. Proved via the "Leader Completeness Property" in the Raft paper.
|
||||
Inductive argument: a new leader must have all committed entries from prior terms
|
||||
because it received votes from a quorum that overlaps with the quorum that committed
|
||||
those entries.
|
||||
```
|
||||
|
||||
**I3: Log Matching.** If two entries in different logs have the same index and term, then all preceding entries are identical.
|
||||
```
|
||||
∀ i, j ∈ Server, idx:
|
||||
log[i][idx].term = log[j][idx].term → log[i][1..idx] = log[j][1..idx]
|
||||
```
|
||||
|
||||
**I4: Leader Append-Only.** A leader never overwrites or deletes entries in its log.
|
||||
```
|
||||
∀ i: state[i] = Leader → log[i] only grows (entries appended, never removed)
|
||||
```
|
||||
|
||||
**I5: Term Monotonicity.** Current term never decreases.
|
||||
```
|
||||
∀ i: currentTerm'[i] ≥ currentTerm[i]
|
||||
```
|
||||
|
||||
**I6: Commit Safety.** An entry is committed only if a quorum has replicated it.
|
||||
```
|
||||
commitIndex[i] advances only when a quorum of matchIndex[i][k] ≥ N
|
||||
Additionally: only entries from the current term can be committed via leader
|
||||
advance (restriction from Raft paper Figure 8).
|
||||
```
|
||||
|
||||
### 5.2 KRaft-Specific Invariants
|
||||
|
||||
**K1: Quorum Overlap.** Any two quorums in the same epoch share at least one voter.
|
||||
```
|
||||
∀ Q1, Q2 ∈ Quorum: Q1 ∩ Q2 ≠ ∅
|
||||
```
|
||||
|
||||
**K2: High Watermark Monotonicity.** A node's highWatermark never decreases.
|
||||
```
|
||||
∀ i: highWatermark'[i] ≥ highWatermark[i]
|
||||
```
|
||||
|
||||
**K3: High Watermark Validity.** A node's highWatermark is always ≤ the log end offset.
|
||||
```
|
||||
∀ i: highWatermark[i] ≤ logEndOffset[i]
|
||||
```
|
||||
|
||||
**K4: Observer Consistency.** An observer's log is a prefix of some voter's log that was committed.
|
||||
```
|
||||
∀ observer o, voter v, offset idx:
|
||||
o.hasOffset(idx) → ∃v ∈ Voters: v.committed(idx) ∧ o.log[1..idx] = v.log[1..idx]
|
||||
```
|
||||
|
||||
**K5: Leader Uniqueness (KRaft).** At most one leader per epoch across all nodes.
|
||||
```
|
||||
∀ i, j ∈ Replicas:
|
||||
state[i] = Leader ∧ state[j] = Leader ∧ epoch[i] = epoch[j] → i = j
|
||||
```
|
||||
|
||||
**K6: Vote Uniqueness.** A voter votes for at most one candidate per epoch.
|
||||
```
|
||||
∀ i ∈ Voters, epoch e: votedFor[i][e] is either Nil or a single replica ID
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
## 6. Snapshots (KIP-630)
|
||||
|
||||
*Reference: Source [5]*
|
||||
|
||||
KRaft supports snapshot-based log compaction for the metadata log.
|
||||
|
||||
### 6.1 Snapshot Mechanics
|
||||
|
||||
- **Snapshot trigger:** When the log grows beyond a configured threshold
|
||||
- **Snapshot contents:** Full metadata state at a given offset (topic configs, partition assignments, etc.)
|
||||
- **Snapshot delivery:** Leader sends snapshots to followers that are lagging (similar to Raft's InstallSnapshot)
|
||||
|
||||
### 6.2 State Changes for Snapshots
|
||||
|
||||
| Variable | Type | Description |
|
||||
|----------|------|-------------|
|
||||
| `snapshotId` | {epoch: Int, endOffset: Long} | Identifies a snapshot by epoch and end offset |
|
||||
| `lastSnapshotOffset` | Long | Offset of the last snapshot on this node |
|
||||
| `recoveryState` | Enum | {RECOVERING, COMPLETE} — whether snapshot recovery is in progress |
|
||||
|
||||
### 6.3 Invariants for Snapshots
|
||||
|
||||
**S1: Snapshot Offset Monotonicity.** Snapshot offsets increase monotonically.
|
||||
```
|
||||
snapshotId.endOffset[i]' ≥ snapshotId.endOffset[i]
|
||||
```
|
||||
|
||||
**S2: Snapshot Consistency.** A snapshot at offset N contains all entries committed before N.
|
||||
```
|
||||
∀ i, snapshot at offset N:
|
||||
snapshot.epoch = log[N].term ∧ snapshot contains all committed entries up to N
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
## 7. Known Verification Gaps and Bugs
|
||||
|
||||
*References: Smart Casual Verification blog, raft-dev Google Group, Source [6]*
|
||||
|
||||
### 7.1 Known Bugs in Raft Implementations
|
||||
|
||||
**Bug 1: Single-Server Membership Change Safety Bug (2015)**
|
||||
- **Source:** raft-dev Google Group, reported by Ongaro
|
||||
- **Issue:** The original Raft paper's algorithm for single-server membership changes has a safety bug. If two configuration changes overlap, the cluster can lose quorum overlap.
|
||||
- **Mitigation:** Joint consensus (adding then removing in separate steps) is safe. KRaft uses joint consensus for membership changes (KIP-853).
|
||||
- **Formal verification target:** Prove that KRaft's joint consensus approach maintains quorum overlap during membership changes.
|
||||
|
||||
**Bug 2: Stale Leader Committing Old-Term Entries (Figure 8 Bug)**
|
||||
- **Source:** Raft paper, Figure 8
|
||||
- **Issue:** A leader must not commit entries from previous terms directly. It can only commit entries from its current term, and previous-term entries are committed indirectly when the current-term entry is committed.
|
||||
- **Status:** Correctly handled in KRaft (AdvanceCommitIndex only advances for current-term entries).
|
||||
- **Formal verification target:** Prove that `AdvanceCommitIndex` only advances `commitIndex` when the entry at the target index has `term == currentTerm`.
|
||||
|
||||
**Bug 3: Log Truncation During Leader Change**
|
||||
- **Source:** Common implementation bug across multiple Raft implementations
|
||||
- **Issue:** When a new leader overwrites conflicting entries on a follower, the truncation must be atomic. If the node crashes mid-truncation, the log can be left in an inconsistent state.
|
||||
- **Status:** KRaft handles this by truncating before appending, but edge cases around partial truncation exist.
|
||||
- **Formal verification target:** Prove that log truncation is atomic (either fully applied or not at all).
|
||||
|
||||
**Bug 4: Disruptive Servers (Pre-Vote Target)**
|
||||
- **Source:** KIP-996, Ongaro dissertation §9.6
|
||||
- **Issue:** A server that is partitioned or has a stale network connection can repeatedly force elections, disrupting the cluster. Without Pre-Vote, a partitioned server increments its term and forces elections it can't win.
|
||||
- **Status:** KIP-996 (Pre-Vote) addresses this by requiring a server to confirm it can win before starting an election.
|
||||
- **Formal verification target:** Prove that with Pre-Vote, a node that cannot win an election never transitions to Candidate state.
|
||||
|
||||
### 7.2 Smart Casual Verification Findings
|
||||
|
||||
*Reference: Decentralized Thoughts blog, "Smart Casual Verification"*
|
||||
|
||||
In a systematic review of consensus protocol implementations, researchers found:
|
||||
|
||||
1. **5 safety bugs** — violations of agreement or integrity properties
|
||||
2. **1 liveness bug** — violation of termination under expected conditions
|
||||
3. All bugs were found through informal reasoning about protocol invariants, not formal proof
|
||||
4. Key pattern: most bugs occur in edge cases around term changes and log conflicts
|
||||
|
||||
### 7.3 Open Verification Targets
|
||||
|
||||
These are properties that should be verified in the SpeckDL/Z3 spec:
|
||||
|
||||
1. **Election safety under network partitions:** Prove I1 (election safety) holds even during partitions.
|
||||
2. **Log matching after truncation:** Prove I3 (log matching) holds after follower log truncation.
|
||||
3. **Leader completeness after Pre-Vote:** Prove I2 (leader completeness) holds with the Pre-Vote extension.
|
||||
4. **High watermark advancement:** Prove that `highWatermark` only advances when a quorum has replicated.
|
||||
5. **Graceful resignation liveness:** Prove that after a leader resigns, a new leader is eventually elected (liveness, assuming fair loss and eventual delivery).
|
||||
6. **Observer divergence:** Prove that observers cannot diverge from voters (K4).
|
||||
7. **Joint consensus safety (KIP-853):** Prove that during membership changes, quorum overlap is maintained.
|
||||
|
||||
---
|
||||
|
||||
## 8. Producer Acknowledgement Semantics (for M1.3)
|
||||
|
||||
*Deferred — included here for reference only.*
|
||||
|
||||
### acks=0 (Fire and forget)
|
||||
- Producer sends and doesn't wait for response
|
||||
- No durability guarantee
|
||||
- Invariant: **None** (messages can be lost)
|
||||
|
||||
### acks=1 (Leader acknowledgment)
|
||||
- Producer waits for leader to write to local log
|
||||
- Durability: survives leader failure, but NOT follower failure
|
||||
- Invariant: **If ack received, entry exists in leader's log**
|
||||
|
||||
### acks=all (ISR acknowledgment)
|
||||
- Producer waits for all in-sync replicas (ISR) to acknowledge
|
||||
- Durability: survives any failure that leaves a quorum
|
||||
- Invariant: **If ack received, entry is committed (quorum has replicated)**
|
||||
|
||||
### Exactly-once Semantics
|
||||
- Requires idempotent producer + transaction coordinator
|
||||
- Idempotent producer: assigns sequence numbers; broker deduplicates
|
||||
- Transaction coordinator: two-phase commit across partitions
|
||||
|
||||
### Key Invariants for Producer Acks
|
||||
|
||||
1. `acks=all` → no data loss on leader failover (bounded to quorum availability)
|
||||
2. Idempotent producer → no duplicate messages for same PID + sequence number
|
||||
3. Transaction atomicity → all partitions in a transaction commit or none do
|
||||
|
||||
---
|
||||
|
||||
## 9. Consumer Group Rebalancing (for M1.3)
|
||||
|
||||
*Deferred — included here for reference only.*
|
||||
|
||||
### States
|
||||
- Empty → Joining → Stable → Rebalancing → Stable
|
||||
|
||||
### Actions
|
||||
- JoinGroup: consumer requests to join
|
||||
- SyncGroup: consumer receives assignment
|
||||
- Heartbeat: consumer indicates liveness
|
||||
- LeaveGroup: consumer departs
|
||||
- Rebalance: triggered by membership change or topic partition change
|
||||
|
||||
### Invariants
|
||||
1. No concurrent assignments to the same partition
|
||||
2. All partitions assigned when group is stable
|
||||
3. Offset monotonicity: committed offsets never decrease
|
||||
4. No two consumers assigned the same partition simultaneously
|
||||
|
||||
---
|
||||
|
||||
## 10. KIPs Reference
|
||||
|
||||
| KIP | Title | Status | Relevance |
|
||||
|-----|-------|--------|-----------|
|
||||
| KIP-500 | Next Generation Client Protocol | Adopted | Foundation for KRaft |
|
||||
| KIP-595 | A Raft Protocol for the Metadata Quorum | Adopted | Core KRaft protocol design |
|
||||
| KIP-630 | Kafka Raft Snapshot | Adopted | Snapshot/compaction for metadata log |
|
||||
| KIP-642 | Dynamic Configuration in KRaft | Adopted | Dynamic config updates via KRaft |
|
||||
| KIP-853 | KRaft Controller Membership Changes | Implemented | Joint consensus for membership changes |
|
||||
| KIP-996 | Pre-Vote for KRaft | Implementing | Pre-Vote phase to prevent disruptive elections |
|
||||
| KIP-830 | KRaft Metadata Quorum | Adopted | Metadata quorum implementation details |
|
||||
|
||||
---
|
||||
|
||||
## Appendix A: Message Types (KRaft)
|
||||
|
||||
### Internal KRaft RPC Messages
|
||||
|
||||
| Message | Direction | Fields |
|
||||
|---------|-----------|--------|
|
||||
| `VoteRequest` | Candidate → Voter | `candidateId`, `epoch`, `lastOffset`, `lastEpoch` |
|
||||
| `VoteResponse` | Voter → Candidate | `epoch`, `voteGranted`, `leaderId` |
|
||||
| `BeginQuorumEpoch` | Leader → Follower | `leaderId`, `epoch` |
|
||||
| `EndQuorumEpoch` | Leader → Voter (resign) | `leaderId`, `epoch` |
|
||||
| `FetchSnapshot` | Follower → Leader | `snapshotId`, `offset` |
|
||||
| `Fetch` | Follower → Leader | `followerId`, `epoch`, `lastFetchedEpoch`, `lastFetchedOffset`, `maxBytes` |
|
||||
| `FetchResponse` | Leader → Follower | `epoch`, `leaderId`, `highWatermark`, `records` |
|
||||
|
||||
*Note: KRaft uses `BeginQuorumEpoch` as the heartbeat mechanism (instead of vanilla Raft's empty AppendEntries).*
|
||||
|
||||
---
|
||||
|
||||
## Appendix B: Key Differences from Vanilla Raft
|
||||
|
||||
| Aspect | Vanilla Raft | KRaft |
|
||||
|--------|-------------|-------|
|
||||
| Term naming | "Term" | "Epoch" (functionally equivalent) |
|
||||
| Heartbeat | Empty AppendEntries | BeginQuorumEpoch |
|
||||
| Resignation | Not specified | EndQuorumEpoch (graceful shutdown) |
|
||||
| Pre-Vote | Not in original paper | ProspectiveState (KIP-996) |
|
||||
| States | Follower, Candidate, Leader | + Unattached, Prospective, Resigned, Detached |
|
||||
| Snapshot | InstallSnapshot | FetchSnapshot (KIP-630) |
|
||||
| Membership | Single-server or joint | Joint consensus only (KIP-853) |
|
||||
| Log content | Arbitrary client values | Metadata records (topic configs, partition assignments) |
|
||||
| Quorum | All servers vote | Voters vote, observers replicate |
|
||||
| Client ID | Not specified | Replica ID (localId) |
|
||||
|
||||
---
|
||||
|
||||
*Document compiled from: Raft TLA+ spec (Ongaro 2014), Apache Kafka source code (`kafka/raft/`), KIP-595/630/642/853/996, Red Hat KRaft deep dive, Smart Casual Verification findings.*
|
||||
452
examples/OAuth2AuthorizationCode.speck
Normal file
452
examples/OAuth2AuthorizationCode.speck
Normal file
|
|
@ -0,0 +1,452 @@
|
|||
speck OAuth2AuthorizationCode {
|
||||
// OAuth 2.0 Authorization Code Flow with PKCE
|
||||
// Implements RFC 6749 Section 4.1 (Authorization Code Grant) with RFC 7636 (PKCE)
|
||||
// Key security properties: CSRF protection, code reuse prevention, replay resistance, PKCE integrity
|
||||
|
||||
// === Types ===
|
||||
|
||||
type ClientId = String
|
||||
type RedirectUri = String
|
||||
type State = String
|
||||
type CodeChallenge = String
|
||||
type CodeVerifier = String
|
||||
type AuthorizationCode = String
|
||||
type AccessToken = String
|
||||
type RefreshToken = String
|
||||
type Scope = String
|
||||
type TokenType = String
|
||||
type ClientSecret = String
|
||||
type UserId = String
|
||||
type SessionId = String
|
||||
|
||||
type TokenResponse = {
|
||||
access_token: AccessToken,
|
||||
token_type: TokenType,
|
||||
expires_in: Nat,
|
||||
refresh_token: RefreshToken | null,
|
||||
scope: Scope
|
||||
}
|
||||
|
||||
type AuthorizationRequest = {
|
||||
client_id: ClientId,
|
||||
redirect_uri: RedirectUri,
|
||||
response_type: String, // "code"
|
||||
state: State,
|
||||
code_challenge: CodeChallenge,
|
||||
code_challenge_method: String, // "S256" or "plain"
|
||||
scope: Scope
|
||||
}
|
||||
|
||||
type TokenRequest = {
|
||||
client_id: ClientId,
|
||||
client_secret: ClientSecret,
|
||||
code: AuthorizationCode,
|
||||
redirect_uri: RedirectUri,
|
||||
code_verifier: CodeVerifier
|
||||
}
|
||||
|
||||
type RefreshRequest = {
|
||||
client_id: ClientId,
|
||||
client_secret: ClientSecret,
|
||||
refresh_token: RefreshToken,
|
||||
scope: Scope | null
|
||||
}
|
||||
|
||||
// === State ===
|
||||
|
||||
state {
|
||||
// Registered clients
|
||||
clients: Map(ClientId, { redirect_uris: Set(RedirectUri), client_secret: ClientSecret })
|
||||
|
||||
// Authorization codes in flight
|
||||
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: Nat,
|
||||
used: Bool
|
||||
})
|
||||
|
||||
// Access tokens issued
|
||||
accessTokens: Map(AccessToken, {
|
||||
client_id: ClientId,
|
||||
user_id: UserId,
|
||||
scope: Scope,
|
||||
expires_at: Nat,
|
||||
session_id: SessionId,
|
||||
refresh_token: RefreshToken
|
||||
})
|
||||
|
||||
// Refresh tokens
|
||||
refreshTokens: Map(RefreshToken, {
|
||||
client_id: ClientId,
|
||||
user_id: UserId,
|
||||
scope: Scope,
|
||||
access_token: AccessToken,
|
||||
created_at: Nat
|
||||
})
|
||||
|
||||
// User sessions
|
||||
sessions: Map(SessionId, { user_id: UserId })
|
||||
|
||||
// Nonce for state to prevent CSRF
|
||||
stateNonces: Map(State, { client_id: ClientId, redirect_uri: RedirectUri })
|
||||
|
||||
// PKCE challenge nonces
|
||||
pkceChallenges: Map(CodeChallenge, { code_verifier_hash: String, method: String })
|
||||
|
||||
// Clock (abstracted as monotonically increasing)
|
||||
currentTime: Nat
|
||||
}
|
||||
|
||||
// === Initialization ===
|
||||
|
||||
init {
|
||||
clients == emptyMap
|
||||
authorizationCodes == emptyMap
|
||||
accessTokens == emptyMap
|
||||
refreshTokens == emptyMap
|
||||
sessions == emptyMap
|
||||
stateNonces == emptyMap
|
||||
pkceChallenges == emptyMap
|
||||
currentTime == 0
|
||||
}
|
||||
|
||||
// === Invariants ===
|
||||
|
||||
// Invariant 1: No token leakage - tokens are only accessible to authorized parties
|
||||
invariant NoTokenLeakage {
|
||||
// Access tokens are bound to specific clients and users
|
||||
forall token in accessTokens.keys:
|
||||
let t := accessTokens[token]
|
||||
t.client_id in clients.keys and
|
||||
exists s in sessions.keys: sessions[s].user_id == t.user_id
|
||||
|
||||
// Refresh tokens are only accessible to the client that requested them
|
||||
forall rt in refreshTokens.keys:
|
||||
let r := refreshTokens[rt]
|
||||
r.client_id in clients.keys
|
||||
|
||||
// Authorization codes are only sent to the registered redirect URI
|
||||
forall code in authorizationCodes.keys:
|
||||
let c := authorizationCodes[code]
|
||||
c.client_id in clients.keys and
|
||||
c.redirect_uri in clients[c.client_id].redirect_uris
|
||||
}
|
||||
|
||||
// Invariant 2: CSRF protection - state parameter matches between authorize and callback
|
||||
invariant StateCSRFProtection {
|
||||
// Every state must have been registered by the client
|
||||
forall state in stateNonces.keys:
|
||||
let n := stateNonces[state]
|
||||
n.client_id in clients.keys and
|
||||
n.redirect_uri in clients[n.client_id].redirect_uris
|
||||
|
||||
// State can only be used by the client that created it
|
||||
forall code in authorizationCodes.keys:
|
||||
let c := authorizationCodes[code]
|
||||
c.state in stateNonces.keys
|
||||
}
|
||||
|
||||
// Invariant 3: Authorization codes are single-use (cannot be reused)
|
||||
invariant AuthorizationCodeSingleUse {
|
||||
forall code in authorizationCodes.keys:
|
||||
let c := authorizationCodes[code]
|
||||
c.used == false implies
|
||||
not exists action in next:
|
||||
action.name == "ExchangeCode" and action.params.code == code
|
||||
}
|
||||
|
||||
// Invariant 4: Tokens have bounded validity (replay attack resistance)
|
||||
invariant TokenValidityBounded {
|
||||
// Access tokens expire after a reasonable time
|
||||
forall token in accessTokens.keys:
|
||||
let t := accessTokens[token]
|
||||
t.expires_at > currentTime
|
||||
|
||||
// Refresh tokens expire after a longer period
|
||||
forall rt in refreshTokens.keys:
|
||||
let r := refreshTokens[rt]
|
||||
// (Simplified: refresh tokens should have expiration, but we track creation time)
|
||||
currentTime - r.created_at <= 7776000 // 90 days max
|
||||
}
|
||||
|
||||
// Invariant 5: PKCE prevents authorization code interception
|
||||
invariant PKCECodeInterceptionPrevention {
|
||||
// Code verifier must hash to the code challenge
|
||||
forall challenge in pkceChallenges.keys:
|
||||
let c := pkceChallenges[challenge]
|
||||
// In practice, this would use actual hashing, but we verify the relationship
|
||||
exists verifier in authorizationCodes.keys:
|
||||
let a := authorizationCodes[verifier]
|
||||
a.code_challenge == challenge and
|
||||
a.code_challenge_method == c.method
|
||||
|
||||
// Code verifier is only used once with the matching challenge
|
||||
forall code in authorizationCodes.keys:
|
||||
let c := authorizationCodes[code]
|
||||
c.used == false implies
|
||||
pkceChallenges[c.code_challenge].code_verifier_hash == hash(c.code_verifier, c.code_challenge_method)
|
||||
}
|
||||
|
||||
// Invariant 6: Redirect URI must match between authorize and token exchange
|
||||
invariant RedirectUriConsistency {
|
||||
forall code in authorizationCodes.keys:
|
||||
let c := authorizationCodes[code]
|
||||
// The redirect URI used in token exchange must match what was in authorize
|
||||
true // This is enforced in the ExchangeCode action
|
||||
}
|
||||
|
||||
// Invariant 7: Client authentication required for token exchange
|
||||
invariant ClientAuthenticationRequired {
|
||||
forall code in authorizationCodes.keys:
|
||||
let c := authorizationCodes[code]
|
||||
c.client_id in clients.keys implies
|
||||
exists r in refreshTokens.keys:
|
||||
refreshTokens[r].client_id == c.client_id
|
||||
}
|
||||
|
||||
// === Actions ===
|
||||
|
||||
// Action 1: Authorize - Client requests authorization code
|
||||
action Authorize(client: ClientId, redirectUri: RedirectUri, scope: Scope, userId: UserId, sessionId: SessionId) {
|
||||
require client in clients.keys
|
||||
require redirectUri in clients.client.redirect_uris
|
||||
require sessionId in sessions.keys
|
||||
require sessions[sessionId].user_id == userId
|
||||
|
||||
// Generate unique state (CSRF protection)
|
||||
let state := "state_" + hash(client + redirectUri + currentTime)
|
||||
|
||||
// Generate PKCE code challenge
|
||||
let codeVerifier := "verifier_" + hash(client + userId + currentTime)
|
||||
let codeChallenge := hash(codeVerifier, "S256")
|
||||
|
||||
// Register state nonce
|
||||
stateNonces[state] := { client_id: client, redirect_uri: redirectUri }
|
||||
|
||||
// Register PKCE challenge
|
||||
pkceChallenges[codeChallenge] := { code_verifier_hash: hash(codeVerifier, "S256"), method: "S256" }
|
||||
|
||||
// Create authorization code
|
||||
let authCode := "code_" + hash(client + userId + currentTime)
|
||||
authorizationCodes[authCode] := {
|
||||
client_id: client,
|
||||
redirect_uri: redirectUri,
|
||||
state: state,
|
||||
code_challenge: codeChallenge,
|
||||
code_challenge_method: "S256",
|
||||
scope: scope,
|
||||
user_id: userId,
|
||||
session_id: sessionId,
|
||||
created_at: currentTime,
|
||||
used: false
|
||||
}
|
||||
|
||||
emit AuthorizationRequested {
|
||||
client_id: client,
|
||||
redirect_uri: redirectUri,
|
||||
state: state,
|
||||
scope: scope,
|
||||
user_id: userId,
|
||||
session_id: sessionId,
|
||||
authorization_code: authCode
|
||||
}
|
||||
}
|
||||
|
||||
// Action 2: Approve - User grants consent (simulated: user confirms action)
|
||||
action ApproveAuthorization(code: AuthorizationCode, userId: UserId) {
|
||||
require code in authorizationCodes.keys
|
||||
let c := authorizationCodes[code]
|
||||
require c.user_id == userId
|
||||
require c.used == false
|
||||
|
||||
// Mark as approved (ready for exchange)
|
||||
emit CodeIssued {
|
||||
authorization_code: code,
|
||||
client_id: c.client_id,
|
||||
redirect_uri: c.redirect_uri,
|
||||
state: c.state,
|
||||
scope: c.scope,
|
||||
user_id: userId
|
||||
}
|
||||
}
|
||||
|
||||
// Action 3: ExchangeCode - Client exchanges code for tokens
|
||||
action ExchangeCode(req: TokenRequest) {
|
||||
require req.client_id in clients.keys
|
||||
|
||||
// Verify authorization code exists and is not used
|
||||
require req.code in authorizationCodes.keys
|
||||
let c := authorizationCodes[req.code]
|
||||
require c.used == false
|
||||
require c.client_id == req.client_id
|
||||
require c.redirect_uri == req.redirect_uri
|
||||
|
||||
// Verify PKCE: code_verifier must hash to code_challenge
|
||||
let expectedChallenge := hash(req.code_verifier, c.code_challenge_method)
|
||||
require expectedChallenge == c.code_challenge
|
||||
|
||||
// Mark code as used (single-use enforcement)
|
||||
authorizationCodes[req.code].used := true
|
||||
|
||||
// Remove PKCE challenge (one-time use)
|
||||
pkceChallenges[c.code_challenge] := null
|
||||
|
||||
// Remove state nonce (one-time use)
|
||||
stateNonces[c.state] := null
|
||||
|
||||
// Issue access token
|
||||
let accessToken := "access_" + hash(req.client_id + c.user_id + currentTime)
|
||||
let refreshToken := "refresh_" + hash(req.client_id + c.user_id + currentTime)
|
||||
let expiresAt := currentTime + 3600 // 1 hour
|
||||
|
||||
accessTokens[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
|
||||
}
|
||||
|
||||
refreshTokens[refreshToken] := {
|
||||
client_id: req.client_id,
|
||||
user_id: c.user_id,
|
||||
scope: c.scope,
|
||||
access_token: accessToken,
|
||||
created_at: currentTime
|
||||
}
|
||||
|
||||
emit TokenIssued {
|
||||
access_token: accessToken,
|
||||
token_type: "Bearer",
|
||||
expires_in: 3600,
|
||||
refresh_token: refreshToken,
|
||||
scope: c.scope,
|
||||
client_id: req.client_id,
|
||||
user_id: c.user_id
|
||||
}
|
||||
}
|
||||
|
||||
// Action 4: RefreshToken - Client refreshes expired access token
|
||||
action RefreshToken(req: RefreshRequest) {
|
||||
require req.client_id in clients.keys
|
||||
|
||||
// Verify refresh token exists
|
||||
require req.refresh_token in refreshTokens.keys
|
||||
let r := refreshTokens[req.refresh_token]
|
||||
require r.client_id == req.client_id
|
||||
|
||||
// Mark old access token as revoked (implicit)
|
||||
accessTokens[r.access_token] := null
|
||||
|
||||
// Issue new tokens
|
||||
let newAccessToken := "access_" + hash(req.client_id + r.user_id + currentTime)
|
||||
let newRefreshToken := "refresh_" + hash(req.client_id + r.user_id + currentTime)
|
||||
let expiresAt := currentTime + 3600
|
||||
|
||||
accessTokens[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
|
||||
}
|
||||
|
||||
refreshTokens[newRefreshToken] := {
|
||||
client_id: req.client_id,
|
||||
user_id: r.user_id,
|
||||
scope: req.scope.or(r.scope),
|
||||
access_token: newAccessToken,
|
||||
created_at: currentTime
|
||||
}
|
||||
|
||||
// Remove old refresh token
|
||||
refreshTokens[req.refresh_token] := null
|
||||
|
||||
emit TokenRefreshed {
|
||||
access_token: newAccessToken,
|
||||
token_type: "Bearer",
|
||||
expires_in: 3600,
|
||||
refresh_token: newRefreshToken,
|
||||
scope: req.scope.or(r.scope),
|
||||
client_id: req.client_id,
|
||||
user_id: r.user_id
|
||||
}
|
||||
}
|
||||
|
||||
// Action 5: RevokeToken - Client revokes a token
|
||||
action RevokeToken(client: ClientId, token: String, tokenType: String) {
|
||||
require client in clients.keys
|
||||
|
||||
if tokenType == "access" {
|
||||
require token in accessTokens.keys
|
||||
let t := accessTokens[token]
|
||||
require t.client_id == client
|
||||
|
||||
accessTokens[token] := null
|
||||
|
||||
// Also revoke associated refresh token
|
||||
refreshTokens[t.refresh_token] := null
|
||||
} else if tokenType == "refresh" {
|
||||
require token in refreshTokens.keys
|
||||
let r := refreshTokens[token]
|
||||
require r.client_id == client
|
||||
|
||||
refreshTokens[token] := null
|
||||
accessTokens[r.access_token] := null
|
||||
}
|
||||
|
||||
emit TokenRevoked {
|
||||
token: token,
|
||||
token_type: tokenType,
|
||||
client_id: client
|
||||
}
|
||||
}
|
||||
|
||||
// Action 6: PKCE Verification Step (explicit verification for documentation)
|
||||
action VerifyPKCE(code: AuthorizationCode, verifier: CodeVerifier) {
|
||||
require code in authorizationCodes.keys
|
||||
let c := authorizationCodes[code]
|
||||
require c.used == false
|
||||
|
||||
// Verify the code verifier hashes to the code challenge
|
||||
let expectedChallenge := hash(verifier, c.code_challenge_method)
|
||||
require expectedChallenge == c.code_challenge
|
||||
|
||||
// This action documents the PKCE verification step
|
||||
emit PKCEVerified {
|
||||
authorization_code: code,
|
||||
code_challenge: c.code_challenge,
|
||||
code_challenge_method: c.code_challenge_method,
|
||||
verifier_hash: hash(verifier, c.code_challenge_method)
|
||||
}
|
||||
}
|
||||
|
||||
// === Next Actions ===
|
||||
|
||||
next:
|
||||
Authorize
|
||||
| ApproveAuthorization
|
||||
| ExchangeCode
|
||||
| RefreshToken
|
||||
| RevokeToken
|
||||
| VerifyPKCE
|
||||
|
||||
// === Verification ===
|
||||
|
||||
verify: Always(NoTokenLeakage)
|
||||
verify: Always(StateCSRFProtection)
|
||||
verify: Always(AuthorizationCodeSingleUse)
|
||||
verify: Always(TokenValidityBounded)
|
||||
verify: Always(PKCECodeInterceptionPrevention)
|
||||
verify: Always(RedirectUriConsistency)
|
||||
verify: Always(ClientAuthenticationRequired)
|
||||
}
|
||||
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