12. 意味いみモデル・中間表現ちゅうかんひょうげんの補足不変条件ほそくふへんじょうけん
方針ほうしん
interfaces/model.json はsourceのform表ひょうと別べつの、lower後ごの意味値いみち・実行じっこうIRの構造こうぞうを記述きじゅつする。surfaceとmeaningのSchemaRefは別べつにする。Rustで型かたを分わけ、wireで両者りょうしゃを混同こんどうしない。
1. 値あたいと参照さんしょう
JSON内ないの record は [fieldName, typeExpression] の順序付じゅんじょつきarrayであり、その順序じゅんじょをNDF recordのfield順じゅんとする。sum はvariant名めいをkeyとするmapで、各かくpayloadも同おなじ順序付じゅんじょつきfield array。空からrecord/payloadは空からarrayとする。field名めいは各かくarray内ないで一意いちい。union はvariant名めいからrecord型がたへのmap。sum/unionおよびcontractsのvariantsのkey順じゅんには意味いみを持もたせず、NDFではVariantNameの文字列もじれつで識別しきべつする。数値すうちordinalをJSON objectの列挙順れっきょじゅんから割わり当あてない。List/OptionはNDFの対応たいおうtag。Naturalはnonnegative Integer。Name/LanguageTagはTextに対たいして各かくdomainの制約せいやくを追加ついかする。
Source由来ゆらいの意味値いみちはOriginを関連付かんれんづけられる。各かくRecordが共有きょうゆうできるようにnative実装じっそうをarenaにしてもよいが、公開値こうかいちの意味いみをpointerに依存いぞんさせない。wireは参照さんしょうtable付つきbundleを使つかい、全ぜんNodeRef/OriginRefが有効ゆうこうであることを検査けんさする。意味上いみじょうの構造木こうぞうきと回路かいろgraphのcycle制約せいやくは異ことなる。
r4ではNodeRef/OriginRef、Origin、SyntaxNode/FieldValue、SyntaxBundle/ForeignSyntax、EnvironmentRefを共通きょうつうfoundation所有しょゆうのcontractsへ移うつした。modelはexternal_typesから参照さんしょうし、同おなじ名義型めいぎがたを二重定義にじゅうていぎしない。SyntaxBundleはsources、nodes、origins、root、environmentsを持もつ。ForeignSyntax.rootとguest bundle.rootは等ひとしくなければならず、guestのnode/origin IDはそのbundle内ないだけで解決かいけつする。ForeignSyntax.environmentはforeign slotを所有しょゆうするhost bundleのEnvironmentEntryのid/digestへ一致いっちさせる。guestへの無条件むじょうけんの名前空間継承なまえくうかんけいしょうは行おこなわない。
EnvironmentEntryはid/digest/valueを持もち、Environmentは明示的めいじてきなnamespace/name/value/originのbinding列れつとresource列れつを持もつ。同おなじnamespace/nameのbindingとresource IDの重複ちょうふくを拒否きょひする。bindingのOriginRefはそのentryの所属しょぞくbundle内ないで解決かいけつする。entry digestはASCII NEPL3-ENVIRONMENT-1、zero byte、canonical NDFで符号化ふごうかしたEnvironment recordのSHA-256とする。型付かたつきnative graph検査けんさはentryの選択せんたくと参照さんしょうを検査けんさし、wire adapterはcanonical digestとresource元もとbyte列れつのdigestも再検査さいけんさする。
Doc/Math等とうの意味値いみちが単体たんたいForeignを保持ほじする場合ばあいはForeignClosureを使つかう。syntaxのguest arenaとownerEnvironment/ownerOrigins/ownerSources/ownerSourceMapsのarenaは独立どくりつする。同おなじ数値すうちの環境かんきょうID・OriginRefでも両者りょうしゃの値あたいを置換ちかんしない。元もとownerOrigin列れつを保持ほじし、環境かんきょうdigestを変かえない。ForeignClosure.captureは検査済けんさずみownerの実じつForeign fieldだけを取とり出だし、ownerの構文こうぶんnodeは所有化しょゆうかしない。受信時じゅしんじは外側そとがわschemaとguest rootのschema、root ID、選択せんたくしたowner環境かんきょうのid/digest、owner/guestそれぞれの閉包へいほうを検査けんさし、portable adapterは両環境りょうかんきょうの内容ないようdigestを再計算さいけいさんする。raw閉包へいほうの成立せいりつから言語固有げんごこゆうの意味いみlowerやhostによる環境授権かんきょうじゅけんを推定すいていしない。
portable境界きょうかいの停止理由ていしりゆうは型付かたつき原因げんいんから取とり出だす。Schema、Source、Origin、View、Syntax、Fact、Reportに包つつまれたStoppedも元もとStopReasonを保持ほじし、domain側がわの通常つうじょうInvalidへ縮約しゅくやくしない。WireErrorの直接ちょくせつStoppedだけを認識にんしきしていた停止抽出ていしちゅうしゅつを訂正ていせいする(R047)。意味いみエラーを、無関係むかんけいに停止ていししたBudgetの状態じょうたいで上書うわがきする規則きそくではない。
通常つうじょうのsource nodeではheadはcover内ない、各子かくこのcoverは親おやcover内ないかつhead.end以降いこうで、子同士こどうしはfield順じゅんに重複ちょうふくしない。graph/位置検査いちけんさだけでformのarity・引数ひきすうcategory・各かくfield型がたまで検査けんさしたことにはしない。surface LanguagePackageの検査けんさを別べつに行おこなう。生成せいせいnodeに架空かくうのcoverを要求ようきゅうしない。
SourceMapはsource/target SpanとExactまたはTransformedのMapping列れつを持もつ。Exactは元もとと先さきのbyte列れつが等ひとしく、局所逆写像きょくしょぎゃくしゃぞうはoffset差さで求もとめる。Transformedは対応たいおうするfragment間かんの関係かんけいだけを表あらわし、任意にんいの部分区間ぶぶんくかんを逆変換ぎゃくへんかんできるとはしない。重かさなった複数ふくすうの候補こうほはAmbiguous、非可逆ひかぎゃくはIrreversibleとしてrename等とうへ返かえす。
map循環じゅんかんの頂点ちょうてんはsnapshotとbyte位置いちである。非空範囲ひくうはんいは半開区間内はんかいくかんないの各かくbyte、空範囲くうはんいはそのoffsetの独立どくりつしたanchor頂点ちょうてんとし、同おなじoffsetの内容ないようbyteとanchorを混同こんどうしない。Exactはoffset差さを保存ほぞんするedge、Transformedは元もとfragmentの全頂点ぜんちょうてんから先さきfragmentの全頂点ぜんちょうてんへの関係かんけいである。この有限ゆうげんgraphのcycleを拒否きょひする。同一どういつsnapshot内ないでも一方向いちほうこうへ進すすむ重複ちょうふくExact区間くかんや、互たがいに接続せつぞくしない範囲はんいはcycleとしない。検査量けんさりょうの超過ちょうかはStoppedであり、粗あらいsnapshot依存いぞんだけを根拠こんきょにCycleと返かえさない。
1.1 foundation制約せいやくID
constraint IDはstructural descriptorとともにdigestへ含ふくめる。共通きょうつうRust constructor・boundary adapterは次つぎを検査けんさする。descriptorにIDがあるだけで検査けんさを実行じっこうしたとは扱あつかわない。
| ID | 検査けんさする不変条件ふへんじょうけん |
|---|---|
| source.identity | 空からでないopaque IDと明示的めいじてきなrevision/content digest |
| source.content | locator profile、UTF-8元もとbyte列れつ、content digestの一致いっち |
| source.bundle | snapshot宣言せんげんの一意性いちいせい、同おなじID/revisionの矛盾拒否むじゅんきょひ、共有操作きょうゆうそうさでの入力予算にゅうりょくよさん |
| source.span | 指定していsnapshotの範囲はんい・半開順序はんかいじゅんじょ・UTF-8 scalar境界きょうかい |
| schema.reference / schema.type-reference | 空からでないpackage/type名めいと、選択せんたくされた版ばん・digestまたは記号的参照先きごうてきさんしょうさき |
| schema.descriptor | 重複宣言拒否ちょうふくせんげんきょひ、canonical descriptor、全参照ぜんさんしょうのfinalize |
| operation.reporting | すべての結果けっかの累積るいせきUsage、共有きょうゆうLimits、停止理由ていしりゆうの維持いじ、partialをCheckedとしない |
| report.trace-overflow | 実際じっさいの未受理みじゅりevent件数けんすうが正せい、単一たんいつの報告ほうこく、EventLimitの停止ていし |
| namespace.reference | 明示めいじしたschemaと空からでないnamespace名めい |
| environment.bindings / environment.digest | binding/resourceの一意性いちいせい、範囲はんいと型かた、canonical entry digest |
| syntax.graph / syntax.foreign | bundle局所参照きょくしょさんしょう、有限ゆうげんgraph、source geometry、host環境かんきょうとguest rootの一致いっち |
| source.map / origin.graph | 上記じょうきのmap関係かんけいとOrigin DAG、所属しょぞくsnapshot・OperationRef・参照先さんしょうさき |
| source.reservation | 空からでないhost予約よやくSourceId、revision、絶対ぜったいlogical URI。生成せいせいbytesからdigestを計算けいさんし、異ことなる結果けっかへの予約再利用よやくさいりようを拒否きょひ |
| schema.kind-id | 選択せんたくschemaの型名かためいscalar順じゅんに割わり当あてたlocalKindとdescriptorの対応たいおう |
| view.graph | Tokenごとに局所的きょくしょてきなview参照さんしょう、DAG、field名めいの一意性いちいせい、source範囲はんい |
| token.boundary | token head・triviaのsnapshotと境界きょうかい、内部ないぶviewの包含ほうがん、payloadの型かたはreader/form契約けいやくで検査けんさ |
| view.presentation | schemaが所有しょゆうする表示分類名ひょうじぶんるいめいと明示めいじされたfallback role |
SyntaxBundleはtokensのtableを持もち、SyntaxNode.tokenは同おなじbundleのTokenRefを指さす。Tokenはpayload、内部ないぶViewBundle、leadingTriviaを保持ほじする。ViewRefはそのTokenのViewBundle内ないだけ、TokenRefはそのSyntaxBundle内ないだけで解決かいけつする。ForeignSyntaxのguest bundleは自身じしんのtableを持もつため、同おなじ数値すうちIDをhostへ解決かいけつしない。通常つうじょうのsource由来ゆらいnodeにはheadに対応たいおうするtokenをengineが要求ようきゅうし、synthetic/recovery nodeのtoken不在ふざいはOptionで明示めいじする。graphの検査けんさとformのarity・payload型がたの検査けんさを区別くべつする。
sourceMapsはSyntaxBundleの所有列しょゆうれつであり、全ぜんsource/targetをそのbundleのsourcesで解決かいけつする。SourceMapの幾何きか・Exact内容一致ないよういっち・非循環ひじゅんかんを検査けんさしたproofだけをmapped view包含ほうがんに使用しようする。standalone Token/ViewBundleのvalidateはmapを持もたない直接包含ちょくせつほうがんの入口いりぐちとし、変換へんかんviewはvalidate_with_mapsまたはSyntaxBundle境界きょうかいを使つかう。包含ほうがんは02章しょうの全逆経路規則ぜんぎゃくけいろきそくに従したがい、sourceがhost storeに偶然存在ぐうぜんそんざいすることを所有証明しょゆうしょうめいにしない。
ValidatedSourceMapは不変ふへんなsnapshot identity上じょうのmap関係かんけいのproofであり、任意にんいの後続こうぞくSourceStoreへの所属しょぞくproofではない。Token/Viewのvalidate_with_mapsは使用時しようじのstoreで全ぜんmap端点たんてんの宣言閉包せんげんへいほうを再照合さいしょうごうする。SourceMap.contains単体たんたいは関係上かんけいじょうの包含計算ほうがんけいさんであり、transport source tableの所属しょぞくを検査けんさする入口いりぐちとは区別くべつする。
内部ないぶviewは外側そとがわのchildrenやarityへ加算かさんしない。SentenceLiteralの構造化こうぞうかpayloadとview、Codeが保持ほじするforeign syntaxのtoken・triviaはnativeとNDFの両経路りょうけいろで保存ほぞんし、元もとsourceの再さいparseを情報保持じょうほうほじの代替だいたいにしない。
Token.payloadは、その型かたが所有しょゆうする独立どくりつbundleまたは明示めいじsource参照さんしょうを持もつ。まだ構築こうちくされていない外側そとがわSyntaxBundleのNodeRefを暗黙あんもくに参照さんしょうしない。payload内ないに現あらわれる数値すうちを外側そとがわnode IDと推測すいそくして再採番さいさいばんしない。この所有契約しょゆうけいやくにより、outer nodeのcanonical再採番さいさいばんはopaque payloadを壊こわさず行おこなえる。
DocのSentenceLiteralはlower後ごにDoc:Sentenceとなる。raw Textには注釈構文ちゅうしゃくこうぶんを再適用さいてきようしない。MathのNumberは有限十進ゆうげんじっしんで表現ひょうげんできるRational(約分後やくぶんごの分母ぶんぼの素因数そいんすうが2と5だけ)と元もとの表記範囲ひょうきはんいを持もち、SymbolNameはMath:Symbolへ統合とうごうする。違反いはんはNonFiniteDecimalNumber。Numeric spellingを表示ひょうじに使つかう場合ばあいは、そのsnapshotと値あたいが一致いっちしていることを検査けんさする。生成せいせいNumberはcanonicalな整数せいすうまたは有限十進ゆうげんじっしんでprintする。任意有理数にんいゆうりすうからの式構築しきこうちくと著者ちょしゃのFracの保存ほぞんはMath章しょうの規則きそくに従したがう。
ForeignSyntaxはguestのopaque bundleを持もち、host coreはguestの意味型いみがたをimportしない。suiteで登録済とうろくずみschemaに検査けんさしてからguest操作そうさに渡わたす。Doc:DocGuestもForeignSyntaxを保持ほじする。Codeの準備じゅんびはbundleの安全性あんぜんせいを検査けんさしてsourceとviewを表示ひょうじし、guestのlower・意味いみcheck・evaluateを呼よばない。
2. Checked値ちの境界きょうかい
Rust内部ないぶのChecked/Preparedのconstructorはprivateにする。wireでCheckedEnvelopeを受信じゅしんしただけで検査済けんさずみと信用しんようしない。外部がいぶproviderからの結果けっかにはschema検査けんさ・構造不変条件検査こうぞうふへんじょうけんけんさを行おこない、利用りようする操作そうさに必要ひつような意味検査いみけんさを再実行さいじっこうする。digestは同一性どういつせいの情報じょうほうであって証明書しょうめいしょではない。
process/session内ないで検査結果けんさけっかを再利用さいりようする場合ばあいは、provider・input・schema・environmentを固定こていしたhost所有しょゆうhandleを使つかえる。別べつprocessへ生なまのpointerやprivateなhandleを送おくらない。
3. 回路かいろIR
NetNode.idはnodesのindexに一致いっちし、orderは組合くみあわせDAGの全ぜんnodeを一度いちどずつ含ふくむ順序じゅんじょ。Input/State/Constantのinputsは空から、Not/Sliceは1、And/Or/Xor/Nor/Add/Concatは2、Muxは3。InputとStateは有効ゆうこうなport/slotを参照さんしょうする。Slice/Mux/Concatのwidth条件じょうけんはCircuit章しょうの通とおり。
outputNodesの長ながさはoutputsと等ひとしく、各かくnodeの幅はばがportと一致いっちする。StateSlot.nextは有効ゆうこうnodeで同おなじ幅はば。初期値しょきちは幅内はばない。state次値じちへのedgeを現在げんざいstate readの依存いぞんへ戻もどさない。
NorNetlistはbit順じゅんをport宣言順せんげんじゅん、その中なかをLSB→MSBとする。stateもslot順じゅん、その中なかをLSB→MSB。nextBits/outputBitsの長ながさは対応幅たいおうはばの和わ。Nor2の参照さんしょうはtopologicalに前まえのnodeだけ。InputBit/StateBitは有効範囲ゆうこうはんい。originsはnodesと同おなじ長ながさ。
4. Markup安全性あんぜんせい
Markup modelがname/attributeをTextとして運はこべることは、任意にんいのtagを許可きょかすることを意味いみしない。nepl3-markupは目的もくてきcategoryに対たいして検査けんさする。
HTMLでは文書構造ぶんしょこうぞう・注釈ちゅうしゃく・コード・リンクに加くわえ、ul/ol/li、table/caption/thead/tbody/tr/th/td、imgを扱あつかう。全要素ぜんようその列挙れっきょは design/markup.json を正本せいほんとし、内容ないようモデルと型付かたつき属性ぞくせいは HTML fragment契約けいやく に従したがう。MathML: math, mrow, mi, mn, mo, mtext, mfrac, msqrt, mroot, msub, msup, msubsup, munder, mover, munderover, mtable, mtr, mtd, mspace。SVG: svg, g, rect, line, path, polyline, circle, text, title, desc。
全要素ぜんようそ・属性ぞくせい・属性値制約ぞくせいちせいやくの正本せいほんは design/markup.json。属性ぞくせいを受うけ入いれる集合しゅうごうはglobal、namespace、elementの各かくallowlistの和わとし、列挙れっきょされていない属性ぞくせいは拒否きょひする。SVGのpath/points等とうは自由じゆうな文字列もじれつとして受うけず、記述きじゅつした型付かたつき構造こうぞうからserializerが綴つづりを生成せいせいする。userから任意にんいのon*、style、script、foreignObject、SVG image、任意にんいのnamespace URLを受うけない。HTMLのhrefは型付かたつきFragment/Artifact/BetweenArtifacts/Externalを使つかい、URIの許可規則きょかきそくと内部ないぶtargetの存在そんざい、文書間ぶんしょかんrouteの対応たいおうをそれぞれ検査けんさする。HTML imgのsrcは検査済けんさずみartifact内ないの相対そうたいpathであり、任意にんいの外部画像がいぶがぞうURLを許可きょかしない。字句検査じくけんさだけでassetの存在そんざい・内容ないよう・権限けんげんを検証済けんしょうずみとせず、文書準備時ぶんしょじゅんびじの解決かいけつを別べつに要求ようきゅうする。CSSはbackendが所有しょゆうする固定こていassetであり、本文文字列ほんぶんもじれつをCSSに埋うめ込こまない。
MathMLのmspaceのwidth/height/depthはNonnegativeMathLengthとする。非負ひふのcanonical有限十進ゆうげんじっしんにemを付つけ、zeroは0em、百分率ひゃくぶんりつ・指数表記しすうひょうき・他単位たたんい・負値ふち・冗長じょうちょうなzeroを拒否きょひする。これはMathML Coreのlength-percentageのうち本ほんprofileが使用しようする部分集合ぶぶんしゅうごうであり、SVGの座標用ざひょうようDecimalとは区別くべつする。違反いはんはInvalidMarkupAttribute。
MarkupのTextと属性値ぞくせいちは、UTF-8の妥当性だとうせいに加くわえ、XML 1.0 Charの集合しゅうごう(U+0009、U+000A、U+000D、U+0020..D7FF、U+E000..FFFD、U+10000..10FFFF)を共通きょうつうの許可集合きょかしゅうごうとする。それ以外いがいはInvalidMarkupCharacterで拒否きょひし、削除さくじょや置換文字ちかんもじによる黙殺もくさつをしない。Doc/Mathの一般いっぱんText値ちをこの出力用制約しゅつりょくようせいやくで狭せばめるのではなく、Markup構築こうちく・検査境界けんさきょうかいで適用てきようする。
serializerはHTML5とXMLを区別くべつし、namespace、void element、属性ぞくせいescapeを適切てきせつに出だす。属性順ぞくせいじゅんは固定こてい。Textと属性ぞくせいのescapeおよび改行保存かいぎょうほぞんは再現性章さいげんせいしょうに従したがう。文書ぶんしょテキストを文字列置換もじれつちかんでHTMLへ挿入そうにゅうしない。
5. operationの具体型ぐたいけい
interfaces/contracts.json のDomainSyntax/CheckedDomain等とうはoperationごとに本ほんファイルの対応たいおうdomain型がたへ特殊化とくしゅかするための表記ひょうき。例たとえばmath.lowerの結果けっかはMath/Expr、circuit.elaborateの結果けっかはCircuit:PreparedNetlist、doc.prepareの結果けっかはDoc:PreparedArticle。異ことなるdomainのTypedValueを同おなじ入力にゅうりょくとして受うけ付つけない。
Grammar packageのReaderExpr/ReadSpec/Binding/StyleのpayloadはGrammarのschemaで定義ていぎしたADTを使用しようできる。参照さんしょうを解決かいけつした索引さくいんtableを追加ついかしてよいが、意味正規形いみせいきけいは参照先さんしょうさきの識別子しきべつしと契約けいやくに従したがって比較ひかくする。無限再帰むげんさいきのRust型がたやSerde表現ひょうげんをwireへ押おし付つけない。
HTMLのdocument shell(html/head/meta/style/body)は固定こていのshell生成処理せいせいしょりが作つくり、userが与あたえるMarkupFragmentの要素ようそとして受うけ取とらない。内部ないぶのDoc/Math/SVG namespace遷移せんいとphrasing/block制約せいやくもmarkup.jsonに従したがう。最適化さいてきかや資源追加しげんついかの都合つごうでこのallowlistを迂回うかいしない。