Class: Ibex::Verify::LanguageWitness

Inherits:
Object
  • Object
show all
Defined in:
lib/ibex/verify/language_witness.rb,
sig/ibex/verify/language_witness.rbs

Overview

Compares canonical and submitted parser acceptance over a bounded set of terminal sequences. This is a semantic witness, not a proof of language equivalence: the reference collection is complete within its budgets and the token enumeration is deliberately finite.

Defined Under Namespace

Classes: CanonicalMachine, Difference, Machine, Result

Instance Method Summary collapse

Constructor Details

#initialize(grammar, target, max_tokens: 6, max_cases: 10_000, max_states: 100_000, max_items: 1_000_000) ⇒ LanguageWitness

Returns a new instance of LanguageWitness.

RBS:

  • (IR::Grammar grammar, IR::Automaton target, ?max_tokens: Integer, ?max_cases: Integer, ?max_states: Integer, ?max_items: Integer) -> void

Parameters:

  • grammar (IR::Grammar)
  • target (IR::Automaton)
  • max_tokens: (Integer) (defaults to: 6)
  • max_cases: (Integer) (defaults to: 10_000)
  • max_states: (Integer) (defaults to: 100_000)
  • max_items: (Integer) (defaults to: 1_000_000) 


61
62
63
64
65
66
67
68
69
70
71
72
73
 
# File 'lib/ibex/verify/language_witness.rb', line 61

def initialize(grammar, target, max_tokens: 6, max_cases: 10_000, max_states: 100_000,
               max_items: 1_000_000)
  raise ArgumentError, "max_tokens must be nonnegative" if max_tokens.negative?
  raise ArgumentError, "max_cases must be positive" unless max_cases.positive?

  @grammar = grammar
  @target = target
  @max_tokens = max_tokens
  @max_cases = max_cases
  @canonical = CanonicalMachine.new(
    grammar, max_states: max_states, max_items: max_items
  )
end

Instance Method Details

#input_tokens ⇒ Array[IR::GrammarSymbol]

RBS:

  • () -> Array[IR::GrammarSymbol]

Returns:



96
97
98
 
# File 'lib/ibex/verify/language_witness.rb', line 96

def input_tokens
  @grammar.terminals.reject { |terminal| ["$eof", "error"].include?(terminal.name) }
end

#simulate_target(entry, tokens) ⇒ witness_status

RBS:

  • (String entry, Array[Integer]) -> witness_status

Parameters:

  • entry (String)
  • (Array[Integer])

Returns:

  • (witness_status) 


132
133
134
135
136
137
138
 
# File 'lib/ibex/verify/language_witness.rb', line 132

def simulate_target(entry, tokens)
  initial = @target.entry_states[entry]
  return :missing_entry unless initial

  machine = Machine.new(@target.states, @grammar)
  machine.simulate(initial, tokens)
end

#token_name(id) ⇒ String

RBS:

  • (Integer id) -> String

Parameters:

  • id (Integer)

Returns:

  • (String) 


127
128
129
 
# File 'lib/ibex/verify/language_witness.rb', line 127

def token_name(id)
  @grammar.symbol_by_id(id)&.name || raise(Ibex::Error, "missing terminal #{id}")
end

#verify ⇒ Result

RBS:

  • () -> Result

Returns:



76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
 
# File 'lib/ibex/verify/language_witness.rb', line 76

def verify
  differences = [] #: Array[Difference]
  explored = 0
  truncated = false
  token_ids = input_tokens.map(&:id)

  @grammar.starts.each do |entry|
    explored, truncated = verify_entry(entry, token_ids, differences, explored)
    break if truncated
  end

  Result.new(
    differences: differences.freeze, explored: explored, truncated: truncated,
    max_tokens: @max_tokens, max_cases: @max_cases
  )
end

#verify_entry(entry, token_ids, differences, explored) ⇒ [ Integer, bool ]

RBS:

  • (String, Array[Integer], Array[Difference], Integer) -> [Integer, bool]

Parameters:

  • (String)
  • (Array[Integer])
  • (Array[Difference])
  • (Integer)

Returns:

  • ([ Integer, bool ]) 


101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
 
# File 'lib/ibex/verify/language_witness.rb', line 101

def verify_entry(entry, token_ids, differences, explored)
  queue = [[]] #: Array[Array[Integer]]
  until queue.empty?
    tokens = queue.shift
    return [explored, true] if explored >= @max_cases

    explored += 1
    canonical = @canonical.simulate(entry, tokens)
    target = simulate_target(entry, tokens)
    if canonical != target
      differences << Difference.new(
        entry: entry, tokens: tokens.map { |id| token_name(id) },
        canonical: canonical, target: target
      )
      return [explored, false]
    end

    # Keep the worklist breadth-first so a reported witness is as short
    # as possible for each entry.
    queue.concat(token_ids.map { |token_id| tokens + [token_id] }) if
      tokens.length < @max_tokens
  end
  [explored, false]
end