necoherence - v0.2.0

necoherence/semantic_composition

Types

AvailableValue 

pub type AvailableValue {
  AvailableValue(
    producer: ProducerRef,
    contract: semantic_types.SlotContract,
    resource: option.Option(ResourceLotRef),
  )
}

Constructors

BindingCompatibility 

pub type BindingCompatibility {
  Inclusion(certificate: InclusionCertificate)
  SuppliedBindingValue(
    value: semantic_types.SlotValue(exact_json.JsonValue),
  )
}

Constructors

BindingExpr 

pub type BindingExpr {
  Source(
    value: ValueRef,
    projection: semantic_validation.ProjectionCertificate,
    compatibility: BindingCompatibility,
  )
  Product(
    construction: String,
    type_ref: semantic_types.TypeRef,
    fields: List(#(String, BindingExpr)),
  )
}

Constructors

BranchFact 

pub type BranchFact {
  BranchFact(
    guard: GuardId,
    inspected: ValueRef,
    arm: GuardArm,
    refinement: option.Option(semantic_types.SlotContract),
    assumptions: List(semantic_validation.ProjectionAssumption),
    exact: option.Option(
      semantic_types.SlotValue(exact_json.JsonValue),
    ),
  )
}

Constructors

BranchTrace 

pub type BranchTrace {
  BranchTrace(steps: List(TraceStep), terminal: ReturnPlan)
}

Constructors

CandidateBudget 

pub type CandidateBudget {
  CandidateBudget(
    bindings: Int,
    branch_nodes: Int,
    exhausted_bindings: Bool,
    exhausted_branches: Bool,
  )
}

Constructors 

  • CandidateBudget(
  bindings: Int,
  branch_nodes: Int,
  exhausted_bindings: Bool,
  exhausted_branches: Bool,
)

CandidateTree 

pub type CandidateTree {
  CandidateTree(
    tree: PlanTree,
    success: Bool,
    certificates: List(ResourceTraceCertificate),
    nodes: Int,
  )
}

Constructors

CheckedAcyclic

opaque 
pub opaque type CheckedAcyclic

CheckedClosure

opaque 
pub opaque type CheckedClosure

CheckedComposition

opaque 
pub opaque type CheckedComposition

CheckedCompositionClosure

opaque 
pub opaque type CheckedCompositionClosure

CheckedInclusion

opaque 
pub opaque type CheckedInclusion

CheckedReachability

opaque 
pub opaque type CheckedReachability

ChoiceCoverage 

pub type ChoiceCoverage {
  ChoiceCoverage(choice: ChoiceSkeleton, children: List(Int))
}

Constructors

ChoiceSkeleton 

pub type ChoiceSkeleton {
  InvocationChoice(
    invocation: InvocationPlan,
    outcomes: List(OutcomeId),
    empty_outcomes: List(OutcomeId),
  )
  GuardChoice(
    guard: GuardId,
    inspected: ValueRef,
    arms: List(GuardArm),
  )
}

Constructors

ClosedSearchState 

pub type ClosedSearchState {
  ClosedSearchState(
    state: SearchState,
    terminals: List(TerminalCoverage),
    choices: List(ChoiceCoverage),
    rejected_connections: List(ConnectionFailure),
    missing_supply: List(MissingSupply),
  )
}

Constructors

CompatibilityDecision 

pub type CompatibilityDecision {
  Compatible(certificate: InclusionCertificate)
  Incompatible(certificate: CounterexampleCertificate)
  CompatibilityUnknown(obligations: List(TypeObligation))
}

Constructors

CompositionClosureWitness 

pub type CompositionClosureWitness {
  CompositionClosureWitness(
    input_snapshot: CompositionInput,
    root: Int,
    states: List(ClosedSearchState),
  )
}

Constructors

CompositionDecision 

pub type CompositionDecision {
  Solved(
    composition: CheckedComposition,
    selection: SelectionEvidence,
  )
  Unreachable(closure: CompositionClosureWitness)
  CompositionUnknown(
    obligations: List(UnresolvedObligation),
    frontier: List(SearchState),
    rejected_connections: List(ConnectionFailure),
  )
  Ambiguous(
    candidates: List(VerifiedCompositionCandidate),
    canonical_plans: List(String),
  )
}

Constructors

CompositionEffect 

pub type CompositionEffect {
  PureFunction
  HttpRequestResponse
  DataOnly
}

Constructors 

  • PureFunction
  • HttpRequestResponse
  • DataOnly

CompositionEngineFailure 

pub type CompositionEngineFailure {
  ContractViolation(reason: String)
  ResourceFailure(failure: typed_mapping.SolverFailure)
  Witness(failure: WitnessFailure)
}

Constructors

CompositionInput 

pub type CompositionInput {
  CompositionInput(
    identity: String,
    revision: String,
    basis: SemanticBasis,
    signatures: List(FunctionSignature),
    initial_inputs: List(InitialInput),
    initial_resources: List(ResourceLot),
    goal: GoalSpec,
    invocation_domain: InvocationDomain,
    allowed_effects: List(CompositionEffect),
    explicit_order: List(#(SiteId, SiteId)),
    selection_policy: option.Option(SelectionPolicy),
    bounds: SearchBounds,
  )
}

Constructors

CompositionInputFailure 

pub type CompositionInputFailure {
  InputBasisMismatch
  DuplicateIdentity(kind: String, identity: String)
  UnresolvedType(reference: semantic_types.TypeRef)
  UnresolvedFunction(reference: FunctionRef)
  InvalidSignature(function: FunctionRef, reason: String)
  InvalidInitialValue(
    input: InputId,
    failure: semantic_types.ValueFailure,
  )
  InvalidInitialCertificate(input: InputId, condition: String)
  InvalidInvocationDomain(reason: String)
  InvalidResourceDeclaration(reason: String)
  InvalidBound(reason: String)
  OperationEffectMismatch(
    operation: semantic_types.DefinitionRef,
    expected: CompositionEffect,
    supplied: CompositionEffect,
  )
}

Constructors

CompositionPlan 

pub type CompositionPlan {
  CompositionPlan(
    input_identity: String,
    input_revision: String,
    root: PlanTree,
  )
}

Constructors 

  • CompositionPlan(
  input_identity: String,
  input_revision: String,
  root: PlanTree,
)

CompositionWitness 

pub type CompositionWitness {
  CompositionWitness(
    input_snapshot: CompositionInput,
    initial_membership: List(
      #(InputId, semantic_types.SlotValue(exact_json.JsonValue)),
    ),
    resource_traces: List(ResourceTraceCertificate),
  )
}

Constructors

ConnectionFailure 

pub type ConnectionFailure {
  ConnectionFailure(
    value: option.Option(ValueRef),
    destination: semantic_types.SlotContract,
    counterexample: CounterexampleCertificate,
  )
}

Constructors

ConstructionRule 

pub type ConstructionRule {
  ConstructionRule(
    identity: String,
    type_ref: semantic_types.TypeRef,
    nested_fields: List(#(String, String)),
    field_constraints: List(FieldConstraint),
  )
}

Constructors

CounterexampleCertificate 

pub type CounterexampleCertificate {
  CounterexampleCertificate(
    basis: SemanticBasis,
    source: semantic_types.SlotContract,
    destination: semantic_types.SlotContract,
    value: semantic_types.SlotValue(exact_json.JsonValue),
    destination_failure: semantic_types.ValueFailure,
  )
}

Constructors

DeclaredGuard 

pub type DeclaredGuard {
  DeclaredGuard(
    id: GuardId,
    source_type: semantic_types.TypeRef,
    path: List(semantic_types.PathStep),
    kind: GuardKind,
  )
}

Constructors

Enumeration 

pub type Enumeration {
  Enumeration(
    terminals: List(ReturnPlan),
    choices: List(ChoiceSkeleton),
    unknown: List(UnresolvedObligation),
    failures: List(ConnectionFailure),
    missing: List(MissingSupply),
    budget: CandidateBudget,
  )
}

Constructors

FailureEmbedding 

pub type FailureEmbedding {
  FailureEmbedding(
    id: FailureEmbeddingId,
    origin: FailureOrigin,
    contract: semantic_types.SlotContract,
    final_resources: List(ResourceGoal),
  )
}

Constructors

FailureEmbeddingId 

pub type FailureEmbeddingId {
  FailureEmbeddingId(value: String)
}

Constructors 

  • FailureEmbeddingId(value: String)

FailureOrigin 

pub type FailureOrigin {
  FunctionFailure(function: FunctionRef, outcome: OutcomeId)
  GuardFailure(guard: GuardId, arm: GuardArm)
}

Constructors

FieldConstraint 

pub type FieldConstraint {
  FieldConstraint(
    field: String,
    source: SourceConstraint,
    presence: FieldPresence,
  )
}

Constructors

FieldPresence 

pub type FieldPresence {
  Required
  Optional
}

Constructors 

  • Required
  • Optional

FunctionForm 

pub type FunctionForm {
  Pure
  Operation(reference: semantic_types.DefinitionRef)
  DeclaredTransform
}

Constructors

FunctionRef 

pub type FunctionRef {
  FunctionRef(
    identity: String,
    revision: String,
    content_digest: String,
  )
}

Constructors 

  • FunctionRef(
  identity: String,
  revision: String,
  content_digest: String,
)

FunctionSignature 

pub type FunctionSignature {
  FunctionSignature(
    reference: FunctionRef,
    form: FunctionForm,
    effect: CompositionEffect,
    inputs: List(InputPort),
    outcomes: List(OutcomeContract),
    resource_inputs: List(ResourceRequirement),
    assumption_ref: String,
    handles_failure: option.Option(FailureOrigin),
  )
}

Constructors

GoalPort 

pub type GoalPort {
  GoalPort(
    id: GoalPortId,
    contract: semantic_types.SlotContract,
    source_constraint: SourceConstraint,
  )
}

Constructors

GoalPortId 

pub type GoalPortId {
  GoalPortId(value: String)
}

Constructors 

  • GoalPortId(value: String)

GoalSpec 

pub type GoalSpec {
  GoalSpec(
    outputs: List(GoalPort),
    failures: List(FailureEmbedding),
    final_resources: List(ResourceGoal),
  )
}

Constructors

GuardArm 

pub type GuardArm {
  GuardPresent
  GuardAbsent
  GuardNull
  GuardVariant(tag: String)
  UnknownVariant
  GuardAccepted
  GuardRejected
}

Constructors 

  • GuardPresent
  • GuardAbsent
  • GuardNull
  • GuardVariant(tag: String)
  • UnknownVariant
  • GuardAccepted
  • GuardRejected

GuardId 

pub type GuardId {
  GuardId(value: String)
}

Constructors 

  • GuardId(value: String)

GuardKind 

pub type GuardKind {
  Presence
  Variants
  Validate(contract: semantic_types.SlotContract)
}

Constructors

InclusionCertificate 

pub type InclusionCertificate {
  InclusionCertificate(
    basis: SemanticBasis,
    source: semantic_types.SlotContract,
    destination: semantic_types.SlotContract,
    root: Int,
    empty_types: List(semantic_types.TypeRef),
    pairs: List(PairEntry),
  )
}

Constructors

InclusionFailure 

pub type InclusionFailure {
  InclusionBasisMismatch
  ContractMismatch
  UndefinedMeaning(
    obligations: List(semantic_types.SemanticObligation),
  )
  MissingPair
  PairMismatch(index: Int)
  RuleMismatch(index: Int)
  ChildCoverage(index: Int)
  ForgedEmptiness
  CounterexampleMismatch
  InclusionUnresolved(obligation: TypeObligation)
}

Constructors 

  • InclusionBasisMismatch
  • ContractMismatch
  • UndefinedMeaning(
  obligations: List(semantic_types.SemanticObligation),
)
  • MissingPair
  • PairMismatch(index: Int)
  • RuleMismatch(index: Int)
  • ChildCoverage(index: Int)
  • ForgedEmptiness
  • CounterexampleMismatch
  • InclusionUnresolved(obligation: TypeObligation)

InclusionRule 

pub type InclusionRule {
  EmptySource
  InclusionBoolean
  IntegerIntersection
  FiniteStrings
  StringConditions
  BytesLength
  InclusionUnit
  JsonDomain
  PlainObjectDomain
  UnfoldSource
  UnfoldDestination
  InclusionArray
  InclusionProduct
  SourceUnion
  DestinationUnion
  SourceRecord
  DestinationRecord
  ProductTagCases
}

Constructors 

  • EmptySource
  • InclusionBoolean
  • IntegerIntersection
  • FiniteStrings
  • StringConditions
  • BytesLength
  • InclusionUnit
  • JsonDomain
  • PlainObjectDomain
  • UnfoldSource
  • UnfoldDestination
  • InclusionArray
  • InclusionProduct
  • SourceUnion
  • DestinationUnion
  • SourceRecord
  • DestinationRecord
  • ProductTagCases

InitialInput 

pub type InitialInput {
  InitialInput(
    id: InputId,
    contract: semantic_types.SlotContract,
    source: InitialSource,
    resource: option.Option(LotId),
  )
}

Constructors

InitialSource 

pub type InitialSource {
  Argument
  SuppliedValue(
    value: semantic_types.SlotValue(exact_json.JsonValue),
  )
}

Constructors

InputId 

pub type InputId {
  InputId(value: String)
}

Constructors 

  • InputId(value: String)

InputPort 

pub type InputPort {
  InputPort(
    id: PortId,
    contract: semantic_types.SlotContract,
    source_constraint: SourceConstraint,
    resource_requirement: option.Option(RequirementId),
  )
}

Constructors

InvocationDomain 

pub type InvocationDomain {
  InvocationDomain(
    identity: String,
    revision: String,
    sites: List(InvocationSite),
    permitted_projections: List(PermittedProjection),
    permitted_constructions: List(ConstructionRule),
    permitted_transforms: List(FunctionRef),
    guards: List(DeclaredGuard),
  )
}

Constructors

InvocationPlan 

pub type InvocationPlan {
  InvocationPlan(
    site: SiteId,
    function: FunctionRef,
    bindings: List(#(PortId, BindingExpr)),
    resources: List(ResourceBinding),
  )
}

Constructors

InvocationSite 

pub type InvocationSite {
  InvocationSite(id: SiteId, function: FunctionRef)
}

Constructors

LotId 

pub type LotId {
  LotId(value: String)
}

Constructors 

  • LotId(value: String)

LoweringFailure 

pub type LoweringFailure {
  InvalidLowering(reason: String)
  UnknownLowering(obligation: UnresolvedObligation)
}

Constructors

MissingSupply 

pub type MissingSupply {
  MissingSupply(
    site: option.Option(SiteId),
    port: String,
    contract: semantic_types.SlotContract,
  )
}

Constructors

NormalizedResourceBinding 

pub type NormalizedResourceBinding {
  NormalizedResourceBinding(
    transition: String,
    lot: ResourceLotRef,
    read: Int,
    consume: Int,
    required_revision: Int,
  )
}

Constructors 

  • NormalizedResourceBinding(
  transition: String,
  lot: ResourceLotRef,
  read: Int,
  consume: Int,
  required_revision: Int,
)

OutcomeContract 

pub type OutcomeContract {
  OutcomeContract(
    id: OutcomeId,
    form: OutcomeForm,
    value_ports: List(OutputPort),
    produced_resources: List(ResourceProduction),
  )
}

Constructors

OutcomeForm 

pub type OutcomeForm {
  Success
  DeclaredFailure
}

Constructors 

  • Success
  • DeclaredFailure

OutcomeId 

pub type OutcomeId {
  OutcomeId(value: String)
}

Constructors 

  • OutcomeId(value: String)

OutputPort 

pub type OutputPort {
  OutputPort(
    id: PortId,
    contract: semantic_types.SlotContract,
    resource_production: option.Option(ProductionId),
  )
}

Constructors

PairEntry 

pub type PairEntry {
  PairEntry(
    pair: TypePair,
    source_shape: semantic_types.TypeShape,
    destination_shape: semantic_types.TypeShape,
    rule: InclusionRule,
    children: List(Int),
  )
}

Constructors

PermittedProjection 

pub type PermittedProjection {
  PermittedProjection(
    source_type: semantic_types.TypeRef,
    path: List(semantic_types.PathStep),
  )
}

Constructors

PlanNode 

pub type PlanNode {
  Invoke(
    invocation: InvocationPlan,
    arms: List(#(OutcomeId, PlanTree)),
    empty_outcomes: List(OutcomeId),
  )
  Guard(
    guard: GuardId,
    inspected: ValueRef,
    arms: List(#(GuardArm, PlanTree)),
  )
  Return(terminal: ReturnPlan)
}

Constructors

PlanTree 

pub type PlanTree {
  PlanTree(rank: Int, node: PlanNode)
}

Constructors

PortId 

pub type PortId {
  PortId(value: String)
}

Constructors 

  • PortId(value: String)

PreparedCompositionInput

opaque 
pub opaque type PreparedCompositionInput

ProducerRef 

pub type ProducerRef {
  Initial(id: InputId)
  InvocationOutcome(
    site: SiteId,
    outcome: OutcomeId,
    port: PortId,
  )
}

Constructors

ProductionId 

pub type ProductionId {
  ProductionId(value: String)
}

Constructors 

  • ProductionId(value: String)

RawComposition 

pub type RawComposition {
  RawComposition(
    plan: CompositionPlan,
    witness: CompositionWitness,
    selection: SelectionEvidence,
  )
}

Constructors

RequirementId 

pub type RequirementId {
  RequirementId(value: String)
}

Constructors 

  • RequirementId(value: String)

ResourceBinding 

pub type ResourceBinding {
  ResourceBinding(
    requirement: RequirementId,
    lot: ResourceLotRef,
    inclusion: InclusionCertificate,
  )
}

Constructors

ResourceBounds 

pub type ResourceBounds {
  ResourceBounds(
    max_bindings: Int,
    max_search_steps: Int,
    max_tokens: Int,
  )
}

Constructors 

  • ResourceBounds(
  max_bindings: Int,
  max_search_steps: Int,
  max_tokens: Int,
)

ResourceCorrespondence 

pub type ResourceCorrespondence {
  ResourceCorrespondence(
    lots: List(ResourceLotCorrespondence),
    values: List(ValueCorrespondence),
    normalized_bindings: List(NormalizedResourceBinding),
    execution_order: List(String),
  )
}

Constructors

ResourceGoal 

pub type ResourceGoal {
  ResourceGoal(
    lot: ResourceLotRef,
    multiplicity: Int,
    revision: Int,
  )
}

Constructors 

  • ResourceGoal(
  lot: ResourceLotRef,
  multiplicity: Int,
  revision: Int,
)

ResourceIdentityConstraint 

pub type ResourceIdentityConstraint {
  AnyResource
  Exactly(producer: ResourceProducer)
}

Constructors

ResourceLot 

pub type ResourceLot {
  ResourceLot(
    id: LotId,
    token_type: semantic_types.TypeRef,
    producer: ResourceProducer,
    revision: Int,
    quantity: Int,
    provenance: String,
  )
}

Constructors

ResourceLotCorrespondence 

pub type ResourceLotCorrespondence {
  ResourceLotCorrespondence(
    lot: ResourceLotRef,
    place: String,
    producer: ResourceProducer,
    token_target: String,
    token_type: String,
    revision: Int,
    quantity: Int,
    provenance: String,
  )
}

Constructors 

  • ResourceLotCorrespondence(
  lot: ResourceLotRef,
  place: String,
  producer: ResourceProducer,
  token_target: String,
  token_type: String,
  revision: Int,
  quantity: Int,
  provenance: String,
)

ResourceLotRef 

pub type ResourceLotRef {
  InitialLot(id: LotId)
  ProducedLot(
    site: SiteId,
    outcome: OutcomeId,
    production: ProductionId,
  )
}

Constructors

ResourceProducer 

pub type ResourceProducer {
  InitialResource(identity: String, revision: String)
  OutcomeResource(site: SiteId, outcome: OutcomeId)
}

Constructors 

  • InitialResource(identity: String, revision: String)
  • OutcomeResource(site: SiteId, outcome: OutcomeId)

ResourceProduction 

pub type ResourceProduction {
  ResourceProduction(
    id: ProductionId,
    token_type: semantic_types.TypeRef,
    revision: Int,
    quantity: Int,
    provenance: String,
  )
}

Constructors

ResourceRequirement 

pub type ResourceRequirement {
  ResourceRequirement(
    id: RequirementId,
    token_type: semantic_types.TypeRef,
    mode: typed_mapping.BindingMode,
    multiplicity: Int,
    required_revision: Int,
    identity: ResourceIdentityConstraint,
  )
}

Constructors

ResourceTraceCertificate 

pub type ResourceTraceCertificate {
  ResourceTraceCertificate(
    trace: BranchTrace,
    lowering: typed_mapping.SolverInput,
    correspondence: ResourceCorrespondence,
    reachability: typed_mapping.ReachabilityWitness,
    acyclicity: typed_mapping.AcyclicWitness,
    value_sources: List(
      #(
        ProducerRef,
        semantic_types.SlotValue(exact_json.JsonValue),
      ),
    ),
  )
}

Constructors

ReturnPlan 

pub type ReturnPlan {
  ReturnSuccess(outputs: List(#(GoalPortId, BindingExpr)))
  ReturnFailure(
    embedding: FailureEmbeddingId,
    value: BindingExpr,
  )
}

Constructors

SampleObligation 

pub type SampleObligation {
  SampleBound
}

Constructors 

  • SampleBound

SampleResult 

pub type SampleResult(a) {
  SampleResult(
    values: List(a),
    obligations: List(SampleObligation),
  )
}

Constructors

SearchBounds 

pub type SearchBounds {
  SearchBounds(
    max_expanded_states: Int,
    max_binding_candidates: Int,
    max_type_obligations: Int,
    max_branch_nodes: Int,
    resource_bounds: option.Option(ResourceBounds),
    max_sample_length: Int,
  )
}

Constructors 

  • SearchBounds(
  max_expanded_states: Int,
  max_binding_candidates: Int,
  max_type_obligations: Int,
  max_branch_nodes: Int,
  resource_bounds: option.Option(ResourceBounds),
  max_sample_length: Int,
)

SearchState 

pub type SearchState {
  SearchState(
    available: List(AvailableValue),
    used_sites: List(SiteId),
    used_guards: List(GuardId),
    facts: List(BranchFact),
    trace: List(TraceStep),
    pending_failure: option.Option(FailureOrigin),
  )
}

Constructors

SelectionEvidence 

pub type SelectionEvidence {
  AnyFeasibleEvidence
  Unique(
    closure: CompositionClosureWitness,
    canonical_plan: String,
  )
}

Constructors

SelectionPolicy 

pub type SelectionPolicy {
  RequireUnique
  AnyFeasible
}

Constructors 

  • RequireUnique
  • AnyFeasible

SemanticBasis 

pub type SemanticBasis {
  SemanticBasis(
    profile: semantic_types.SemanticProfile,
    sources: List(semantic_types.SourceRef),
  )
}

Constructors

SiteId 

pub type SiteId {
  SiteId(value: String)
}

Constructors 

  • SiteId(value: String)

SourceConstraint 

pub type SourceConstraint {
  AnyCompatible
  InitialOnly(
    input: InputId,
    path: List(semantic_types.PathStep),
  )
  ProducedBy(
    site: SiteId,
    outcome: OutcomeId,
    port: PortId,
    path: List(semantic_types.PathStep),
  )
}

Constructors

TerminalAssessment 

pub type TerminalAssessment {
  Feasible(certificate: ResourceTraceCertificate)
  ResourceUnreachable(
    trace: BranchTrace,
    lowering: typed_mapping.SolverInput,
    correspondence: ResourceCorrespondence,
    closure: typed_mapping.ClosureWitness,
  )
  RejectedLowering(trace: BranchTrace, reason: String)
  EmptyValues(producers: List(ProducerRef))
  TerminalUnknown(obligations: List(UnresolvedObligation))
}

Constructors

TerminalCoverage 

pub type TerminalCoverage {
  TerminalCoverage(
    terminal: ReturnPlan,
    assessment: TerminalAssessment,
  )
}

Constructors

TraceStep 

pub type TraceStep {
  InvocationStep(invocation: InvocationPlan, outcome: OutcomeId)
  GuardStep(guard: GuardId, inspected: ValueRef, arm: GuardArm)
}

Constructors

TypeObligation 

pub type TypeObligation {
  TypeObligation(
    pair: TypePair,
    path: List(semantic_types.PathStep),
    reason: TypeObligationReason,
  )
}

Constructors

TypeObligationReason 

pub type TypeObligationReason {
  TypeMeaning(
    obligations: List(semantic_types.SemanticObligation),
  )
  ConstraintImplication
  TypePresence
  UnionRemainder
  ExtraField(name: String)
  TypeInhabitation
  ObligationBoundExhausted
}

Constructors 

  • TypeMeaning(obligations: List(semantic_types.SemanticObligation))
  • ConstraintImplication
  • TypePresence
  • UnionRemainder
  • ExtraField(name: String)
  • TypeInhabitation
  • ObligationBoundExhausted

TypePair 

pub type TypePair {
  TypePair(
    source: semantic_types.SlotContract,
    destination: semantic_types.SlotContract,
    source_tag: option.Option(String),
  )
}

Constructors

UnresolvedObligation 

pub type UnresolvedObligation {
  UnresolvedTypeObligation(
    value: option.Option(ValueRef),
    obligations: List(TypeObligation),
  )
  UnresolvedMeaning(
    obligations: List(semantic_types.SemanticObligation),
  )
  InvalidValidationCertificate(condition: String)
  Inhabitation(
    producer: ProducerRef,
    contract: semantic_types.SlotContract,
  )
  BranchInhabitation
  StateBoundExhausted
  BindingBoundExhausted
  BranchBoundExhausted
  ResourceSolverUnknown(reason: typed_mapping.UnknownReason)
  ResourceCapacityBound(required: Int, limit: Int)
  UnresolvedUniqueness
}

Constructors

ValueCorrespondence 

pub type ValueCorrespondence {
  ValueCorrespondence(
    producer: ProducerRef,
    place: String,
    token_target: String,
    revision: Int,
  )
}

Constructors 

  • ValueCorrespondence(
  producer: ProducerRef,
  place: String,
  token_target: String,
  revision: Int,
)

ValueRef 

pub type ValueRef {
  ValueRef(
    producer: ProducerRef,
    path: List(semantic_types.PathStep),
  )
}

Constructors

VerifiedCompositionCandidate

opaque 
pub opaque type VerifiedCompositionCandidate

WitnessFailure 

pub type WitnessFailure {
  InputRevisionMismatch
  InitialMembership(input: InputId)
  ProducerMismatch(value: ValueRef)
  ProjectionMismatch(
    failure: semantic_validation.ProjectionFailure,
  )
  SourceConstraintMismatch(value: ValueRef)
  InclusionMismatch(failure: InclusionFailure)
  SuppliedValueMismatch(value: ValueRef)
  ConstructionMismatch(reference: semantic_types.TypeRef)
  MissingBinding(identity: String)
  SignatureMismatch(site: SiteId)
  GuardNotDominating(value: ValueRef)
  IncompleteBranchCoverage(identity: String)
  FailureEmbeddingMismatch(embedding: FailureEmbeddingId)
  GoalMismatch
  RankViolation
  ResourceLoweringMismatch(reason: String)
  ResourceReplayMismatch(reason: String)
  ForgedClosure(reason: String)
  ForgedAcyclicity(reason: String)
  MissingEvidence(reason: String)
}

Constructors 

  • InputRevisionMismatch
  • InitialMembership(input: InputId)
  • ProducerMismatch(value: ValueRef)
  • ProjectionMismatch(
  failure: semantic_validation.ProjectionFailure,
)
  • SourceConstraintMismatch(value: ValueRef)
  • InclusionMismatch(failure: InclusionFailure)
  • SuppliedValueMismatch(value: ValueRef)
  • ConstructionMismatch(reference: semantic_types.TypeRef)
  • MissingBinding(identity: String)
  • SignatureMismatch(site: SiteId)
  • GuardNotDominating(value: ValueRef)
  • IncompleteBranchCoverage(identity: String)
  • FailureEmbeddingMismatch(embedding: FailureEmbeddingId)
  • GoalMismatch
  • RankViolation
  • ResourceLoweringMismatch(reason: String)
  • ResourceReplayMismatch(reason: String)
  • ForgedClosure(reason: String)
  • ForgedAcyclicity(reason: String)
  • MissingEvidence(reason: String)

Values

acyclic_input 

pub fn acyclic_input(
  checked: CheckedAcyclic,
) -> typed_mapping.SolverInput

acyclic_witness 

pub fn acyclic_witness(
  checked: CheckedAcyclic,
) -> typed_mapping.AcyclicWitness

add_discriminator 

pub fn add_discriminator(
  tag_model: option.Option(semantic_types.TagModel),
  value: exact_json.JsonValue,
  tag: String,
) -> option.Option(exact_json.JsonValue)

at 

pub fn at(values: List(a), index: Int) -> option.Option(a)

bounded_slot_samples 

pub fn bounded_slot_samples(
  graph: semantic_types.SemanticGraph,
  contract: semantic_types.SlotContract,
  limit: Int,
  max_sample_length: Int,
) -> SampleResult(semantic_types.SlotValue(exact_json.JsonValue))

candidate_components 

pub fn candidate_components(
  prepared: PreparedCompositionInput,
  candidate: CandidateTree,
) -> Result(
  #(CompositionPlan, CompositionWitness),
  CompositionEngineFailure,
)

candidate_key 

pub fn candidate_key(
  input: CompositionInput,
  candidate: CandidateTree,
) -> String

candidate_plan 

pub fn candidate_plan(
  candidate: VerifiedCompositionCandidate,
) -> CompositionPlan

candidate_prepared 

pub fn candidate_prepared(
  candidate: VerifiedCompositionCandidate,
) -> PreparedCompositionInput

candidate_witness 

pub fn candidate_witness(
  candidate: VerifiedCompositionCandidate,
) -> CompositionWitness

check_assignable 

pub fn check_assignable(
  graph: semantic_types.SemanticGraph,
  source: semantic_types.SlotContract,
  destination: semantic_types.SlotContract,
  max_obligations: Int,
) -> CompatibilityDecision

check_assignable_bounded 

pub fn check_assignable_bounded(
  graph: semantic_types.SemanticGraph,
  source: semantic_types.SlotContract,
  destination: semantic_types.SlotContract,
  bounds: SearchBounds,
) -> CompatibilityDecision

check_function 

pub fn check_function(
  graph: semantic_types.SemanticGraph,
  input: CompositionInput,
  function: FunctionSignature,
) -> Result(Nil, CompositionInputFailure)

check_return 

pub fn check_return(
  prepared: PreparedCompositionInput,
  state: SearchState,
  terminal: ReturnPlan,
) -> Result(Bool, WitnessFailure)

checked_inclusion_certificate 

pub fn checked_inclusion_certificate(
  checked: CheckedInclusion,
) -> InclusionCertificate

checked_inclusion_graph 

pub fn checked_inclusion_graph(
  checked: CheckedInclusion,
) -> semantic_types.SemanticGraph

checked_plan 

pub fn checked_plan(
  checked: CheckedComposition,
) -> CompositionPlan

checked_prepared 

pub fn checked_prepared(
  checked: CheckedComposition,
) -> PreparedCompositionInput

checked_raw 

pub fn checked_raw(checked: CheckedComposition) -> RawComposition

checked_witness 

pub fn checked_witness(
  checked: CheckedComposition,
) -> CompositionWitness

choice_states 

pub fn choice_states(
  prepared: PreparedCompositionInput,
  state: SearchState,
  choice: ChoiceSkeleton,
) -> Result(List(SearchState), WitnessFailure)

closure_canonical_plans 

pub fn closure_canonical_plans(
  checked: CheckedCompositionClosure,
) -> List(String)

closure_witness 

pub fn closure_witness(
  checked: CheckedCompositionClosure,
) -> CompositionClosureWitness

collect 

pub fn collect(
  values: List(a),
  action: fn(a) -> Result(b, e),
) -> Result(List(b), e)

decide_ambiguous 

pub fn decide_ambiguous(
  prepared: PreparedCompositionInput,
  first: CandidateTree,
  second: CandidateTree,
) -> Result(CompositionDecision, CompositionEngineFailure)

decide_unreachable 

pub fn decide_unreachable(
  prepared: PreparedCompositionInput,
  closure: CompositionClosureWitness,
) -> Result(CompositionDecision, CompositionEngineFailure)

default_resource_token_bound 

pub const default_resource_token_bound: Int

default_search_bounds 

pub fn default_search_bounds() -> SearchBounds

distinct_candidates 

pub fn distinct_candidates(
  input: CompositionInput,
  candidates: List(CandidateTree),
) -> List(CandidateTree)

effective_projection 

pub fn effective_projection(
  prepared: PreparedCompositionInput,
  state: SearchState,
  value: ValueRef,
) -> Result(
  semantic_validation.ProjectionCertificate,
  WitnessFailure,
)

enumerate_state 

pub fn enumerate_state(
  prepared: PreparedCompositionInput,
  state: SearchState,
  budget: CandidateBudget,
) -> Enumeration

evaluate_guard_arm 

pub fn evaluate_guard_arm(
  graph: semantic_types.SemanticGraph,
  guard: DeclaredGuard,
  inspected: semantic_types.SlotValue(exact_json.JsonValue),
) -> Result(GuardArm, semantic_types.ValueDecision)

fresh_budget 

pub fn fresh_budget() -> CandidateBudget

goal_unreachable 

pub fn goal_unreachable(
  checked: CheckedCompositionClosure,
) -> Bool

guard_declaration 

pub fn guard_declaration(
  input: CompositionInput,
  id: GuardId,
) -> option.Option(DeclaredGuard)

inclusion_samples 

pub fn inclusion_samples(
  graph: semantic_types.SemanticGraph,
  source: semantic_types.TypeRef,
  destination: semantic_types.TypeRef,
  limit: Int,
) -> List(exact_json.JsonValue)

inclusion_samples_bounded 

pub fn inclusion_samples_bounded(
  graph: semantic_types.SemanticGraph,
  source: semantic_types.TypeRef,
  destination: semantic_types.TypeRef,
  bounds: SearchBounds,
) -> SampleResult(exact_json.JsonValue)

inclusion_slot_samples 

pub fn inclusion_slot_samples(
  graph: semantic_types.SemanticGraph,
  source: semantic_types.SlotContract,
  destination: semantic_types.TypeRef,
  limit: Int,
) -> List(semantic_types.SlotValue(exact_json.JsonValue))

index_of 

pub fn index_of(
  values: List(a),
  value: a,
  index: Int,
) -> option.Option(Int)

initial_state 

pub fn initial_state(
  prepared: PreparedCompositionInput,
) -> SearchState

lower_resource_trace 

pub fn lower_resource_trace(
  prepared: PreparedCompositionInput,
  trace: BranchTrace,
) -> Result(
  #(typed_mapping.SolverInput, ResourceCorrespondence),
  LoweringFailure,
)

merge_choice 

pub fn merge_choice(
  input: CompositionInput,
  state: SearchState,
  choice: ChoiceSkeleton,
  children: List(List(CandidateTree)),
  budget: CandidateBudget,
) -> #(List(CandidateTree), CandidateBudget)

prepare_composition 

pub fn prepare_composition(
  graph: semantic_types.SemanticGraph,
  input: CompositionInput,
  check_signature: fn(FunctionSignature) -> Result(
    Nil,
    CompositionInputFailure,
  ),
) -> Result(PreparedCompositionInput, CompositionInputFailure)

prepared_empty 

pub fn prepared_empty(
  prepared: PreparedCompositionInput,
) -> List(semantic_types.TypeRef)

prepared_graph 

pub fn prepared_graph(
  prepared: PreparedCompositionInput,
) -> semantic_types.SemanticGraph

prepared_initial_obligations 

pub fn prepared_initial_obligations(
  prepared: PreparedCompositionInput,
) -> List(semantic_types.SemanticObligation)

prepared_input 

pub fn prepared_input(
  prepared: PreparedCompositionInput,
) -> CompositionInput

project_owned 

pub fn project_owned(
  tag_model: option.Option(semantic_types.TagModel),
  value: semantic_types.SlotValue(exact_json.JsonValue),
  path: List(semantic_types.PathStep),
) -> semantic_types.SlotValue(exact_json.JsonValue)

reachability_input 

pub fn reachability_input(
  checked: CheckedReachability,
) -> typed_mapping.SolverInput

reachability_witness 

pub fn reachability_witness(
  checked: CheckedReachability,
) -> typed_mapping.ReachabilityWitness

replace_at 

pub fn replace_at(
  values: List(a),
  index: Int,
  value: a,
) -> List(a)

require 

pub fn require(condition: Bool, failure: e) -> Result(Nil, e)

resolved_shape 

pub fn resolved_shape(
  graph: semantic_types.SemanticGraph,
  reference: semantic_types.TypeRef,
) -> option.Option(semantic_types.TypeShape)

resource_closure_input 

pub fn resource_closure_input(
  checked: CheckedClosure,
) -> typed_mapping.SolverInput

resource_closure_witness 

pub fn resource_closure_witness(
  checked: CheckedClosure,
) -> typed_mapping.ClosureWitness

resource_trace_meaning 

pub fn resource_trace_meaning(
  prepared: PreparedCompositionInput,
  correspondence: ResourceCorrespondence,
) -> Result(Nil, UnresolvedObligation)

sample_value_fuel 

pub fn sample_value_fuel(
  graph: semantic_types.SemanticGraph,
  reference: semantic_types.TypeRef,
  active: List(semantic_types.TypeRef),
  fuel: Int,
  max_sample_length: Int,
) -> SampleResult(exact_json.JsonValue)

samples 

pub fn samples(
  graph: semantic_types.SemanticGraph,
  reference: semantic_types.TypeRef,
  active: List(semantic_types.TypeRef),
  limit: Int,
) -> List(exact_json.JsonValue)

semantic_basis 

pub fn semantic_basis(
  graph: semantic_types.SemanticGraph,
) -> SemanticBasis

slot_empty 

pub fn slot_empty(
  contract: semantic_types.SlotContract,
  empty: List(semantic_types.TypeRef),
) -> Bool

slot_samples 

pub fn slot_samples(
  graph: semantic_types.SemanticGraph,
  contract: semantic_types.SlotContract,
  limit: Int,
) -> List(semantic_types.SlotValue(exact_json.JsonValue))

unique 

pub fn unique(values: List(a)) -> List(a)

verify_acyclic_witness 

pub fn verify_acyclic_witness(
  input: typed_mapping.SolverInput,
  witness: typed_mapping.AcyclicWitness,
) -> Result(CheckedAcyclic, WitnessFailure)

verify_closure_witness 

pub fn verify_closure_witness(
  input: typed_mapping.SolverInput,
  witness: typed_mapping.ClosureWitness,
) -> Result(CheckedClosure, WitnessFailure)

verify_composition 

pub fn verify_composition(
  prepared: PreparedCompositionInput,
  raw: RawComposition,
) -> Result(CheckedComposition, WitnessFailure)

verify_composition_closure 

pub fn verify_composition_closure(
  prepared: PreparedCompositionInput,
  witness: CompositionClosureWitness,
) -> Result(CheckedCompositionClosure, WitnessFailure)

verify_counterexample 

pub fn verify_counterexample(
  graph: semantic_types.SemanticGraph,
  certificate: CounterexampleCertificate,
) -> Result(Nil, InclusionFailure)

verify_inclusion 

pub fn verify_inclusion(
  graph: semantic_types.SemanticGraph,
  source: semantic_types.SlotContract,
  destination: semantic_types.SlotContract,
  certificate: InclusionCertificate,
) -> Result(CheckedInclusion, InclusionFailure)

verify_reachability_witness 

pub fn verify_reachability_witness(
  input: typed_mapping.SolverInput,
  witness: typed_mapping.ReachabilityWitness,
) -> Result(CheckedReachability, WitnessFailure)

verify_return_values 

pub fn verify_return_values(
  prepared: PreparedCompositionInput,
  terminal: ReturnPlan,
  values: List(
    #(ProducerRef, semantic_types.SlotValue(exact_json.JsonValue)),
  ),
) -> Result(Nil, WitnessFailure)

verify_unreachable_composition 

pub fn verify_unreachable_composition(
  prepared: PreparedCompositionInput,
  witness: CompositionClosureWitness,
) -> Result(Nil, WitnessFailure)

verify_value_models 

pub fn verify_value_models(
  prepared: PreparedCompositionInput,
  state: SearchState,
  values: List(
    #(ProducerRef, semantic_types.SlotValue(exact_json.JsonValue)),
  ),
) -> Result(Nil, WitnessFailure)
✨ Search Document