Class: Ibex::VerificationReport::Builder

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

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.

RBS:

  • (IR::Automaton automaton, table: TableArtifact::Document, source_records: Array[GenerationInput], table_path: String, strict: bool, max_states: Integer, max_items: Integer) -> void

Parameters:



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

#automaton_digest ⇒ String

RBS:

  • () -> String

Returns:

  • (String) 


144
145
146
 
# File 'lib/ibex/verification_report/builder.rb', line 144

def automaton_digest
  @automaton_digest ||= "sha256:#{Digest::SHA256.hexdigest(IR::Serialize.dump(@automaton))}"
end

#bounds ⇒ Hash[Symbol, Integer]

RBS:

  • () -> Hash[Symbol, Integer]

Returns:

  • (Hash[Symbol, Integer]) 


58
59
60
 
# File 'lib/ibex/verification_report/builder.rb', line 58

def bounds
  { max_states: @max_states, max_items: @max_items }
end

#grammar_digest ⇒ String

RBS:

  • () -> String

Returns:

  • (String) 


139
140
141
 
# File 'lib/ibex/verification_report/builder.rb', line 139

def grammar_digest
  @grammar_digest ||= "sha256:#{Digest::SHA256.hexdigest(IR::Serialize.dump(@automaton.grammar))}"
end

#input_identity ⇒ Hash[String, json_value]

RBS:

  • () -> Hash[String, json_value]

Returns:

  • (Hash[String, json_value]) 


90
91
92
93
94
95
96
97
98
99
 
# File 'lib/ibex/verification_report/builder.rb', line 90

def input_identity
  files = @source_records.map.with_index do |record, index|
    {
      "logical_path" => LogicalPath.input(record.path, index),
      "sha256" => prefixed_digest(record.sha256),
      "bytesize" => record.bytesize
    }
  end
  { "digest" => TableArtifact::Serializer.digest(files), "files" => files }
end

#ir_identity ⇒ Hash[String, json_value]

RBS:

  • () -> Hash[String, json_value]

Returns:

  • (Hash[String, json_value]) 


102
103
104
105
106
107
108
109
110
111
112
113
114
115
 
# File 'lib/ibex/verification_report/builder.rb', line 102

def ir_identity
  {
    "identity_scope" => IR_IDENTITY_SCOPE,
    "grammar" => {
      "schema_version" => @automaton.grammar.schema_version,
      "digest" => grammar_digest
    },
    "automaton" => {
      "schema_version" => @automaton.schema_version,
      "algorithm" => @automaton.algorithm,
      "digest" => automaton_digest
    }
  }
end

#prefixed_digest(digest) ⇒ String

RBS:

  • (String digest) -> String

Parameters:

  • digest (String)

Returns:

  • (String) 


149
150
151
 
# File 'lib/ibex/verification_report/builder.rb', line 149

def prefixed_digest(digest)
  digest.start_with?("sha256:") ? digest : "sha256:#{digest}"
end

#render ⇒ String

RBS:

  • () -> String

Returns:

  • (String) 


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

#requested_checks ⇒ Array[String]

RBS:

  • () -> Array[String]

Returns:

  • (Array[String]) 


63
64
65
 
# File 'lib/ibex/verification_report/builder.rb', line 63

def requested_checks
  Verify::Verifier::DEFAULT_CHECKS + (@strict ? Verify::Verifier::STRICT_CHECKS : [])
end

#stringify_keys(value) ⇒ Hash[String, String]

RBS:

  • (Hash[Symbol, String] value) -> Hash[String, String]

Parameters:

  • value (Hash[Symbol, String])

Returns:

  • (Hash[String, String]) 


154
155
156
 
# File 'lib/ibex/verification_report/builder.rb', line 154

def stringify_keys(value)
  value.to_h { |key, child| [key.to_s, child] }
end

#table_identity ⇒ Hash[String, json_value]

RBS:

  • () -> Hash[String, json_value]

Returns:

  • (Hash[String, json_value]) 


118
119
120
121
122
123
124
125
126
127
 
# File 'lib/ibex/verification_report/builder.rb', line 118

def table_identity
  {
    "logical_path" => @table_path,
    "artifact_type" => TableArtifact::ARTIFACT_TYPE,
    "schema_version" => TableArtifact::SCHEMA_VERSION,
    "representation" => @table.payload.dig("table_format", "representation"),
    "artifact_digest" => prefixed_digest(Digest::SHA256.hexdigest(@table.dump)),
    "payload_digest" => @table.identity.fetch("payload_digest")
  }
end

#validate_table_identity! ⇒ void

This method returns an undefined value.

RBS:

  • () -> void



130
131
132
133
134
135
136
 
# File 'lib/ibex/verification_report/builder.rb', line 130

def validate_table_identity!
  identity = @table.identity
  return if identity.fetch("grammar_digest") == grammar_digest &&
            identity.fetch("automaton_digest") == automaton_digest

  raise ArgumentError, "table artifact does not match the supplied Automaton IR"
end

#verification_outcome ⇒ Hash[String, json_value]

RBS:

  • () -> Hash[String, json_value]

Returns:

  • (Hash[String, json_value]) 


68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
 
# File 'lib/ibex/verification_report/builder.rb', line 68

def verification_outcome
  result = Verify::Verifier.new(
    @automaton, strict: @strict, max_states: @max_states, max_items: @max_items
  ).verify
  {
    "status" => result.valid? ? "pass" : "violations",
    "requested_checks" => requested_checks,
    "executed_checks" => result.checks,
    "violations" => result.violations.map { |violation| stringify_keys(violation.to_h) },
    "exhaustion" => nil
  }
rescue Verify::BudgetExceeded => e
  {
    "status" => "exhausted",
    "requested_checks" => requested_checks,
    "executed_checks" => [],
    "violations" => [],
    "exhaustion" => { "kind" => "reference_collection_budget", "message" => e.message }
  }
end