🥮 mooncakes.io

moonspdx

ROBDD equivalence and implication proofs for SPDX expressions

spdx
logic
robdd
proof
counterexample
Download zip
Version
0.3.0
License
Apache-2.0
Repository
Last updated
14 hours ago
Downloads
2

Dependencies

#MoonSPDX

MoonSPDX is a MoonBit library and CLI for proving Boolean relationships between SPDX license expressions. It compiles expressions into reduced ordered binary decision diagrams (ROBDDs), proves equivalence and implication, and returns a minimum, replayable truth assignment when a claim is false.

The project answers questions such as:

  • Did a metadata rewrite preserve the exact expression semantics?
  • Does every choice allowed by one expression also satisfy another expression?
  • Which smallest assignment disproves an incorrect equivalence or implication?
  • Is the left expression narrower, broader, equal, or incomparable?
  • Which source atoms can actually influence the decision function?
  • Can a set of semantic invariants be enforced as a deterministic CI gate?

Each license identifier, including an identifier with WITH, is treated as an independent Boolean atom. These are formal expression semantics, not legal compatibility or compliance conclusions.

#Why v0.2 is different

MoonSPDX v0.1.0 was a license inventory and policy auditor. It failed the hackathon initial review because that workflow overlapped the maintained MoonCakes projects clbbbb/moonbit-license-audit and liyun/moonseal. v0.2 is a real redesign, not a wording change: the policy, inventory, obligation, drift, notice, and compatibility-matrix modules were removed from the current tree.

ProjectIts central workflowMoonSPDX v0.2 boundary
clbbbb/moonbit-license-auditScan project evidence and inventories, apply policies and obligations, compare findings, suggest remediationMoonSPDX does not scan files or decide compliance; it proves Boolean expression claims and produces counterexamples
liyun/moonsealAudit MoonBit release readiness and dependencies, generate CycloneDX/SARIF/provenance outputsMoonSPDX does not parse manifests, audit releases, generate SBOMs, detect license text, or emit provenance

MoonSPDX can serve as a lower-level proof layer for any metadata tool that wants to verify a rewrite, but it does not depend on or replace either auditor.

#Quick start

moon update
moon test --target wasm-gc
moon run cmd/main --target js -- demo

Prove distributivity across two differently written SPDX expressions:

moon run cmd/main --target js -- equivalent \
  --left 'MIT AND (Apache-2.0 OR BSD-3-Clause)' \
  --right 'MIT AND Apache-2.0 OR MIT AND BSD-3-Clause'

Disprove an invalid implication and receive a minimum witness:

moon run cmd/main --target js -- implies \
  --premise 'MIT' \
  --conclusion 'MIT AND Apache-2.0'

Output includes:

COUNTEREXAMPLE Apache-2.0=false, MIT=true

#Semantic regression suites

A suite uses one pipe-separated claim per line:

commute|equivalent|MIT OR Apache-2.0|Apache-2.0 OR MIT
distribute|equivalent|MIT AND (Apache-2.0 OR BSD-3-Clause)|MIT AND Apache-2.0 OR MIT AND BSD-3-Clause
subset|implies|MIT AND Apache-2.0|MIT

Run the checked example as one escaped CLI value:

moon run cmd/main --target js -- verify \
  --claims 'commute|equivalent|MIT OR Apache-2.0|Apache-2.0 OR MIT\ndistribute|equivalent|MIT AND (Apache-2.0 OR BSD-3-Clause)|MIT AND Apache-2.0 OR MIT AND BSD-3-Clause\nsubset|implies|MIT AND Apache-2.0|MIT'

Exit 0 means every claim was proven. Exit 1 means at least one claim was disproven and its witness is present. Exit 2 means invalid input or usage.

#CLI

moonspdx equivalent  --left TEXT --right TEXT [--json]
moonspdx implies     --premise TEXT --conclusion TEXT [--json]
moonspdx fingerprint --expression TEXT [--json]
moonspdx model       --expression TEXT [--json]
moonspdx truth-table --expression TEXT [--json]
moonspdx verify      --claims TEXT [--json]
moonspdx compare     --left TEXT --right TEXT [--json]
moonspdx influence   --expression TEXT [--json]
moonspdx normalize   --expression TEXT
moonspdx inspect     --expression TEXT
moonspdx demo

#Library API

