diff --git a/crates/sqlquack-syntax-coverage/src/check/_helpers/fingerprints.rs b/crates/sqlquack-syntax-coverage/src/check/_helpers/fingerprints.rs
index 38c04ff8b..a82981833 100644
--- a/crates/sqlquack-syntax-coverage/src/check/_helpers/fingerprints.rs
+++ b/crates/sqlquack-syntax-coverage/src/check/_helpers/fingerprints.rs
@@ -4,7 +4,7 @@ use std::collections::BTreeMap;
 
 use crate::check::models::{CaseResult, LocalVerdict, ObligationResult};
 use crate::formats::main::content_sha256::content_sha256;
-use crate::formats::models::{Form, Obligation};
+use crate::formats::models::{Form, Obligation, Reading};
 
 /// The local verdict as fingerprint text: `accepted` with its tree hash, `rejected`, or the failure.
 fn verdict_text(local: &LocalVerdict) -> String {
@@ -38,8 +38,15 @@ pub(crate) fn form_fingerprint(obligations: &[ObligationResult]) -> String {
     content_sha256(text.as_bytes())
 }
 
-/// SHA-256 of the form's catalogue entry and own obligations as compact JSON; empty if unserializable.
-pub(crate) fn form_definition(form: &Form, obligations: &[&Obligation]) -> String {
-    serde_json::to_vec(&(form, obligations))
-        .map_or_else(|_| String::new(), |bytes| content_sha256(&bytes))
+/// SHA-256 of the form's catalogue entry, own obligations and any reading as JSON; empty on failure.
+pub(crate) fn form_definition(
+    form: &Form,
+    obligations: &[&Obligation],
+    reading: Option<&Reading>,
+) -> String {
+    let bytes = match reading {
+        Some(reading) => serde_json::to_vec(&(form, obligations, reading)),
+        None => serde_json::to_vec(&(form, obligations)),
+    };
+    bytes.map_or_else(|_| String::new(), |bytes| content_sha256(&bytes))
 }
diff --git a/crates/sqlquack-syntax-coverage/src/check/_helpers/forms.rs b/crates/sqlquack-syntax-coverage/src/check/_helpers/forms.rs
index 966ec3695..af4bd245b 100644
--- a/crates/sqlquack-syntax-coverage/src/check/_helpers/forms.rs
+++ b/crates/sqlquack-syntax-coverage/src/check/_helpers/forms.rs
@@ -16,11 +16,10 @@ fn obligation_result(obligation: &Obligation, joined: &Joined) -> ObligationResu
         .iter()
         .filter_map(|case_id| joined.cases.get(case_id).cloned())
         .collect();
+    let unobservable: Option<Reason> = joined.unobservable.get(obligation.id.as_str()).copied();
     let reason: Option<Reason> = match () {
         () if cases.is_empty() => Some(Reason::MissingCase),
-        () if joined.unobservable.contains(obligation.id.as_str()) => {
-            Some(Reason::UnverifiableInternalError)
-        }
+        () if unobservable.is_some() => unobservable,
         () => cases.iter().filter_map(|case| case.reason).min(),
     };
     ObligationResult {
@@ -62,7 +61,8 @@ pub(crate) fn form_result(form: &Form, family: &str, context: &FamilyContext) ->
         .map(|obligation| obligation_result(obligation, context.joined))
         .collect();
     let fingerprint: String = form_fingerprint(&obligations);
-    let definition_sha256: String = form_definition(form, declared);
+    let reading = context.joined.readings.get(form.id.as_str()).copied();
+    let definition_sha256: String = form_definition(form, declared, reading);
     let review: Option<Reason> =
         review_reason(&form.id, (&fingerprint, &definition_sha256), context);
     let reasons: Vec<Reason> = form_reasons(&obligations, review);
diff --git a/crates/sqlquack-syntax-coverage/src/check/_helpers/join.rs b/crates/sqlquack-syntax-coverage/src/check/_helpers/join.rs
index a63a49737..50f13d9eb 100644
--- a/crates/sqlquack-syntax-coverage/src/check/_helpers/join.rs
+++ b/crates/sqlquack-syntax-coverage/src/check/_helpers/join.rs
@@ -3,9 +3,9 @@
 use std::collections::BTreeMap;
 
 use crate::check::_helpers::receipts::case_result;
-use crate::check::models::{CaseResult, Joined, LocalVerdict};
+use crate::check::models::{CaseResult, Joined, LocalVerdict, Reason};
 use crate::formats::main::obligation_form::obligation_form;
-use crate::formats::models::{Form, Obligation, Receipt, SyntaxCoverage};
+use crate::formats::models::{Form, Obligation, Receipt, SyntaxCoverage, UnobservableCause};
 
 fn forms_by_id(coverage: &SyntaxCoverage) -> BTreeMap<&str, &Form> {
     coverage
@@ -75,7 +75,18 @@ pub(crate) fn join<'a>(
         unobservable: coverage
             .unobservable
             .iter()
-            .map(|entry| entry.obligation.as_str())
+            .map(|entry| {
+                let reason: Reason = match entry.cause {
+                    Some(UnobservableCause::NotSubmitted) => Reason::UnverifiableNotSubmitted,
+                    None => Reason::UnverifiableInternalError,
+                };
+                (entry.obligation.as_str(), reason)
+            })
+            .collect(),
+        readings: coverage
+            .readings
+            .iter()
+            .map(|reading| (reading.form.as_str(), reading))
             .collect(),
     }
 }
diff --git a/crates/sqlquack-syntax-coverage/src/check/_helpers/receipts.rs b/crates/sqlquack-syntax-coverage/src/check/_helpers/receipts.rs
index 0513df16d..84f269362 100644
--- a/crates/sqlquack-syntax-coverage/src/check/_helpers/receipts.rs
+++ b/crates/sqlquack-syntax-coverage/src/check/_helpers/receipts.rs
@@ -1,9 +1,9 @@
 //! One case's result: its receipts against the current parser verdict.
 
-use std::collections::BTreeSet;
+use std::collections::{BTreeMap, BTreeSet};
 
 use crate::check::models::{CaseResult, LocalVerdict, Reason};
-use crate::formats::models::{Case, Expect, Phase, Receipt};
+use crate::formats::models::{AccountSetting, Case, Expect, Phase, Receipt};
 
 /// A syntax receipt bound to exactly this case's SQL, setup, session and capture, with a query id.
 fn admissible(case: &Case, receipt: &Receipt) -> bool {
@@ -84,5 +84,11 @@ pub(crate) fn case_result(case: &Case, receipts: &[&Receipt], local: LocalVerdic
         local,
         reason,
         semantic_only,
+        account_state: receipts
+            .iter()
+            .filter(|receipt| admissible(case, receipt))
+            .flat_map(|receipt| receipt.account_state.iter().flatten())
+            .map(|(name, setting)| (name.clone(), setting.clone()))
+            .collect::<BTreeMap<String, AccountSetting>>(),
     }
 }
diff --git a/crates/sqlquack-syntax-coverage/src/check/_helpers/references.rs b/crates/sqlquack-syntax-coverage/src/check/_helpers/references.rs
index 4847e454a..7f702c4f3 100644
--- a/crates/sqlquack-syntax-coverage/src/check/_helpers/references.rs
+++ b/crates/sqlquack-syntax-coverage/src/check/_helpers/references.rs
@@ -77,6 +77,11 @@ pub(crate) fn reference_problems(
             }
         }
     }
