The Graph Invariants Prover

The Graph Invariants Prover: the reflection API makes promises - order respects edges, roots have no dependencies, depth is the longest path, leaves feed nothing. Documentation asserts these; this referee PROVES them, across four plan shapes including a deliberate cycle. Exit 0 is a certificate, not a shrug.

source on github

a real captured run

GRAPH INVARIANTS PROVER (7 invariants x 4 plan shapes)

  chain (a->b->c->d):
    order is a permutation of the task set               proved
    order respects every edge (acyclic only)             proved
    roots are exactly the tasks with no dependencies     proved
    leaves are exactly the tasks nothing depends on      proved
    depth is 1 + max dependency depth (acyclic only)     proved
    max_depth and max_fan_in agree with their sources    proved
    every needs: label appears on its edge               proved

  diamond (labeled join):
    order is a permutation of the task set               proved
    order respects every edge (acyclic only)             proved
    roots are exactly the tasks with no dependencies     proved
    leaves are exactly the tasks nothing depends on      proved
    depth is 1 + max dependency depth (acyclic only)     proved
    max_depth and max_fan_in agree with their sources    proved
    every needs: label appears on its edge               proved

  forest (3 trees + orphan):
    order is a permutation of the task set               proved
    order respects every edge (acyclic only)             proved
    roots are exactly the tasks with no dependencies     proved
    leaves are exactly the tasks nothing depends on      proved
    depth is 1 + max dependency depth (acyclic only)     proved
    max_depth and max_fan_in agree with their sources    proved
    every needs: label appears on its edge               proved

  cycle (x<->y):
    order is a permutation of the task set               proved
    roots are exactly the tasks with no dependencies     proved
    leaves are exactly the tasks nothing depends on      proved
    max_depth and max_fan_in agree with their sources    proved
    every needs: label appears on its edge               proved

  26 proofs, 0 violations. two invariants excuse themselves
  on the cycle - and finding THAT was the prover's first catch: depth
  means "longest path from a root", and cyclic graphs have no such
  number, so the promise is scoped, not broken. these are the promises
  every graph tool built in rounds 5-8 leans on - the forest drawing, the
  spec generator, the merge, the diff. a reflection API that ships
  without its invariants proved is asking consumers to prove them
  one production incident at a time.

source

# frozen_string_literal: true

# The Graph Invariants Prover: the reflection API makes promises -
# order respects edges, roots have no dependencies, depth is the
# longest path, leaves feed nothing. Documentation asserts these;
# this referee PROVES them, across four plan shapes including a
# deliberate cycle. Exit 0 is a certificate, not a shrug.
#
#   bundle exec ruby examples/graph_invariants.rb
#
# Runs offline; exits 1 if any invariant is violated.

require class="s">"bundler/setup"
require class="s">"agentic"

def task(name)
  Agentic:class="y">:Task.new(description: name, agent_spec: {class="s">"name" => name, class="s">"instructions" => class="s">"work"})
end

def chain_plan
  orchestrator = Agentic:class="y">:PlanOrchestrator.new
  a, b, c, d = %w[a b c d].map { |n| task(n) }
  orchestrator.add_task(a)
  orchestrator.add_task(b, [a])
  orchestrator.add_task(c, [b])
  orchestrator.add_task(d, [c])
  orchestrator
end

def diamond_plan
  orchestrator = Agentic:class="y">:PlanOrchestrator.new
  top, left, right, bottom = %w[top left right bottom].map { |n| task(n) }
  orchestrator.add_task(top)
  orchestrator.add_task(left, [top])
  orchestrator.add_task(right, [top])
  orchestrator.add_task(bottom, needs: {l: left, r: right})
  orchestrator
end

def forest_plan
  orchestrator = Agentic:class="y">:PlanOrchestrator.new
  trees = %w[oak elm ash].map { |n| task(n) }
  trees.each { |t| orchestrator.add_task(t) }
  crown = task(class="s">"crown")
  orchestrator.add_task(crown, trees)
  lone = task(class="s">"lone")
  orchestrator.add_task(lone)
  orchestrator
end

def cyclic_plan
  orchestrator = Agentic:class="y">:PlanOrchestrator.new
  x, y = %w[x y].map { |n| task(n) }
  orchestrator.add_task(x, [y.id])
  orchestrator.add_task(y, [x])
  orchestrator
end

