Issues

docs(skills): design 層を検証に使うとき、何を書き何を回すか — 見つけたい誤りで破れる性質を宣言で書く・設計変更に diff を足す・原子性の宣言は実装側のテストで確かめる(事前登録実験、2 題材)

ymm-oss/fsl#1304 · opened

on Oct 11, 2026

governance: a failed preservation does not affect check/verify result or exit code

ymm-oss/fsl#1303 · opened

on Oct 11, 2026

refine: --depth before the positional arguments is read as a file path (io error)

ymm-oss/fsl#1301 · opened

on Oct 11, 2026

docs(skills): AI 実装の入力としての requirements spec — 拒否の規則は散文でなく宣言で書き、意図を確かめる前に conformance で実装を合わせ込ませない(事前登録の ablation 実験から)

ymm-oss/fsl#1300 · opened

on Oct 11, 2026

fix(compose): 部品の状態を参照する leadsTo が「public Kernel cannot type identifier」で exit 2 になる

ymm-oss/fsl#1297 · opened

on Oct 9, 2026

feat(verify,runtime): 探索と solver の上限を共通の `Budget` 型にまとめて打ち切りを型で `unknown_budget` へ運び、BMC と induction に資源上限（rlimit）を入れる

ymm-oss/fsl#1288 · opened

on Oct 8, 2026

· M23 主張の勘定: 義務台帳と fail-closed

refactor(verify): verify のパイプライン（段の順序・エンジン選択・auto の fallback・lemma 判定）を bin module の verification.rs から library へ出し、Worker も同じ関数を呼んで status を返す

ymm-oss/fsl#1287 · opened

on Oct 8, 2026

· M11 内部品質: 単一オーナーシップと契約整合

refactor(outcome): 結果の意味（result の分類・exit 表・RefinementVerdict の公開語・verify の節の型）を fsl-tools より下の層へ移し、html・ledger・document・Worker が JSON を文字列 key で読み直さないようにする

ymm-oss/fsl#1286 · opened

on Oct 8, 2026

· M11 内部品質: 単一オーナーシップと契約整合

refactor(forbidden): acceptance / forbidden の契約を、gate を通った値しか受け取れない型にする（parse, don't validate）

ymm-oss/fsl#1285 · opened

on Oct 8, 2026

· M23 主張の勘定: 義務台帳と fail-closed

refactor(core): 名前の内部表記と公開表記の変換（compose の `__`↔`.`、合成の違反名 `_partial_`・`_bounds_` など）を 1 つの型にまとめる

ymm-oss/fsl#1284 · opened

on Oct 8, 2026

· M11 内部品質: 単一オーナーシップと契約整合

perf(mutate): `--oracle-attribution` が killed の mutant ごとに主 oracle を計算し直す — 主 oracle の結果を再利用する

ymm-oss/fsl#1282 · opened

on Oct 8, 2026

· M4 検証・分析エビデンス強化

perf(mutate): mutant の oracle と baseline が Z3 BMC 固定で、explicit なら桁違いに速い spec でも遅い — explicit 先行（`--engine auto` と同じ規則）にし、mutant ごとの進捗を stderr に出す

ymm-oss/fsl#1281 · opened

on Oct 8, 2026

· M4 検証・分析エビデンス強化

feat(mutate): 単独の対応づけファイルによる `refine` を kill oracle に加える

ymm-oss/fsl#1280 · opened

on Oct 7, 2026

feat(testgen): 実装への配線を生成ファイルの外に置き、再生成で消えないようにする

ymm-oss/fsl#1279 · opened

on Oct 7, 2026

feat(document): 外部文書（MyST など）から FSL 要素を参照するための索引を出す。business 層も対象にする

ymm-oss/fsl#1278 · opened

on Oct 7, 2026

fix(document): 生成要件文書の frontmatter `source:` が `document check` に束縛されず、MyST では不正なキーになる

ymm-oss/fsl#1277 · opened

on Oct 7, 2026

fix(refine): `preserve progress` の `respond` にハイフンを含む leadsTo 名（`POL-WAIT-001`）を書けない

ymm-oss/fsl#1276 · opened

on Oct 7, 2026

fix(verify): inline `implements` 内の `preserve progress` を受理するが検査せず、進行の喪失を見逃す

ymm-oss/fsl#1275 · opened

on Oct 7, 2026

fix(induction): step 義務が checked i64 overflow を含まないため、`--depth` を越えて到達する overflow を見ないまま proved を返す

ymm-oss/fsl#1263 · opened

on Oct 6, 2026

· M23 主張の勘定: 義務台帳と fail-closed

fix(verify): `--depth` ちょうどの状態の guard の定義性を、bmc は問わず explicit は問うため、同じ spec・同じ depth で verified と error に分かれる

ymm-oss/fsl#1261 · opened

on Oct 6, 2026

· M23 主張の勘定: 義務台帳と fail-closed

1

fix(verifier): symbolic は absent の Option でもパターン変数を束縛し、状態変数と同名のとき or の右辺でその状態変数を拘束のない値で隠す

