Skip to content
Merged
147 changes: 110 additions & 37 deletions src/v2/compiler/self_host.dag
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
module v2.compiler.self_host

import extdeps.communication.medium { Medium }
import v2.std.algebra { fold_list }
import v2.std.collection { List }
import v2.std.logic { Bool }
import v2.std.diagnostic {
Expand All @@ -11,15 +13,17 @@ import v2.std.diagnostic {
port_locus,
Rejected,
Unavailable,
diagnostics_singleton
diagnostics_singleton,
outcome_accepted
}
import v2.std.find_witness {
CandidateSet,
PreservationPredicate,
UniqueOnly,
find_witness,
}
import v2.std.node { content_hash, Hash, Node, Symbol }
import v2.std.node { combine_hash, byte_limb_hash_peano_digest, Hash, Node, Symbol, symbol_identity_digest }
import v2.std.text { String, string_is_empty }
import v2.std.witness {
Holds,
StructuralPropertyWitness,
Expand All @@ -30,13 +34,15 @@ import v2.std.witness {
type CoreNode = Node

type SourceModels {
model_corpus: List<CoreNode>
stage1_committed_seed_source: Medium<String>
stage2_regen_emitted_source: Medium<String>
}

data self_host_equality_authority: Symbol = ^canonical_node_emission
data self_host_equality_authority: Symbol = ^canonical_emitted_bytes

type SelfHostStageEmission {
node: CoreNode
source: Medium<String>
digest: Hash
}

Expand Down Expand Up @@ -86,10 +92,31 @@ fn self_host_fixpoint_digest_mismatch_diagnostic(
}
}

fn self_host_stage_emission(node: CoreNode) -> SelfHostStageEmission {
fn source_text_code_unit_digest(text: String) -> Hash {
fold_list(
xs: text,
empty: symbol_identity_digest(sym: ^source_text_code_unit_digest_nil),
cons: fn(acc, ch) {
combine_hash(a: acc, b: byte_limb_hash_peano_digest(limb: ch))
}
)
}

fn canonical_emitted_bytes_digest(source: Medium<String>) -> Hash {
combine_hash(
a: symbol_identity_digest(sym: ^canonical_emitted_bytes),
b: source_text_code_unit_digest(text: source.carried)
)
}

fn self_host_stage_emission(
node: CoreNode,
source: Medium<String>
) -> SelfHostStageEmission {
SelfHostStageEmission {
node: node,
digest: content_hash(n: node)
source: source,
digest: canonical_emitted_bytes_digest(source: source)
}
}

Expand Down Expand Up @@ -129,45 +156,65 @@ fn self_host_fixpoint_witness(
}
}

fn candidate_promotion_witness(
stage1_candidate: CoreNode,
reference_stage1: CoreNode
) -> PromotionWitness {
PromotionWitness {
candidate_bootstrap_roundtrip_sub_check: bootstrap_roundtrip_scaffold(
produced_stage: stage1_candidate,
expected_stage: reference_stage1
),
candidate_fixed_point_sub_check: fixed_point_scaffold(
emitted_stage: stage1_candidate,
reference_stage: reference_stage1
)
}
fn source_models_regen_byte_pair_ready(models: SourceModels) -> Bool {
!string_is_empty(s: models.stage1_committed_seed_source.carried)
&& !string_is_empty(s: models.stage2_regen_emitted_source.carried)
}

fn bootstrap_roundtrip_scaffold(
fn bootstrap_roundtrip_check(
produced_stage: CoreNode,
expected_stage: CoreNode
) -> BootstrapRoundtripCheck {
Violates {
diagnostic: Diagnostic {
reason: ^bootstrap_roundtrip_not_realized,
at: node_locus(node: expected_stage),
correction: Unavailable { reason: ExternalContractUnknown }
}
match stage_emission_equality(
emitted_candidate: produced_stage,
reference_stage1: expected_stage
) {
Holds { value: eq } =>
Holds {
value: BootstrapRoundtripEqual {
produced_stage: eq.right,
expected_stage: eq.left
}
}
Violates { diagnostic: d } => Violates { diagnostic: d }
}
}

fn fixed_point_scaffold(
emitted_stage: CoreNode,
reference_stage: CoreNode
stage1_node: CoreNode,
stage2_node: CoreNode,
source_models: SourceModels
) -> FixedPointCheck {
self_host_fixpoint_witness(
stage1: self_host_stage_emission(node: reference_stage),
stage2: self_host_stage_emission(node: emitted_stage)
stage1: self_host_stage_emission(
node: stage1_node,
source: source_models.stage1_committed_seed_source
),
stage2: self_host_stage_emission(
node: stage2_node,
source: source_models.stage2_regen_emitted_source
)
)
}

fn candidate_promotion_witness(
stage1_candidate: CoreNode,
reference_stage1: CoreNode,
source_models: SourceModels
) -> PromotionWitness {
PromotionWitness {
candidate_bootstrap_roundtrip_sub_check: bootstrap_roundtrip_check(
produced_stage: stage1_candidate,
expected_stage: reference_stage1
),
candidate_fixed_point_sub_check: fixed_point_scaffold(
stage1_node: reference_stage1,
stage2_node: stage1_candidate,
source_models: source_models
)
}
}

fn stage_emission_closedness(reference_stage1: CoreNode) -> StructuralPropertyWitness {
StructuralPropertyWitness {
property: ^stage_emission_equality_closed_candidates,
Expand All @@ -176,12 +223,19 @@ fn stage_emission_closedness(reference_stage1: CoreNode) -> StructuralPropertyWi
}

fn self_host_fixed_point_digests_match(
emitted_stage1: CoreNode,
emitted_stage2: CoreNode
stage1_node: CoreNode,
stage2_node: CoreNode,
source_models: SourceModels
) -> Bool {
self_host_snake_closes(
stage1: self_host_stage_emission(node: emitted_stage1),
stage2: self_host_stage_emission(node: emitted_stage2)
stage1: self_host_stage_emission(
node: stage1_node,
source: source_models.stage1_committed_seed_source
),
stage2: self_host_stage_emission(
node: stage2_node,
source: source_models.stage2_regen_emitted_source
)
)
}

Expand Down Expand Up @@ -218,7 +272,26 @@ fn self_host_fixed_point_validate(
source_models: SourceModels,
reference_stage1: CoreNode
) -> Outcome<PromotionWitness> {
Rejected {
diagnostics: diagnostics_singleton(d: self_host_runner_not_realized_diagnostic())
if !source_models_regen_byte_pair_ready(models: source_models) {
Rejected {
diagnostics: diagnostics_singleton(d: self_host_runner_not_realized_diagnostic())
}
} else {
match fixed_point_scaffold(
stage1_node: reference_stage1,
stage2_node: stage1_candidate,
source_models: source_models
) {
Holds { value: _ } =>
outcome_accepted(
value: candidate_promotion_witness(
stage1_candidate: stage1_candidate,
reference_stage1: reference_stage1,
source_models: source_models
)
)
Violates { diagnostic: d } =>
Rejected { diagnostics: diagnostics_singleton(d: d) }
}
}
}
4 changes: 4 additions & 0 deletions src/v2/std/node.dag
Original file line number Diff line number Diff line change
Expand Up @@ -680,6 +680,10 @@ fn combine_hash(a: Hash, b: Hash) -> Hash {
hash_combine(a: a, b: b)
}

fn symbol_identity_digest(sym: Symbol) -> Hash {
atom_identity_hash(s: sym)
}

data byte_offset_residual_quotient_magnitude_shift_limbs: Int = 4

data byte_offset_residual_quotient_magnitude_max_shift: Int = 28
Expand Down
Loading