+    for reading in &coverage.readings {
+        if !forms.contains_key(reading.form.as_str()) {
+            problems.push(format!("reading {}: form is not catalogued", reading.form));
+        }
+    }
     let sources: BTreeSet<&str> = coverage
         .sources
         .iter()
diff --git a/crates/sqlquack-syntax-coverage/src/check/models.rs b/crates/sqlquack-syntax-coverage/src/check/models.rs
index 0b35ed23a..405fc97b5 100644
--- a/crates/sqlquack-syntax-coverage/src/check/models.rs
+++ b/crates/sqlquack-syntax-coverage/src/check/models.rs
@@ -4,7 +4,9 @@ use std::collections::{BTreeMap, BTreeSet};
 
 use serde::{Deserialize, Serialize};
 
-use crate::formats::models::{Form, Obligation, ObligationKind, Phase, Review};
+use crate::formats::models::{
+    AccountSetting, Form, Obligation, ObligationKind, Phase, Reading, Review,
+};
 
 /// The current parser's verdict on one case's SQL.
 #[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
@@ -48,6 +50,8 @@ pub enum Reason {
     MissingCase,
     /// Unverifiable: Snowflake answers the construct only with an internal error (decision D87).
     UnverifiableInternalError,
+    /// Unverifiable: the cases are never submitted, such as side-effecting calls a guard holds.
+    UnverifiableNotSubmitted,
     /// A citing case has no receipt.
     MissingReceipt,
     /// A citing extreme case awaits Snowflake's answer (`expect = "observe"`).
@@ -85,6 +89,9 @@ pub struct CaseResult {
     pub reason: Option<Reason>,
     /// Agrees, while Snowflake stopped after parsing (semantic, runtime or unsupported phase).
     pub semantic_only: bool,
+    /// The account parameters its admissible receipts ran under (decision D120).
+    #[serde(skip_serializing_if = "BTreeMap::is_empty")]
+    pub account_state: BTreeMap<String, AccountSetting>,
 }
 
 /// One obligation's result.
@@ -156,8 +163,10 @@ pub(crate) struct Joined<'a> {
     pub(crate) citing: BTreeMap<&'a str, Vec<&'a str>>,
     /// Each case's result by case id.
     pub(crate) cases: BTreeMap<&'a str, CaseResult>,
-    /// Obligations listed as unobservable, which never count as satisfied.
-    pub(crate) unobservable: BTreeSet<&'a str>,
+    /// Obligations listed as unobservable, with the reason they report; never satisfied.
+    pub(crate) unobservable: BTreeMap<&'a str, Reason>,
+    /// Each form's reading by form id.
+    pub(crate) readings: BTreeMap<&'a str, &'a Reading>,
 }
 
 /// What every form of one family is judged against besides its own obligations.
diff --git a/crates/sqlquack-syntax-coverage/src/check/tests/helpers.rs b/crates/sqlquack-syntax-coverage/src/check/tests/helpers.rs
index 41ed7cb22..e5b8b9547 100644
--- a/crates/sqlquack-syntax-coverage/src/check/tests/helpers.rs
+++ b/crates/sqlquack-syntax-coverage/src/check/tests/helpers.rs
@@ -316,6 +316,16 @@ pub(crate) fn verified_tree(root: &Path) {
         "receipts/run-1.jsonl",
         &format!("{}\n", receipts.join("\n")),
     );
+    write(
+        root,
+        "limits.toml",
+        &format!(
+            "[[reading]]\nform = \"sf.query.select\"\ngrammar_sha256 = \"{SHA_A}\"\n\
+             grammar = [\"SELECT <expr> read as one expression\"]\nreason = \"r\"\n\
+             [[reading]]\nform = \"sf.query.select.top\"\ngrammar_sha256 = \"{SHA_A}\"\n\
+             grammar = [\"SELECT TOP <n> <expr> read as one count\"]\nreason = \"r\"\n"
+        ),
+    );
     review(root);
 }
 
@@ -381,6 +391,22 @@ pub(crate) fn unobservable(root: &Path, obligation: &str, case_id: &str, sql: &s
     );
 }
 
