fix: INSERT Form B value-count UX (ADR-0033 Amendment 5)

Three layered fixes for advanced/simple-mode positional INSERT
value-count mismatches (e.g. `insert into T values (...)` with the
wrong number of values for T's column count), plus ADR-0033
Amendment 5 recording the gate refinement.

Walker diagnostic (dml_insert_arity_diagnostics): the function's own
doc-comment recorded the no-column-list (Form B) case as deferred.
This commit closes that gap. Form B mismatches now emit a new
diagnostic.insert_arity_mismatch_form_b ERROR per offending tuple,
keyed off the target table's column count from the schema cache. The
[ERR] validity indicator (ADR-0027) lights up at typing time for the
reported scenario, no longer needing a submit.

Cross-mode pointer gate (advanced_alternative_note): refactored from
a hand-rolled Form B count check to a single input_verdict_in_mode(
input, schema, Mode::Advanced) call. The pointer fires only when the
verdict is None — the ADR-0027 sense of "valid". Any future static
check added to the verdict pipeline participates automatically; no
per-feature maintenance.

Teaching notes for the value-count cases users can hit before the
indicator turns red:
  - simple-mode submit: insert.form_b_extra_values_note covers under-,
    in-window, and over-supply against the Form B contract; suppressed
    when the cross-mode pointer fires (to avoid parallel advice).
  - advanced-mode dispatch pre-flight:
    insert.form_b_positional_count_mismatch_note catches a submitted
    mismatch with a teaching message before the engine produces its
    raw NOT-NULL / type error.

The advanced_mode.also_valid_sql pointer wording was reworked to
"trying to write SQL? switch with `mode advanced`, or prefix `:` to
run once". One insta snapshot regenerated.

ADR-0033 Amendment 5 records the gate change: Amendment 3's "would
parse in advanced mode" now reads as "valid in advanced mode" in the
explicit verdict-is-None sense, with the precise definition spelled
out so future readers can't drift back to the syntactic-only reading.
ADR-0000 index entry updated; docs/requirements.md H1a citation added
listing the three new pedagogical strings.

Tests added (8): four walker arity tests (under-supply, over-supply,
match, unknown-table); two app-level teaching-note tests for the
sibling cases (under-supply, over-supply beyond total); one pointer-
gate unit test pinning the bug-case suppression; one gate-precedence
test ensuring only one advice line per error. Existing
simple_mode_submit_of_sql_construct_appends_advanced_pointer updated
to use a known schema (the new validity gate requires it).

Full suite: 2031 passed, 0 failed, 0 unexpected skips. Clippy clean.

src/app.rs

@@ -1340,6 +1340,27 @@ impl App {
                 vec![Action::Replay { path }]
             }
             Ok(cmd) => {
+                // Issue #1 sub-task 3: advanced-mode positional
+                // `INSERT INTO T VALUES (…)` (no column list) with a
+                // value count that doesn't match the column count gets
+                // a teaching note here, *before* dispatch. The engine
+                // would otherwise surface a raw NOT-NULL / type error
+                // that doesn't mention the column-list override.
+                if let Some(note) = crate::input_render::form_b_positional_count_mismatch_note(
+                    &cmd,
+                    &self.schema_cache,
+                ) {
+                    self.push_output(OutputLine {
+                        text: crate::t!("dsl.running", input = input),
+                        kind: OutputKind::Echo,
+                        mode_at_submission: mode,
+                        styled_runs: None,
+                    });
+                    self.note_error(note);
+                    return vec![Action::JournalFailure {
+                        source: input.to_string(),
+                    }];
+                }
                 self.push_output(OutputLine {
                     text: crate::t!("dsl.running", input = input),
                     kind: OutputKind::Echo,
@@ -1405,6 +1426,19 @@ impl App {
                 {
                     self.note_error(note);
                 }
+                // Issue #1 sub-task 2: append a teaching note when the
+                // Form B `insert into <T> values (…)` line failed
+                // because the user supplied more values than the
+                // non-auto-generated columns expect. The parse error
+                // shows the literal "expected `)`"; the note explains
+                // *why* fewer values are expected and shows the
+                // column-list override path.
+                if mode == Mode::Simple
+                    && let Some(note) =
+                        crate::input_render::form_b_extra_values_note(input, &self.schema_cache)
+                {
+                    self.note_error(note);
+                }
                 // ADR-0021 §2: append the usage block (if a
                 // known command-entry keyword was consumed) or
                 // the available-commands fallback (§5).
@@ -2842,15 +2876,293 @@ mod tests {
         );
     }
 
+    /// Helper: install a `Customers(id serial, Name text, Age int,
+    /// SerNo serial)` schema cache on `app` for the Form-B education
+    /// tests (issue #1).
+    fn install_customers_schema_two_serials(app: &mut App) {
+        use crate::completion::TableColumn;
+        use crate::dsl::types::Type;
+        let cols = [
+            ("id", Type::Serial),
+            ("Name", Type::Text),
+            ("Age", Type::Int),
+            ("SerNo", Type::Serial),
+        ];
+        app.schema_cache.tables.push("Customers".to_string());
+        let tc: Vec<TableColumn> = cols
+            .iter()
+            .map(|(n, t)| TableColumn {
+                name: (*n).to_string(),
+                user_type: *t,
+                not_null: false,
+                has_default: false,
+            })
+            .collect();
+        for c in &tc {
+            app.schema_cache.columns.push(c.name.clone());
+        }
+        app.schema_cache
+            .table_columns
+            .insert("Customers".to_string(), tc);
+    }
+
+    #[test]
+    fn simple_mode_submit_form_b_extra_value_shows_only_one_advice_line() {
+        // Issue #1 sub-task 2 + sub-task 1 interaction: in the
+        // 3-column Form B case (`Customers(id serial, Name, Email)` +
+        // 3 values, e.g. `insert into Customers values (1, 'Alice',
+        // 'a@b.c')`) the line IS valid in advanced mode, so the
+        // cross-mode pointer fires. The sub-task 2 teaching note
+        // ("list every column") would be parallel advice — both are
+        // valid escape hatches — and showing both clutters the error.
+        // The teaching note must defer to the cross-mode pointer.
+        use crate::completion::TableColumn;
+        use crate::dsl::types::Type;
+        let mut app = App::new();
+        let cols = [
+            ("id", Type::Serial),
+            ("Name", Type::Text),
+            ("Email", Type::Text),
+        ];
+        app.schema_cache.tables.push("Customers".to_string());
+        let tc: Vec<TableColumn> = cols
+            .iter()
+            .map(|(n, t)| TableColumn {
+                name: (*n).to_string(),
+                user_type: *t,
+                not_null: false,
+                has_default: false,
+            })
+            .collect();
+        for c in &tc {
+            app.schema_cache.columns.push(c.name.clone());
+        }
+        app.schema_cache
+            .table_columns
+            .insert("Customers".to_string(), tc);
+        type_str(
+            &mut app,
+            "insert into Customers values (1, 'Alice', 'a@b.c')",
+        );
+        let _ = submit(&mut app);
+        let out = error_lines(&app);
+        // The cross-mode pointer (sub-task 1) fires — the line works
+        // in advanced. Substring "mode advanced" is the durable
+        // actionable fragment.
+        assert!(
+            out.contains("mode advanced"),
+            "cross-mode pointer must fire for the 3-col line: {out}",
+        );
+        // The sub-task 2 teaching note is suppressed: no "list every
+        // column" / "auto-generated and filled" prose alongside it.
+        assert!(
+            !out.contains("auto-generated and filled"),
+            "sub-task 2 note must defer to the cross-mode pointer: {out}",
+        );
+    }
+
+    #[test]
+    fn advanced_mode_submit_of_form_b_value_count_mismatch_shows_preflight_note() {
+        // Issue #1 sub-task 3: advanced-mode positional `INSERT INTO T
+        // VALUES (…)` (no column list) requires every column. When the
+        // value count doesn't match, today's flow lets the engine
+        // produce a raw constraint or type error; we'd rather catch it
+        // at dispatch time and surface a teaching note that names the
+        // table's columns and shows the column-list override.
+        let mut app = App::new();
+        install_customers_schema_two_serials(&mut app);
+        app.mode = Mode::Advanced;
+        type_str(&mut app, "insert into Customers values ('Oli', 52, 3)");
+        let actions = submit(&mut app);
+        // The pre-flight rejected the line — no ExecuteDsl dispatch.
+        assert!(
+            !actions
+                .iter()
+                .any(|a| matches!(a, Action::ExecuteDsl { .. })),
+            "advanced-mode pre-flight must suppress dispatch on Form-B count mismatch; got: {actions:?}",
+        );
+        let out = error_lines(&app);
+        // The teaching note names the rule …
+        assert!(
+            out.contains("every column"),
+            "missing the positional-VALUES rule in: {out}",
+        );
+        // … names the table's columns so the user can see what's needed …
+        assert!(
+            out.contains("Name") && out.contains("Age") && out.contains("id") && out.contains("SerNo"),
+            "missing the column-name list in: {out}",
+        );
+        // … and shows the column-list override targeting the non-auto columns.
+        assert!(
+            out.contains("insert into Customers (Name, Age)"),
+            "missing the column-list override example in: {out}",
+        );
+    }
+
+    #[test]
+    fn simple_mode_submit_of_form_b_extra_value_teaches_serial_skip() {
+        // Issue #1 sub-task 2: when the user supplies too many positional
+        // values in simple-mode Form B, the bare "expected `)`" parse
+        // error doesn't explain why fewer values are expected. The
+        // submit error gets a teaching line that names the columns
+        // Form B fills automatically, names the columns it expects
+        // values for, and points at the column-list (Form A) override.
+        let mut app = App::new();
+        install_customers_schema_two_serials(&mut app);
+        type_str(&mut app, "insert into Customers values ('Oli', 52, 3)");
+        let _ = submit(&mut app);
+        let out = error_lines(&app);
+        // The teaching line names the user-supplied columns …
+        assert!(out.contains("Name") && out.contains("Age"), "missing non-auto column names in: {out}");
+        // … the auto-generated columns …
+        assert!(out.contains("id") && out.contains("SerNo"), "missing auto column names in: {out}");
+        // … signals the contract …
+        assert!(
+            out.contains("auto-generated"),
+            "missing the contract word in: {out}",
+        );
+        // … and shows the Form-A override path with every column listed.
+        assert!(
+            out.contains("insert into Customers (id, Name, Age, SerNo)"),
+            "missing the Form-A override example in: {out}",
+        );
+        // Issue #1 sub-task 1 gate: the cross-mode pointer must be
+        // suppressed for the user's reported case (count mismatches in
+        // advanced too — switching modes wouldn't help). Without this
+        // assertion, a regression of the gate would silently restore
+        // the misleading pointer alongside the teaching note.
+        assert!(
+            !out.contains("mode advanced"),
+            "cross-mode pointer must NOT fire for the 4-col mismatch case: {out}",
+        );
+    }
+
+    #[test]
+    fn simple_mode_submit_of_form_b_undersupply_teaches() {
+        // Issue #1 siblings task: simple-mode under-supply
+        // (`insert into Customers values ('Oli')` for a 4-col table
+        // whose Form B expects 2 values for `Name`, `Age`). Today the
+        // user sees a bare parse error; with the extended teaching
+        // note they get the same forward-looking explanation as the
+        // over-supply case — what's expected, what's auto-filled, how
+        // to use the column-list form to override.
+        let mut app = App::new();
+        install_customers_schema_two_serials(&mut app);
+        type_str(&mut app, "insert into Customers values ('Oli')");
+        let _ = submit(&mut app);
+        let out = error_lines(&app);
+        assert!(
+            out.contains("Name") && out.contains("Age"),
+            "missing non-auto column names in: {out}",
+        );
+        assert!(
+            out.contains("id") && out.contains("SerNo"),
+            "missing auto column names in: {out}",
+        );
+        assert!(
+            out.contains("auto-generated"),
+            "missing contract word in: {out}",
+        );
+        assert!(
+            out.contains("insert into Customers (id, Name, Age, SerNo)"),
+            "missing column-list override in: {out}",
+        );
+    }
+
+    #[test]
+    fn simple_mode_submit_of_form_b_oversupply_beyond_total_teaches() {
+        // Issue #1 siblings task: simple-mode over-supply *beyond* the
+        // total column count (5 values for a 4-col table). The
+        // teaching note still fires — the explanation of Form B's
+        // contract applies regardless of how far past Form B's count
+        // the user went.
+        let mut app = App::new();
+        install_customers_schema_two_serials(&mut app);
+        type_str(
+            &mut app,
+            "insert into Customers values ('Oli', 52, 3, 13, 99)",
+        );
+        let _ = submit(&mut app);
+        let out = error_lines(&app);
+        assert!(
+            out.contains("Name") && out.contains("Age"),
+            "missing non-auto column names in: {out}",
+        );
+        assert!(
+            out.contains("auto-generated"),
+            "missing contract word in: {out}",
+        );
+        assert!(
+            out.contains("insert into Customers (id, Name, Age, SerNo)"),
+            "missing column-list override in: {out}",
+        );
+    }
+
+    #[test]
+    fn advanced_mode_submit_with_all_values_for_serials_succeeds_no_preflight() {
+        // Issue #1 — the user explicitly confirmed that supplying every
+        // column including the serials works in advanced mode
+        // (`insert into Customers values (13, 'Oli', 42, 13)`). The
+        // pre-flight must not interfere with that happy path: it fires
+        // only on count mismatch, and the dispatch reaches the worker
+        // normally. This locks down the bottom edge of the pre-flight
+        // gate.
+        let mut app = App::new();
+        install_customers_schema_two_serials(&mut app);
+        app.mode = Mode::Advanced;
+        type_str(
+            &mut app,
+            "insert into Customers values (13, 'Oli', 42, 13)",
+        );
+        let actions = submit(&mut app);
+        assert!(
+            actions
+                .iter()
+                .any(|a| matches!(a, Action::ExecuteDsl { .. })),
+            "the line must dispatch normally; pre-flight must not fire when value count matches column count; got: {actions:?}",
+        );
+        // And no teaching note prose appears in the output …
+        let out = error_lines(&app);
+        assert!(
+            !out.contains("requires a value for every column"),
+            "pre-flight must stay silent when counts match: {out}",
+        );
+    }
+
     #[test]
     fn simple_mode_submit_of_sql_construct_appends_advanced_pointer() {
-        // ADR-0033 Amendment 3: submitting a line in simple mode that
-        // fails as DSL but would run as SQL in advanced mode appends
-        // the `advanced_mode.also_valid_sql` pointer to the parse
-        // error — keeping the DSL detail and pointing at advanced
-        // mode. Multi-row VALUES is a definite DSL error and valid SQL
-        // (no schema needed).
+        // ADR-0033 Amendment 3 (+ Amendment 5): submitting a line in
+        // simple mode that fails as DSL but would be valid in advanced
+        // mode appends the `advanced_mode.also_valid_sql` pointer to
+        // the parse error — keeping the DSL detail and pointing at
+        // advanced mode. Multi-row VALUES is a definite DSL error and
+        // valid SQL with a real schema (the validity verdict needs the
+        // table to exist; an unknown-table diagnostic would correctly
+        // suppress the pointer).
+        use crate::completion::TableColumn;
+        use crate::dsl::types::Type;
         let mut app = App::new();
+        app.schema_cache.tables.push("T".to_string());
+        let tc = vec![
+            TableColumn {
+                name: "a".to_string(),
+                user_type: Type::Int,
+                not_null: false,
+                has_default: false,
+            },
+            TableColumn {
+                name: "b".to_string(),
+                user_type: Type::Int,
+                not_null: false,
+                has_default: false,
+            },
+        ];
+        for c in &tc {
+            app.schema_cache.columns.push(c.name.clone());
+        }
+        app.schema_cache
+            .table_columns
+            .insert("T".to_string(), tc);
         type_str(&mut app, "insert into T values (1, 2), (3, 4)");
         let actions = submit(&mut app);
         assert!(
@@ -2860,7 +3172,7 @@ mod tests {
         let has_pointer = app
             .output
             .iter()
-            .any(|l| l.kind == OutputKind::Error && l.text.contains("advanced mode"));
+            .any(|l| l.kind == OutputKind::Error && l.text.contains("mode advanced"));
         assert!(
             has_pointer,
             "expected the advanced-mode pointer on submit; output:\n{}",
@@ -2876,10 +3188,15 @@ mod tests {
         let mut app = App::new();
         type_str(&mut app, "frobulate widgets");
         let _ = submit(&mut app);
+        // The pointer's current phrasing (`also_valid_sql`) is
+        // "trying to write SQL? …"; an unknown command produces no
+        // advanced-mode hint at all, so we look for any line carrying
+        // the "mode advanced" actionable fragment that the pointer
+        // always emits.
         let has_pointer = app
             .output
             .iter()
-            .any(|l| l.text.contains("valid as SQL in advanced mode"));
+            .any(|l| l.text.contains("mode advanced"));
         assert!(!has_pointer, "unknown command must not point at advanced mode");
     }
 

src/dsl/walker/mod.rs

@@ -1397,11 +1397,12 @@ fn dml_auto_column_diagnostics(
     diagnostics
 }
 
-/// `insert_arity_mismatch` ERROR (ADR-0033 §8.1, sub-phase 3i).
+/// `insert_arity_mismatch` ERROR (ADR-0033 §8.1, sub-phase 3i; Form B
+/// branch added 2026-05-28 per issue #1 / ADR-0033 Amendment 5).
 ///
-/// Walker pre-flight when the explicit `(column_name_list)` arity
-/// disagrees with a row's arity — pre-empting the engine's
-/// less-helpful "N values for M columns". Two row-source shapes:
+/// Walker pre-flight when the value-tuple arity disagrees with the
+/// expected arity — pre-empting the engine's less-helpful
+/// "N values for M columns". Two row-source shapes:
 ///
 /// - **VALUES**: each `value_tuple` is checked independently;
 ///   **each** offending row emits its own diagnostic on that tuple's
@@ -1412,10 +1413,17 @@ fn dml_auto_column_diagnostics(
 ///   projection isn't the first `select` token) — the engine still
 ///   reports it; a false positive would be worse than deferring.
 ///
-/// Only fires when an explicit column list is present; the
-/// no-column-list form (arity vs the table's full column count)
-/// is deferred (needs the schema and is outside the 3i exit gate).
-fn dml_insert_arity_diagnostics(path: &MatchedPath) -> Vec<outcome::Diagnostic> {
+/// Expected arity comes from one of two sources:
+/// - **Form A** (explicit `(col, …)` list): the list's length.
+/// - **Form B** (no column list): the target table's column count —
+///   requires the schema and a known table; otherwise this pass is
+///   silent and the engine reports the mismatch as before. This
+///   covers the user-reported issue #1 case (advanced positional
+///   INSERT with wrong value count).
+fn dml_insert_arity_diagnostics(
+    path: &MatchedPath,
+    schema: Option<&crate::completion::SchemaCache>,
+) -> Vec<outcome::Diagnostic> {
     use crate::dsl::grammar::IdentSource;
     use outcome::{Diagnostic, MatchedKind, Severity};
 
@@ -1432,9 +1440,36 @@ fn dml_insert_arity_diagnostics(path: &MatchedPath) -> Vec<outcome::Diagnostic>
             )
         })
         .count();
-    if col_arity == 0 {
-        return Vec::new();
-    }
+
+    // Resolve the expected arity + which message template to use.
+    // Form A: explicit column list → its own length.
+    // Form B: no list → the target table's column count, *if* we know
+    // it. Without a schema or a recognised target the pass goes
+    // silent (the unknown-table case is flagged by the schema-
+    // existence pass instead).
+    let (expected, message_key): (usize, &'static str) = if col_arity > 0 {
+        (col_arity, "diagnostic.insert_arity_mismatch")
+    } else {
+        let Some(schema) = schema else {
+            return Vec::new();
+        };
+        let Some(target) = path.items.iter().find_map(|it| match it.kind {
+            MatchedKind::Ident {
+                source: IdentSource::Tables,
+                role: "insert_target_table",
+            } => Some(it.text.as_str()),
+            _ => None,
+        }) else {
+            return Vec::new();
+        };
+        let Some(cols) = schema.table_columns.get(target) else {
+            return Vec::new();
+        };
+        if cols.is_empty() {
+            return Vec::new();
+        }
+        (cols.len(), "diagnostic.insert_arity_mismatch_form_b")
+    };
 
     // Index of the row-source keyword (first VALUES / SELECT / WITH).
     let Some(kw_idx) = path
@@ -1456,9 +1491,9 @@ fn dml_insert_arity_diagnostics(path: &MatchedPath) -> Vec<outcome::Diagnostic>
             severity: Severity::Error,
             span,
             message: crate::friendly::translate(
-                "diagnostic.insert_arity_mismatch",
+                message_key,
                 &[
-                    ("expected", &col_arity as &dyn std::fmt::Display),
+                    ("expected", &expected as &dyn std::fmt::Display),
                     ("actual", &actual as &dyn std::fmt::Display),
                 ],
             ),
@@ -1483,7 +1518,7 @@ fn dml_insert_arity_diagnostics(path: &MatchedPath) -> Vec<outcome::Diagnostic>
                 }
                 MatchedKind::Punct(')') => {
                     depth -= 1;
-                    if depth == 0 && tuple_arity != col_arity {
+                    if depth == 0 && tuple_arity != expected {
                         emit((tuple_start, it.span.1), tuple_arity, &mut diagnostics);
                     }
                 }
@@ -1522,7 +1557,7 @@ fn dml_insert_arity_diagnostics(path: &MatchedPath) -> Vec<outcome::Diagnostic>
                 }
             }
         }
-        if proj_arity != col_arity {
+        if proj_arity != expected {
             emit(anchor.unwrap_or(path.items[kw_idx].span), proj_arity, &mut diagnostics);
         }
     }
@@ -2483,10 +2518,13 @@ fn decide(
             // (ADR-0033 Amendment 3). "This is SQL" is reserved for
             // entry words with no DSL form (`select` / `with`): there
             // the DSL surface has nothing to offer. For a DSL line
-            // that fails here but *would* run in advanced mode, a
-            // "(valid as SQL in advanced mode)" pointer is appended at
-            // the rendering layer (see `advanced_alternative_note`),
-            // combining the DSL fix with the mode hint.
+            // that fails here but would be *valid* in advanced mode (the
+            // ADR-0027 sense, per ADR-0033 Amendment 5: verdict `None`,
+            // i.e. parse succeeds + no Warning/Error from any
+            // diagnostic pass), a "Trying to write SQL?" pointer is
+            // appended at the rendering layer (see
+            // `advanced_alternative_note`), combining the DSL fix with
+            // the mode hint.
             match simple.first() {
                 Some(&(sidx, snode)) => Decision::Commit { idx: sidx, node: snode },
                 None => {
@@ -2768,10 +2806,12 @@ fn walk_one_command<'a>(
         // ADR-0033 §8.2 — WARNING when a SQL INSERT lists a
         // serial/shortid (auto-generated) column explicitly.
         d.extend(dml_auto_column_diagnostics(&path, ctx.schema));
-        // ADR-0033 §8.1 — ERROR when a column list's arity disagrees
-        // with a VALUES tuple (per row) or the INSERT…SELECT
-        // projection.
-        d.extend(dml_insert_arity_diagnostics(&path));
+        // ADR-0033 §8.1 (+ Amendment 5, issue #1) — ERROR when the
+        // arity disagrees with a VALUES tuple (per row) or the
+        // INSERT…SELECT projection. Form A uses the column list's
+        // length; Form B uses the schema's column count for the
+        // target table.
+        d.extend(dml_insert_arity_diagnostics(&path, ctx.schema));
         // ADR-0033 §8.3 — WARNING when an INSERT's column list omits
         // a NOT-NULL-no-default (non-auto-gen) column.
         d.extend(dml_not_null_missing_diagnostics(&path, ctx.schema));
@@ -5019,6 +5059,96 @@ mod tests {
         );
     }
 
+    #[test]
+    fn insert_form_b_arity_mismatch_under_supply_fires() {
+        // Issue #1: advanced-mode positional INSERT without a column
+        // list requires a value for every column. Three values for a
+        // 4-column table (the user's reported bug case) is a
+        // mismatch — the diagnostic powers the validity verdict that
+        // drives the [ERR] indicator and ADR-0033 Amendment 5's
+        // `also_valid_sql` gate.
+        let schema = schema_with(
+            "Customers",
+            &[
+                ("id", Type::Serial),
+                ("Name", Type::Text),
+                ("Age", Type::Int),
+                ("SerNo", Type::Serial),
+            ],
+        );
+        let diags = diag_keys(
+            "insert into Customers values ('Oli', 52, 3)",
+            &schema,
+        );
+        assert!(
+            diags.iter().any(|d| d.contains("value(s) are given")),
+            "Form B under-supply must fire arity diagnostic; got {diags:?}",
+        );
+    }
+
+    #[test]
+    fn insert_form_b_arity_mismatch_over_supply_fires() {
+        // Symmetric case: more values than columns — engine would
+        // reject; the diagnostic catches it pre-flight.
+        let schema = schema_with(
+            "Customers",
+            &[
+                ("id", Type::Serial),
+                ("Name", Type::Text),
+                ("Age", Type::Int),
+                ("SerNo", Type::Serial),
+            ],
+        );
+        let diags = diag_keys(
+            "insert into Customers values ('Oli', 52, 3, 13, 99)",
+            &schema,
+        );
+        assert!(
+            diags.iter().any(|d| d.contains("value(s) are given")),
+            "Form B over-supply must fire arity diagnostic; got {diags:?}",
+        );
+    }
+
+    #[test]
+    fn insert_form_b_arity_match_is_silent() {
+        // The user's confirmed happy path: every column supplied
+        // positionally (autos included) — no arity diagnostic.
+        let schema = schema_with(
+            "Customers",
+            &[
+                ("id", Type::Serial),
+                ("Name", Type::Text),
+                ("Age", Type::Int),
+                ("SerNo", Type::Serial),
+            ],
+        );
+        let diags = diag_keys(
+            "insert into Customers values (13, 'Oli', 42, 13)",
+            &schema,
+        );
+        assert!(
+            !diags.iter().any(|d| d.contains("value(s) are given")),
+            "matched Form B arity must not fire; got {diags:?}",
+        );
+    }
+
+    #[test]
+    fn insert_form_b_arity_unknown_table_is_silent() {
+        // Defensive: when the target table isn't in the schema cache,
+        // we can't know the expected count — defer to the engine
+        // (the schema-existence pass flags the unknown table, not the
+        // arity pass).
+        let schema = schema_with("Customers", &[("Name", Type::Text)]);
+        let diags = diag_keys(
+            "insert into Strangers values ('Oli', 52, 3)",
+            &schema,
+        );
+        assert!(
+            !diags.iter().any(|d| d.contains("value(s) are given")),
+            "unknown table must not trigger an arity diagnostic; got {diags:?}",
+        );
+    }
+
     #[test]
     fn insert_arity_match_is_silent() {
         let schema = schema_with("t", &[("a", Type::Int), ("b", Type::Int)]);
@@ -6211,8 +6341,10 @@ mod dispatch_3a_tests {
         // DSL candidate, even when the input matches only the SQL
         // tail. The DSL grammar then rejects the SQL-only tail with a
         // normal parse error (a `Mismatch`), surfacing the actionable
-        // DSL detail; the "(valid as SQL in advanced mode)" pointer is
-        // added at the rendering layer, not here. "This is SQL" as a
+        // DSL detail; the "Trying to write SQL?" pointer (ADR-0033
+        // Amendment 3, gated per Amendment 5 on the line being *valid*
+        // in advanced mode — verdict `None`) is added at the rendering
+        // layer, not here. "This is SQL" as a
         // dispatch outcome is reserved for entry words with no DSL
         // form (see `simple_mode_sql_only_entry_word_is_this_is_sql`).
         let cands = shared();

src/friendly/keys.rs

@@ -45,6 +45,12 @@ pub const KEYS_AND_PLACEHOLDERS: &[(&str, &[&str])] = &[
     ("diagnostic.duplicate_cte", &["name"]),
     ("diagnostic.eq_null", &[]),
     ("diagnostic.insert_arity_mismatch", &["expected", "actual"]),
+    // ADR-0033 §8.1 / Amendment 5: Form B (no column list) variant.
+    // Cited from issue #1 — every column must be supplied positionally.
+    (
+        "diagnostic.insert_arity_mismatch_form_b",
+        &["expected", "actual"],
+    ),
     ("diagnostic.not_null_missing", &["column"]),
     ("diagnostic.like_numeric", &["column", "type"]),
     ("diagnostic.projection_alias_misplaced", &["alias", "clause"]),
@@ -339,6 +345,20 @@ pub const KEYS_AND_PLACEHOLDERS: &[(&str, &[&str])] = &[
     // ---- Advanced-mode SQL surface (ADR-0030) ----
     ("advanced_mode.sql_in_simple", &["command"]),
     ("advanced_mode.also_valid_sql", &[]),
+    // Education note appended to a simple-mode INSERT Form B
+    // parse error when the user supplied more values than the
+    // non-auto-generated columns expect (issue #1 sub-task 2).
+    (
+        "insert.form_b_extra_values_note",
+        &["table", "expected_phrase", "auto_phrase", "all_cols"],
+    ),
+    // Pre-flight teaching note for advanced-mode positional
+    // `INSERT INTO T VALUES (…)` (no column list) when the value
+    // count doesn't match the column count (issue #1 sub-task 3).
+    (
+        "insert.form_b_positional_count_mismatch_note",
+        &["table", "col_count", "col_list", "supplied", "non_auto_csv"],
+    ),
     ("select.internal_table", &["table"]),
     (
         "cli.invalid_value",

src/friendly/strings/en-US.yaml

@@ -573,6 +573,8 @@ diagnostic:
   # ADR-0033 §8 — Phase-3 DML diagnostic keys.
   auto_column_overridden: "column `{column}` is auto-generated (`{type}`); providing an explicit value bypasses the auto-counter and may collide with later auto-generated values"
   insert_arity_mismatch: "the column list names {expected} column(s) but {actual} value(s) are given"
+  # ADR-0033 §8.1 / Amendment 5: Form B (no column list) variant.
+  insert_arity_mismatch_form_b: "with no column list, all {expected} column(s) need a value but {actual} value(s) are given"
   not_null_missing: "column `{column}` is required (`NOT NULL`, no default); the statement will fail when run"
 
 # Engine-error translations: an engine-rejected SQL statement
@@ -705,8 +707,22 @@ advanced_mode:
   sql_in_simple: "`{command}` is SQL — available in advanced mode. Switch with `mode advanced`, or prefix the line with `:` to run it once."
   # Appended to a simple-mode DSL error when the same line would run
   # in advanced mode — keeps the actionable DSL fix and adds the mode
-  # pointer (ADR-0033 Amendment 3).
-  also_valid_sql: "(valid as SQL in advanced mode — `mode advanced` or prefix `:`)"
+  # pointer (ADR-0033 Amendment 3). Suppressed by `advanced_alternative_note`
+  # for cases the advanced engine would also reject (issue #1).
+  also_valid_sql: "(trying to write SQL? switch with `mode advanced`, or prefix `:` to run once)"
+
+# ---- Insert education hints (issue #1 sub-task 2) -------------------
+# Appended to a simple-mode INSERT Form B parse error when the user
+# supplied more values than Form B's non-auto-generated columns expect
+# (but not more than every column). Teaches the contract that excludes
+# `serial` / `shortid` columns and points at the column-list form.
+insert:
+  form_b_extra_values_note: "`insert into {table} values (…)` expects {expected_phrase} — {auto_phrase}. To set them explicitly, list every column: `insert into {table} ({all_cols}) values (…)`."
+  # Pre-flight teaching note for advanced-mode positional
+  # `INSERT INTO T VALUES (…)` (no column list) when the value count
+  # doesn't match the column count (issue #1 sub-task 3). The override
+  # uses the non-auto columns so the user can omit serial/shortid.
+  form_b_positional_count_mismatch_note: "Positional `insert into {table} values (…)` requires a value for every column. `{table}` has {col_count} columns ({col_list}); you supplied {supplied}. To omit auto-generated columns, list the columns you want: `insert into {table} ({non_auto_csv}) values (…)`."
 
 # ---- SQL SELECT (advanced mode; ADR-0030 / ADR-0031) ----------------
 select:

src/input_render.rs

@@ -300,11 +300,24 @@ pub fn ambient_hint_in_mode(
 /// The `advanced_mode.also_valid_sql` pointer string, or `None`.
 ///
 /// Returns the pointer when a simple-mode line is a *definite* DSL
-/// error (not merely incomplete) yet parses in advanced mode. Used to
-/// combine the DSL fix with the mode hint — both while typing
-/// (`ambient_hint_in_mode`) and on submit (`App::dispatch_dsl`) — so
-/// the pointer reaches SQL constructs that surface only on submit,
-/// e.g. `delete … returning` (ADR-0033 Amendment 3).
+/// error (not merely incomplete) yet would be **valid** in advanced
+/// mode (ADR-0033 Amendment 5).
+///
+/// "Valid" is the ADR-0027 sense: the advanced-mode input-validity
+/// verdict comes back as `None` (no Warning, no Error) after every
+/// static check — parse, schema existence, type slots, INSERT arity,
+/// predicate warnings, and any future addition. The pointer fires only
+/// when switching modes is **actually** the next step the user can
+/// take to make the line valid: a `Severity::Warning` or
+/// `Severity::Error` from the advanced-mode pipeline means switching
+/// wouldn't resolve the line, so the pointer would mislead.
+///
+/// Issue #1 origin: previously the gate was a syntactic "would parse"
+/// check, which fired for the user's reported case (4-col table,
+/// 3 positional values) where the line parses but fails at the engine.
+/// Now the gate reads `input_verdict_in_mode` so any static
+/// rejection — including the Form B arity diagnostic added in this
+/// same change (issue #1) — suppresses the pointer automatically.
 #[must_use]
 pub fn advanced_alternative_note(
     input: &str,
@@ -317,10 +330,228 @@ pub fn advanced_alternative_note(
     if !definite_dsl_error {
         return None;
     }
-    if parse_command_with_schema_in_mode(input, cache, Mode::Advanced).is_ok() {
-        Some(crate::t!("advanced_mode.also_valid_sql"))
+    // The validity-verdict-driven gate (ADR-0033 Amendment 5): the
+    // line must be fully valid (verdict `None`) in advanced mode.
+    if crate::dsl::walker::input_verdict_in_mode(input, Some(cache), Mode::Advanced).is_some()
+    {
+        return None;
+    }
+    Some(crate::t!("advanced_mode.also_valid_sql"))
+}
+
+/// Education note for the simple-mode INSERT Form B count-mismatch
+/// case (issue #1 sub-task 2).
+///
+/// When a simple-mode `insert into <T> values (…)` (Form B) supplies
+/// more values than the non-auto-generated columns of `<T>` — but no
+/// more than every column — the bare "expected `)`" parse error
+/// doesn't explain the contract that excluded the serial / shortid
+/// columns. This helper returns a note that names the columns Form B
+/// expects values for, names the auto-generated ones it skips, and
+/// shows the column-list (Form A) override.
+///
+/// Returns `None` when the input doesn't match the pattern (e.g. the
+/// advanced parse fails, the schema isn't known, the table has no
+/// auto-generated columns, the value count is at or below the non-auto
+/// count, or the value count exceeds the total column count — which is
+/// a different error class the engine surfaces directly).
+///
+/// Also `None` when the cross-mode `advanced_alternative_note` pointer
+/// would fire for the same input: those two pieces of advice overlap
+/// (both are escape hatches from the Form-B mismatch — one to advanced
+/// mode, one to Form A) and showing both would clutter the error
+/// without adding pedagogy. The cross-mode pointer wins because it
+/// only fires when switching modes actually works (issue #1 sub-task
+/// 1's gate); when it doesn't fire, this note steps in.
+#[must_use]
+pub fn form_b_extra_values_note(
+    input: &str,
+    cache: &crate::completion::SchemaCache,
+) -> Option<String> {
+    use crate::dsl::command::Command;
+    use crate::dsl::types::Type;
+    if advanced_alternative_note(input, cache).is_some() {
+        return None;
+    }
+    let parsed = parse_command_with_schema_in_mode(input, cache, Mode::Advanced).ok()?;
+    let Command::SqlInsert {
+        target_table,
+        listed_columns,
+        literal_rows,
+        ..
+    } = parsed
+    else {
+        return None;
+    };
+    if !listed_columns.is_empty() || literal_rows.is_empty() {
+        return None;
+    }
+    let table_cols = cache.table_columns.get(&target_table)?;
+    let is_auto = |t: Type| matches!(t, Type::Serial | Type::ShortId);
+    let auto: Vec<&str> = table_cols
+        .iter()
+        .filter(|c| is_auto(c.user_type))
+        .map(|c| c.name.as_str())
+        .collect();
+    if auto.is_empty() {
+        return None;
+    }
+    let non_auto: Vec<&str> = table_cols
+        .iter()
+        .filter(|c| !is_auto(c.user_type))
+        .map(|c| c.name.as_str())
+        .collect();
+    // Defence in depth: a table that is all-auto has no non-auto
+    // column to talk about. The cross-mode-pointer gate above would
+    // normally shield us (the line works in advanced — the pointer
+    // fires and we return early), but the helper is `pub` and should
+    // not produce "expects 0 values for " on its own.
+    if non_auto.is_empty() {
+        return None;
+    }
+    // Fire whenever the supplied count differs from Form B's expected
+    // count — the teaching message is forward-looking (it states what
+    // Form B expects + the override path) so it works for under-supply,
+    // over-supply within the column range, and over-supply past the
+    // total column count alike (issue #1 siblings task — over- /
+    // under-supply previously fell through to the bare parse error).
+    let value_count = literal_rows[0].len();
+    if value_count == non_auto.len() {
+        return None;
+    }
+    let expected_phrase = if non_auto.len() == 1 {
+        format!("1 value for {}", quote_join_and(&non_auto))
     } else {
-        None
+        format!(
+            "{count} values for {names}",
+            count = non_auto.len(),
+            names = quote_join_and(&non_auto),
+        )
+    };
+    let auto_phrase = if auto.len() == 1 {
+        format!(
+            "{name} is auto-generated and filled automatically",
+            name = quote_join_and(&auto),
+        )
+    } else {
+        format!(
+            "{names} are auto-generated and filled automatically",
+            names = quote_join_and(&auto),
+        )
+    };
+    let all_cols = table_cols
+        .iter()
+        .map(|c| c.name.as_str())
+        .collect::<Vec<_>>()
+        .join(", ");
+    Some(crate::t!(
+        "insert.form_b_extra_values_note",
+        table = target_table,
+        expected_phrase = expected_phrase,
+        auto_phrase = auto_phrase,
+        all_cols = all_cols,
+    ))
+}
+
+/// Pre-flight note for advanced-mode `insert into <T> values (…)`
+/// (positional, no column list) when the value count doesn't match
+/// the table's column count (issue #1 sub-task 3).
+///
+/// The advanced-mode SQL grammar accepts any positional value count;
+/// the engine then rejects the line with a NOT-NULL / type-mismatch
+/// error that doesn't tell the user about the column-list override.
+/// This helper detects the case at dispatch time and returns a note
+/// that names the rule, lists the target table's columns, and shows
+/// the column-list (Form A) override.
+///
+/// Returns `None` when the input doesn't match the pattern (the parse
+/// isn't a Form B `SqlInsert`, the schema isn't known, the table has
+/// no auto-generated columns or no non-auto columns, the literal-row
+/// shape is empty, or every row's value count already matches the
+/// column count).
+///
+/// Conservative on multi-row VALUES: fires only when **every** row's
+/// value count is the same wrong number. Mixed-length rows fall
+/// through to the engine error — they're a different shape of mistake.
+#[must_use]
+pub fn form_b_positional_count_mismatch_note(
+    parsed: &crate::dsl::command::Command,
+    cache: &crate::completion::SchemaCache,
+) -> Option<String> {
+    use crate::dsl::command::Command;
+    use crate::dsl::types::Type;
+    let Command::SqlInsert {
+        target_table,
+        listed_columns,
+        literal_rows,
+        ..
+    } = parsed
+    else {
+        return None;
+    };
+    if !listed_columns.is_empty() || literal_rows.is_empty() {
+        return None;
+    }
+    let table_cols = cache.table_columns.get(target_table)?;
+    let col_count = table_cols.len();
+    let row_lens: Vec<usize> = literal_rows.iter().map(Vec::len).collect();
+    // Only fire when every row is the same (wrong) length.
+    let first_len = row_lens[0];
+    if !row_lens.iter().all(|n| *n == first_len) {
+        return None;
+    }
+    if first_len == col_count {
+        return None;
+    }
+    let is_auto = |t: Type| matches!(t, Type::Serial | Type::ShortId);
+    // The override only makes sense when (a) there's something to
+    // skip and (b) something to list. A table that is all-auto can't
+    // omit anything via the column list; a table with no autos
+    // doesn't benefit from the column-list form for this purpose.
+    let has_auto = table_cols.iter().any(|c| is_auto(c.user_type));
+    if !has_auto {
+        return None;
+    }
+    let non_auto: Vec<&str> = table_cols
+        .iter()
+        .filter(|c| !is_auto(c.user_type))
+        .map(|c| c.name.as_str())
+        .collect();
+    if non_auto.is_empty() {
+        return None;
+    }
+    let all_cols_list = quote_join_and(
+        &table_cols
+            .iter()
+            .map(|c| c.name.as_str())
+            .collect::<Vec<_>>(),
+    );
+    let non_auto_csv = non_auto.join(", ");
+    Some(crate::t!(
+        "insert.form_b_positional_count_mismatch_note",
+        table = target_table,
+        col_count = col_count,
+        col_list = all_cols_list,
+        supplied = first_len,
+        non_auto_csv = non_auto_csv,
+    ))
+}
+
+/// Format `items` as an English-prose list with backtick-quoted
+/// identifiers: `["a"]` → `` `a` ``, `["a","b"]` → `` `a` and `b` ``,
+/// `["a","b","c"]` → `` `a`, `b`, and `c` `` (Oxford comma).
+fn quote_join_and(items: &[&str]) -> String {
+    match items {
+        [] => String::new(),
+        [only] => format!("`{only}`"),
+        [a, b] => format!("`{a}` and `{b}`"),
+        rest => {
+            let head: Vec<String> = rest[..rest.len() - 1]
+                .iter()
+                .map(|s| format!("`{s}`"))
+                .collect();
+            format!("{}, and `{}`", head.join(", "), rest[rest.len() - 1])
+        }
     }
 }
 
@@ -1124,8 +1355,10 @@ mod tests {
                 // The DSL detail survives …
                 assert!(p.contains("Name"), "expected DSL slot detail, got: {p:?}");
                 // … and the advanced-mode pointer is appended.
+                // Substring "mode advanced" is the actionable fragment
+                // (the switch command) that survives wording revisions.
                 assert!(
-                    p.contains("advanced mode"),
+                    p.contains("mode advanced"),
                     "expected the advanced-mode pointer, got: {p:?}",
                 );
             }
@@ -1145,12 +1378,40 @@ mod tests {
         let input = "insert into Customers values ('Alice')";
         if let Some(AmbientHint::Prose(p)) = ambient_hint(input, input.len(), None, &cache) {
             assert!(
-                !p.contains("advanced mode"),
+                !p.contains("mode advanced"),
                 "a valid DSL command must not carry the advanced pointer, got: {p:?}",
             );
         }
     }
 
+    #[test]
+    fn ambient_hint_omits_advanced_pointer_when_form_b_value_count_wouldnt_match() {
+        // Issue #1: simple-mode rejects `insert into Customers values
+        // ('Oli', 52, 3)` because Form B skips both serials and expects
+        // 2 values for `Name`, `Age`. The same line ALSO fails in
+        // advanced mode: positional VALUES requires every column (4
+        // total) but only 3 were supplied. The cross-mode pointer would
+        // be misleading — switching modes wouldn't help — so it must
+        // not be appended.
+        use crate::dsl::types::Type;
+        let cache = schema_with_columns(
+            "Customers",
+            &[
+                ("id", Type::Serial),
+                ("Name", Type::Text),
+                ("Age", Type::Int),
+                ("SerNo", Type::Serial),
+            ],
+        );
+        let input = "insert into Customers values ('Oli', 52, 3)";
+        let note = advanced_alternative_note(input, &cache);
+        assert!(
+            note.is_none(),
+            "Form B mismatch where advanced mode would also reject — \
+             the cross-mode pointer must be suppressed; got: {note:?}",
+        );
+    }
+
     #[test]
     fn ambient_hint_at_insert_second_value_shows_text_prose() {
         use crate::dsl::types::Type;