🥮 mooncakes.io
    Sign in

    moonnormal

    Bounded relational schema normalization, decomposition verification and tuple audits

    database
    normalization
    functional-dependencies
    bcnf
    lossless-join
    Download zip
    Version
    0.1.0
    License
    MIT
    Repository
    Last updated
    8 hours ago
    Downloads
    2

    Dependencies

    #MoonNormal

    有预算上限的关系数据库模式规范化与分解验证库。

    MoonNormal 将给定函数依赖转成可检查的候选键、2NF/3NF/BCNF 诊断、 3NF 综合和 BCNF 分解，并检查依赖保持与无损连接。 它也能生成有损分解的有限反例、审计字符串元组和比较迁移前后的布局。 它不是 SQL 执行器，也不从少量观察数据推断普遍成立的依赖。

    #安装

    需要支持现代 moon.mod 的 MoonBit。验收使用官方 moonc v0.10.15+943464bfa / moon 0.1.20261012 (748b63c)。

    moon add LuoYunxin1/moonnormal@0.1.0

    下游 moon.pkg：

    import {
      "LuoYunxin1/moonnormal" @normal,
    }

    #使用

    let s = @normal.parse_schema_text(
      "attributes: Student,Course,Tutor\nStudent,Course -> Tutor\nTutor -> Course",
    )
    let third = s.synthesize_3nf()
    let bcnf = s.decompose_bcnf()
    let audit = s.audit_plan(bcnf)
    // BCNF 无损，但可能不保持 Student,Course -> Tutor。
    let report = s.plan_report(bcnf)

    这些调用会抛出 DesignError，在调用函数声明 raise 或用 catch 处理。 Invalid 表示不合约的输入；Budget 表示预算不足，不是否定的数学结论。

    #API 分组

    • 建模：schema、parse_schema_text、resolve、names、closure、entails。
    • 键：candidate_keys、is_candidate_key、key_profile、prime_attributes。
    • 理论：minimal_cover、grouped_cover、equivalent、compare_theory。
    • 规范化：normal_form_violations、relation_profile、synthesize_3nf、decompose_bcnf。
    • 分解验收：project_dependencies、dependency_preservation、binary_lossless、 lossless_chase、audit_plan、verify_split_trace、verify_chase_trace。
    • 反例：lossy_counterexample、verify_lossy_counterexample。
    • 数据：table、project、natural_join、reconstruct、audit_dependencies、 key_collisions、column_profiles。
    • 集成：Schema/Table/Plan JSON，CSV，dependency_locality、review_migration、 sql_advice 和可读报告。完整签名见 pkg.generated.mbti。

    #三个完整示例

    moon run examples/design
moon run examples/migration
moon run examples/quality

    示例分别完成数据库设计取舍、迁移回归审查和 CSV 数据质量审计； 每个示例包含断言，详细输入输出见 examples。

    #数据和边界

    • 属性为 1–16 个有序唯一 ASCII 标识符，声明 FD 至多 256 条。 属性索引从 0 开始；FD 内部集合会规范化，表列必须已排序且唯一。
    • 属性/依赖/表输入会复制，Schema/Table 字段私有，getter 返回副本。 公开结果记录可修改；不得将外部修改后的计划或轨迹当作认证证明。
    • 空决定项允许表示常量依赖。candidate_keys(relation=[] ) 表示整关系； 单独判断空关系请用 is_candidate_key([], [])。
    • 元组是字符串集合，重复行去重，空串是普通值，不模拟 SQL NULL。 FD 违规行号指向去重后的输入顺序。
    • 子集枚举是指数级。默认预算 work=2,000,000、results=4,096、rows=4,096、 cells=65,536；16 属性是验证上限，并非所有 16 属性任务都能在默认预算完成。
    • JSON 版本字段必须匹配且不接受额外字段；core JSON 对重复对象键采用末项， 此格式不用于签名、安全规范化或不可信深层结构。CSV 支持双引号、换行、CRLF， 不接受无引号字段中的引号或闭引号后的多余字符。
    • Chase 的结构校验 validate_chase_witness 只检查定点与证据行的一致性； 证明来源使用确定性重算的 verify_chase_trace。
    • SQL 输出只有建议性 TEXT NOT NULL / PRIMARY KEY；不能保证任意 FD， 不推导外键，不执行迁移。MVD、4NF/5NF、SQL AST/优化器/ORM 不在范围内。

    #复现

    moon info