+/// Lists `obligation` as never submitted, citing `case_id` with the hash of `sql`, with `runs`.
+pub(crate) fn not_submitted(root: &Path, obligation: &str, case_id: &str, sql: &str, runs: &str) {
+    write(
+        root,
+        "unobservable/query.toml",
+        &format!(
+            "[[unobservable]]\nobligation = \"{obligation}\"\nform = \"sf.query.select\"\n\
+             construct = \"a construct\"\nreason = \"not submitted: held by the capture guard\"\n\
+             cause = \"not_submitted\"\n\
+             cases = [{{ case_id = \"{case_id}\", sql_sha256 = \"{}\" }}]\n\
+             runs = [{runs}]\nprobes = []\n",
+            sha256(sql)
+        ),
+    );
+}
+
 /// Adds a note to the obligation `id` of kind `kind`, an edit the obligations file alone sees.
 pub(crate) fn note_obligation(root: &Path, id: &str, kind: &str) {
     let declared: String = format!("id = \"{id}\"\nkind = \"{kind}\"\nrequired = true\n");
diff --git a/crates/sqlquack-syntax-coverage/src/check/tests/test_check_coverage.rs b/crates/sqlquack-syntax-coverage/src/check/tests/test_check_coverage.rs
index 69b650df9..7d835c496 100644
--- a/crates/sqlquack-syntax-coverage/src/check/tests/test_check_coverage.rs
+++ b/crates/sqlquack-syntax-coverage/src/check/tests/test_check_coverage.rs
@@ -2,12 +2,12 @@ use crate::check::main::check_coverage::check_coverage;
 use crate::check::models::{FormState, Reason};
 use crate::check::tests::helpers::{
     OTHER_TREE, SETUP, TREE, append_receipt, case_in_zone, case_line, crashing,
-    crashing_on_select_from, drop_lines, exclusion_review, form, hanging, move_form,
+    crashing_on_select_from, drop_lines, exclusion_review, form, hanging, move_form, not_submitted,
     note_obligation, obligation, opaque, pin_definitions, pin_fingerprints, read, receipt_line,
     rejecting, replace, reshaped, rewrite_select_17, select_17, select_17_setup_sha256, sha256,
     structural, unobservable, verified_tree, with_fields, write,
 };
-use crate::check::tests::test_types::CheckTestCase;
+use crate::check::tests::test_types::{AccountStateTestCase, CheckTestCase, Parameters};
 use crate::formats::main::load_coverage::load_coverage;
 
 #[test]
@@ -521,6 +521,47 @@ fn given_a_changed_tree_when_checking_then_the_form_fails_closed_with_its_reason
             expected_reason: Some(Reason::UnverifiableInternalError),
             expected_problem: None,
         },
+        CheckTestCase {
+            description: "a never-submitted obligation whose case otherwise agrees",
+            mutate: |root| {
+                not_submitted(root, "sf.query.select.o001", "select-17", "SELECT 17", "")
+            },
+            parse: structural,
+            parser_tree: Some(TREE),
+            form: "sf.query.select",
+            expected_state: FormState::Unverified,
+            expected_reason: Some(Reason::UnverifiableNotSubmitted),
+            expected_problem: None,
+        },
+        CheckTestCase {
+            description: "a never-submitted entry whose case hash is stale",
+            mutate: |root| {
+                not_submitted(root, "sf.query.select.o001", "select-17", "SELECT 18", "")
+            },
+            parse: structural,
+            parser_tree: Some(TREE),
+            form: "sf.query.select",
+            expected_state: FormState::Unverified,
+            expected_reason: Some(Reason::UnverifiableNotSubmitted),
+            expected_problem: Some("case select-17 is not a case with that sql_sha256"),
+        },
+        CheckTestCase {
+            description: "a reading of a form that is not catalogued",
+            mutate: |root| {
+                replace(
+                    root,
+                    "limits.toml",
+                    "form = \"sf.query.select.top\"",
+                    "form = \"sf.query.tops\"",
+                )
+            },
+            parse: structural,
+            parser_tree: Some(TREE),
+            form: "sf.query.select",
+            expected_state: FormState::Verified,
+            expected_reason: None,
+            expected_problem: Some("reading sf.query.tops: form is not catalogued"),
+        },
         CheckTestCase {
             description: "an unobservable entry naming an undeclared obligation",
             mutate: |root| unobservable(root, "sf.query.select.o009", "select-17", "SELECT 17"),
@@ -989,6 +1030,37 @@ fn given_a_review_binding_each_form_when_its_family_files_change_then_only_that_
             expected_reason: Some(Reason::StaleReview),
             expected_problem: None,
         },
+        CheckTestCase {
+            description: "the form's own reading edited after review",
+            mutate: |root| {
+                pin_definitions(root);
+                replace(
+                    root,
+                    "limits.toml",
+                    "read as one expression",
+                    "read as a list",
+                );
+            },
+            parse: structural,
+            parser_tree: Some(TREE),
+            form: "sf.query.select",
+            expected_state: FormState::Unverified,
+            expected_reason: Some(Reason::StaleReview),
+            expected_problem: None,
+        },
+        CheckTestCase {
+            description: "another form's reading edited in the same limits file",
+            mutate: |root| {
+                pin_definitions(root);
+                replace(root, "limits.toml", "read as one count", "read as a list");
+            },
+            parse: structural,
+            parser_tree: Some(TREE),
+            form: "sf.query.select",
+            expected_state: FormState::Verified,
+            expected_reason: None,
+            expected_problem: None,
+        },
         CheckTestCase {
             description: "a review binding the family's files still goes stale on another form's edit",
             mutate: |root| note_obligation(root, "sf.query.select.top.o001", "positive"),
@@ -1033,3 +1105,67 @@ fn given_a_review_binding_each_form_when_its_family_files_change_then_only_that_
         );
     }
 }
+
+#[test]
+fn given_a_receipt_with_account_state_when_checking_then_only_its_case_carries_it() {
+    let test_cases = [
+        AccountStateTestCase {
+            description: "a parameter with its value",
+            account_state: ",\"account_state\":{\"CORTEX_MODELS_ALLOWLIST\":\
+                            {\"value\":\"NONE\",\"basis\":\"D120: set by sa-01\"}}",
+            expected_cases: vec![
+                ("select-17", vec![("CORTEX_MODELS_ALLOWLIST", Some("NONE"))]),
+                ("select-from", vec![]),
+                ("select-top", vec![]),
+            ],
+        },
+        AccountStateTestCase {
+            description: "a parameter whose value is null for want of a usable recorded_at",
+            account_state: ",\"account_state\":{\"CORTEX_MODELS_ALLOWLIST\":\
+                            {\"value\":null,\"basis\":\"D120: no usable recorded_at\"}}",
+            expected_cases: vec![
+                ("select-17", vec![("CORTEX_MODELS_ALLOWLIST", None)]),
+                ("select-from", vec![]),
+                ("select-top", vec![]),
+            ],
+        },
+    ];
+
+    for test_case in test_cases {
+        let directory = tempfile::tempdir().expect("temporary directory");
+        verified_tree(directory.path());
+        replace(
+            directory.path(),
+            "receipts/run-1.jsonl",
+            "\"phase_basis\":\"errno\"",
+            &format!("\"phase_basis\":\"errno\"{}", test_case.account_state),
+        );
+        let coverage = load_coverage(directory.path())
+            .unwrap_or_else(|problems| panic!("{}: {problems:#?}", test_case.description));
+        let check = check_coverage(&coverage, Some(TREE), &structural);
+        let cases: Vec<(&str, Parameters)> = check
+            .forms
+            .iter()
+            .flat_map(|form| &form.obligations)
+            .flat_map(|obligation| &obligation.cases)
+            .map(|case| {
+                let state = case
+                    .account_state
+                    .iter()
+                    .map(|(name, setting)| (name.as_str(), setting.value.as_deref()))
+                    .collect();
+                (case.case_id.as_str(), state)
+            })
+            .collect();
+        assert_eq!(cases, test_case.expected_cases, "{}", test_case.description);
+        assert!(
+            check
+                .forms
+                .iter()
+                .filter(|form| form.family == "query")
+                .all(|form| form.state == FormState::Verified),
+            "{}: account state is provenance and changes no verdict",
+            test_case.description
+        );
+    }
+}
diff --git a/crates/sqlquack-syntax-coverage/src/check/tests/test_types.rs b/crates/sqlquack-syntax-coverage/src/check/tests/test_types.rs
index 9336dc2ea..012001a06 100644
--- a/crates/sqlquack-syntax-coverage/src/check/tests/test_types.rs
+++ b/crates/sqlquack-syntax-coverage/src/check/tests/test_types.rs
@@ -17,3 +17,15 @@ pub(crate) struct CheckTestCase {
     /// A fragment of a reference problem; none when there must be no problem.
     pub(crate) expected_problem: Option<&'static str>,
 }
