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.contentlocator profile、UTF-8もとbyteれつ、content digestの一致いっち
source.bundlesnapshot宣言せんげん一意性いちいせいおなじ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.digestbinding/resourceの一意性いちいせい範囲はんいかた、canonical entry digest
syntax.graph / syntax.foreignbundle局所参照きょくしょさんしょう有限ゆうげん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.graphTokenごとに局所的きょくしょてきなview参照さんしょう、DAG、fieldめい一意性いちいせい、source範囲はんい
token.boundarytoken head・triviaのsnapshotと境界きょうかい内部ないぶviewの包含ほうがん、payloadのかたはreader/form契約けいやく検査けんさ
view.presentationschemaが所有しょゆうする表示分類名ひょうじぶんるいめい明示めいじされた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を迂回うかいしない。