Sign in

    moontxnwitness

    Offline transactional history analysis with independently verifiable dependency-cycle witnesses

    transactions
    serializability
    witness
    consistency
    offline
    Download zip
    Author
    Version
    0.2.2
    License
    Apache-2.0
    Last updated
    53 minutes ago
    Downloads
    102

    No dependencies

    #MoonTxnWitness

    自动诊断采集:使用 instrument_engine/局部 psycopg 工厂 在业务启动时接入,保留实际执行和结果;当前新入口输出执行诊断;完整来源自动映射仍在开发。

    把事务读写日志变成可解释、可缩减、可回放的反例。 MoonBit 实现离线分析核心,提供 Mooncakes 库、JavaScript SDK、命令行和可选 PostgreSQL 采集器。

    English: An offline MoonBit transaction-history checker with shortest-cycle witnesses, bounded serial completion, counterexample reduction and replay.

    #v0.2.2 支持范围

    本版新增指定 engine/连接工厂启动插桩,并保留有界寄存器分析、固定键普通表存在性与 CRUD、固定 ORM SQL 模板/缓存及局部来源诊断、追加列表、关系集合、已选中环解读和独立执行诊断包。前提、推荐入口、预算和限制集中在稳定支持矩阵。

    模型与诊断各自保留未知提交、来源缺口和计算额度;包可重放不表示数据库真实性、无故障或完整应用修复。全部自动 SQL、完整 ORM、六模型分类及完整 MLflow/dislock 生产接入继续后续迭代。

    本版实际构建、回归、安装和公开下载以 verification/releases/0.2.2/ 收据与发行记录为准。默认生产解析器沿用已发布17版完整实现;ASCII 复用和 v0.2.1 结构化优化候选未通过性能控制,原试验与失败结果保留并已回退。本版不据这些候选声明提速或 RSS 收益。

    #运行演示

    下载并解压 portable ZIP,需要 Node.js ≥20:

    node dist/moontxnwitness.mjs --version node dist/demo.mjs

    Windows 可双击 run-demo.cmd。演示使用合成案例,在新目录生成中文报告、7→2 事务缩减和可回放证据,先打开 report.md。

    #检查、缩减与回放

    node dist/moontxnwitness.mjs check examples/write-skew.json --profile balanced node dist/moontxnwitness.mjs shrink examples/noisy-write-skew.json --profile balanced --history mini.json node dist/moontxnwitness.mjs check mini.json --profile balanced --format markdown --output report.md --capsule case.json node dist/moontxnwitness.mjs replay case.json node dist/moontxnwitness.mjs compare-models examples/strict-realtime.json

    导出拒绝覆盖已有文件。check 支持 text/json/markdown/dot。

    状态退出码含义
    consistent0在提供的模型、观察及约束内有可行串行执行
    violation1发现直接异常、依赖环或完整搜索无解
    invalid2输入或约束不合法
    inconclusive3观察不足或预算耗尽

    complete 不认证采集者或数据库全局完整性。oneMinimal 表示当前规则与预算下不能再单独删除任一剩余事务,不保证全局最小。

    #库与 SDK

    moon add HhWw96/moontxnwitness@0.2.2

    import {analyzeWithOptions, shrinkWithOptions, replayReport} from './dist/sdk.mjs'; const report = analyzeWithOptions(history); const reduced = shrinkWithOptions(history, {maxChecks: 256}); console.log(report.status, reduced.oneMinimal); console.log(replayReport(reduced.reducedHistory, reduced.report));

    MoonBit 对应 analyze_with_options、reduce_with_options 等;旧入口和默认预算保持。每次同键写入必须使用唯一版本,业务值相同也不能复用版本。搜索补全单独标记,不变成已观察到的版本顺序。

    范围默认入口balanced 入口
    图分析512 事务 / 10,000 操作 / 50,000 依赖相同
    精确串行补全8 个提交事务12 个提交事务
    补全操作 / 初始键512 / 128相同
    搜索前缀 / 操作检查100,000 / 1,000,000相同,可调低
    缩减64 事务 / 2,048 操作 / 128 次检查512 事务 / 10,000 操作 / 256 次检查

    高级缓存最多 50,000 项,满后停止插入。核心历史 JSON 限 1,048,576 UTF-16 单元,CLI 历史限 2 MiB UTF-8、深度 64。见输入格式和高级分析。

    #PostgreSQL 接入

    按自动采集说明配置版本列与点查询映射,通过连接入口包装应用连接,保存采集文档后运行:

    node dist/moontxnwitness.mjs ingest capture-trace.json --history history.json node dist/moontxnwitness.mjs check history.json --profile balanced --capsule case.json node dist/postgres-demo.mjs

    ready 表示可导出历史;inconclusive 或 invalid 保持 history:null。采集器保留文档所述驱动结果与异常,不添加业务重试。需要受控写者、一致初始快照和受支持 SQL。

    真实演示需要 PostgreSQL 18 和可选 Python 驱动,保存实际结果、提交/回滚、40001 重试及复现包;缺少数据库时明确未执行。见数据库流程和SQLite 案例。

    #有界追加列表

    列表 SDK提供 normalizeListCaptureV3、analyzeListV3、reduceListV3、verifyListV3、makeListCapsuleV3、replayListCapsuleV3。入口要求显式 traceSchema:3、dataModel:"append-list-v1",保留调用者原始 JSON 字符串;不能混入其他数据模型。

    node examples/list-roundtrip.mjs

    演示使用合成历史,将三个事务缩为两个事务的追加环反例,并保存分析、缩减、复现包及逐文件摘要。每个元素需要唯一身份,值为字符串且允许重复。精确分析最多六个已提交事务、128 个 append/read,默认最多 100,000 个状态和 1,000,000 次语义检查;缩减最多 256 次候选检查。来源不足、未知提交和计算未完成保持无法判定,oneMinimal 只表示同一规则下的事务单删最小。

    胶囊 valid:true 表示报告可重算,仍须读取 status 与覆盖标记;它也可能重放如实记录的 invalid 或 inconclusive 诊断。列表入口不提供自动 SQL 采集或完整隔离级别分类,语义与额度见模型说明。

    #有界关系集合

    关系 SDK提供规范化、分析、缩减、验证和复现包重放六个入口,要求显式 dataModel:"relation-set-v1"。支持完整结果集合与空结果、字段等值/区间 AND 谓词,以及插入、更新、删除和保存点;实际写影响与完整查询分别记录。

    node examples/relation-roundtrip.mjs

    合成示例将四个事务缩为三个,保留被异常事务读取的生产者。删除该生产者会丢失来源,不能为了得到更小反例而忽略。类型、完整性与精确搜索额度见关系模型;任意 SQL 自动映射、混合模型和完整隔离分类仍不支持。

    #ORM 模板与来源诊断

    Python 模板入口提供固定 FastAPI Users SQLAlchemy v7.0.0 base-user 的按 ID 查询、创建、修改及删除 SQL。普通导入无需可选依赖,编译时使用 SQLAlchemy 2.0.55。缓存只保存不可变计划,默认最多 128 项、1 MiB 计费条目字节;参数、结果与事务状态不进入缓存。该入口本身不执行 SQL。

    MoonBit 来源诊断核验原始 SQL、同语句来源、回滚与效果账本的对应关系。局部证明成功仍保留 analysisCoverageAccepted:false,不能据此推断完整事务历史。ProvenanceObserver、安装迁移及完整 ORM 采集仍为实验能力。

    #证据解读与执行诊断

    node examples/register-cycle-roundtrip.mjs 解读已有且完整验证的点寄存器环,保存原模型包和独立派生解释;它不搜索全部类别或接受隔离模型。node examples/execution-roundtrip.mjs 离线比较两份旧 MLflow 组件观察,分别重放模型和执行诊断;40P01、未知结果及原 capture.py 来源缺口保留。用法见环解读和执行诊断包。

    已声明输入的 v3 寄存器、列表与关系工作流使用 check-v3、reduce-v3、verify-v3、replay-v3;旧 v1/v2 默认规则保持。显式引擎兼容名单与预算见支持矩阵,兼容不改写业务版本。

    #实验与后续

    分段日志与来源窗口、扩展普通表/ORM 来源安装、dislock 完整生命周期、六模型与更广 SQL 自动接入仍按各自实验契约推进。受控组件案例不是生产采用证明,不把这些工作作为已经交付的完整应用集成。未支持 SQL 和缺失来源始终可见。

    #开发与验证

    需要 MoonBit、Node.js 和 Python,无需 npm install:

    npm run build npm test npm run package

    测试覆盖跨目标核心、独立串行重放、环证据、解析差分、缩减、CLI 及各 SDK;数量与执行目标取当前版本真实收据,发行包另在全新目录构建和运行。见开发说明。

    性能优化保持完整报告、依赖来源及预算语义。测量和环境见性能报告,进一步提速与扩容按后续路线推进。

    Apache-2.0。依赖和参考来源见 THIRD_PARTY.md;逐版测试与下载记录在 verification/releases/,详细证据见开发记录。

    AnalysisOptions

    pub(all) struct AnalysisOptions {
    max_attempts : Int
    max_operation_checks : Int
    max_cached_states : Int
    } derive(Eq)

    AnalysisOptions::equal

    AnalysisOptions::not_equal

    fn AnalysisOptions::not_equal(x : AnalysisOptions, y : AnalysisOptions) -> Bool

    AnalysisResult

    pub(all) struct AnalysisResult {
    report : Report
    options : AnalysisOptions
    cache_hits : Int
    cached_states : Int
    } derive(Eq)

    AnalysisResult::equal

    AnalysisResult::not_equal

    fn AnalysisResult::not_equal(x : AnalysisResult, y : AnalysisResult) -> Bool

    Dependency

    pub(all) enum Dependency {
    WR
    WW
    RW
    RT
    } derive(Eq, Hash)

    Dependency::equal

    fn Dependency::equal(Dependency, Dependency) -> Bool

    Dependency::hash

    fn Dependency::hash(self : Dependency) -> Int

    Dependency::hash_combine

    fn Dependency::hash_combine(Dependency, Hasher) -> Unit

    Dependency::not_equal

    fn Dependency::not_equal(x : Dependency, y : Dependency) -> Bool

    Edge

    pub(all) struct Edge {
    from : String
    to : String
    kind : Dependency
    key : String?
    from_op : Int?
    to_op : Int?
    from_version : String?
    to_version : String?
    reason : String
    } derive(Eq, Hash)

    Operation indexes are zero-based. Initial versions have no transaction.

    Edge::equal

    fn Edge::equal(Edge, Edge) -> Bool

    Edge::hash

    fn Edge::hash(self : Edge) -> Int

    Edge::hash_combine

    fn Edge::hash_combine(Edge, Hasher) -> Unit

    Edge::not_equal

    fn Edge::not_equal(x : Edge, y : Edge) -> Bool

    Finding

    pub(all) struct Finding {
    code : String
    severity : String
    message : String
    transactions : Array[String]
    key : String?
    ops : Array[Int]
    } derive(Eq)

    Finding::equal

    fn Finding::equal(Finding, Finding) -> Bool

    Finding::not_equal

    fn Finding::not_equal(x : Finding, y : Finding) -> Bool

    GraphInfo

    pub(all) struct GraphInfo {
    analyzed : Bool
    components : Int
    cyclic_components : Int
    cyclic_transactions : Int
    bfs_roots : Int
    edge_budget_exceeded : Bool
    } derive(Eq)

    GraphInfo::equal

    fn GraphInfo::equal(GraphInfo, GraphInfo) -> Bool

    GraphInfo::not_equal

    fn GraphInfo::not_equal(x : GraphInfo, y : GraphInfo) -> Bool

    History

    pub(all) struct History {
    model : Model
    initial : Map[String, String]
    version_orders : Map[String, Array[String]]
    transactions : Array[Transaction]
    } derive(Eq)

    Version orders contain the initial version followed by all committed final writes.

    History::equal

    fn History::equal(History, History) -> Bool

    History::not_equal

    fn History::not_equal(x : History, y : History) -> Bool

    KeyCoverage

    pub(all) struct KeyCoverage {
    key : String
    committed_reads : Int
    committed_final_writes : Int
    unresolved_reads : Int
    } derive(Eq)

    KeyCoverage::equal

    fn KeyCoverage::equal(KeyCoverage, KeyCoverage) -> Bool

    KeyCoverage::not_equal

    fn KeyCoverage::not_equal(x : KeyCoverage, y : KeyCoverage) -> Bool

    Model

    pub(all) enum Model {
    Serializable
    StrictSerializable
    } derive(Eq)

    Model::equal

    fn Model::equal(Model, Model) -> Bool

    Model::not_equal

    fn Model::not_equal(x : Model, y : Model) -> Bool

    OpKind

    pub(all) enum OpKind {
    Read
    Write
    } derive(Eq)

    The supported workload is a versioned, point-read register workload.

    OpKind::equal

    fn OpKind::equal(OpKind, OpKind) -> Bool

    OpKind::not_equal

    fn OpKind::not_equal(x : OpKind, y : OpKind) -> Bool

    Operation

    pub(all) struct Operation {
    kind : OpKind
    key : String
    version : String
    } derive(Eq)

    Operation::equal

    fn Operation::equal(Operation, Operation) -> Bool

    Operation::not_equal

    fn Operation::not_equal(x : Operation, y : Operation) -> Bool

    Outcome

    pub(all) enum Outcome {
    Consistent
    Violation
    Inconclusive
    Invalid
    } derive(Eq)

    Outcome::equal

    fn Outcome::equal(Outcome, Outcome) -> Bool

    Outcome::not_equal

    fn Outcome::not_equal(x : Outcome, y : Outcome) -> Bool

    Reduction

    pub(all) struct Reduction {
    history : History
    report : Report
    status : String
    removed : Array[String]
    checks : Int
    one_minimal : Bool
    reason : String
    } derive(Eq)

    Reduction::equal

    fn Reduction::equal(Reduction, Reduction) -> Bool

    Reduction::not_equal

    fn Reduction::not_equal(x : Reduction, y : Reduction) -> Bool

    ReductionOptions

    pub(all) struct ReductionOptions {
    max_checks : Int
    analysis : AnalysisOptions
    } derive(Eq)

    ReductionOptions::equal

    ReductionOptions::not_equal

    fn ReductionOptions::not_equal(x : ReductionOptions, y : ReductionOptions) -> Bool

    ReductionResult

    pub(all) struct ReductionResult {
    reduction : Reduction
    analysis : AnalysisResult
    cached_checks : Int
    max_checks : Int
    } derive(Eq)

    ReductionResult::equal

    ReductionResult::not_equal

    fn ReductionResult::not_equal(x : ReductionResult, y : ReductionResult) -> Bool

    Report

    pub(all) struct Report {
    outcome : Outcome
    model : Model
    findings : Array[Finding]
    edges : Array[Edge]
    witness : Array[Edge]
    serial_order : Array[String]
    transaction_count : Int
    committed_count : Int
    operation_count : Int
    inferred_orders : Map[String, Array[String]]
    order_sources : Map[String, String]
    search : SearchInfo
    graph : GraphInfo
    coverage : Array[KeyCoverage]
    } derive(Eq)

    Consistent is a claim about the supplied complete history and asserted version orders.

    Report::equal

    fn Report::equal(Report, Report) -> Bool

    Report::not_equal

    fn Report::not_equal(x : Report, y : Report) -> Bool

    SearchInfo

    pub(all) struct SearchInfo {
    status : String
    attempts : Int
    operation_checks : Int
    reason : String
    blockers : Array[Finding]
    } derive(Eq)

    SearchInfo::equal

    fn SearchInfo::equal(SearchInfo, SearchInfo) -> Bool

    SearchInfo::not_equal

    fn SearchInfo::not_equal(x : SearchInfo, y : SearchInfo) -> Bool

    Transaction

    pub(all) struct Transaction {
    id : String
    status : TxStatus
    ops : Array[Operation]
    start : Int64?
    end : Int64?
    } derive(Eq)

    Transaction::equal

    fn Transaction::equal(Transaction, Transaction) -> Bool

    Transaction::not_equal

    fn Transaction::not_equal(x : Transaction, y : Transaction) -> Bool

    TxStatus

    pub(all) enum TxStatus {
    Committed
    Aborted
    Unknown
    } derive(Eq)

    TxStatus::equal

    fn TxStatus::equal(TxStatus, TxStatus) -> Bool

    TxStatus::not_equal

    fn TxStatus::not_equal(x : TxStatus, y : TxStatus) -> Bool

    analysis_options

    fn analysis_options(max_attempts? : Int, max_operation_checks? : Int, max_cached_states? : Int) -> AnalysisOptions

    analysis_result_json

    fn analysis_result_json(result : AnalysisResult) -> Json

    analyze

    fn analyze(h : History) -> Report

    Analyze point reads and unique versioned writes. No arrival/commit order is invented.

    analyze_json

    fn analyze_json(text : String) -> String

    Main portable host entry. Syntax/schema errors have the same report envelope.

    analyze_options_json

    fn analyze_options_json(text : String, options_text : String) -> String

    analyze_v3_json

    fn analyze_v3_json(text : String, options_text : String) -> String

    analyze_with_options

    fn analyze_with_options(h : History, options? : AnalysisOptions) -> AnalysisResult

    benchmark_cycle

    fn benchmark_cycle(h : History, r : Report) -> Int

    benchmark_infer

    fn benchmark_infer(h : History) -> Report

    Development-only phase hooks. Timers live in the host, not the analyzer.

    benchmark_parser_agreement

    fn benchmark_parser_agreement(text : String) -> String

    benchmark_reduce_balanced

    fn benchmark_reduce_balanced(h : History) -> ReductionResult

    benchmark_render

    fn benchmark_render(r : Report) -> String

    fn benchmark_search(h : History, r : Report) -> Int

    benchmark_search_balanced

    fn benchmark_search_balanced(h : History, r : Report) -> Int

    capsule_content_json

    fn capsule_content_json(text : String) -> String

    Parse a capsule with duplicate-key/depth limits. Cryptographic hashes belong to the host.

    capsule_v3_content_json

    fn capsule_v3_content_json(text : String) -> String

    Host transports bytes and SHA-256; bounded duplicate-key parsing stays in MoonBit.

    compare_models

    fn compare_models(h : History) -> Json

    compare_models_json

    fn compare_models_json(text : String) -> String

    dislock_sql_v3_proof_json

    fn dislock_sql_v3_proof_json(text : String) -> String

    Independent semantic diagnostic; successful matching does not authenticate that the input came from a database. It grants no normalization exemptions.

    history_json

    fn history_json(h : History) -> Json

    Explicit history export is useful to library consumers and retains all recorded operations.

    inspect_execution_failures_v3_json

    fn inspect_execution_failures_v3_json(text : String) -> String

    Describe recorded driver failures independently of the isolation judgment. A SQLSTATE is an observation supplied by the caller, not database attestation.

    normalize_capture_json

    fn normalize_capture_json(text : String) -> String

    Validate a complete capture envelope before exposing an ordinary history. Declared capture scope is an assumption, not authenticated source evidence.

    normalize_capture_v3_json

    fn normalize_capture_v3_json(text : String) -> String

    normalize_capture_v3_options_json

    fn normalize_capture_v3_options_json(text : String, options_text : String) -> String

    normalize_list_capture_v3_json

    fn normalize_list_capture_v3_json(text : String) -> String

    normalize_presence_capture_json

    fn normalize_presence_capture_json(text : String) -> String

    Experimental presence facts are internally checked observations, not database authentication. Predecessors constrain factual version order and never create a read operation. The old trace-1 lifecycle validator remains the authority for event sequence, transaction outcomes, clocks and coverage.

    normalize_relation_capture_v3_json

    fn normalize_relation_capture_v3_json(text : String) -> String

    orm_sql_source2_v3_proof_json

    fn orm_sql_source2_v3_proof_json(text : String) -> String

    orm_sql_v3_proof_json

    fn orm_sql_v3_proof_json(text : String) -> String

    parse_history

    fn parse_history(text : String) -> Result[History, String]

    Parse the versioned-register input schema. Unknown fields are rejected.

    parse_history_optimized

    fn parse_history_optimized(text : String) -> Result[History, String]

    Valid-input fast path; legacy decoding retains exact errors and uncommon cases.

    reduce_history

    fn reduce_history(h : History, max_checks? : Int) -> Reduction

    Delta debugging followed by a complete singleton pass proves one-minimality. The predicate is a definite Violation from this analyzer, not absence of a serial replay with unknown sources.

    reduce_v3_json

    fn reduce_v3_json(text : String, options_text : String) -> String

    Every candidate is source-validated again. No searched orders become capture facts.

    reduce_with_options

    fn reduce_with_options(h : History, options? : ReductionOptions) -> ReductionResult

    reduction_json

    fn reduction_json(r : Reduction) -> Json

    reduction_options

    fn reduction_options(max_checks? : Int, analysis? : AnalysisOptions) -> ReductionOptions

    reduction_result_json

    fn reduction_result_json(result : ReductionResult) -> Json

    render_report

    fn render_report(r : Report, format : String) -> String

    Render local text, Markdown, JSON or Graphviz DOT. No external renderer is required.

    replay_report_json

    fn replay_report_json(history_text : String, report_text : String) -> String

    Recompute semantic fields. Supplemental presentation/coverage fields are not authenticated.

    report_json

    fn report_json(r : Report) -> Json

    run_json

    fn run_json(text : String, format : String) -> String

    Host transport combines a structured result and its MoonBit-rendered presentation.

    run_options_json

    fn run_options_json(text : String, format : String) -> String

    shrink_json

    fn shrink_json(text : String) -> String

    shrink_options_json

    fn shrink_options_json(text : String, options_text : String) -> String

    verify_certificate_json

    fn verify_certificate_json(history_text : String, certificate_text : String) -> String

    verify_cycle

    fn verify_cycle(h : History, witness : Array[Edge]) -> Bool

    Verify edge provenance and cycle closure without running cycle search again.

    verify_v3_json

    fn verify_v3_json(text : String, report_text : String) -> String

    version

    fn version() -> String