+
+/// Account parameter names with their values.
+pub(crate) type Parameters<'a> = Vec<(&'a str, Option<&'a str>)>;
+
+/// A receipt `account_state` fragment and the account state each case must then carry.
+pub(crate) struct AccountStateTestCase {
+    pub(crate) description: &'static str,
+    /// Inserted after the first receipt's `phase_basis`, the receipt of `select-17`.
+    pub(crate) account_state: &'static str,
+    /// Each case id with its parameter names and values, in case-id order.
+    pub(crate) expected_cases: Vec<(&'static str, Parameters<'static>)>,
+}
diff --git a/crates/sqlquack-syntax-coverage/src/formats/_helpers/records.rs b/crates/sqlquack-syntax-coverage/src/formats/_helpers/records.rs
index b26dee81d..55f726692 100644
--- a/crates/sqlquack-syntax-coverage/src/formats/_helpers/records.rs
+++ b/crates/sqlquack-syntax-coverage/src/formats/_helpers/records.rs
@@ -14,9 +14,9 @@ use crate::formats::constants::{
 };
 use crate::formats::main::obligation_form::obligation_form;
 use crate::formats::models::{
-    Alias, CaptureMethod, Case, Definition, Diagnostic, Exclusion, Expect, Form, FormKind,
-    FormStatus, Index, Obligation, ObligationKind, Phase, Receipt, Review, Source, SourceStatus,
-    Unobservable, UnobservableCase, UnobservableProbe,
+    AccountSetting, Alias, CaptureMethod, Case, Definition, Diagnostic, Exclusion, Expect, Form,
+    FormKind, FormStatus, Index, Obligation, ObligationKind, Phase, Reading, Receipt, Review,
+    Source, SourceStatus, Unobservable, UnobservableCase, UnobservableCause, UnobservableProbe,
 };
 
 fn blank(text: &str) -> bool {
@@ -354,7 +354,31 @@ pub(crate) fn check_receipt(receipt: &Receipt) -> Vec<String> {
         receipt.inner_message.as_ref(),
         receipt.dcm_project.as_ref(),
     ];
-    if text.iter().flatten().any(|field| identifying(field)) {
+    let settings: Vec<(&String, &AccountSetting)> =
+        receipt.account_state.iter().flatten().collect();
+    if receipt
+        .account_state
+        .as_ref()
+        .is_some_and(BTreeMap::is_empty)
+        || settings.iter().any(|(name, setting)| {
+            blank(name) || setting.value.as_deref().is_some_and(blank) || blank(&setting.basis)
+        })
+    {
+        problems.push(format!(
+            "receipt {id}: account_state names at least one parameter, each with a value and basis"
+        ));
+    }
+    let account_text = settings
+        .iter()
+        .flat_map(|(name, setting)| [Some(*name), setting.value.as_ref(), Some(&setting.basis)])
+        .flatten();
+    if text
+        .iter()
+        .flatten()
+        .copied()
+        .chain(account_text)
+        .any(|field| identifying(field))
+    {
         problems.push(format!(
             "receipt {id}: holds an account, host, URL or address"
         ));
@@ -567,6 +591,9 @@ pub(crate) fn check_review(review: &Review) -> Vec<String> {
 }
 
 pub(crate) fn check_unobservable(entry: &Unobservable, family: &str) -> Vec<String> {
+    if entry.cause == Some(UnobservableCause::NotSubmitted) {
+        return check_not_submitted(entry, family);
+    }
     check_record(
         &UnobservableRecord {
             obligation: &entry.obligation,
@@ -598,6 +625,32 @@ pub(crate) fn check_diagnostic(entry: &Diagnostic, family: &str) -> Vec<String>
     )
 }
 
+/// A never-submitted entry: a reason and cases, but no runs or probes, since nothing ran.
+fn check_not_submitted(entry: &Unobservable, family: &str) -> Vec<String> {
+    let id: &str = &entry.obligation;
+    let mut problems: Vec<String> = Vec::new();
+    if obligation_form(id, family) != Some(entry.form.as_str()) {
+        problems.push(format!(
+            "unobservable {id}: not an obligation of form {} in family {family}",
+            entry.form
+        ));
+    }
+    if blank(&entry.construct) || blank(&entry.reason) || entry.cases.is_empty() {
+        problems.push(format!(
+            "unobservable {id}: needs a construct, a reason and at least one case"
+        ));
+    }
+    if !entry.runs.is_empty() || !entry.probes.is_empty() {
+        problems.push(format!(
+            "unobservable {id}: a not_submitted entry has no runs or probes"
+        ));
+    }
+    if entry.cases.iter().any(|case| !is_sha256(&case.sql_sha256)) {
+        problems.push(format!("unobservable {id}: a sql_sha256 is not a SHA-256"));
+    }
+    problems
+}
+
 /// The fields an unobservable entry and a diagnostic share.
 struct UnobservableRecord<'a> {
     obligation: &'a str,
@@ -685,3 +738,24 @@ pub(crate) fn check_restatements<'a>(
     );
     problems
 }
+
+/// A reading pins the page grammar it reads, by hash or prose heading, and gives its reason.
+pub(crate) fn check_reading(reading: &Reading) -> Vec<String> {
+    let id: &str = &reading.form;
+    let mut problems: Vec<String> = Vec::new();
+    let prose: bool = reading
+        .grammar_sha256
+        .strip_prefix(PROSE_HASH_PREFIX)
+        .is_some_and(|heading| !blank(heading));
+    if !prose && !is_sha256(&reading.grammar_sha256) {
+        problems.push(format!(
+            "reading {id}: grammar_sha256 is neither a SHA-256 nor a prose heading"
+        ));
+    }
+    if reading.grammar.iter().any(|line| blank(line)) || blank(&reading.reason) {
+        problems.push(format!(
+            "reading {id}: needs a reason and no blank grammar line"
+        ));
+    }
+    problems
+}
diff --git a/crates/sqlquack-syntax-coverage/src/formats/_helpers/sections.rs b/crates/sqlquack-syntax-coverage/src/formats/_helpers/sections.rs
index 73811f3a5..07b222ef4 100644
--- a/crates/sqlquack-syntax-coverage/src/formats/_helpers/sections.rs
+++ b/crates/sqlquack-syntax-coverage/src/formats/_helpers/sections.rs
@@ -8,18 +8,18 @@ use crate::formats::_helpers::files::{
 };
 use crate::formats::_helpers::records::{
     check_alias, check_case, check_definition, check_diagnostic, check_form, check_index,
-    check_obligation, check_receipt, check_restatements, check_review, check_source,
+    check_obligation, check_reading, check_receipt, check_restatements, check_review, check_source,
     check_unobservable,
 };
 use crate::formats::_helpers::retired::{retire, withdrawn_receipts};
 use crate::formats::constants::{
-    ALIASES_FILE, CASES_DIR, CATALOGUE_DIR, INDEXES_FILE, OBLIGATIONS_DIR, RECEIPT_REPORT_SUFFIX,
-    RECEIPTS_DIR, REVIEWS_DIR, SOURCES_FILE, UNOBSERVABLE_DIR,
+    ALIASES_FILE, CASES_DIR, CATALOGUE_DIR, INDEXES_FILE, LIMITS_FILE, OBLIGATIONS_DIR,
+    RECEIPT_REPORT_SUFFIX, RECEIPTS_DIR, REVIEWS_DIR, SOURCES_FILE, UNOBSERVABLE_DIR,
 };
 use crate::formats::models::{
-    Alias, AliasesFile, Case, CatalogueFile, Diagnostic, Index, IndexesFile, Obligation,
-    ObligationsFile, Receipt, Review, ReviewsFile, Source, SourcesFile, Unobservable,
-    UnobservableFile,
+    Alias, AliasesFile, Case, CatalogueFile, Diagnostic, Index, IndexesFile, LimitsFile,
+    Obligation, ObligationsFile, Reading, Receipt, Review, ReviewsFile, Source, SourcesFile,
+    Unobservable, UnobservableFile,
 };
 use crate::formats::types::FamilyCatalogue;
 
@@ -249,6 +249,24 @@ pub(crate) fn load_unobservable(root: &Path) -> Section<(Vec<Unobservable>, Vec<
     Section::of((records, diagnostics), Vec::new(), problems)
 }
 
+/// The readings in `limits.toml`, which must exist: without it no form's definition holds its reading.
+pub(crate) fn load_readings(root: &Path) -> Section<Vec<Reading>> {
+    match read_toml::<LimitsFile>(&root.join(LIMITS_FILE)) {
+        Ok((file, _)) => {
+            let mut problems: Vec<String> = file.readings.iter().flat_map(check_reading).collect();
+            let mut seen: BTreeSet<&str> = BTreeSet::new();
+            problems.extend(
+                file.readings
+                    .iter()
+                    .filter(|reading| !seen.insert(reading.form.as_str()))
+                    .map(|reading| format!("reading {}: listed twice", reading.form)),
+            );
+            Section::of(file.readings, Vec::new(), problems)
+        }
+        Err(problem) => Section::of(Vec::new(), Vec::new(), vec![problem]),
+    }
+}
+
 pub(crate) fn load_reviews(root: &Path) -> Section<Vec<Review>> {
     let (paths, others) = listed(&root.join(REVIEWS_DIR), "toml");
     let mut problems: Vec<String> = others.iter().map(|path| stray(path, "toml")).collect();
@@ -277,6 +295,7 @@ pub(crate) struct Sections {
     pub(crate) receipts: Section<(Vec<Receipt>, Vec<String>)>,
     pub(crate) reviews: Section<Vec<Review>>,
     pub(crate) unobservable: Section<(Vec<Unobservable>, Vec<Diagnostic>)>,
+    pub(crate) readings: Section<Vec<Reading>>,
 }
 
 impl Sections {
@@ -292,6 +311,7 @@ impl Sections {
             &self.receipts.problems,
             &self.reviews.problems,
             &self.unobservable.problems,
+            &self.readings.problems,
         ]
         .into_iter()
         .flatten()
@@ -327,6 +347,7 @@ pub(crate) fn load_sections(root: &Path) -> Sections {
         receipts: load_receipts(root),
         reviews: load_reviews(root),
         unobservable: load_unobservable(root),
+        readings: load_readings(root),
         sources,
     }
 }
diff --git a/crates/sqlquack-syntax-coverage/src/formats/constants.rs b/crates/sqlquack-syntax-coverage/src/formats/constants.rs
index dc9c46c56..a8b13e9a0 100644
--- a/crates/sqlquack-syntax-coverage/src/formats/constants.rs
+++ b/crates/sqlquack-syntax-coverage/src/formats/constants.rs
@@ -20,6 +20,8 @@ pub const RECEIPTS_DIR: &str = "receipts";
 pub const REVIEWS_DIR: &str = "reviews";
 /// Obligations Snowflake answers only with an internal error, one optional TOML file per family.
 pub const UNOBSERVABLE_DIR: &str = "unobservable";
+/// Hand-added limits, suppressions and grammar readings; the checker loads the readings.
+pub const LIMITS_FILE: &str = "limits.toml";
 /// Every family, each with a catalogue, an obligation and a case file.
 pub const FAMILIES: [&str; 10] = [
     "query",
diff --git a/crates/sqlquack-syntax-coverage/src/formats/main/load_coverage.rs b/crates/sqlquack-syntax-coverage/src/formats/main/load_coverage.rs
index ff2c233ee..32e8c851f 100644
--- a/crates/sqlquack-syntax-coverage/src/formats/main/load_coverage.rs
+++ b/crates/sqlquack-syntax-coverage/src/formats/main/load_coverage.rs
@@ -36,6 +36,7 @@ pub fn load_coverage(root: &Path) -> Result<SyntaxCoverage, Vec<String>> {
         reviews: sections.reviews.records,
         unobservable: sections.unobservable.records.0,
         diagnostics: sections.unobservable.records.1,
+        readings: sections.readings.records,
         file_hashes,
     })
 }
diff --git a/crates/sqlquack-syntax-coverage/src/formats/models.rs b/crates/sqlquack-syntax-coverage/src/formats/models.rs
index 6d6686de6..97db6155b 100644
--- a/crates/sqlquack-syntax-coverage/src/formats/models.rs
+++ b/crates/sqlquack-syntax-coverage/src/formats/models.rs
@@ -343,6 +343,9 @@ pub struct Receipt {
     /// The position the inner error points at, when its text gives one.
     #[serde(default)]
     pub definition_position: Option<u32>,
+    /// Account parameters the capture ran under, by name (decision D120); provenance, never phase.
+    #[serde(default)]
+    pub account_state: Option<BTreeMap<String, AccountSetting>>,
 }
 
 #[derive(Clone, Copy, Debug, PartialEq, Eq, Deserialize, Serialize)]
@@ -449,7 +452,38 @@ pub struct UnobservableFile {
     pub diagnostics: Vec<Diagnostic>,
 }
 
-/// An obligation Snowflake answers only with an internal error; never verified (decision D87).
+/// One account parameter a receipt's capture ran under, and why it held that value.
+#[derive(Clone, Debug, PartialEq, Eq, Deserialize, Serialize)]
+#[serde(deny_unknown_fields)]
+pub struct AccountSetting {
+    /// Null when the receipt has no usable `recorded_at` to read the value at.
+    pub value: Option<String>,
+    pub basis: String,
+}
+
+/// `limits.toml`. The checker reads only the readings; the obligation builder owns the other tables.
+#[derive(Clone, Debug, PartialEq, Deserialize, Serialize)]
+#[serde(deny_unknown_fields)]
+pub struct LimitsFile {
+    #[serde(default, rename = "limit")]
+    pub limits: Vec<toml::Table>,
+    #[serde(default, rename = "suppress")]
+    pub suppressions: Vec<toml::Table>,
+    #[serde(default, rename = "reading")]
+    pub readings: Vec<Reading>,
+}
+
+/// How a form's page grammar is read where it is ambiguous; part of the form's definition (D118).
+#[derive(Clone, Debug, PartialEq, Eq, Deserialize, Serialize)]
+#[serde(deny_unknown_fields)]
+pub struct Reading {
+    pub form: String,
+    pub grammar_sha256: String,
+    pub grammar: Vec<String>,
+    pub reason: String,
+}
+
+/// An obligation no capture can establish a phase for; never verified (decision D87).
 #[derive(Clone, Debug, PartialEq, Eq, Deserialize, Serialize)]
 #[serde(deny_unknown_fields)]
 pub struct Unobservable {
@@ -457,6 +491,9 @@ pub struct Unobservable {
     pub form: String,
     pub construct: String,
     pub reason: String,
+    /// Why no phase exists; absent means Snowflake answered only with an internal error (603).
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub cause: Option<UnobservableCause>,
     /// The captured cases, kept in the cases file without a receipt.
     pub cases: Vec<UnobservableCase>,
     /// The capture, re-run and probe runs; none of them imported.
@@ -464,6 +501,14 @@ pub struct Unobservable {
     pub probes: Vec<UnobservableProbe>,
 }
 
+/// Why an unobservable obligation has no phase, other than a 603 internal error.
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Deserialize, Serialize)]
+#[serde(rename_all = "snake_case")]
+pub enum UnobservableCause {
+    /// The cases were never submitted, such as side-effecting calls a capture guard holds.
+    NotSubmitted,
+}
+
 /// A 603 record on a construct no obligation requires any more; listed, never scored.
 #[derive(Clone, Debug, PartialEq, Eq, Deserialize, Serialize)]
 #[serde(deny_unknown_fields)]
@@ -512,6 +557,8 @@ pub struct SyntaxCoverage {
     pub reviews: Vec<Review>,
     pub unobservable: Vec<Unobservable>,
     pub diagnostics: Vec<Diagnostic>,
+    /// Each form's reading from `limits.toml`, hashed into its definition.
+    pub readings: Vec<Reading>,
     /// SHA-256 of the sources, aliases, catalogue and obligation files, by relative path.
     pub file_hashes: BTreeMap<String, String>,
 }
diff --git a/crates/sqlquack-syntax-coverage/src/formats/tests/helpers.rs b/crates/sqlquack-syntax-coverage/src/formats/tests/helpers.rs
index 110a1290b..a0183cb23 100644
--- a/crates/sqlquack-syntax-coverage/src/formats/tests/helpers.rs
+++ b/crates/sqlquack-syntax-coverage/src/formats/tests/helpers.rs
@@ -74,6 +74,17 @@ pub(crate) fn receipt_line() -> String {
     )
 }
 
+/// Where a receipt line takes an `account_state` field.
+pub(crate) const ACCOUNT_STATE_AT: &str = "\"phase_basis\":\"ran\"";
+
+/// `ACCOUNT_STATE_AT` followed by one account parameter whose basis is `basis`.
+pub(crate) fn account_state(basis: &str) -> String {
+    format!(
+        "{ACCOUNT_STATE_AT},\"account_state\":{{\"CORTEX_MODELS_ALLOWLIST\":\
+         {{\"basis\":\"{basis}\",\"value\":\"NONE\"}}}}"
+    )
+}
+
 /// `receipt_line()` as a failed DCM PLAN of its case, its inner error ending the whole message.
 pub(crate) fn dcm_line(inner_message: &str, position: &str) -> String {
     let message: String = format!(
@@ -160,6 +171,16 @@ pub(crate) fn valid_tree(root: &Path) {
         ),
     );
     write(root, "cases/query.jsonl", &format!("{}\n", case_line()));
+    write(
+        root,
+        "limits.toml",
+        &format!(
+            "[[limit]]\nform = \"sf.query.select\"\nkind = \"boundary_above\"\n\
+             [[suppress]]\nform = \"sf.query.select\"\nreason = \"r\"\n\
+             [[reading]]\nform = \"sf.query.select\"\ngrammar_sha256 = \"{SHA_A}\"\n\
+             grammar = [\"SELECT <expr>\"]\nreason = \"r\"\n"
+        ),
+    );
     write(
         root,
         "receipts/first.jsonl",
diff --git a/crates/sqlquack-syntax-coverage/src/formats/tests/test_load_coverage.rs b/crates/sqlquack-syntax-coverage/src/formats/tests/test_load_coverage.rs
index 1ae3b5ac1..475bdd3c4 100644
--- a/crates/sqlquack-syntax-coverage/src/formats/tests/test_load_coverage.rs
+++ b/crates/sqlquack-syntax-coverage/src/formats/tests/test_load_coverage.rs
@@ -4,8 +4,8 @@ use std::path::Path;
 use crate::formats::constants::{COVERAGE_ROOT, FAMILIES};
 use crate::formats::main::load_coverage::load_coverage;
 use crate::formats::tests::helpers::{
-    dcm_line, line_sha256, receipt_line, replace, restated_page, superseding_line, valid_tree,
-    write,
+    ACCOUNT_STATE_AT, account_state, dcm_line, line_sha256, receipt_line, replace, restated_page,
+    superseding_line, valid_tree, write,
 };
 use crate::formats::tests::test_types::{
     CommittedTestCase, FormatFaultTestCase, LoadTestCase, LoadedCounts,
@@ -234,6 +234,18 @@ fn given_a_valid_tree_when_loading_then_every_record_is_kept() {
                 ..counts(0)
             },
         },
+        LoadTestCase {
+            description: "a receipt recording the account parameter its capture ran under",
+            tree: |root| {
+                valid_tree(root);
+                write(
+                    root,
+                    "receipts/first.jsonl",
+                    &receipt_line().replace(ACCOUNT_STATE_AT, &account_state("D120")),
+                );
+            },
+            expected_counts: counts(1),
+        },
         LoadTestCase {
             description: "a tree without renames or reviews yet",
             tree: |root| {
@@ -755,6 +767,32 @@ fn given_a_format_fault_when_loading_then_the_problem_is_named() {
             },
             expected_problem: "query-1: declared twice",
         },
+        FormatFaultTestCase {
+            description: "no limits.toml, so no form's reading can be hashed",
+            mutate: |root| std::fs::remove_file(root.join("limits.toml")).expect("remove"),
+            expected_problem: "limits.toml: No such file",
+        },
+        FormatFaultTestCase {
+            description: "a form read twice",
+            mutate: |root| {
+                let limits = std::fs::read_to_string(root.join("limits.toml")).expect("read");
+                let reading = &limits[limits.find("[[reading]]").expect("reading")..];
+                write(root, "limits.toml", &format!("{limits}{reading}"));
+            },
+            expected_problem: "reading sf.query.select: listed twice",
+        },
+        FormatFaultTestCase {
+            description: "a misspelt table in limits.toml",
+            mutate: |root| {
+                let limits = std::fs::read_to_string(root.join("limits.toml")).expect("read");
+                write(
+                    root,
+                    "limits.toml",
+                    &limits.replace("[[reading]]", "[[readings]]"),
+                );
+            },
+            expected_problem: "unknown field `readings`",
+        },
         FormatFaultTestCase {
             description: "an unobservable obligation of another form",
             mutate: |root| {
@@ -784,6 +822,39 @@ fn given_a_format_fault_when_loading_then_the_problem_is_named() {
             },
             expected_problem: "unobservable sf.query.select.o001: a sql_sha256 is not a SHA-256",
         },
+        FormatFaultTestCase {
+            description: "an unobservable entry with an unknown cause",
+            mutate: |root| {
+                write(
+                    root,
+                    "unobservable/query.toml",
+                    "[[unobservable]]\nobligation = \"sf.query.select.o001\"\nform = \"sf.query.select\"\nconstruct = \"c\"\nreason = \"held\"\ncause = \"held_by_guard\"\ncases = [{ case_id = \"query.select-17\", sql_sha256 = \"aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa\" }]\nruns = []\nprobes = []\n",
+                )
+            },
+            expected_problem: "unknown variant `held_by_guard`",
+        },
+        FormatFaultTestCase {
+            description: "a never-submitted entry that lists a run",
+            mutate: |root| {
+                write(
+                    root,
+                    "unobservable/query.toml",
+                    "[[unobservable]]\nobligation = \"sf.query.select.o001\"\nform = \"sf.query.select\"\nconstruct = \"c\"\nreason = \"held\"\ncause = \"not_submitted\"\ncases = [{ case_id = \"query.select-17\", sql_sha256 = \"aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa\" }]\nruns = [\"run-1\"]\nprobes = []\n",
+                )
+            },
+            expected_problem: "unobservable sf.query.select.o001: a not_submitted entry has no runs or probes",
+        },
+        FormatFaultTestCase {
+            description: "a 603 entry without runs",
+            mutate: |root| {
+                write(
+                    root,
+                    "unobservable/query.toml",
+                    "[[unobservable]]\nobligation = \"sf.query.select.o001\"\nform = \"sf.query.select\"\nconstruct = \"c\"\nreason = \"603\"\ncases = [{ case_id = \"query.select-17\", sql_sha256 = \"aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa\" }]\nruns = []\nprobes = []\n",
+                )
+            },
+            expected_problem: "unobservable sf.query.select.o001: needs at least one case and one run",
+        },
         FormatFaultTestCase {
             description: "an unobservable entry without cases",
             mutate: |root| {
@@ -964,6 +1035,44 @@ fn given_a_format_fault_when_loading_then_the_problem_is_named() {
             },
             expected_problem: "cases/query.jsonl:1:",
         },
+        FormatFaultTestCase {
+            description: "an account parameter without its basis",
+            mutate: |root| {
+                write(
+                    root,
+                    "receipts/first.jsonl",
+                    &receipt_line().replace(ACCOUNT_STATE_AT, &account_state(" ")),
+                )
+            },
+            expected_problem: "receipt query.select-17: account_state names at least one parameter",
+        },
+        FormatFaultTestCase {
+            description: "an account parameter whose basis holds an address",
+            mutate: |root| {
+                write(
+                    root,
+                    "receipts/first.jsonl",
+                    &receipt_line().replace(
+                        ACCOUNT_STATE_AT,
+                        &account_state("set by someone@example.com"),
+                    ),
+                )
+            },
+            expected_problem: "receipt query.select-17: holds an account, host, URL or address",
+        },
+        FormatFaultTestCase {
+            description: "an account parameter with an unknown field",
+            mutate: |root| {
+                write(
+                    root,
+                    "receipts/first.jsonl",
+                    &receipt_line()
+                        .replace(ACCOUNT_STATE_AT, &account_state("D120"))
+                        .replace("\"value\":\"NONE\"", "\"value\":\"NONE\",\"scope\":\"x\""),
+                )
+            },
+            expected_problem: "unknown field `scope`",
+        },
         FormatFaultTestCase {
             description: "a receipt holding an address",
             mutate: |root| {
diff --git a/docs/syntax-coverage.md b/docs/syntax-coverage.md
index 1e8fbbb7d..ef55e59e2 100644
--- a/docs/syntax-coverage.md
+++ b/docs/syntax-coverage.md
@@ -108,6 +108,13 @@ placeholder. Add prose-documented limits by hand, with their anchor. Where Snowf
 limit, the obligation's `note` says `no documented bound`, and its `depths` list the depths that
 were tested. Nothing claims to be exhaustive.
 
+`limits.toml` holds the hand-added `[[limit]]` and `[[suppress]]` rows the obligation builder
+reads, and the `[[reading]]` rows: how an ambiguous page grammar is read, with `form`,
+`grammar_sha256` (the form's grammar hash, or `prose:<heading>` for a prose form), `grammar` (its
+lines, none blank; empty for a lexical form the `reason` alone explains) and `reason`. The checker requires the
+file, refuses any other table, a reading of a form that is not catalogued, and a form read twice,
+and hashes each form's reading into its definition (below).
+
 ## Cases (`cases/<family>.jsonl`)
 
 Each line is one JSON object. Blank lines are refused.
@@ -168,6 +175,10 @@ committed one.
   `statements_in_request`, `completed_statements`, `after_sql` and `category`.
   `completed_statements` is the number of statements in the request that completed before it
   stopped. It is provenance only and does not change the phase.
+- Optional `account_state`: the account parameters the capture ran under, by name, each as
+  `{ "value": …, "basis": … }` with both non-empty, such as
+  `{ "CORTEX_MODELS_ALLOWLIST": { "value": "NONE", "basis": "D120: …" } }` (decision D120). It
+  is provenance only and does not change the phase; when present it names at least one parameter.
 - Optional `reason_category` and `reason_category_basis`, always together, and only on a phase
   after parsing (`semantic_error`, `runtime_error` or `unsupported_feature`). The category is one
   of `missing_object`, `invalid_option_or_value`, `type` or `other`. The basis says what the
@@ -250,7 +261,14 @@ internal error (603), so no capture can establish a phase (decision D87). It has
 family; each listed case must exist with that `sql_sha256` and cite the obligation; an obligation is
 listed at most once. Such an obligation stays in the denominator, never counts as satisfied, and is
 reported as `unverifiable_internal_error` ("unverifiable: Snowflake internal error"). Probe results
-are diagnostics, never syntax evidence. A `[[diagnostic]]` in the same file has the same fields,
+are diagnostics, never syntax evidence.
+
+An entry may set `cause = "not_submitted"` when its cases were never sent to Snowflake, such as
+side-effecting calls a capture guard holds. Such an entry has empty `runs` and `probes`, a
+`reason` naming the rule that holds the cases, and at least one case, checked as above. The
+obligation stays in the denominator, never counts as satisfied, and is reported as
+`unverifiable_not_submitted`. An absent `cause` means a 603 internal error; any other value is
+refused. A `[[diagnostic]]` in the same file has the same fields,
 with `captured` in place of `cases`: a 603 record on a construct no obligation requires any more,
 whose retired cases are not resolved against the cases file. Diagnostics are format-checked and
 listed, never scored. The checker ignores `semantic-limits/` and `lane-reviews/`.
@@ -282,8 +300,9 @@ A `[[review]]` has these fields:
   hash when it was reviewed, as `{ "<form id>" = "<sha256>" }`, one for every listed form. A
   review with `definitions` binds each form by its definition and fingerprint alone and has no
   `catalogue_sha256`, `obligations_sha256` or exclusions. An edit to another form in the same
-  catalogue or obligations file leaves it current; any change to the form's own catalogue entry,
-  obligations or fingerprint makes it stale for that form (decision D118).
+  catalogue or obligations file, or to another form's reading, leaves it current; any change to
+  the form's own catalogue entry, obligations, reading or fingerprint makes it stale for that form
+  (decision D118).
 - `[[review.exclusion]]`: exactly one of `form` (a form id of the review's family) or `source` (a
   page id, used for out-of-scope and syntax-less pages), plus a `reason`. A page review excludes
   pages only, and a family review excludes forms only.
@@ -328,7 +347,8 @@ followed by a tab. `family --json` prints each form's `fingerprint`. A parser ch
 every case of a form parsing into the same tree, and every rejection still a rejection, leaves its
 fingerprint and so its review unchanged; a changed tree or verdict, or an added or removed case,
 changes it. A form's definition hash is the SHA-256 of the compact JSON array of its catalogue
-entry and its own obligations in file order, as loaded; `family --json` prints it as
+entry and its own obligations in file order, as loaded, followed by its `[[reading]]` from
+`limits.toml` when it has one; `family --json` prints it as
 `definition_sha256`. A form is excluded only by an approved review that is current in the
 same way. Absent forms keep their ids and are never counted. The headline denominator is the
 catalogued forms: 3,348 on the frozen catalogue `e863d7de` (decision D81).