let left = @moonspdx.parse_expression(
  "MIT AND (Apache-2.0 OR BSD-3-Clause)",
).unwrap()
let right = @moonspdx.parse_expression(
  "MIT AND Apache-2.0 OR MIT AND BSD-3-Clause",
).unwrap()
let proof = @moonspdx.prove_equivalent(left, right)
  .unwrap()
assert_true(proof.holds())

let suite = @moonspdx.verify_claims(
  "subset|implies|MIT AND Apache-2.0|MIT",
).unwrap()
assert_true(suite.all_proven())

The generated public interface is in pkg.generated.mbti.

All APIs that build a decision diagram return Result in v0.3. To customize the safety budget, construct SemanticLimits and call the corresponding *_with_limits function:

let limits = @moonspdx.SemanticLimits::new(16, 2048, 25000).unwrap()
let proof = @moonspdx.prove_implication_with_limits(
  left,
  right,
  limits,
).unwrap()

#Algorithm and limits

MoonSPDX uses catalog-stable atom ordering, a unique table, memoized Boolean AND/OR/XOR, complement construction, and ROBDD reduction (low == high) to produce canonical decision functions. Failed relations are represented as left XOR right or premise AND NOT conclusion; a dynamic path search chooses a satisfying witness with the minimum number of true atoms.

Bidirectional implication classifies expression pairs as equivalent, left-narrower, left-broader, or incomparable. Cofactor comparison checks each atom's semantic influence; relevant atoms include assignments before and after the atom is flipped, while absorbed atoms are reported as redundant.

  • Source expression limit: 4,096 characters.
  • Parser nesting limit: 64 parenthesis levels.
  • Claim suite limit: 128 records.
  • Complete truth tables: at most 10 distinct atoms.
  • Default semantic budget: 32 variables, 4,096 decision nodes, and 50,000 counted recursive/table-probe operations per proof or compilation.
  • CLI overrides: --max-variables, --max-nodes, and --max-operations.
  • Supported input profile: 44 common SPDX identifiers and 10 exceptions.
  • LicenseRef-*, DocumentRef-*, SPDX documents, and legal compatibility are unsupported.

See architecture, support profile, and direction record.

#Verification

moon fmt --check
moon check --target wasm-gc --deny-warn
moon check --target wasm --deny-warn
moon check --target js --deny-warn
moon check --target native --deny-warn
moon test --target wasm-gc
moon test --target wasm
moon test --target js
moon test --target native

GitHub Actions repeats all targets and compares real JavaScript/native CLI output with fixtures under examples/. Tests also exhaustively compare ROBDD proofs against direct AST truth evaluation for a pairwise formula corpus and verify global minimum-counterexample cardinality.

#License

Apache-2.0. See LICENSE and THIRD_PARTY.md.

AtomInfluence

source
pub struct AtomInfluence {
  atom : String
  relevant : Bool
  when_false : TruthAssignment?
  when_true : TruthAssignment?
  false_result : Bool
  true_result : Bool
} derive(Eq, 
Debug)

AtomInfluence::atom

source
fn AtomInfluence::atom(self : AtomInfluence) -> String

AtomInfluence::false_result

source
fn AtomInfluence::false_result(self : AtomInfluence) -> Bool

AtomInfluence::relevant

source
fn AtomInfluence::relevant(self : AtomInfluence) -> Bool

AtomInfluence::true_result

source
fn AtomInfluence::true_result(self : AtomInfluence) -> Bool

AtomInfluence::when_false

source
fn AtomInfluence::when_false(self : AtomInfluence) -> TruthAssignment?

AtomInfluence::when_true

source
fn AtomInfluence::when_true(self : AtomInfluence) -> TruthAssignment?

ClaimRelation

source
pub enum ClaimRelation {
  EquivalentClaim
  ImplicationClaim
} derive(Eq, 
Debug)

ClaimRelation::name

source
fn ClaimRelation::name(self : ClaimRelation) -> String

ClaimResult

source
pub struct ClaimResult {
  claim : SemanticClaim
  proof : SemanticProof
} derive(Eq, 
Debug)

ClaimResult::claim

source

ClaimResult::proof

source

CommandResult

source
pub struct CommandResult {
  exit_code : Int
  output : String
} derive(Eq, 
Debug)

CommandResult::exit_code

source
fn CommandResult::exit_code(self : CommandResult) -> Int

CommandResult::output

source
fn CommandResult::output(self : CommandResult) -> String

Diagnostic

