Skip to content

KR-6: two-parser equivalence (KRLAdapter.jl ≡ quandledb/server/krl) differential test #24

@hyperpolymath

Description

@hyperpolymath

Source: PROOF-NARRATIVE.md §3 KR-6 (added in PR #23).

Claim

For every input string s, KRLAdapter.jl::parse_krl(s) and quandledb/server/krl/Parser.jl::parse_any(s) either both succeed with equal ASTs or both fail.

Why valuable

Two implementations exist by design — one for end-user code (KRLAdapter.jl, canonical), one for query-time parsing (quandledb/server/krl/, server-side). If they accept different languages, the server can run queries the canonical parser rejects, and vice versa. Soundness regression.

Assumptions

  • [[A-KR-6.1]] Both implementations target the same EBNF grammar (spec/grammar.ebnf v0.1.0).
  • [[A-KR-6.2]] Both implementations share the same Token enumeration: keyword set, identifier shape, integer/string literal shapes.

Acceptance criteria

  • Add KRLAdapter.jl/test/differential_test.jl (or in quandledb/server/krl/test/ — pick one canonical home and cross-reference).
  • Test corpus must include:
    • Every program in krl/examples/*.krl (4 known + any added).
    • Every test input from KRLAdapter.jl/test/parser_test.jl.
    • Every test input from quandledb/server/krl/test/parser_test.jl.
    • Random byte strings (1000 trials, length 1-200, MersenneTwister seed for reproducibility).
  • For each input s:
    r1 = try (true, KRLAdapter.parse_krl(s)) catch e (false, e) end
    r2 = try (true, QuandleDB.KRL.parse_any(s)) catch e (false, e) end
    
    @test r1[1] == r2[1]                              # same success/failure
    if r1[1] && r2[1]
        @test ast_equal(r1[2], r2[2])                 # same AST shape
    end
  • ast_equal helper must canonicalise across the two AST representations (the two implementations have slightly different node types — see KRLAdapter.jl/src/parser/ast.jl vs quandledb/server/krl/Ast.jl). Either pick a common canonical form or define an explicit isomorphism.
  • Failures must report the smallest input that distinguishes the two parsers.

Effort

~1 day. The hard part is the ast_equal canonicaliser; both parsers produce structurally similar but not byte-equal ASTs.

Cross-references

  • PROOF-NARRATIVE.md §3 KR-6
  • ASSUMPTIONS.md A-KR-6.1, A-KR-6.2
  • Cross-repo: hyperpolymath/quandledb QD-10 (same obligation, mirrored).

Out of scope

  • Semantic equivalence after lowering. KR-6 is about the surface ASTs only.
  • Performance comparison. Worth doing separately; not in scope here.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions