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
33 changes: 33 additions & 0 deletions dag/gunbc/host_crypto_digest_seed_growth.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
module gunbc.host_crypto_digest_seed_growth

import gunbc.roadmap_model { RoadmapNodeId }
import gunbc.seed_growth { SeedGrowthJustification }
import std.decl_ref { DeclarationRef, WholeDeclaration }

// FORWARD-FREEZE RECEIPT for the host crypto digest seams in v1_interpreter, enumerated because
// gunbc.seed_growth_admission makes unenumerated hand growth in src/v1 a stop-line.
//
// TWO SEAMS, ONE RECEIPT. hmac_sha256_hex_tag (the HMAC-SHA-256 mint behind extdeps.crypto.mac
// mac_sign) landed with no receipt; it is enumerated here beside sha256_hex_of_text_digest, which this
// change adds, because they are one boundary: RustCrypto sha2 reached from the interpreter.
//
// WHY A HOST SEAM AND NOT THE PURE FOLD. extdeps.crypto.sha2 sha256_hex is the substrate's SHA-256 and
// stays its authority and oracle, but interpreted it costs ~200k eval steps per 64-octet block
// (measured with claim_batch on test.claim.sha256_host_known_answer_witness), and the fabric store
// door (gunbc.fabric_store_operation_admission) digests an approved intent on every protected write.
//
// NOT COUNTED BELOW, disclosed: the interpreter arms free_call.hmac_sha256_hex, free_call.hmac_sha256_
// verify_hex and free_call.sha256_hex_of_text (macro arms inside eval_builtin_inner, not citable
// declarations). The generated v1_interpreter_dispatch_generated.rs and v1_compiler_infer_method.rs
// project gunbc.v1_interpreter_primitive_surface and v1.compiler.infer_method, whose authorities
// change with them.
data host_crypto_digest_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification {
hand_authored_declarations: [
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "sha256_hex_of_text_digest", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "hmac_sha256_hex_tag", field: WholeDeclaration }
],
reason: "A cryptographic digest over a text's bytes is realized by the host's audited RustCrypto sha2 exactly as HMAC already is: the substrate's pure fold (extdeps.crypto.sha2) remains the authority and the differential oracle, and the host seam changes cost only -- ~200k interpreted eval steps per block becomes one native call on the store door's per-write path. Correctness is established by known answers shared with the grandfathered sha256_fips_witness (pure fold == NIST/RFC values) and by host-vs-known-answer claims over the padding boundaries.",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "Delete when the digest is realized by EMITTED code rather than the interpreter's host arm: a rt_function_registry bridge row for sha256_hex_of_text (and hmac_sha256_hex) with its v1_rt runtime body, admitted by the #12389 primitive-runtime-body gate, so the self-emitted store door and mac_sign call the emitted body. Sufficient means both digests run in an emitted crate with the same known-answer claims green; an interpreter-only arm does not satisfy it.",
current_boundary: "sha256_hex_of_text_digest returns hex(Sha256::digest(text.as_bytes())); hmac_sha256_hex_tag decodes a hex key and returns hex(HMAC-SHA-256(key, message)) or none for non-hex key material. Neither holds state, reads anything but its arguments, or makes a decision; every refusal and every use is in the .dag callers."
}
1 change: 1 addition & 0 deletions dag/gunbc/primitive_egress/dispositions_text.dag
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,7 @@ fn dispositions_text_rows() -> List<PrimitiveEvidence> {
evidence_row(name: "is_xid_continue", category: Unicode, external_subject: NoExternalSubject, computation: computes(authority: authority_required(home: "extdeps.unicode (pinned UCD version; generated property tables are artifacts, never hand rows)"), inputs: "cp: Int", result: "Bool: XID_Continue per the pinned UCD; total", body: DagBodyRequired), refusals: RefusalsTyped, realization: NoNativeRealizationClaim, compiler_query: NotACompilerQuery, conflict: NoMeaningConflict, located: "is_xid_continue: the realization surfaces the census joins (registry row / contract row / algebra template / rt bridge / interpreter arm as present) and the authority named in the computation standing", next: "the owning lane lands the .dag body under the declared authority and switches one production consumer; the interpreter arm and bridge then delete for that consumer"),
evidence_row(name: "is_emoji_ident", category: Unicode, external_subject: NoExternalSubject, computation: computes(authority: authority_required(home: "extdeps.unicode (pinned UCD version; generated property tables are artifacts, never hand rows)"), inputs: "cp: Int", result: "Bool: the identifier-admissible emoji property per the pinned UCD; total", body: DagBodyRequired), refusals: RefusalsTyped, realization: NoNativeRealizationClaim, compiler_query: NotACompilerQuery, conflict: NoMeaningConflict, located: "is_emoji_ident: the realization surfaces the census joins (registry row / contract row / algebra template / rt bridge / interpreter arm as present) and the authority named in the computation standing", next: "the owning lane lands the .dag body under the declared authority and switches one production consumer; the interpreter arm and bridge then delete for that consumer"),
evidence_row(name: "hmac_sha256_hex", category: Crypto, external_subject: NoExternalSubject, computation: computes(authority: authority_required(home: "extdeps.crypto.mac (HMAC-SHA-256 over the ENCODING-0 byte substrate and the NUMERIC-BIT-0 words)"), inputs: "key_hex: String, message: String", result: "String?: the lowercase hex tag; Absent when key_hex is not hex -- a deterministic function of its inputs (RFC 2104 / FIPS 180-4)", body: DagBodyRequired), refusals: RefusalsTyped, realization: NoNativeRealizationClaim, compiler_query: NotACompilerQuery, conflict: NoMeaningConflict, located: "hmac_sha256_hex: the realization surfaces the census joins (registry row / contract row / algebra template / rt bridge / interpreter arm as present) and the authority named in the computation standing", next: "the owning lane lands the .dag body under the declared authority and switches one production consumer; the interpreter arm and bridge then delete for that consumer"),
evidence_row(name: "sha256_hex_of_text", category: Crypto, external_subject: NoExternalSubject, computation: computes(authority: authority_required(home: "std.primitives sha256_hex_of_text_contract (SHA-256 over the text's UTF-8 bytes; the pure extdeps.crypto.sha2 sha256_hex shares its known answers)"), inputs: "text: String", result: "String: the lowercase hex SHA-256 digest of the UTF-8 bytes; total (FIPS 180-4)", body: DagBodyRequired), refusals: RefusalsTyped, realization: NoNativeRealizationClaim, compiler_query: NotACompilerQuery, conflict: NoMeaningConflict, located: "sha256_hex_of_text: the realization surfaces the census joins (registry row / contract row / algebra template / rt bridge / interpreter arm as present) and the authority named in the computation standing", next: "the owning lane lands the .dag body under the declared authority and switches one production consumer; the interpreter arm and bridge then delete for that consumer"),
evidence_row(name: "hmac_sha256_verify_hex", category: Crypto, external_subject: NoExternalSubject, computation: computes(authority: authority_required(home: "extdeps.crypto.mac (HMAC-SHA-256 over the ENCODING-0 byte substrate and the NUMERIC-BIT-0 words)"), inputs: "key_hex: String, message: String, tag_hex: String", result: "Bool: constant-time tag equality; the comparison is part of the modeled contract (hmac_sha256_verify_hex_contract)", body: DagBodyRequired), refusals: RefusalsTyped, realization: NoNativeRealizationClaim, compiler_query: NotACompilerQuery, conflict: NoMeaningConflict, located: "hmac_sha256_verify_hex: the realization surfaces the census joins (registry row / contract row / algebra template / rt bridge / interpreter arm as present) and the authority named in the computation standing", next: "the owning lane lands the .dag body under the declared authority and switches one production consumer; the interpreter arm and bridge then delete for that consumer"),
evidence_row(name: "contiguous_loop_elementwise_kernel", category: NumericBit, external_subject: NoExternalSubject, computation: computes(authority: declared_authority(module_path: "std.primitives", decl_name: "contiguous_loop_elementwise_kernel_contract"), inputs: "xs: List<Int>, f: fn(Int) -> Int", result: "List<Int>: elementwise map over a contiguous carrier; total", body: DagBodyRequired), refusals: RefusalsTyped, realization: NoNativeRealizationClaim, compiler_query: NotACompilerQuery, conflict: NoMeaningConflict, located: "contiguous_loop_elementwise_kernel: the realization surfaces the census joins (registry row / contract row / algebra template / rt bridge / interpreter arm as present) and the authority named in the computation standing", next: "the owning lane lands the .dag body under the declared authority and switches one production consumer; the interpreter arm and bridge then delete for that consumer"),
evidence_row(name: "contiguous_loop_elementwise_float_kernel", category: NumericBit, external_subject: NoExternalSubject, computation: computes(authority: declared_authority(module_path: "std.primitives", decl_name: "contiguous_loop_elementwise_float_kernel_contract"), inputs: "xs: List<Float>, f: fn(Float) -> Float", result: "List<Float>: elementwise map; total", body: DagBodyRequired), refusals: RefusalsTyped, realization: NoNativeRealizationClaim, compiler_query: NotACompilerQuery, conflict: NoMeaningConflict, located: "contiguous_loop_elementwise_float_kernel: the realization surfaces the census joins (registry row / contract row / algebra template / rt bridge / interpreter arm as present) and the authority named in the computation standing", next: "the owning lane lands the .dag body under the declared authority and switches one production consumer; the interpreter arm and bridge then delete for that consumer"),
Expand Down
2 changes: 2 additions & 0 deletions dag/gunbc/seed_growth_admission.dag
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ import gunbc.decl_facts_authored_string_attach_seed_growth {
}
import gunbc.keyed_declaration_read_seed_growth { keyed_declaration_read_seed_growth_justification }
import gunbc.keyed_dependency_edge_read_seed_growth { keyed_dependency_edge_read_seed_growth_justification }
import gunbc.host_crypto_digest_seed_growth { host_crypto_digest_seed_growth_justification }
import gunbc.census_memo_seed_growth { census_memo_seed_growth_justification }
import gunbc.fabric_door_socket_seed_growth { fabric_door_socket_seed_growth_justification }
import gunbc.kind_reflection_seed_growth { kind_reflection_seed_growth_justification }
Expand Down Expand Up @@ -310,6 +311,7 @@ fn seed_growth_justification_roster() -> List<SeedGrowthJustification> {
with_authored_string_literals_seed_growth_justification,
keyed_declaration_read_seed_growth_justification,
keyed_dependency_edge_read_seed_growth_justification,
host_crypto_digest_seed_growth_justification,
cli_wire_host_seed_growth_justification,
filesystem_create_new_seed_growth_justification,
required_lane_judgment_seed_growth_justification,
Expand Down
9 changes: 9 additions & 0 deletions dag/gunbc/v1/v1_interpreter_primitive_surface.dag
Original file line number Diff line number Diff line change
Expand Up @@ -506,6 +506,15 @@ fn v1_interpreter_authored_roster_arms() -> List<InterpreterPrimitiveDispatchArm
dispatch_emit_site: EvalBuiltinInnerSite,
enumeration: AuthoredInRoster,
},
InterpreterPrimitiveDispatchArm {
arm: InterpreterPrimitiveArmId { identity: "free_call.sha256_hex_of_text" },
form: FreeCall,
authored_spelling: "sha256_hex_of_text",
realization_module: "v1_interpreter",
dispatch_symbol: "eval_builtin_inner",
dispatch_emit_site: EvalBuiltinInnerSite,
enumeration: AuthoredInRoster,
},
InterpreterPrimitiveDispatchArm {
arm: InterpreterPrimitiveArmId { identity: "free_call.hmac_sha256_hex" },
form: FreeCall,
Expand Down
18 changes: 18 additions & 0 deletions dag/std/primitives.dag
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,22 @@ data hmac_sha256_verify_hex_contract: PrimitiveContract = {
carrier_cost: CarrierInsensitive
}

// SHA-256 OF A TEXT'S UTF-8 BYTES, lowercase hex (FIPS 180-4). A host seam beside the HMAC ones for
// one reason, measured: the pure fold (extdeps.crypto.sha2 sha256_hex) costs ~500-600k interpreted
// eval steps over a ~150-byte text, and the fabric store door digests an approved intent on every
// protected write (gunbc.fabric_store_operation_admission). The pure fold stays as its differential
// oracle through the known answers they share (test.claim.sha256_host_known_answer_witness).
// A DECLARED FRONTIER (DESIGN §3c): its production consumer is gunbc.fabric_store_operation_admission
// intent_digest, which lands in d0_store_operation_wall PR 4a (gunbc#12537). TRIGGER: that change lands
// calling sha256_hex_of_text; if the door digests some other way, this primitive is deleted with it.
data sha256_hex_of_text_contract: PrimitiveContract = {
name: "sha256_hex_of_text",
work: "n",
output_size: "64",
certainty: Proven,
carrier_cost: CarrierInsensitive
}

// Issuance: work linear in the message, output the 64 lowercase hex digits of a 32-octet tag. A
// SECOND contract rather than a widened verify, because only the key holder mints; a verifier keeps
// its one-bit answer (hmac_sha256_verify_hex_contract above) and never sees a tag to compare.
Expand Down Expand Up @@ -564,6 +580,7 @@ fn builtin_registry_surface_names() -> List<String> {
[
"hmac_sha256_verify_hex",
"hmac_sha256_hex",
"sha256_hex_of_text",
"count",
"string_length",
"code_point",
Expand Down Expand Up @@ -723,6 +740,7 @@ fn primitive_contract_roster() -> List<PrimitiveContract> {
string_length_contract,
hmac_sha256_verify_hex_contract,
hmac_sha256_hex_contract,
sha256_hex_of_text_contract,
substring_contract,
string_contains_contract,
starts_with_contract,
Expand Down
56 changes: 56 additions & 0 deletions dag/test/claim/sha256_host_known_answer_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
module test.claim.sha256_host_known_answer_witness

import std.logic { Bool }
import std.types { String }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

// THE HOST SHA-256 AGAINST KNOWN ANSWERS, one host call per claim. sha256_hex_of_text (the host
// seam, RustCrypto sha2) must equal the known answer for each text. For the empty, "abc" and NIST
// 448-bit texts the known answer is the FIPS 180-4 published value that test.claim.sha256_fips_witness_
// test asserts of the pure fold (extdeps.crypto.sha2 sha256_hex), so host == pure holds transitively
// through the shared value. For the padding boundaries (55 octets, the last that fits one block with
// its length field; 56, which forces a second; 63/64/65, straddling the block edge; 130, three blocks)
// the known answers are computed by an independent implementation (Python hashlib); the pure fold is
// not asserted on those here, because interpreting it costs ~200k eval steps per block. The direct
// pure-vs-host comparison on all nine vectors ran as a local receipt (see the PR).
fn matches_known(text: String, known: String) -> Bool {
sha256_hex_of_text(text: text) == known
}

test fn the_host_digest_of_the_empty_text_is_the_known_answer() -> Bool {
matches_known(text: "", known: "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855")
}

test fn the_host_digest_of_abc_is_the_known_answer() -> Bool {
matches_known(text: "abc", known: "ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad")
}

test fn the_host_digest_of_a_55_octet_text_is_the_known_answer() -> Bool {
matches_known(text: "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", known: "9f4390f8d30c2dd92ec9f095b65e2b9ae9b0a925a5258e241c9f1e910f734318")
}

test fn the_host_digest_of_a_56_octet_text_is_the_known_answer() -> Bool {
matches_known(text: "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", known: "b35439a4ac6f0948b6d6f9e3c6af0f5f590ce20f1bde7090ef7970686ec6738a")
}

test fn the_host_digest_of_a_63_octet_text_is_the_known_answer() -> Bool {
matches_known(text: "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", known: "7d3e74a05d7db15bce4ad9ec0658ea98e3f06eeecf16b4c6fff2da457ddc2f34")
}

test fn the_host_digest_of_a_64_octet_text_is_the_known_answer() -> Bool {
matches_known(text: "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", known: "ffe054fe7ae0cb6dc65c3af9b61d5209f439851db43d0ba5997337df154668eb")
}

test fn the_host_digest_of_a_65_octet_text_is_the_known_answer() -> Bool {
matches_known(text: "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", known: "635361c48bb9eab14198e76ea8ab7f1a41685d6ad62aa9146d301d4f17eb0ae0")
}

test fn the_host_digest_of_a_130_octet_three_block_text_is_the_known_answer() -> Bool {
matches_known(text: "gunbc-gunbc-gunbc-gunbc-gunbc-gunbc-gunbc-gunbc-gunbc-gunbc-gunbc-gunbc-gunbc-gunbc-gunbc-gunbc-gunbc-gunbc-gunbc-gunbc-gunbc-abcd", known: "3de7e15aa1b453dc3833d796643b52713e80cdff8bf8738fece1c2d4a352a052")
}

test fn the_host_digest_of_the_nist_448_bit_text_is_the_known_answer() -> Bool {
matches_known(text: "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq", known: "248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1")
}
1 change: 1 addition & 0 deletions src/v1/04_method.dag
Original file line number Diff line number Diff line change
Expand Up @@ -294,6 +294,7 @@ data builtin_function_registry: Map<String, BuiltinSignature> = {
"count": derived_signature_and_return(names: ["xs"], method: "count"),
"hmac_sha256_verify_hex": BuiltinSignature { params: [BuiltinParam { name: "key_hex", ty: NamedTemplate { name: "String" } }, BuiltinParam { name: "message", ty: NamedTemplate { name: "String" } }, BuiltinParam { name: "tag_hex", ty: NamedTemplate { name: "String" } }], returns: bool_type },
"hmac_sha256_hex": BuiltinSignature { params: [BuiltinParam { name: "key_hex", ty: NamedTemplate { name: "String" } }, BuiltinParam { name: "message", ty: NamedTemplate { name: "String" } }], returns: with_optional_cardinality(n: string_type) },
"sha256_hex_of_text": BuiltinSignature { params: [BuiltinParam { name: "text", ty: NamedTemplate { name: "String" } }], returns: string_type },
"string_length": BuiltinSignature { params: [BuiltinParam { name: "s", ty: NamedTemplate { name: "String" } }], returns: int_type },
"code_point": BuiltinSignature { params: [BuiltinParam { name: "c", ty: NamedTemplate { name: "String" } }], returns: int_type },
"to_int": derived_signature(names: ["s"], method: "to_int", returns: int_type),
Expand Down
9 changes: 9 additions & 0 deletions src/v1/stage0/src/v1_compiler_infer_method.rs
Original file line number Diff line number Diff line change
Expand Up @@ -338,6 +338,15 @@ pub fn builtin_function_registry() -> Rc<HashMap<String, Rc<BuiltinSignature>>>
}),
})]),
returns: crate::v1_std_core::with_optional_cardinality(string_type()),
}));
__m.insert("sha256_hex_of_text".to_string(), Rc::new(BuiltinSignature {
params: Rc::new(vec![Rc::new(BuiltinParam {
name: "text".to_string(),
ty: Rc::new(AlgebraTypeTemplate::NamedTemplate {
name: "String".to_string(),
}),
})]),
returns: string_type(),
}));
__m.insert("string_length".to_string(), Rc::new(BuiltinSignature {
params: Rc::new(vec![Rc::new(BuiltinParam {
Expand Down
Loading
Loading