Module: Ibex::VerificationReport

Defined in:
lib/ibex/verification_report.rb,
lib/ibex/verification_report/builder.rb,
lib/ibex/verification_report/validator.rb,
lib/ibex/verification_report/canonical_ir.rb,
lib/ibex/verification_report/logical_path.rb

Overview

A versioned, scoped report that binds bounded verification to input and data-only parser table identities without claiming to verify opaque code.

Defined Under Namespace

Modules: LogicalPath Classes: Builder, CanonicalIR, ValidationError, Validator

Constant Summary collapse

IDENTIFIER =

: String

"scoped_verification"
SCHEMA_VERSION =

: Integer

1
IR_IDENTITY_SCOPE =

: String

"source-logical-v1"
DEFAULT_MAX_STATES =

: Integer

100_000
DEFAULT_MAX_ITEMS =

: Integer

1_000_000
EXCLUDED_TRUST = 
%w[
  source_to_ir table_semantic_derivation generated_wrapper semantic_actions lexer_actions
  runtime application_hooks grammar_unambiguity
].freeze

Class Method Summary collapse

Class Method Details

.canonical_automaton(automaton, source_records:) ⇒ Object

Rebuild the supplied Automaton IR with path-neutral source locations for one bundle.



33
34
35
 
# File 'lib/ibex/verification_report.rb', line 33

def canonical_automaton(automaton, source_records:)
  CanonicalIR.new(automaton, source_records: source_records).build
end

.render(automaton, table:, source_records:, table_path:, strict: false, max_states: DEFAULT_MAX_STATES, max_items: DEFAULT_MAX_ITEMS) ⇒ Object 



40
41
42
43
44
45
46
 
# File 'lib/ibex/verification_report.rb', line 40

def render(automaton, table:, source_records:, table_path:, strict: false,
           max_states: DEFAULT_MAX_STATES, max_items: DEFAULT_MAX_ITEMS)
  Builder.new(
    automaton, table: table, source_records: source_records, table_path: table_path,
               strict: strict, max_states: max_states, max_items: max_items
  ).render
end

.validate(source) ⇒ Object

Validate the closed report shape and its canonical evidence digest.



50
51
52
 
# File 'lib/ibex/verification_report.rb', line 50

def validate(source)
  Validator.new.validate(source)
end

.validate_bundle(manifest_source:, report_source:, table_source:) ⇒ Object

Validate report, table, and manifest bytes as one non-cyclic bundle.



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

def validate_bundle(manifest_source:, report_source:, table_source:)
  Validator.new.validate_bundle(
    manifest_source: manifest_source, report_source: report_source, table_source: table_source
  )
end

.validate_bundle_file(manifest_path) ⇒ Object

Resolve the report and table through a manifest and validate every published artifact before checking the cross-artifact identities.



65
66
67
 
# File 'lib/ibex/verification_report.rb', line 65

def validate_bundle_file(manifest_path)
  Validator.new.validate_bundle_file(manifest_path)
end