moon fmt --check
moon check --target wasm-gc --deny-warn
moon test --target wasm-gc --deny-warn
moon build --target wasm-gc --deny-warn
bash scripts/verify.sh wasm-gc
python scripts/measure.py

    CI 在 wasm-gc / wasm / js / native 上运行严格检查、全部测试、构建与三个示例。 测试包含 4,096 个三属性 singleton-conclusion FD 理论：32,768 个独立闭包/键/cover 比较、8,192 个分解计划、49,152 个二元连接判据与 chase 比较。 此穷举不等于大模式的形式化证明，也没有宣称性能优于其他实现。

    #设计与许可

    原创 MIT 库。直接复用 MIT 的 Zh666-lab/moonconcept@0.1.1 做 Armstrong 闭包与依赖约简；这里新增关系模式、分解 chase 和元组语义，不重复开发 FCA 核心。 见 architecture、security、 dependency attribution、AI use 与 bounded ecosystem review。

    DesignError

    source
    pub suberror DesignError {
      Invalid(String)
      Budget(String)
    } derive(
    Debug    )

    ChaseMerge

    source
    pub(all) struct ChaseMerge {
      dependency_index : Int
      first_row : Int
      second_row : Int
      column : Int
      eliminated : Int
      representative : Int
    } derive(Eq, 
    Debug    )

    ChaseMerge::equal

    source
    fn ChaseMerge::equal(ChaseMerge, ChaseMerge) -> Bool

    ChaseMerge::not_equal

    source
    fn ChaseMerge::not_equal(x : ChaseMerge, y : ChaseMerge) -> Bool

    ChaseMerge::to_repr

    source

    ChaseResult

    source
    pub(all) struct ChaseResult {
      lossless : Bool
      witness_row : Int?
      initial : Array[Array[Int]]
      final_tableau : Array[Array[Int]]
      merges : Array[ChaseMerge]
      rounds : Int
    } derive(Eq, 
    Debug    )

    ChaseResult::equal

    source
    fn ChaseResult::equal(ChaseResult, ChaseResult) -> Bool

    ChaseResult::not_equal

    source
    fn ChaseResult::not_equal(x : ChaseResult, y : ChaseResult) -> Bool

    ChaseResult::to_repr

    source

    Collision

    source
    pub(all) struct Collision {
      first_row : Int
      second_row : Int
      determinant_values : Array[String]
    } derive(Eq, 
    Debug    )

    Collision::equal

    source
    fn Collision::equal(Collision, Collision) -> Bool

    Collision::not_equal

    source
    fn Collision::not_equal(x : Collision, y : Collision) -> Bool

    Collision::to_repr

    source

    ColumnProfile

    source
    pub(all) struct ColumnProfile {
      attribute : Int
      distinct_values : Int
      empty_values : Int
      maximum_code_units : Int
    } derive(Eq, 
    Debug    )

    ColumnProfile::equal

    source

    ColumnProfile::not_equal

    source
    fn ColumnProfile::not_equal(x : ColumnProfile, y : ColumnProfile) -> Bool

    ColumnProfile::to_repr

    source

    DataAudit

    source
    pub(all) struct DataAudit {
      checked_dependencies : Array[Int]
      skipped_dependencies : Array[Int]
      violations : Array[TupleViolation]
    } derive(Eq, 
    Debug    )

    DataAudit::equal

    source
    fn DataAudit::equal(DataAudit, DataAudit) -> Bool

    DataAudit::not_equal

    source
    fn DataAudit::not_equal(x : DataAudit, y : DataAudit) -> Bool

    DataAudit::to_repr

    source

    DependencyLocality

    source
    pub(all) struct DependencyLocality {
      dependency : FD
      containing_relations : Array[Int]
      jointly_preserved : Bool
    } derive(Eq, 
    Debug    )

    DependencyLocality::equal

    source

    DependencyLocality::not_equal

    source

    DependencyLocality::to_repr

    source

    pub(all) struct FD {
      left : Array[Int]
      right : Array[Int]
    } derive(Eq, 
    Debug    )

    FD::equal

    source
    fn FD::equal(FD, FD) -> Bool

    FD::not_equal

    source
    fn FD::not_equal(x : FD, y : FD) -> Bool

    FD::to_repr

    source

    KeyProfile

    source
    pub(all) struct KeyProfile {
      keys : Array[Array[Int]]
      prime : Array[Int]
      essential : Array[Int]
      minimum_width : Int
      maximum_width : Int
    } derive(Eq, 
    Debug    )

    KeyProfile::equal

    source
    fn KeyProfile::equal(KeyProfile, KeyProfile) -> Bool

    KeyProfile::not_equal

    source
    fn KeyProfile::not_equal(x : KeyProfile, y : KeyProfile) -> Bool

    KeyProfile::to_repr

    source

    LayoutDelta

    source
    pub(all) struct LayoutDelta {
      unchanged : Array[Array[Int]]
      removed : Array[Array[Int]]
      added : Array[Array[Int]]
      duplicated_attributes_before : Array[Int]
      duplicated_attributes_after : Array[Int]
    } derive(Eq, 
    Debug    )

    LayoutDelta::equal

    source
    fn LayoutDelta::equal(LayoutDelta, LayoutDelta) -> Bool

    LayoutDelta::not_equal

    source
    fn LayoutDelta::not_equal(x : LayoutDelta, y : LayoutDelta) -> Bool

    LayoutDelta::to_repr

    source

    Limits

    source
    pub(all) struct Limits {
      max_work : Int
      max_results : Int
      max_rows : Int
      max_cells : Int
    } derive(Eq, 
    Debug    )

    Limits::equal

    source
    fn Limits::equal(Limits, Limits) -> Bool

    Limits::not_equal

    source
    fn Limits::not_equal(x : Limits, y : Limits) -> Bool

    Limits::to_repr

    source

    LossyWitness

    source
    pub(all) struct LossyWitness {
      instance : Table
      spurious_row : Array[String]
      projected_presence : Array[Bool]
      chase : ChaseResult
    } derive(
    Debug    )

    MigrationReview

    source
    pub(all) struct MigrationReview {
      before : PlanAudit
      after : PlanAudit
      layout : LayoutDelta
      lost_dependencies : Array[FD]
      gained_dependencies : Array[FD]
      lossless_regression : Bool
      normal_form_regression : Bool
      locality : Array[DependencyLocality]
    } derive(Eq, 
    Debug    )

    MigrationReview::equal

    source

    MigrationReview::not_equal

    source
    fn MigrationReview::not_equal(x : MigrationReview, y : MigrationReview) -> Bool

    MigrationReview::summary

    source
    fn MigrationReview::summary(self : MigrationReview, owner : Schema) -> String raise DesignError

    MigrationReview::to_repr

    source

    NormalForm

    source
    pub(all) enum NormalForm {
      Second
      Third
      BoyceCodd
    } derive(Eq, 
    Debug    )

    NormalForm::equal

    source
    fn NormalForm::equal(NormalForm, NormalForm) -> Bool

    NormalForm::not_equal

    source
    fn NormalForm::not_equal(x : NormalForm, y : NormalForm) -> Bool

    NormalForm::to_repr

    source

    Plan

    source
    pub(all) struct Plan {
      target : NormalForm
      relations : Array[Array[Int]]
      splits : Array[SplitStep]
      added_key_relation : Bool
    } derive(Eq, 
    Debug    )

    Plan::equal

    source
    fn Plan::equal(Plan, Plan) -> Bool

    Plan::not_equal

    source
    fn Plan::not_equal(x : Plan, y : Plan) -> Bool

    Plan::to_json

    source
    fn Plan::to_json(self : Plan, owner : Schema) -> Json raise DesignError

    Plan::to_repr

    source

    PlanAudit

    source
    pub(all) struct PlanAudit {
      lossless : Bool
      dependency_preserving : Bool
      target_satisfied : Bool
      missing_dependencies : Array[FD]
      violations : Array[Violation]
      chase : ChaseResult
    } derive(Eq, 
    Debug    )

    PlanAudit::equal

    source
    fn PlanAudit::equal(PlanAudit, PlanAudit) -> Bool

    PlanAudit::not_equal

    source
    fn PlanAudit::not_equal(x : PlanAudit, y : PlanAudit) -> Bool

    PlanAudit::to_repr

    source

    Preservation

    source
    pub(all) struct Preservation {
      preserved : Bool
      missing : Array[FD]
      projected_dependency_count : Int
    } derive(Eq, 
    Debug    )

    Preservation::equal

    source

    Preservation::not_equal

    source
    fn Preservation::not_equal(x : Preservation, y : Preservation) -> Bool

    Preservation::to_repr

    source

    Reconstruction

    source
    pub(all) struct Reconstruction {
      exact : Bool
      original_rows : Int
      reconstructed_rows : Int
      spurious : Array[Array[String]]
      missing : Array[Array[String]]
      reconstructed : Table
    } derive(
    Debug    )

    RelationProfile

    source
    pub(all) struct RelationProfile {
      attributes : Array[Int]
      keys : Array[Array[Int]]
      prime : Array[Int]
      second : Bool
      third : Bool
      boyce_codd : Bool
    } derive(Eq, 
    Debug    )

    RelationProfile::equal

    source

    RelationProfile::not_equal

    source
    fn RelationProfile::not_equal(x : RelationProfile, y : RelationProfile) -> Bool

    RelationProfile::to_repr

    source

    Schema

    source
    pub struct Schema {
      // private fields
    } derive(
    Debug    )

    Schema::attribute

    source
    fn Schema::attribute(self : Schema, label : String) -> Int?

    Schema::attribute_count

    source
    fn Schema::attribute_count(self : Schema) -> Int

    Schema::attributes

    source
    fn Schema::attributes(self : Schema) -> Array[String]

    Schema::audit_plan

    source
    fn Schema::audit_plan(self : Schema, plan : Plan, limits? : Limits) -> PlanAudit raise DesignError

    Schema::binary_lossless

    source
    fn Schema::binary_lossless(self : Schema, first : Array[Int], second : Array[Int], limits? : Limits) -> Bool raise DesignError

    Schema::candidate_keys

    source
    fn Schema::candidate_keys(self : Schema, relation? : Array[Int], limits? : Limits) -> Array[Array[Int]] raise DesignError

    Schema::closure

    source
    fn Schema::closure(self : Schema, seed : Array[Int], limits? : Limits) -> Array[Int] raise DesignError

    Schema::compare_layouts

    source
    fn Schema::compare_layouts(self : Schema, before : Array[Array[Int]], after : Array[Array[Int]]) -> LayoutDelta raise DesignError

    Schema::compare_theory

    source
    fn Schema::compare_theory(self : Schema, proposed : Schema, limits? : Limits) -> TheoryDelta raise DesignError

    Schema::decompose_bcnf

    source
    fn Schema::decompose_bcnf(self : Schema, limits? : Limits) -> Plan raise DesignError

    Schema::dependencies

    source
    fn Schema::dependencies(self : Schema) -> Array[FD]

    Schema::dependency_locality

    source
    fn Schema::dependency_locality(self : Schema, relations : Array[Array[Int]], limits? : Limits) -> Array[DependencyLocality] raise DesignError

    Schema::dependency_preservation

    source
    fn Schema::dependency_preservation(self : Schema, relations : Array[Array[Int]], limits? : Limits) -> Preservation raise DesignError

    Schema::entails

    source
    fn Schema::entails(self : Schema, fd : FD, limits? : Limits) -> Bool raise DesignError

    Schema::equivalent

    source
    fn Schema::equivalent(self : Schema, other : Schema, limits? : Limits) -> Bool raise DesignError

    Schema::essential_attributes

    source
    fn Schema::essential_attributes(self : Schema) -> Array[Int]

    Schema::grouped_cover

    source
    fn Schema::grouped_cover(self : Schema, limits? : Limits) -> Array[FD] raise DesignError

    Schema::in_normal_form

    source
    fn Schema::in_normal_form(self : Schema, relation : Array[Int], form : NormalForm, limits? : Limits) -> Bool raise DesignError

    Schema::is_candidate_key

    source
    fn Schema::is_candidate_key(self : Schema, seed : Array[Int], relation : Array[Int], limits? : Limits) -> Bool raise DesignError

    Schema::is_superkey

    source
    fn Schema::is_superkey(self : Schema, seed : Array[Int], relation : Array[Int], limits? : Limits) -> Bool raise DesignError

    Schema::key_profile

    source
    fn Schema::key_profile(self : Schema, limits? : Limits) -> KeyProfile raise DesignError

    Schema::lossless_chase

    source
    fn Schema::lossless_chase(self : Schema, relations : Array[Array[Int]], limits? : Limits) -> ChaseResult raise DesignError

    Schema::lossy_counterexample

    source
    fn Schema::lossy_counterexample(self : Schema, relations : Array[Array[Int]], limits? : Limits) -> LossyWitness? raise DesignError

    Schema::minimal_cover

    source
    fn Schema::minimal_cover(self : Schema, limits? : Limits) -> Array[FD] raise DesignError

    Schema::names

    source
    fn Schema::names(self : Schema, attrs : Array[Int]) -> Array[String] raise DesignError

    Schema::normal_form_violations

    source
    fn Schema::normal_form_violations(self : Schema, relation : Array[Int], form : NormalForm, limits? : Limits) -> Array[Violation] raise DesignError

    Schema::plan_report

    source
    fn Schema::plan_report(self : Schema, plan : Plan, limits? : Limits) -> String raise DesignError

    Schema::prime_attributes

    source
    fn Schema::prime_attributes(self : Schema, relation : Array[Int], limits? : Limits) -> Array[Int] raise DesignError

    Schema::project_dependencies

    source
    fn Schema::project_dependencies(self : Schema, relation : Array[Int], limits? : Limits) -> Array[FD] raise DesignError

    Schema::relation_profile

    source
    fn Schema::relation_profile(self : Schema, relation : Array[Int], limits? : Limits) -> RelationProfile raise DesignError

    Schema::resolve

    source
    fn Schema::resolve(self : Schema, names : Array[String]) -> Array[Int] raise DesignError

    Schema::review_migration

    source
    fn Schema::review_migration(self : Schema, before : Plan, after : Plan, limits? : Limits) -> MigrationReview raise DesignError

    Schema::sql_advice

    source
    fn Schema::sql_advice(self : Schema, plan : Plan, prefix : String, limits? : Limits) -> SqlAdvice raise DesignError

    Schema::synthesize_3nf

    source
    fn Schema::synthesize_3nf(self : Schema, limits? : Limits) -> Plan raise DesignError

    Schema::to_json

    source
    fn Schema::to_json(self : Schema) -> Json

    Schema::to_repr

    source

    Schema::to_text

    source
    fn Schema::to_text(self : Schema) -> String

    Schema::validate_chase_witness

    source
    fn Schema::validate_chase_witness(self : Schema, result : ChaseResult, limits? : Limits) -> Bool raise DesignError

    Schema::verify_chase_trace

    source
    fn Schema::verify_chase_trace(self : Schema, relations : Array[Array[Int]], result : ChaseResult, limits? : Limits) -> Bool raise DesignError

    Schema::verify_lossy_counterexample

    source
    fn Schema::verify_lossy_counterexample(self : Schema, relations : Array[Array[Int]], witness : LossyWitness, limits? : Limits) -> Bool raise DesignError

    Schema::verify_split_trace

    source
    fn Schema::verify_split_trace(self : Schema, plan : Plan, limits? : Limits) -> Bool raise DesignError

    SplitStep

    source
    pub(all) struct SplitStep {
      input : Array[Int]
      dependency : FD
      first : Array[Int]
      second : Array[Int]
    } derive(Eq, 
    Debug    )

    SplitStep::equal

    source
    fn SplitStep::equal(SplitStep, SplitStep) -> Bool

    SplitStep::not_equal

    source
    fn SplitStep::not_equal(x : SplitStep, y : SplitStep) -> Bool

    SplitStep::to_repr

    source

    SqlAdvice

    source
    pub(all) struct SqlAdvice {
      statements : Array[String]
      warnings : Array[String]
      primary_keys : Array[Array[Int]]
    } derive(Eq, 
    Debug    )

    SqlAdvice::equal

    source
    fn SqlAdvice::equal(SqlAdvice, SqlAdvice) -> Bool

    SqlAdvice::not_equal

    source
    fn SqlAdvice::not_equal(x : SqlAdvice, y : SqlAdvice) -> Bool

    SqlAdvice::to_repr

    source

    SqlAdvice::to_text

    source
    fn SqlAdvice::to_text(self : SqlAdvice) -> String

    Table

    source
    pub struct Table {
      // private fields
    } derive(
    Debug    )

    Table::audit_dependencies

    source
    fn Table::audit_dependencies(self : Table, owner : Schema, limits? : Limits) -> DataAudit raise DesignError

    Table::audit_report

    source
    fn Table::audit_report(self : Table, owner : Schema, limits? : Limits) -> String raise DesignError

    Table::column_names

    source
    fn Table::column_names(self : Table) -> Array[String]

    Table::column_profiles

    source
    fn Table::column_profiles(self : Table, limits? : Limits) -> Array[ColumnProfile] raise DesignError

    Table::columns

    source
    fn Table::columns(self : Table) -> Array[Int]

    Table::key_collisions

    source
    fn Table::key_collisions(self : Table, key : Array[Int], limits? : Limits) -> Array[Collision] raise DesignError

    Table::natural_join

    source
    fn Table::natural_join(self : Table, other : Table, limits? : Limits) -> Table raise DesignError

    Table::project

    source
    fn Table::project(self : Table, columns : Array[Int], limits? : Limits) -> Table raise DesignError

    Table::reconstruct

    source
    fn Table::reconstruct(self : Table, owner : Schema, relations : Array[Array[Int]], limits? : Limits) -> Reconstruction raise DesignError

    Table::row_count

    source
    fn Table::row_count(self : Table) -> Int

    Table::rows

    source
    fn Table::rows(self : Table) -> Array[Array[String]]

    Table::set_equal

    source
    fn Table::set_equal(self : Table, other : Table, limits? : Limits) -> Bool raise DesignError

    Table::to_csv

    source
    fn Table::to_csv(self : Table) -> String

    Table::to_json

    source
    fn Table::to_json(self : Table) -> Json

    Table::to_repr

    source

    TheoryDelta

    source
    pub(all) struct TheoryDelta {
      removed_constraints : Array[FD]
      added_constraints : Array[FD]
      equivalent : Bool
    } derive(Eq, 
    Debug    )

    TheoryDelta::equal

    source
    fn TheoryDelta::equal(TheoryDelta, TheoryDelta) -> Bool

    TheoryDelta::not_equal

    source
    fn TheoryDelta::not_equal(x : TheoryDelta, y : TheoryDelta) -> Bool

    TheoryDelta::to_repr

    source

    TupleViolation

    source
    pub(all) struct TupleViolation {
      dependency_index : Int
      first_row : Int
      second_row : Int
      differing_attributes : Array[Int]
    } derive(Eq, 
    Debug    )

    TupleViolation::equal

    source

    TupleViolation::not_equal

    source
    fn TupleViolation::not_equal(x : TupleViolation, y : TupleViolation) -> Bool

    TupleViolation::to_repr

    source

    Violation

    source
    pub(all) struct Violation {
      relation : Array[Int]
      dependency : FD
      form : NormalForm
    } derive(Eq, 
    Debug    )

    Violation::equal

    source
    fn Violation::equal(Violation, Violation) -> Bool

    Violation::not_equal

    source
    fn Violation::not_equal(x : Violation, y : Violation) -> Bool

    Violation::to_repr

    source

    default_limits

    source
    fn default_limits() -> Limits

    parse_plan_json

    source
    fn parse_plan_json(owner : Schema, text : String) -> Plan raise DesignError

    parse_schema_json

    source
    fn parse_schema_json(text : String) -> Schema raise DesignError

    parse_schema_text

    source
    fn parse_schema_text(text : String) -> Schema raise DesignError

    parse_table_csv

    source
    fn parse_table_csv(owner : Schema, text : String, limits? : Limits) -> Table raise DesignError

    parse_table_json

    source
    fn parse_table_json(owner : Schema, text : String, limits? : Limits) -> Table raise DesignError

    schema

    source
    fn schema(labels : Array[String], dependencies : Array[FD]) -> Schema raise DesignError

    table

    source
    fn table(owner : Schema, columns : Array[Int], rows : Array[Array[String]], limits? : Limits) -> Table raise DesignError

    Source Files

    Powered by MoonBit

    Site sourceReport issuePackagesBuild queueSkillsStatistics

    © 2026 mooncakes.io