source
pub struct Diagnostic {
  code : String
  location : String
  message : String
  expected : String
  actual : String
} derive(Eq, 
Debug)

A stable parse, policy, or inventory failure.

Diagnostic::actual

source
fn Diagnostic::actual(self : Diagnostic) -> String

Diagnostic::code

source
fn Diagnostic::code(self : Diagnostic) -> String

Diagnostic::expected

source
fn Diagnostic::expected(self : Diagnostic) -> String

Diagnostic::location

source
fn Diagnostic::location(self : Diagnostic) -> String

Diagnostic::message

source
fn Diagnostic::message(self : Diagnostic) -> String

Diagnostic::new

source
fn Diagnostic::new(code : String, location : String, message : String, expected : String, actual : String) -> Diagnostic

Diagnostic::to_text

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

Expression

source

Expression::alternatives

source
fn Expression::alternatives(self : Expression) -> Result[Array[Array[LicenseAtom]], Diagnostic]

Expand an expression into at most 64 conjunctive alternatives.

Expression::atoms

source
fn Expression::atoms(self : Expression) -> Array[LicenseAtom]

Expression::canonical

source
fn Expression::canonical(self : Expression) -> String

Render the expression with stable spacing and only semantic parentheses.

Expression::evaluate_assignment

source
fn Expression::evaluate_assignment(self : Expression, assignment : TruthAssignment) -> Bool

Replay an assignment directly against the parsed expression tree.

Expression::stats

source

ExpressionStats

source
pub struct ExpressionStats {
  atoms : Int
  and_operators : Int
  or_operators : Int
  depth : Int
  alternatives : Int
} derive(Eq, 
Debug)

ExpressionStats::alternatives

source
fn ExpressionStats::alternatives(self : ExpressionStats) -> Int

ExpressionStats::and_operators

source
fn ExpressionStats::and_operators(self : ExpressionStats) -> Int

ExpressionStats::atoms

source
fn ExpressionStats::atoms(self : ExpressionStats) -> Int

ExpressionStats::depth

source
fn ExpressionStats::depth(self : ExpressionStats) -> Int

ExpressionStats::or_operators

source
fn ExpressionStats::or_operators(self : ExpressionStats) -> Int

ExpressionStats::to_text

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

InfluenceReport

source
pub struct InfluenceReport {
  expression : String
  influences : Array[AtomInfluence]
  relevant : Int
  redundant : Int
  decision_nodes : Int
  operations : Int
} derive(Eq, 
Debug)

InfluenceReport::decision_nodes

source
fn InfluenceReport::decision_nodes(self : InfluenceReport) -> Int

InfluenceReport::influences

source

InfluenceReport::operations

source
fn InfluenceReport::operations(self : InfluenceReport) -> Int

InfluenceReport::redundant

source
fn InfluenceReport::redundant(self : InfluenceReport) -> Int

InfluenceReport::relevant

source
fn InfluenceReport::relevant(self : InfluenceReport) -> Int

InfluenceReport::to_json

source
fn InfluenceReport::to_json(self : InfluenceReport) -> String

InfluenceReport::to_text

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

LicenseAtom

source
pub struct LicenseAtom {
  id : String
  exception : String?
} derive(Eq, 
Debug)

LicenseAtom::canonical

source
fn LicenseAtom::canonical(self : LicenseAtom) -> String

LicenseAtom::exception

source
fn LicenseAtom::exception(self : LicenseAtom) -> String?

LicenseAtom::id

source
fn LicenseAtom::id(self : LicenseAtom) -> String

LicenseAtom::new

source
fn LicenseAtom::new(id : String, exception? : String?) -> LicenseAtom

ProofSuite

source
pub struct ProofSuite {
  results : Array[ClaimResult]
  passed : Int
  failed : Int
} derive(Eq, 
Debug)

ProofSuite::all_proven

source
fn ProofSuite::all_proven(self : ProofSuite) -> Bool

ProofSuite::failed

source
fn ProofSuite::failed(self : ProofSuite) -> Int

ProofSuite::passed

source
fn ProofSuite::passed(self : ProofSuite) -> Int

ProofSuite::results

source
fn ProofSuite::results(self : ProofSuite) -> Array[ClaimResult]

ProofSuite::to_json

source
fn ProofSuite::to_json(self : ProofSuite) -> String

ProofSuite::to_text

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

SemanticClaim

