Class: Ibex::VerificationReport::Builder

Inherits:
Object
  • Object
show all
Defined in:
lib/ibex/verification_report/builder.rb

Overview

Builds deterministic evidence from an Automaton IR verification run.

Instance Method Summary collapse

Constructor Details

#initialize(automaton, table:, source_records:, table_path:, strict:, max_states:, max_items:) ⇒ Builder

Returns a new instance of Builder.

Raises:

  • (ArgumentError) 


19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
 
# File 'lib/ibex/verification_report/builder.rb', line 19

def initialize(automaton, table:, source_records:, table_path:, strict:, max_states:, max_items:)
  raise ArgumentError, "source_records must not be empty" if source_records.empty?
  if source_records.length > LogicalPath::MAX_INPUT_FILES
    raise ArgumentError, "verification reports support at most #{LogicalPath::MAX_INPUT_FILES} input files"
  end
  raise ArgumentError, "max_states must be positive" unless max_states.is_a?(Integer) && max_states.positive?
  raise ArgumentError, "max_items must be positive" unless max_items.is_a?(Integer) && max_items.positive?

  @automaton = CanonicalIR.new(automaton, source_records: source_records).build
  @table = table
  @source_records = source_records
  @table_path = LogicalPath.table(table_path)
  @strict = strict
  @max_states = max_states
  @max_items = max_items
end

Instance Method Details

#render ⇒ Object 



37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
 
# File 'lib/ibex/verification_report/builder.rb', line 37

def render
  validate_table_identity!
  document = {
    "ibex_report" => IDENTIFIER,
    "schema_version" => SCHEMA_VERSION,
    "checker" => { "name" => "ibex.verify", "version" => Ibex::VERSION },
    "profile" => @strict ? "strict" : "default",
    "bounds" => bounds.transform_keys(&:to_s),
    "input" => input_identity,
    "ir" => ir_identity,
    "table" => table_identity,
    "outcome" => verification_outcome,
    "excluded_trust" => EXCLUDED_TRUST
  }
  document["evidence_digest"] = TableArtifact::Serializer.digest(document)
  TableArtifact::Serializer.dump(document)
end