gudusoft.gsqlparser

Class DynamicSqlProofHarness

Object

gudusoft.gsqlparser.DynamicSqlProofHarness

public final class DynamicSqlProofHarness
extends Object

Proof harness for the dynamic-SQL per-edge publication proof (design: docs/designs/sp/dynamic-sql-fragment-provenance-design.md, Layer 2 / phase "R4 step 2").

This class exists in gudusoft.gsqlparser — NOT in dlineage — because the checks need the real pipeline's internals (lexer accumulation state, parser recovery events), which are package-local here. It is hand-written; it never modifies generated lexer/parser files.

Phase status: built, unwired. No product path calls it yet; it is exercised only by its isolation tests. Everything it reports errs on the side of refusal: a false/failed verdict never causes wrong output, only (later, when wired) a smaller published-edge set.

Provided checks (design Layer 2):

1. Boundary lex check — checkLexBoundary(java.lang.String, gudusoft.gsqlparser.EDbVendor): the literal prefix before the first hole must end in a clean lexer state (no unterminated string/comment/bracketed identifier — observed as non-empty literalbuf accumulation and swallowed characters), with balanced paren depth, a fusion-safe boundary character, and (for MSSQL) no line-comment-ambiguous -- on the boundary line (TLexerMssql classifies -- by inspecting the whole current line, so the hole's same-line content could flip it).
2. Proof-mode parse — proofParse(java.lang.String, gudusoft.gsqlparser.EDbVendor): parse with the real pipeline and refuse when the parse needed ANY recovery (TCustomParser.getProofRecoveryEvents()) or produced syntax errors. Silent keyword rollback counts as recovery: a parse that needed it is not evidence.
3. MSSQL rewrite-horizon audit — DynamicSqlProofHarness.MssqlRewriteAudit: the per-rule forward-window facts from the review-round-2 audit, replacing the unsound single global W.

Deliberately NOT here yet (next increments): the differential prefix+EOF probe and the committed-node (parser commitment) check.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	DynamicSqlProofHarness.BoundaryVerdict Verdict of checkLexBoundary(java.lang.String, gudusoft.gsqlparser.EDbVendor); clean == false means the proof must refuse.
static class	DynamicSqlProofHarness.MssqlRewriteAudit Per-rule forward-window audit of the MSSQL pre-parse machinery (review round 2 replaced the unsound single global W with this table).
static class	DynamicSqlProofHarness.ProofParseResult Result of proofParse(java.lang.String, gudusoft.gsqlparser.EDbVendor); ok == false means the proof must refuse.

Method Summary

Modifier and Type	Method and Description
static DynamicSqlProofHarness.BoundaryVerdict	checkLexBoundary(String prefix, EDbVendor vendor) Check that prefix — the literal text before the first hole — is a safe lexical boundary: every character lexed into complete tokens, no open literal/comment/bracket state, balanced parens/brackets, a fusion-safe final character, and no line-comment ambiguity on the boundary line.
static TCustomParser.ProofLrConfiguration	observeLrConfiguration(String sql, long cutoffOffset) Run the REAL MSSQL parser over sql and report the LR automaton's configuration at cutoffOffset — the state stack the literal prefix committed to, plus every reduction performed before that point.
static DynamicSqlProofHarness.ProofParseResult	proofParse(String sql, EDbVendor vendor) Parse sql with the real vendor pipeline and report whether the parse constitutes proof-grade evidence: zero syntax errors AND zero recovery events.

Methods inherited from class Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

checkLexBoundary

public static DynamicSqlProofHarness.BoundaryVerdict checkLexBoundary(String prefix,
                                                                      EDbVendor vendor)

Check that prefix — the literal text before the first hole — is a safe lexical boundary: every character lexed into complete tokens, no open literal/comment/bracket state, balanced parens/brackets, a fusion-safe final character, and no line-comment ambiguity on the boundary line.

proofParse

public static DynamicSqlProofHarness.ProofParseResult proofParse(String sql,
                                                                 EDbVendor vendor)

Parse sql with the real vendor pipeline and report whether the parse constitutes proof-grade evidence: zero syntax errors AND zero recovery events. Recovery includes silently-successful keyword rollback — a statement that only parses because a keyword was retried as an identifier is not instantiation-independent evidence.

observeLrConfiguration

public static TCustomParser.ProofLrConfiguration observeLrConfiguration(String sql,
                                                                        long cutoffOffset)

Run the REAL MSSQL parser over sql and report the LR automaton's configuration at cutoffOffset — the state stack the literal prefix committed to, plus every reduction performed before that point.

This is the observation half of the commitment check (design R4). It answers "what has the grammar actually committed to here?", which is the question two earlier hand-written schemes got wrong: token adjacency (`hasSolidTokenBetween`) and AST binder-region containment. Neither could see a construct the grammar still allows but the sentinel text does not contain — MSSQL's optional UPDATE ... FROM being the witness.

The real parser is used rather than an offline table simulation on purpose: MSSQL rewrites tokens before the automaton runs (TParserMssqlSql.yyparse) and reads the token stream from inside semantic actions, so a simulation would diverge precisely on the constructs those hacks exist for.

Read-only: the parse proceeds exactly as it otherwise would up to the cutoff, then stops without entering error recovery (recovery unwinds the stack we are reading).

Parameters:

sql - the materialized site text

cutoffOffset - stop before consuming any token at or beyond this character offset — normally the first hole's offset, already retreated by the applicable rewrite horizon

Returns:

the configuration, or null if the parser never needed a token at or beyond the cutoff (e.g. the cutoff is past the statement)