source
pub struct SemanticClaim {
  name : String
  relation : ClaimRelation
  left : Expression
  right : Expression
} derive(Eq, 
Debug)

SemanticClaim::left

source

SemanticClaim::name

source
fn SemanticClaim::name(self : SemanticClaim) -> String

SemanticClaim::relation

source
fn SemanticClaim::relation(self : SemanticClaim) -> ClaimRelation

SemanticClaim::right

source

SemanticComparison

source
pub struct SemanticComparison {
  left : String
  right : String
  relation : SemanticRelation
  left_implies_right : SemanticProof
  right_implies_left : SemanticProof
} derive(Eq, 
Debug)

A four-way comparison based on implication in both directions.

SemanticComparison::left_implies_right

source
fn SemanticComparison::left_implies_right(self : SemanticComparison) -> SemanticProof

SemanticComparison::relation

source

SemanticComparison::right_implies_left

source
fn SemanticComparison::right_implies_left(self : SemanticComparison) -> SemanticProof

SemanticComparison::to_json

source
fn SemanticComparison::to_json(self : SemanticComparison) -> String

SemanticComparison::to_text

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

SemanticLimits

source
pub struct SemanticLimits {
  max_variables : Int
  max_nodes : Int
  max_operations : Int
} derive(Eq, 
Debug)

Resource budget for one symbolic compilation or proof.

SemanticLimits::default

source

SemanticLimits::max_nodes

source
fn SemanticLimits::max_nodes(self : SemanticLimits) -> Int

SemanticLimits::max_operations

source
fn SemanticLimits::max_operations(self : SemanticLimits) -> Int

SemanticLimits::max_variables

source
fn SemanticLimits::max_variables(self : SemanticLimits) -> Int

SemanticLimits::new

source
fn SemanticLimits::new(max_variables : Int, max_nodes : Int, max_operations : Int) -> Result[SemanticLimits, Diagnostic]

SemanticProof

source
pub struct SemanticProof {
  relation : String
  left : String
  right : String
  holds : Bool
  variables : Array[String]
  decision_nodes : Int
  operations : Int
  counterexample : TruthAssignment?
} derive(Eq, 
Debug)

SemanticProof::counterexample

source
fn SemanticProof::counterexample(self : SemanticProof) -> TruthAssignment?

SemanticProof::decision_nodes

source
fn SemanticProof::decision_nodes(self : SemanticProof) -> Int

SemanticProof::holds

source
fn SemanticProof::holds(self : SemanticProof) -> Bool

SemanticProof::operations

source
fn SemanticProof::operations(self : SemanticProof) -> Int

SemanticProof::relation

source
fn SemanticProof::relation(self : SemanticProof) -> String

SemanticProof::to_json

source
fn SemanticProof::to_json(self : SemanticProof) -> String

SemanticProof::to_text

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

SemanticProof::variables

source
fn SemanticProof::variables(self : SemanticProof) -> Array[String]

SemanticRelation

source
pub enum SemanticRelation {
  SemanticallyEquivalent
  LeftNarrower
  LeftBroader
  SemanticallyIncomparable
} derive(Eq, 
Debug)

SemanticRelation::name

source
fn SemanticRelation::name(self : SemanticRelation) -> String

SemanticSummary

source
pub struct SemanticSummary {
  expression : String
  variables : Array[String]
  decision_nodes : Int
  operations : Int
  fingerprint : String
  model : TruthAssignment?
} derive(Eq, 
Debug)

SemanticSummary::decision_nodes

source
fn SemanticSummary::decision_nodes(self : SemanticSummary) -> Int

SemanticSummary::fingerprint

source
fn SemanticSummary::fingerprint(self : SemanticSummary) -> String

SemanticSummary::model

source

SemanticSummary::operations

source
fn SemanticSummary::operations(self : SemanticSummary) -> Int

SemanticSummary::to_json

source
fn SemanticSummary::to_json(self : SemanticSummary) -> String

SemanticSummary::to_text

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

SemanticSummary::variables

source
fn SemanticSummary::variables(self : SemanticSummary) -> Array[String]

TruthAssignment

source
pub struct TruthAssignment {
  values : Array[TruthValue]
} derive(Eq, 
Debug)

A complete assignment over the ordered atoms in a proof.

TruthAssignment::to_json

source
fn TruthAssignment::to_json(self : TruthAssignment) -> String

TruthAssignment::to_text

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

TruthAssignment::true_count

source
fn TruthAssignment::true_count(self : TruthAssignment) -> Int