ymm-oss/fsl#1259 · opened

on Oct 6, 2026

· M23 主張の勘定: 義務台帳と fail-closed

fix(testplan): `` を含む action 名では Public Kernel（`foobar`）と conformance（`foo.bar`）の名前が食い違い、boundary case が黙って落ちる

ymm-oss/fsl#1256 · opened

on Oct 6, 2026

· M12 実装接続: codegen / testgen / replay の実適合

1

fix(compose): conformance の違反名と mutate の target・死 action 注記が、部品の名前を内部表記（`acctInv`・`acctthaw`）で扱う

ymm-oss/fsl#1255 · opened

on Oct 6, 2026

· M12 実装接続: codegen / testgen / replay の実適合

fix(compose): sync の引数置換が文の forall の束縛（where・範囲）を置換せず遮蔽も扱わないため、正しい部品を使う compose が exit 2 になる

ymm-oss/fsl#1254 · opened

on Oct 6, 2026

· M11 内部品質: 単一オーナーシップと契約整合

feat(mutate): 等価 mutant をレビュー済みとして明示的に除外する仕組み

ymm-oss/fsl#1253 · opened

on Oct 6, 2026

· M23 主張の勘定: 義務台帳と fail-closed

Navigation Menu

Repository navigation

Issues

docs(skills): design 層を検証に使うとき、何を書き何を回すか — 見つけたい誤りで破れる性質を宣言で書く・設計変更に diff を足す・原子性の宣言は実装側のテストで確かめる(事前登録実験、2 題材)

governance: a failed preservation does not affect check/verify result or exit code

refine: --depth before the positional arguments is read as a file path (io error)

docs(skills): AI 実装の入力としての requirements spec — 拒否の規則は散文でなく宣言で書き、意図を確かめる前に conformance で実装を合わせ込ませない(事前登録の ablation 実験から)

fix(compose): 部品の状態を参照する leadsTo が「public Kernel cannot type identifier」で exit 2 になる

feat(verify,runtime): 探索と solver の上限を共通の `Budget` 型にまとめて打ち切りを型で `unknown_budget` へ運び、BMC と induction に資源上限（rlimit）を入れる

refactor(verify): verify のパイプライン（段の順序・エンジン選択・auto の fallback・lemma 判定）を bin module の verification.rs から library へ出し、Worker も同じ関数を呼んで status を返す

refactor(outcome): 結果の意味（result の分類・exit 表・RefinementVerdict の公開語・verify の節の型）を fsl-tools より下の層へ移し、html・ledger・document・Worker が JSON を文字列 key で読み直さないようにする

refactor(forbidden): acceptance / forbidden の契約を、gate を通った値しか受け取れない型にする（parse, don't validate）

refactor(core): 名前の内部表記と公開表記の変換（compose の `__`↔`.`、合成の違反名 `_partial_`・`_bounds_` など）を 1 つの型にまとめる

perf(mutate): `--oracle-attribution` が killed の mutant ごとに主 oracle を計算し直す — 主 oracle の結果を再利用する

perf(mutate): mutant の oracle と baseline が Z3 BMC 固定で、explicit なら桁違いに速い spec でも遅い — explicit 先行（`--engine auto` と同じ規則）にし、mutant ごとの進捗を stderr に出す

feat(mutate): 単独の対応づけファイルによる `refine` を kill oracle に加える

feat(testgen): 実装への配線を生成ファイルの外に置き、再生成で消えないようにする

feat(document): 外部文書（MyST など）から FSL 要素を参照するための索引を出す。business 層も対象にする

fix(document): 生成要件文書の frontmatter `source:` が `document check` に束縛されず、MyST では不正なキーになる

fix(refine): `preserve progress` の `respond` にハイフンを含む leadsTo 名（`POL-WAIT-001`）を書けない

fix(verify): inline `implements` 内の `preserve progress` を受理するが検査せず、進行の喪失を見逃す

fix(induction): step 義務が checked i64 overflow を含まないため、`--depth` を越えて到達する overflow を見ないまま proved を返す

fix(verify): `--depth` ちょうどの状態の guard の定義性を、bmc は問わず explicit は問うため、同じ spec・同じ depth で verified と error に分かれる

fix(verifier): symbolic は absent の Option でもパターン変数を束縛し、状態変数と同名のとき or の右辺でその状態変数を拘束のない値で隠す

fix(testplan): `` を含む action 名では Public Kernel（`foobar`）と conformance（`foo.bar`）の名前が食い違い、boundary case が黙って落ちる

fix(compose): conformance の違反名と mutate の target・死 action 注記が、部品の名前を内部表記（`acctInv`・`acctthaw`）で扱う

fix(compose): sync の引数置換が文の forall の束縛（where・範囲）を置換せず遮蔽も扱わないため、正しい部品を使う compose が exit 2 になる

feat(mutate): 等価 mutant をレビュー済みとして明示的に除外する仕組み