The Projection Agreement Prover

The Projection Agreement Prover: relation rules now render twice - the validator enforces them in Ruby, and to_json_schema projects them into draft-07 keywords (dependencies, not-required). Two renderings of one law can drift, so this prover evaluates BOTH against every presence combination and demands they agree. It also walks to the exact frontier where they don't: JSON's null.

source on github

a real captured run

PROJECTION AGREEMENT PROVER (4 fields -> 16 presence combinations)

  {express                                 } validator: reject schema: reject agree
  {express, api_key                        } validator: reject schema: reject agree
  {express, oauth_token                    } validator: reject schema: reject agree
  {api_key, oauth_token                    } validator: reject schema: reject agree
  {express, api_key, oauth_token           } validator: reject schema: reject agree
  {customs_code, api_key, oauth_token      } validator: reject schema: reject agree
  {express, customs_code, api_key, oauth_token} validator: reject schema: reject agree

  16 combinations, 0 disagreement(s) - the dependencies and
  not-required clauses say exactly what the validator enforces,
  proven point by point rather than asserted.

  the frontier: {express: nil}
    typed field:   validator rejects (per-key: nil isn't a boolean)
                   schema    rejects (the property EXISTS - dependencies fire)
    untyped field: validator allows  (nil is ABSENT - rule not triggered)
                   schema    allows  (projection declined - the keyword was never emitted)

  on the nil-free plane the projection is faithful, point by point.
  and at the frontier the projection now knows its own limits: a
  relation over untyped fields is not rendered into keywords it
  cannot render truthfully - it rides x-agentic-rules instead.
  a projection that declines is honest; one that guesses is a trap.

source

# frozen_string_literal: true

# The Projection Agreement Prover: relation rules now render twice -
# the validator enforces them in Ruby, and to_json_schema projects
# them into draft-07 keywords (dependencies, not-required). Two
# renderings of one law can drift, so this prover evaluates BOTH
# against every presence combination and demands they agree. It also
# walks to the exact frontier where they don't: JSON's null.
#
#   bundle exec ruby examples/projection_agreement.rb
#
# Runs offline; exits 1 if the projections disagree on the nil-free plane.

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

SPEC = Agentic:class="y">:CapabilitySpecification.new(
  name: class="s">"connect", description: class="s">"Connect an integration", version: class="s">"1.0.0",
  inputs: {
    express: {type: class="s">"boolean"},
    customs_code: {type: class="s">"string"},
    api_key: {type: class="s">"string"},
    oauth_token: {type: class="s">"string"}
  },
  rules: {
    customs: {relation: class="y">:requires, fields: [class="y">:express, class="y">:customs_code]},
    one_auth: {relation: class="y">:mutually_exclusive, fields: [class="y">:api_key, class="y">:oauth_token]}
  }
)

VALUES = {express: true, customs_code: class="s">"HS-1", api_key: class="s">"k", oauth_token: class="s">"t"}.freeze

# A four-line draft-07 evaluator for exactly the projected keywords
def schema_allows?(schema, payload)
  keys = payload.keys.map(&class="y">:to_s)
  (schema[class="s">"dependencies"] || {}).each do |trigger, needed|
    return false if keys.include?(trigger) && !(needed - keys).empty?
  end
  (schema[class="s">"allOf"] || []).each do |clause|
    required = clause.dig(class="s">"not", class="s">"required")
    return false if required && (required - keys).empty?
  end
  true
end

def validator_allows?(validator, payload)
  validator.validate_inputs!(payload)
  true
rescue Agentic:class="y">:Errors:class="y">:ValidationError
  false
end

schema = SPEC.to_json_schema
validator = Agentic:class="y">:CapabilityValidator.new(SPEC)
fields = VALUES.keys

puts class="s">"PROJECTION AGREEMENT PROVER (#{fields.size} fields -> #{2**fields.size} presence combinations)"
puts

disagreements = 0
(0...2**fields.size).each do |mask|
  payload = fields.each_with_index.select { |_, i| mask[i] == 1 }.to_h { |f, _| [f, VALUES[f]] }
  ruby = validator_allows?(validator, payload)
  json = schema_allows?(schema, payload)
  disagreements += 1 if ruby != json

  next unless ruby != json || !ruby # print the interesting rows only

  puts format(class="s">"  {%-40s} validator: %-6s schema: %-6s %s",
    payload.keys.join(class="s">", "), ruby ? class="s">"allow" : class="s">"reject", json ? class="s">"allow" : class="s">"reject",
    (ruby == json) ? class="s">"agree" : class="s">"DISAGREE")
end

puts
puts class="s">"  #{2**fields.size} combinations, #{disagreements} disagreement(s) - the dependencies and"
puts class="s">"  not-required clauses say exactly what the validator enforces,"
puts class="s">"  proven point by point rather than asserted."
puts

# --- the frontier: explicit nulls ---------------------------------------------
# Ruby's relation presence is "given and non-nil"; JSON Schema's
# dependencies trigger on the PROPERTY existing, null or not. Two
# metaphysics of absence - walk to the exact spot where they part.
#
# First discovery: for TYPED fields the frontier is guarded. An
# explicit nil never reaches the relation check, because per-key
# typing rejects it first ("must be boolean"), and the schema rejects
# it too (dependencies fire) - agreement, but for different reasons.
frontier = {express: nil}
puts class="s">"  the frontier: {express: nil}"
puts format(class="s">"    typed field:   validator %-7s (per-key: nil isn't a boolean)", validator_allows?(validator, frontier) ? class="s">"allows" : class="s">"rejects")
puts format(class="s">"                   schema    %-7s (the property EXISTS - dependencies fire)", schema_allows?(schema, frontier) ? class="s">"allows" : class="s">"rejects")

# In round 10 an untyped field exposed the true divergence: nil
# sailed past per-key checks, the validator's relation read it as
# absent, and the schema's dependencies read null as present. The
# round-11 release closes it from the projection side: a relation
# over any UNTYPED field stays out of the draft-07 keywords entirely
# (it still travels in x-agentic-rules), so the schema never claims
# a law it can't render faithfully.
untyped = Agentic:class="y">:CapabilitySpecification.new(
  name: class="s">"connect", description: class="s">"x", version: class="s">"1.0.0",
  inputs: {express: {}, customs_code: {type: class="s">"string"}},
  rules: {customs: {relation: class="y">:requires, fields: [class="y">:express, class="y">:customs_code]}}
)
ruby = validator_allows?(Agentic:class="y">:CapabilityValidator.new(untyped), frontier)
json = schema_allows?(untyped.to_json_schema, frontier)
projected = untyped.to_json_schema.key?(class="s">"dependencies")
puts format(class="s">"    untyped field: validator %-7s (nil is ABSENT - rule not triggered)", ruby ? class="s">"allows" : class="s">"rejects")
puts format(class="s">"                   schema    %-7s (projection %s)", json ? class="s">"allows" : class="s">"rejects",
  projected ? class="s">"STILL EMITTED - divergence is back!" : class="s">"declined - the keyword was never emitted")
puts
puts class="s">"  on the nil-free plane the projection is faithful, point by point."
puts class="s">"  and at the frontier the projection now knows its own limits: a"
puts class="s">"  relation over untyped fields is not rendered into keywords it"
puts class="s">"  cannot render truthfully - it rides x-agentic-rules instead."
puts class="s">"  a projection that declines is honest; one that guesses is a trap."
exit(1) if projected

exit(disagreements.zero? ? 0 : 1)