TruthAssignment::values

source

TruthRow

source
pub struct TruthRow {
  assignment : TruthAssignment
  result : Bool
} derive(Eq, 
Debug)

TruthRow::assignment

source
fn TruthRow::assignment(self : TruthRow) -> TruthAssignment

TruthRow::result

source
fn TruthRow::result(self : TruthRow) -> Bool

TruthTable

source
pub struct TruthTable {
  expression : String
  variables : Array[String]
  rows : Array[TruthRow]
} derive(Eq, 
Debug)

TruthTable::rows

source
fn TruthTable::rows(self : TruthTable) -> Array[TruthRow]

TruthTable::to_json

source
fn TruthTable::to_json(self : TruthTable) -> String

TruthTable::to_text

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

TruthTable::variables

source
fn TruthTable::variables(self : TruthTable) -> Array[String]

TruthValue

source
pub struct TruthValue {
  atom : String
  value : Bool
} derive(Eq, 
Debug)

One Boolean value in a replayable semantic witness.

TruthValue::atom

source
fn TruthValue::atom(self : TruthValue) -> String

TruthValue::value

source
fn TruthValue::value(self : TruthValue) -> Bool

analyze_influence

source
fn analyze_influence(expression : Expression) -> Result[InfluenceReport, Diagnostic]

Find whether changing each atom can change the expression. Relevant atoms include a minimum context and the two replayable assignments.

analyze_influence_with_limits

source
fn analyze_influence_with_limits(expression : Expression, limits : SemanticLimits) -> Result[InfluenceReport, Diagnostic]

compare_semantics

source
fn compare_semantics(left : Expression, right : Expression) -> Result[SemanticComparison, Diagnostic]

compare_semantics_with_limits

source
fn compare_semantics_with_limits(left : Expression, right : Expression, limits : SemanticLimits) -> Result[SemanticComparison, Diagnostic]

execute

source
fn execute(args : Array[String]) -> CommandResult

help_text

source
let help_text : String

is_known_exception

source
fn is_known_exception(id : String) -> Bool

known_exception_ids

source
fn known_exception_ids() -> Array[String]

known_license_ids

source
fn known_license_ids() -> Array[String]

normalize_expression

source
fn normalize_expression(source : String) -> Result[String, Diagnostic]

parse_claims

source
fn parse_claims(source : String) -> Result[Array[SemanticClaim], Diagnostic]

Parse name|equivalent|left|right or name|implies|premise|conclusion. Blank lines and lines beginning with # are ignored.

parse_expression

source
fn parse_expression(source : String) -> Result[Expression, Diagnostic]

Parse and validate the supported SPDX 2.x expression profile.

prove_equivalent

source
fn prove_equivalent(left : Expression, right : Expression) -> Result[SemanticProof, Diagnostic]

Prove that two expressions denote the same Boolean function.

prove_equivalent_with_limits

source
fn prove_equivalent_with_limits(left : Expression, right : Expression, limits : SemanticLimits) -> Result[SemanticProof, Diagnostic]

prove_implication

source
fn prove_implication(premise : Expression, conclusion : Expression) -> Result[SemanticProof, Diagnostic]

Prove that every assignment satisfying the premise also satisfies the conclusion.

prove_implication_with_limits

source
fn prove_implication_with_limits(premise : Expression, conclusion : Expression, limits : SemanticLimits) -> Result[SemanticProof, Diagnostic]

render_alternative

source
fn render_alternative(atoms : Array[LicenseAtom]) -> String

semantic_summary

source
fn semantic_summary(expression : Expression) -> Result[SemanticSummary, Diagnostic]

Compile one expression into a canonical semantic representation.

semantic_summary_with_limits

source
fn semantic_summary_with_limits(expression : Expression, limits : SemanticLimits) -> Result[SemanticSummary, Diagnostic]

truth_table

source
fn truth_table(expression : Expression) -> Result[TruthTable, Diagnostic]

Generate a complete truth table for expressions with at most 10 atoms.

verify_claims

source
fn verify_claims(source : String) -> Result[ProofSuite, Diagnostic]

verify_claims_with_limits

source
fn verify_claims_with_limits(source : String, limits : SemanticLimits) -> Result[ProofSuite, Diagnostic]

Source Files

Powered by MoonBit

Site sourceReport issuePackagesBuild queueSkillsStatistics

© 2026 mooncakes.io