# Each invariant is a lambda: graph in, list of violations out
INVARIANTS = {
  class="s">"order is a permutation of the task set" => lambda { |g|
    (g[class="y">:order].sort == g[class="y">:tasks].keys.sort) ? [] : [class="s">"order #{g[class="y">:order].size} ids, tasks #{g[class="y">:tasks].size}"]
  },
  class="s">"order respects every edge (acyclic only)" => lambda { |g|
    position = g[class="y">:order].each_with_index.to_h
    g[class="y">:edges].reject { |e| position[e[class="y">:from]] < position[e[class="y">:to]] }
      .map { |e| class="s">"edge #{e[class="y">:from]}->#{e[class="y">:to]} out of order" }
  },
  class="s">"roots are exactly the tasks with no dependencies" => lambda { |g|
    expected = g[class="y">:dependencies].select { |_, deps| deps.empty? }.keys
    (g[class="y">:stats][class="y">:roots].sort == expected.sort) ? [] : [class="s">"roots mismatch"]
  },
  class="s">"leaves are exactly the tasks nothing depends on" => lambda { |g|
    fed = g[class="y">:dependencies].values.flatten
    expected = g[class="y">:tasks].keys - fed
    (g[class="y">:stats][class="y">:leaves].sort == expected.sort) ? [] : [class="s">"leaves mismatch"]
  },
  class="s">"depth is 1 + max dependency depth (acyclic only)" => lambda { |g|
    g[class="y">:tasks].keys.filter_map { |id|
      deps = g[class="y">:dependencies][id]
      expected = deps.empty? ? 1 : 1 + deps.map { |d| g[class="y">:stats][class="y">:depth][d] || 0 }.max
      class="s">"depth[#{id}] = #{g[class="y">:stats][class="y">:depth][id]}, expected #{expected}" if g[class="y">:stats][class="y">:depth][id] != expected
    }
  },
  class="s">"max_depth and max_fan_in agree with their sources" => lambda { |g|
    violations = []
    violations << class="s">"max_depth" if g[class="y">:stats][class="y">:max_depth] != (g[class="y">:stats][class="y">:depth].values.max || 0)
    violations << class="s">"max_fan_in" if g[class="y">:stats][class="y">:max_fan_in] != (g[class="y">:dependencies].values.map(&class="y">:size).max || 0)
    violations
  },
  class="s">"every needs: label appears on its edge" => lambda { |g|
    g[class="y">:needs].flat_map { |task_id, named|
      named.filter_map { |label, dep_id|
        edge = g[class="y">:edges].find { |e| e[class="y">:from] == dep_id && e[class="y">:to] == task_id }
        class="s">"label #{label} missing on #{dep_id}->#{task_id}" if edge.nil? || edge[class="y">:label] != label
      }
    }
  }
}.freeze

PLANS = {
  class="s">"chain (a->b->c->d)" => chain_plan,
  class="s">"diamond (labeled join)" => diamond_plan,
  class="s">"forest (3 trees + orphan)" => forest_plan,
  class="s">"cycle (x<->y)" => cyclic_plan
}.freeze

puts class="s">"GRAPH INVARIANTS PROVER (#{INVARIANTS.size} invariants x #{PLANS.size} plan shapes)"
puts
failures = 0
PLANS.each do |plan_name, orchestrator|
  graph = orchestrator.graph
  cyclic = plan_name.include?(class="s">"cycle")
  puts class="s">"  #{plan_name}:"
  INVARIANTS.each do |invariant_name, check|
    next if cyclic && invariant_name.include?(class="s">"acyclic only")

    violations = check.call(graph)
    failures += violations.size
    status = violations.empty? ? class="s">"proved" : class="s">"VIOLATED: #{violations.join("; class="s">")}"
    puts format(class="s">"    %-52s %s", invariant_name, status)
  end
  puts
end

if failures.zero?
  puts class="s">"  #{INVARIANTS.size * PLANS.size - 2} proofs, 0 violations. two invariants excuse themselves"
  puts class="s">"  on the cycle - and finding THAT was the prover's first catch: depth"
  puts class="s">"  means \"longest path from a root\class="s">", and cyclic graphs have no such"
  puts class="s">"  number, so the promise is scoped, not broken. these are the promises"
  puts class="s">"  every graph tool built in rounds 5-8 leans on - the forest drawing, the"
  puts class="s">"  spec generator, the merge, the diff. a reflection API that ships"
  puts class="s">"  without its invariants proved is asking consumers to prove them"
  puts class="s">"  one production incident at a time."
else
  puts class="s">"  #{failures} VIOLATION(S) - the reflection API broke a promise."
end
exit(failures.zero? ? 0 : 1)