Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ import std.optional { Absent }
import v2.compiler.self_host.closure_emission {
ClosureEmissionLocated, ClosureMemberEmitted, ClosureMemberRefused, emit_closure_from_ingest_located,
}
import v2.compiler.target_carriers { emit_module_decl_separator }
import v2.compiler.source_authority { DagSourceReadWitness }
import v2.extdeps.languages.dag { dag_type_atom_node }
import v2.extdeps.languages.rust { rust_target_model }
Expand All @@ -28,12 +29,14 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
// section 3). Two inhabitance rows still drive the door on this module, on the required gate.
// gunbc.rung_drop identity_cast_route_new_witness_eval_step_cost retired when those inhabitance
// identities billed inside the new-witness eval-step budget on gunbc#13489 required floor run
// 37522243686 (artifact required-floor-claim-cost). The native partner builds and runs the emitted
// text; it is not the last execution of the door.
// 37522243686 (artifact required-floor-claim-cost). Native builds the same member text this
// inhabitance asserts by exact equality.
data identity_cast_source: String = "module v2.test.identity_cast\n\nfn f(x: Int) -> Int { x as Int }\n"

data refused_cast_source: String = "module v2.test.identity_cast\n\nfn f(x: Int) -> Bool { x as Bool }\n"

data identity_cast_supplied_emitted_text: String = concat("fn f(x: i32) -> i32 { x }", emit_module_decl_separator)

type IdentityCastRouteVerdict
= IdentityCastEntryEmitted { text: String, members: Int }
| IdentityCastEntryRefused { reason: Symbol, members: Int }
Expand Down Expand Up @@ -84,7 +87,7 @@ fn refused_cast_route_verdict() -> IdentityCastRouteVerdict {
fn identity_cast_route_admitted_holds(v: IdentityCastRouteVerdict) -> Bool {
match v {
IdentityCastEntryEmitted { text: t, members: n } =>
n == 1 && string_contains(s: t, pattern: "fn f(x: i32) -> i32")
n == 1 && t == identity_cast_supplied_emitted_text
IdentityCastEntryRefused { reason: _, members: _ } => false
IdentityCastClosureRefused { reason: _ } => false
}
Expand Down
34 changes: 16 additions & 18 deletions src/v2/test/claim/execution/emit_host_identity_cast_native_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -14,16 +14,15 @@ import v2.std.text { String }
import v2.std.witness { Violates }
import v2.test.claim.coercion.identity_cast_emission_route {
IdentityCastClosureRefused, IdentityCastEntryEmitted, IdentityCastEntryRefused,
identity_cast_route_admitted_holds, identity_cast_route_verdict,
identity_cast_route_verdict,
}

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

// THE ADMITTED IDENTITY CAST, BUILT AND RUN. identity_cast_route_verdict is the real door; this
// module reads the same verdict the required-gate inhabitance already asserted, then builds and
// runs it. The last merge-time execution of the door is
// v2.test.claim.coercion.identity_cast_emission_route.an_admitted_identity_cast_emits_through_the_closure_route_holds,
// not this module.
// THE ADMITTED IDENTITY CAST, BUILT AND RUN. One native control reads the REAL member text from
// identity_cast_route_verdict and every runtime case builds and runs that artifact (DESIGN section 3
// pairing). The last merge-time execution of the door on the required gate is still
// v2.test.claim.coercion.identity_cast_emission_route.an_admitted_identity_cast_emits_through_the_closure_route_holds.
//
// STANDING, STATED SO IT IS NOT READ AS COVERAGE: this module is outside the required gate
// (v2.workflow.required_floor required_gate_authored_modules) by operator decision, because every
Expand All @@ -46,19 +45,18 @@ fn identity_cast_native_inputs() -> Inputs {
inputs_root_only(root: node_synthetic(kind: v2.std.node.TypeNode { connective: v2.std.node.Atom { identity: ^identity_cast_native_probe } }, children: []))
}

// The entry member's emitted text, read from the route module's shared verdict rather than emitted a
// second time: the text built here is the text the admission row asserted on. Absent when the route
// did not emit exactly the entry.
// The entry member's emitted text from the closure door. Absent when the route did not emit exactly
// one admitted entry. Runtime cases share this control; they do not substitute a supplied spelling.
fn identity_cast_native_emitted() -> Optional<String> {
let v = identity_cast_route_verdict()
if identity_cast_route_admitted_holds(v: v) {
match v {
IdentityCastEntryEmitted { text: t, members: _ } => optional_present(value: t)
IdentityCastEntryRefused { reason: _, members: _ } => optional_absent()
IdentityCastClosureRefused { reason: _ } => optional_absent()
}
} else {
optional_absent()
match identity_cast_route_verdict() {
IdentityCastEntryEmitted { text: t, members: n } =>
if n == 1 {
optional_present(value: t)
} else {
optional_absent()
}
IdentityCastEntryRefused { reason: _, members: _ } => optional_absent()
IdentityCastClosureRefused { reason: _ } => optional_absent()
}
}

Expand Down
Loading