notes mizzy.org

出力リストの長さが入力で決まるなら、deferredは値だけの問題に格下げできる

規範的主張 出典: carina-rs/carina#4286、carina-rs/carina#3589、AWS ACM API Reference(CertificateDetail) 作成

ACM証明書の検証レコードを作るfor opt in cert.domain_validation_options { ... }は、applyまで要素数が分からないのでdeferredになる。effectを確定時点で分けると「個数が後で確定」の段で、planには「この形のものが後で作られる」としか書けない。effectは「何がいつ確定するか」で三つに分かれる

だが、この要素数は本当に分からないわけではない。ACMのAPIリファレンスはDomainValidationOptionsを"contains information about the initial validation of each domain name"と書く。要素はリクエストしたドメイン名ごとに1つで、ドメイン名はdomain_nameとsubject_alternative_namesという入力に書いてある。分からないのは各要素の値(resource_record.name / .value)だけである。

長さの関係をschemaに書く

providerが「この出力リストは、この入力リストの要素ごとに1要素を持つ」という関係を宣言できれば、plannerはplan時にループを展開できる。

いま関係を宣言した後
段個数が後で確定値だけ後で確定
planの表示テンプレート1つ+がN個、集計にも入る
子の識別子位置(何番目か)キー(ドメイン名)
apply時テンプレートを展開する実際のリストが宣言と合うか検査する

効くのは表示だけではない。キーをドメイン名にすれば、SANの並びを入れ替えても子のidentityがずれない。位置で識別すると、並び替えだけで「削除して作り直す」planになる。identityは「何を同一資源と見なすか」の規則であり、stateとは独立軸である

apply時に実際のリストが宣言と食い違ったら、黙って別の集合を作らずに失敗させる。宣言は予測であって、真実はapplyが確立する。食い違いを検査する場所があることで、宣言の誤りが静かに通らない。planは予測であり、真実はapplyが確立する 信頼境界を越えるデータは境界で再検証する

何を取り込もうとしているか

型の言葉で言えば、値の長さを型(schema)に持ち上げて、出力の長さを入力の関数として書くことである。Carinaの型は値を検査する篩型で、Listには既に要素数の上限・下限がある。今回足したいのは定数の範囲ではなく、別の属性との関係である。カスタム型は独立の構成子ではなく篩型である

依存型まで行く必要はない。関係の形を「入力リストの要素ごとに1つ(キー付き)」程度に絞れば、宣言はデータとして書け、検査も機械的にできる。承認の側から同じ問題を見たのがdeferredな作成を承認するなら、個数も承認の対象にするである。

根拠の確度

DomainValidationOptionsの説明はACMのAPIリファレンスから引いた。SubjectAlternativeNamesが証明書のCN(domain_name)を含むことも同じページの記述による。ただし「要素数 = 重複を除いたドメイン名の数」が常に成り立つかは実際のACMで確かめていない。とくに*.example.comとexample.comは同じ検証CNAMEを受け取るので、要素数と作るべきレコードの数が食い違う可能性がある(要確認)。

Listが要素数の範囲を持ち、入力との関係を書く仕組みが無いことは、carina#4256と既存issueの検索で確認した(2026-11-06)。ほかにどの出力リストが入力で長さの決まるものかは調べていない。

#carina #型システム #plan #提案