Skip to content
12 changes: 6 additions & 6 deletions dag/extdeps/boot/freestanding_witness.dag
Original file line number Diff line number Diff line change
Expand Up @@ -45,25 +45,25 @@ fn witness_emitted_entry_point() -> Bool {
fn witness_emitted_first_phdr_is_pt_load_rx() -> Bool {
let bytes = emit_freestanding_elf64(pixel_writer_code_bytes)
match decode_elf64_phdr(bytes, freestanding_phoff) {
PhdrDecoded { value: phdr } =>
ElfDecoded { value: phdr } =>
phdr.segment_type == PtLoad
&& phdr.flags == pf_r + pf_x
&& phdr.offset == freestanding_code_file_offset
&& phdr.vaddr == freestanding_load_vaddr
PhdrRejected { reason: _ } => false
ElfRejected { reason: _ } => false
}
}

fn witness_emitted_load_segment_carries_code() -> Bool {
let bytes = emit_freestanding_elf64(pixel_writer_code_bytes)
match decode_elf64_phdr(bytes, freestanding_phoff) {
PhdrDecoded { value: phdr } =>
ElfDecoded { value: phdr } =>
let seg = elf64_phdr_to_load_segment(phdr)
seg.file_size == count(pixel_writer_code_bytes)
&& seg.permissions.readable == true
&& seg.permissions.writable == false
&& seg.permissions.executable == true
PhdrRejected { reason: _ } => false
ElfRejected { reason: _ } => false
}
}

Expand Down Expand Up @@ -106,10 +106,10 @@ fn witness_shared_encode_roundtrips_hello_static_ehdr() -> Bool {

fn witness_shared_encode_roundtrips_hello_static_phdr() -> Bool {
match decode_elf64_phdr(static_hello_first_phdr_bytes, 0) {
PhdrDecoded { value: phdr } =>
ElfDecoded { value: phdr } =>
let out = encode_elf64_phdr(phdr)
count(out) == elf64_phdr_size && int_lists_equal(static_hello_first_phdr_bytes, out)
PhdrRejected { reason: _ } => false
ElfRejected { reason: _ } => false
}
}

Expand Down
28 changes: 8 additions & 20 deletions dag/extdeps/cache/cache.dag
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ import extdeps.realization.reconcile_in_process {
typed_module_cache_id,
}
import extdeps.realization.resolved_graph { resolved_graph_cache_facts, resolved_graph_cache_id }
import std.cache_identity { CacheInterfaceId, CacheInterfaceProduct }
import std.cache_identity { CacheInterfaceId }
import std.cache_interface {
ArtifactIdentity,
ProducerReceipt,
Expand All @@ -52,18 +52,6 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
}
}

fn cited_cache_interface_facts(product: CacheInterfaceProduct) -> CacheInterfaceCatalogFacts {
match product {
GhaActionsCache => gha_actions_cache_facts
SccacheLocal => sccache_local_facts
BuildbuddyCas => buildbuddy_cas_facts
CargoTargetDir => cargo_target_dir_facts
RustupToolchainStore => rustup_toolchain_store_facts
ResolvedGraphCache => resolved_graph_cache_facts
ParseTableMemo => parse_table_memo_facts
}
}

fn cache_interface_facts_from_catalog(row: CacheInterfaceCatalogFacts) -> CacheInterfaceFacts {
CacheInterfaceFacts {
identity: row.identity
Expand Down Expand Up @@ -134,13 +122,13 @@ fn cache_verified_hit_receipt<T>(
}
}

data gha_actions_cache: CacheInterfaceCatalogFacts = cited_cache_interface_facts(GhaActionsCache)
data sccache_local: CacheInterfaceCatalogFacts = cited_cache_interface_facts(SccacheLocal)
data buildbuddy_cas: CacheInterfaceCatalogFacts = cited_cache_interface_facts(BuildbuddyCas)
data cargo_target_dir: CacheInterfaceCatalogFacts = cited_cache_interface_facts(CargoTargetDir)
data rustup_toolchain_store: CacheInterfaceCatalogFacts = cited_cache_interface_facts(RustupToolchainStore)
data resolved_graph_cache: CacheInterfaceCatalogFacts = cited_cache_interface_facts(ResolvedGraphCache)
data parse_table_memo: CacheInterfaceCatalogFacts = cited_cache_interface_facts(ParseTableMemo)
data gha_actions_cache: CacheInterfaceCatalogFacts = gha_actions_cache_facts
data sccache_local: CacheInterfaceCatalogFacts = sccache_local_facts
data buildbuddy_cas: CacheInterfaceCatalogFacts = buildbuddy_cas_facts
data cargo_target_dir: CacheInterfaceCatalogFacts = cargo_target_dir_facts
data rustup_toolchain_store: CacheInterfaceCatalogFacts = rustup_toolchain_store_facts
data resolved_graph_cache: CacheInterfaceCatalogFacts = resolved_graph_cache_facts
data parse_table_memo: CacheInterfaceCatalogFacts = parse_table_memo_facts
data compile_stage_memo: CacheInterfaceCatalogFacts = compile_stage_memo_facts

data cache_catalog: List<CacheInterfaceCatalogFacts> = [
Expand Down
24 changes: 12 additions & 12 deletions dag/extdeps/formats/elf/hello_static_witness.dag
Original file line number Diff line number Diff line change
Expand Up @@ -156,42 +156,42 @@ fn witness_phnum_is_9() -> Bool {

fn witness_first_segment_is_pt_load() -> Bool {
match decode_elf64_phdr(static_hello_first_phdr_bytes, 0) {
PhdrDecoded { value: phdr } => phdr.segment_type == PtLoad
PhdrRejected { reason: _ } => false
ElfDecoded { value: phdr } => phdr.segment_type == PtLoad
ElfRejected { reason: _ } => false
}
}

fn witness_first_segment_is_read_only() -> Bool {
match decode_elf64_phdr(static_hello_first_phdr_bytes, 0) {
PhdrDecoded { value: phdr } => {
ElfDecoded { value: phdr } => {
let seg = elf64_phdr_to_load_segment(phdr)
phdr.flags == pf_r
&& seg.permissions.readable == true
&& seg.permissions.writable == false
&& seg.permissions.executable == false
}
PhdrRejected { reason: _ } => false
ElfRejected { reason: _ } => false
}
}

fn witness_first_load_segment_vaddr() -> Bool {
match decode_elf64_phdr(static_hello_first_phdr_bytes, 0) {
PhdrDecoded { value: phdr } => elf64_phdr_to_load_segment(phdr).virtual_address == 4194304
PhdrRejected { reason: _ } => false
ElfDecoded { value: phdr } => elf64_phdr_to_load_segment(phdr).virtual_address == 4194304
ElfRejected { reason: _ } => false
}
}

fn witness_first_load_segment_filesz() -> Bool {
match decode_elf64_phdr(static_hello_first_phdr_bytes, 0) {
PhdrDecoded { value: phdr } => elf64_phdr_to_load_segment(phdr).file_size == 652
PhdrRejected { reason: _ } => false
ElfDecoded { value: phdr } => elf64_phdr_to_load_segment(phdr).file_size == 652
ElfRejected { reason: _ } => false
}
}

fn witness_first_load_segment_align() -> Bool {
match decode_elf64_phdr(static_hello_first_phdr_bytes, 0) {
PhdrDecoded { value: phdr } => elf64_phdr_to_load_segment(phdr).alignment == 4096
PhdrRejected { reason: _ } => false
ElfDecoded { value: phdr } => elf64_phdr_to_load_segment(phdr).alignment == 4096
ElfRejected { reason: _ } => false
}
}

Expand All @@ -201,11 +201,11 @@ fn witness_ehdr_encode_decode_roundtrip() -> Bool {

fn witness_phdr_encode_decode_roundtrip() -> Bool {
match decode_elf64_phdr(static_hello_first_phdr_bytes, 0) {
PhdrDecoded { value: phdr } =>
ElfDecoded { value: phdr } =>
let out = encode_elf64_phdr(phdr)
count(out) == elf64_phdr_size
&& int_lists_equal(static_hello_first_phdr_bytes, out)
PhdrRejected { reason: _ } => false
ElfRejected { reason: _ } => false
}
}

Expand Down
26 changes: 9 additions & 17 deletions dag/extdeps/formats/elf/segments.dag
Original file line number Diff line number Diff line change
Expand Up @@ -19,18 +19,10 @@ type Elf64Phdr {
align: Int
}

type PhdrDecodeReason
= PhdrTruncated { required_bytes: Int, available_bytes: Int }
| UnsupportedPhdrType { raw: Int }

type PhdrDecodeOutcome<T>
= PhdrDecoded { value: T }
| PhdrRejected { reason: PhdrDecodeReason }

fn decode_elf_segment_type(raw: Int) -> PhdrDecodeOutcome<ElfSegmentType> {
if raw == pt_load { PhdrDecoded { value: PtLoad } }
else if raw == pt_null { PhdrDecoded { value: PtNull } }
else { PhdrRejected { reason: UnsupportedPhdrType { raw: raw } } }
fn decode_elf_segment_type(raw: Int) -> ElfDecodeOutcome<ElfSegmentType> {
if raw == pt_load { ElfDecoded { value: PtLoad } }
else if raw == pt_null { ElfDecoded { value: PtNull } }
else { ElfRejected { reason: UnsupportedElfSegmentType { raw: raw } } }
}

fn decode_segment_permissions(flags: Int) -> SegmentPermission {
Expand All @@ -41,17 +33,17 @@ fn decode_segment_permissions(flags: Int) -> SegmentPermission {
}
}

fn decode_elf64_phdr(bytes: List<Int>, offset: Int) -> PhdrDecodeOutcome<Elf64Phdr> {
fn decode_elf64_phdr(bytes: List<Int>, offset: Int) -> ElfDecodeOutcome<Elf64Phdr> {
if count(bytes) < offset + elf64_phdr_size {
PhdrRejected {
reason: PhdrTruncated {
ElfRejected {
reason: Truncated {
required_bytes: offset + elf64_phdr_size,
available_bytes: count(bytes),
},
}
} else {
match decode_elf_segment_type(read_u32_le_in_bounds(bytes, offset)) {
PhdrDecoded { value: segment_type } => PhdrDecoded {
ElfDecoded { value: segment_type } => ElfDecoded {
value: Elf64Phdr {
segment_type: segment_type,
flags: read_u32_le_in_bounds(bytes, offset + 4),
Expand All @@ -63,7 +55,7 @@ fn decode_elf64_phdr(bytes: List<Int>, offset: Int) -> PhdrDecodeOutcome<Elf64Ph
align: read_u64_le_in_bounds(bytes, offset + 48),
},
}
PhdrRejected { reason: r } => PhdrRejected { reason: r }
ElfRejected { reason: r } => ElfRejected { reason: r }
}
}
}
Expand Down
3 changes: 3 additions & 0 deletions dag/extdeps/formats/elf/types.dag
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,9 @@ type ElfDecodeReason
| UnsupportedElfData { raw: Int }
| UnsupportedElfFileType { raw: Int }
| UnsupportedElfMachine { raw: Int }
| UnsupportedElfSegmentType { raw: Int }

data elf_phdr_decode_outcome_dissolve_on: String = "dissolve-on: elf.segments.PhdrDecodeOutcome — deleted parallel decode machinery; sole authority is extdeps.formats.elf.types.ElfDecodeOutcome / ElfDecodeReason."

type ElfDecodeOutcome<T>
= ElfDecoded { value: T }
Expand Down
7 changes: 1 addition & 6 deletions dag/extdeps/languages/rust/types.dag
Original file line number Diff line number Diff line change
Expand Up @@ -111,12 +111,7 @@ data common_trait_bounds: List<String> = [
data where_clause_template: String = "where\n \{constraints\}"
data trait_bound_template: String = "\{type\}: \{bound\}"

data integer_types: List<String> = [
"i8", "i16", "i32", "i64", "i128", "isize",
"u8", "u16", "u32", "u64", "u128", "usize"
]

data float_types: List<String> = ["f32", "f64"]
data rust_types_name_catalog_dissolve_on: String = "dissolve-on: rust.types.integer_types/float_types — deleted bare String name lists with zero consumers; sole type-name catalog authority is extdeps.languages.rust.primitives rust_grounding_primitives.target_name rows."

data rust_cast_syntax: CastSyntax = {
template: "\{expr\} as \{type\}",
Expand Down
3 changes: 1 addition & 2 deletions dag/extdeps/shell/gnu_coreutils.dag
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,7 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
data grep_recursive_quiet_flags: NonEmptyStr = "-rqE"
data grep_recursive_numbered_flags: NonEmptyStr = "-rnE"

data diff_recursive_flags: NonEmptyStr = "-r"
data diff_recursive_brief_flags: NonEmptyStr = "-rq"
data gnu_coreutils_diff_flags_dissolve_on: String = "dissolve-on: gnu_coreutils.diff_recursive_flags — deleted fork of diff argv literals; sole authority is extdeps.diffutils shell.Diff.Recursive transport (diff -r \{left\} \{right\})."

data rm_force_recursive_flags: NonEmptyStr = "-rf"

Expand Down
5 changes: 0 additions & 5 deletions dag/gunbc/non_fold_residue.dag
Original file line number Diff line number Diff line change
Expand Up @@ -341,11 +341,6 @@ data non_fold_residue_frontier: List<FrontierRow> = [
reason: nfr_reason_mint_era,
dissolve_on: nfr_dissolve_wildcard_total
},
FrontierRow {
unit: "dag/std/filesystem.dag::is_text_encoding",
reason: nfr_reason_mint_era,
dissolve_on: nfr_dissolve_wildcard_total
},
FrontierRow {
unit: "dag/std/induction.dag::compose_sub_value",
reason: nfr_reason_mint_era,
Expand Down
9 changes: 1 addition & 8 deletions dag/std/cache_identity.dag
Original file line number Diff line number Diff line change
Expand Up @@ -17,11 +17,4 @@ data typed_module_artifact_kind: ArtifactKindId = "typed_module"

data hermetic_fixture_artifact_kind: ArtifactKindId = "hermetic_fixture"

type CacheInterfaceProduct
= GhaActionsCache
| SccacheLocal
| BuildbuddyCas
| CargoTargetDir
| RustupToolchainStore
| ResolvedGraphCache
| ParseTableMemo
data cache_interface_product_dissolve_on: String = "dissolve-on: std.cache_identity.CacheInterfaceProduct — deleted closed enum fork; sole cache-backend identity authority is CacheInterfaceId (extdeps/cache/*.dag cited rows keyed by id)."
17 changes: 8 additions & 9 deletions dag/std/filesystem.dag
Original file line number Diff line number Diff line change
@@ -1,9 +1,11 @@
module std.filesystem

import std.encoding { Encoding }
import std.encoding { Encoding, is_text_encoding }
import std.types { FilePath, MimeType }
import std.filesystem.types { EntryKind, SymlinkTarget }

data filesystem_is_text_encoding_dissolve_on: String = "dissolve-on: std.filesystem.is_text_encoding — deleted duplicate Optional-lifted predicate; sole authority is std.encoding.is_text_encoding (Encoding, not Encoding?)."

type FileEntry {
path: FilePath
kind: EntryKind
Expand All @@ -24,21 +26,18 @@ type PartitionResult {

fn is_text_readable(entry: FileEntry) -> Bool {
match entry.kind {
RegularFile => is_text_encoding(e: entry.encoding)
Symlink => entry.symlink_target == TargetFile && is_text_encoding(e: entry.encoding)
RegularFile => is_text_encoding_optional(e: entry.encoding)
Symlink => entry.symlink_target == TargetFile && is_text_encoding_optional(e: entry.encoding)
Directory => false
Missing => false
Other => false
}
}

fn is_text_encoding(e: Encoding?) -> Bool {
fn is_text_encoding_optional(e: Encoding?) -> Bool {
match e {
Present { value: ASCII } => true
Present { value: UTF8 } => true
Present { value: Latin1 } => true
Present { value: Text } => true
_ => false
Present { value: enc } => is_text_encoding(e: enc)
Absent => false
}
}

Expand Down
56 changes: 9 additions & 47 deletions dag/std/markdown_markup.dag
Original file line number Diff line number Diff line change
@@ -1,59 +1,21 @@
module std.markdown_markup

import std.markup {
MarkupNode, ElementNode, TextNode, MarkupAttr,
MarkupNode,
fragments_to_markup_nodes,
}
import std.markdown {
MarkdownInline,
TextInline,
EmphasisInline,
StrongInline,
CodeInline,
LinkInline,
ImageInline,
markdown_inline_to_fragments,
markdown_inlines_to_fragments,
}

data markdown_markup_inline_mapping_dissolve_on: String = "dissolve-on: std.markdown_markup.markdown_inline_to_markup_nodes — deleted parallel MarkdownInline→MarkupNode mapping; sole authority is std.markdown.markdown_inline_to_fragments composed with std.markup.fragments_to_markup_nodes."

fn markdown_inline_to_markup_nodes(inline: MarkdownInline) -> List<MarkupNode> {
match inline {
TextInline { text } =>
[ TextNode { text: text } ]
CodeInline { text } =>
[ ElementNode { tag: "code", attrs: [], children: [ TextNode { text: text } ] } ]
EmphasisInline { inlines } =>
[ ElementNode {
tag: "em",
attrs: [],
children: markdown_inlines_to_markup_nodes(inlines: inlines),
}
]
StrongInline { inlines } =>
[ ElementNode {
tag: "strong",
attrs: [],
children: markdown_inlines_to_markup_nodes(inlines: inlines),
}
]
LinkInline { inlines, url } =>
[ ElementNode {
tag: "a",
attrs: [ MarkupAttr { name: "href", value: url } ],
children: markdown_inlines_to_markup_nodes(inlines: inlines),
}
]
ImageInline { alt, url } =>
[ ElementNode {
tag: "img",
attrs: [
MarkupAttr { name: "src", value: url },
MarkupAttr { name: "alt", value: alt },
],
children: [],
}
]
}
fragments_to_markup_nodes(frags: markdown_inline_to_fragments(inline: inline))
}

fn markdown_inlines_to_markup_nodes(inlines: List<MarkdownInline>) -> List<MarkupNode> {
reverse(inlines |> fold(init: [], f: fn(acc, inline) {
concat(markdown_inline_to_markup_nodes(inline: inline), acc)
}))
fragments_to_markup_nodes(frags: markdown_inlines_to_fragments(inlines: inlines))
}
Loading
Loading