YONAPO RESEARCH
研究記録
MedDSL(仮称)

RESEARCH / RECORD

P2-a:拡張契約の宣言の書式と検査(実行契約)

原文 docs/research/20-p2-a-contract.md

15 KB

GitHubで見る

版 be280c0

この文書の目次 8項目

作成日:2026-10-19。状態:作成者草案・独立確認前。P2 の研究設計 の P2-a を、実行できる形にした契約です。宣言の書式 p2-extension-manifest-draft-1(P2-n で draft-2 に更新。§8)、その検査(src/med_dsl/extensions.py)、既存の handler への後付けの宣言 10 件(extensions/)、検査のテスト(tests/p2/)を定めます。宣言と検査は意味の正しさを検査しません。確かめるのは、宣言が欠けていないこと、実体と食い違わないこと、防護例が宣言どおりの結果を返すことです。実装・契約(p0-draft-2)の振る舞いは変えていません。

1. 宣言(manifest)

extensions/<id>.json は次の項目をすべて持ちます(未知の項目は拒否)。

項目 内容 検査
schema_version p2-extension-manifest-draft-1(P2-n 以後は p2-extension-manifest-draft-2。§8) 一致
id・version・title 拡張の識別 空でない文字列
status {review_state, independent_review}。独立確認の主張(true)は、記録の仕組みができるまで拒否 型・値
class BASE/HOST/R1〜R6/COMP/JOINT(§2。R6 は P2-b、JOINT は P2-c で追加) 既知のクラス
spec 仕様の実体 {path, sha256}(なければ null)。生バイトの hash 実体の hash と一致
contract_doc 契約文書のパス 実在
implementation.modules 実装のモジュール(src/med_dsl/*.py) 実在、パッケージ内
pins 実装の外にあり、変更すると再検証が要るファイル(仕様・契約・実行時に hash を照合するファイル・共有の入口)。role を持つ 実在
embedded_in pin の hash を埋め込んだ実体(glob)。pin が変わったとき再生成が要る glob の展開(テストで漏れを検査)
depends_on 依存する拡張 {id, version} 登録済みで版が一致
owns 所有する名前:operations・schema_versions・profiles・answer_kinds・predicates・capabilities 実装・仕様の本文に現れる(宣言と実装の食い違いを検出)。重複なし
scope 保存を主張する範囲と、範囲外 空でない
obligations 義務の配列(§3) クラス別の必須項目がそろう
stops unknown_capability・unsupported・resource・invalid_input の振る舞い 4項目がそろう
composition shares_names_with・reads_extensions・order_dependent 共有は空、読む拡張は依存に含める
inherits 継承する断片の宣言(draft-2、P2-n。§8) 元の解決・証人の一致・結ぶ義務
evaluation examples(glob)・tests・budget_sweep・oracle 実在

名前は、末尾が : のものを名前空間(その下のすべての名前を所有)として扱い、重なりを検査します(例:urn:med-dsl:events:role: を所有する拡張がある場合、urn:med-dsl:events: や urn:med-dsl:events:role:key を別の拡張は所有できない)。

2. クラスと必須の義務

19 の §3.3 の R1〜R5・合成に、実装上の二つを加えます。BASE(基底。保存の主張を持たず、核の不変条件を実現する)と HOST(複数の操作が共有する前段。操作を持たない。引き継ぎの識別・仕様と P0 実体の固定)。R5 には、保存を主張しない診断(欠落を否定にする方針変更の診断、旧処理系の可用性の点検)を含めます。合成は COMP。

クラス 必須の義務
すべて K-ID(識別)・K-STOP(停止)・K-INV(核の不変条件 I1〜I7)・K-RES(資源)
R1 R1-1〜R1-5(所有・形と非循環・旧モデルの拡張・追加制約なし・十分条件)
R2 R2-1〜R2-5(書き込みなし・基底語彙へ導出しない・核の採用選択を経由・回答型の分離・自己申告を根拠にしない)
R3 R3-1〜R3-7(E と ρ・充足の対応・被覆・新理論の範囲・履歴と採用の可換・名前の新鮮さ・範囲外の明示)
R4 R4-1〜R4-3(因子化できる問いだけ・喪失の反例・後段や別添えで全体を復元しない)
R5 R5-1〜R5-3(変わる点の記録・認定を出さない・臨床の主張を追加しない)
COMP COMP-1〜COMP-3(実体からの再計算・範囲の交差・損失は回復しない)
R6 R2-1〜R2-5 と R6-1〜R6-6(公理の閉じた宣言・旧データでの無矛盾・結論の健全性と完全性・結論は公理に相対・範囲の明示・情報要求)。P2-b で追加(23 の §4)
JOINT R2-1〜R2-5、R6-1〜R6-6、JOINT-1〜JOINT-6(構造の再計算・独立な併用の分解・共有記号の併用の全体での再判定・鎖の範囲と非回復・範囲の明示・個別と併用の差の開示)。P2-c で追加(25 の §5)

別のクラスの義務を宣言すれば拒否します。

3. 義務・防護例・証拠

各義務は id・statement・evidence・checks・guards(と、必要なら guard_gap・derivation)を持ちます。

  • 証拠の強さ(弱い順):self_declared < individual_io < finite_check < hand_derivation < checked_native_template。拡張全体の強さは最も弱い義務。
  • 検査(checks):テストファイルまたは ファイル::テスト名。実在し、テスト名が本文に現れること。
  • 防護例(guards):{example, path, equals, kind}。その義務のゲートを壊すと結果が変わる例。kind は refusal(拒否)・non_conversion(変換しないこと)・boundary(境界)。登録時に例を実際に評価し、path の値が equals と一致することを確かめる(宣言を信用しない)。
  • 防護例がない義務は、guard_gap に理由を書く(理由なしは拒否)。防護例と guard_gap の併存も拒否。これにより、検査の見逃し(RV-01 の教訓)が宣言から見える。

4. 登録

Registry.register(manifest) は、書式・実体・防護例の検査に続いて、次を検査します。拒否されたら登録は一切変わらない(全か無か)。

規則 拒否の理由
同じ id の再登録 duplicate_extension
基底は最初の一つだけ。他は基底へ到達する依存を持つ base_must_be_first・base_not_registered・must_depend_on_base
depends_on は登録済みで版が一致 unresolved_dependency
名前の所有が既登録と重なる(名前空間を含む) owner_conflict
記号を共有する併用(shares_names_with が空でない) shared_names_need_joint_check。個別の宣言では認めず、併用全体で再判定する(19 の L4)
読む拡張が依存に含まれない undeclared_read

5. 再検証範囲の列挙

affected(registry, changed) は、変更したファイル(リポジトリ相対)から次を返します。

  • 再検証する拡張:実装モジュールまたはその import の閉包、spec・contract_doc・pins に変更が及ぶ拡張、およびそれらに依存する拡張(推移的)。
  • 再生成が要る実体:pin が変わった拡張の embedded_in。共通 manifest(examples/p1-evaluation/manifest.json)は、固定した実体のどれかが変わったとき。

登録の辺:拡張 E の import の閉包を数えるとき、E に(推移的に)依存する拡張が宣言したモジュールへの import は辿らない。ホスト(handover.py、host.py)は、登録(振り分け)のために操作のモジュールを import するが、これは E の意味がそのモジュールに依るという意味ではなく、依存の向きは宣言(操作がホストに依存する)にすでに書かれている。これを辿ると、どの操作の変更もホストを経由して全操作を列挙してしまう(P2-a の最初の実装がそうだった。結果 21 の §3-6)。逆向きの読み取り(ホストが操作の関数を実際に使う)は、列挙では見ず、非干渉の検査(X03:操作を不活性にしたとき、その外の結果が変わらないこと)が見る。依存の宣言がなければ、同じ import は通常の辺として辿る。

拡張の独立(L3、P2-c):independent_pairs(registry) が、基底を除く拡張の組のうち独立なもの(どちらも他方に依存せず、読まず、順序に依存せず、実装の import の閉包が互いの固有のモジュールを含まない。基底が宣言した核のモジュールは除く)を列挙する。独立な拡張の任意の部分集合を同時に載せても、全例の結果が変わらないこと(X08)は tests/p2/test_combinations.py が検査する。

6. 受入条件の実現

条件 実現
X01 宣言の欠落を拒否 必須項目の欠落・書式の不正をそれぞれ検査(tests/p2)。部分適用なし
X02 名前の衝突を拒否 六つの種別すべてと名前空間の重なりを検査
X03 非干渉 各拡張の handler を不活性にして全131例を評価し、その拡張とそれに依存する拡張に属さない例の結果が変わらないこと。不活性化が効いていること(属する例は変わる)も確認。宣言の誤り(未宣言の読み取り)が検出されることも確認
X06 クラス別の義務 クラスの必須の義務を一つずつ外して拒否を確認(全拡張)
X07 防護例 防護例の結果の不一致・実在しない例・理由のない欠落・併存を拒否。防護例のない義務は、最初は24件、追加作業(22)の後は3件で、すべて理由つきの既知の欠落として一覧に固定
X13 再検証範囲 draft-2 の変更(validation.py と P0 契約)から、実際に再固定が要った 27 件の p1-c の例と PR01 などが漏れなく列挙されること。予測した実体は実際にすべて変わったこと

X04・X05・X14 は P2-b(24)、X08〜X10 は P2-c(26)で実現した。X11・X12 は P2-d(設計 27、結果 28)で実現した。

7. 限界

  • 宣言は作成者の主張で、意味の正しさの証拠ではない。防護例は、今ある例が宣言どおりの結果を返すことを保証するだけで、ゲートを壊す実装の変更を検出できるかは、変異検査など別の手段で確かめる(extensions.py 自体は 42 変異で検査した)。
  • owned_name_not_found は、宣言した名前が実装・仕様の本文に文字列として現れることだけを見る。コードが名前を組み立てている場合(接頭辞+値)は、名前空間として宣言する。
  • 拡張ホストの分離(引き継ぎの族のホストと操作の分離、最上位の登録表)は、P2-a の後の追加作業で行った(22)。3 つの族のヘッダー検査の共通化は、エラーの path・code が変わるので行っていない。
  • 独立確認は未実施。independent_review の主張は拒否される。
  • 宣言(extensions/*.json)、宣言が根拠として引く防護例・検査・オラクル、check-extensions.py は、P2-a の後の追加作業で P1-d の固定対象に加えた。例外は audit-preservation.py(固定対象の hash を持つので循環する)。固定対象は同じリポジトリのファイルなので、改ざん防止ではなく、変更を見落とさないための関門である(22)。

8. 継承の欄(P2-n、p2-extension-manifest-draft-2)

宣言の書式を draft-2 に上げ、項目 inherits を足しました(2026-10-21。設計は 59、期待は 60)。他の項目の書式・検査・登録の規則は変わりません。draft-1 の宣言は unsupported_manifest_schema で拒否します(旧い宣言を黙って再解釈しない)。

継承とは、拡張 X が拡張 Y の意味の断片を実装を共有せずに再び述べ、その断片では Y と観測が一致することです。実装の import で共有する場合は依存で、継承ではありません。

項目 内容 検査・拒否の理由
inherits 項目の配列(必須。空は「継承なし」の明示) missing_field、配列でなければ invalid_inherits
from 元の拡張の id 自己でない(self_inheritance)。登録済み(unresolved_inheritance)。from と fragment の組で一意(duplicate_inheritance)
fragment 再び述べた断片の説明(何が一致するか、意図した差も書く) 空でない文字列(invalid_inheritance)
obligation 継承の主張を担う、この宣言の義務の id 実在し(inheritance_obligation_missing)、checks が空でない(inheritance_obligation_without_checks)
witnesses 証人の配列。{from: {example, path}, to: {example, path}}。元の拡張の例と自分の例、結果の中の位置 形(invalid_witness)。from.example は元の拡張の、to.example は自分の evaluation.examples に含まれ(witness_example_not_owned)、実在し(missing_witness_example)、登録時に評価して位置が結果にあり(inheritance_witness_unresolved)、値が一致する(inheritance_witness_mismatch)
witness_gap 証人がない理由。証人が空のときだけ、必須 unexplained_witness_gap、証人と併存は witness_gap_with_witnesses
  • 登録:防護例の評価と同じく、登録する registry が評価の関数を持つときだけ証人を評価する。登録の順は、依存に加えて継承の元を先にする。相互の継承は解決できず拒否される。
  • affected():元の拡張が影響を受けたら、継承する側も影響を受けたとして列挙する(理由 inherits:…)。依存と同様に推移する。継承する側の変更は元に及ばない。
  • independent_pairs:継承で結ばれた組は独立としない。
  • 版の比較の道具:木の宣言と registry は、その木の実装で扱う(p2_checks.tree_affected)。作業ツリーの registry に旧い版の宣言を渡すと、契約の版が違えば拒否されるため。
  • 限界:証人の一致は、断片の一致の有限の証拠で、継承の真偽の証明ではありません。継承がないのに宣言すること、継承があるのに宣言しないことは、機械的には排除できません(疑いの探索は測定だけ。結果 61)。同じ拡張の版の間の継承(P2-l の VR-1)は別の関係で、この欄の対象外です。

P2-a

同じ区分の文書