Repair #12000: device routes gated on the native crypto realization; App Attest counter committed before reads and push updates

dag/extdeps/apple/app_attest.dag

@@ -398,9 +398,10 @@ fn app_attest_root() -> X509Certificate? {
 // verifier does not carry, or a signature that is not an ECDSA-Sig-Value for the issuer's width --
 // and never a verdict. ITS EVIDENCE: the refusing arms are claimed cheaply over the real leaf
 // (test.claim.app_attest_verifier_witness_test); the two verifying links are enrolled there and in
-// test.claim.p384_dag_ecdsa_witness_test and are NOT executed on the interpreter, because a P-384
-// verification at 16 limbs exceeds what a session container holds (one P-256 verify is 15.5 GiB);
-// their executing route is the native gunbc test row the frontier names.
+// test.claim.p384_dag_ecdsa_witness_test and are NOT executed on the interpreter: a P-384
+// verification at 16 limbs exceeds what a session container holds, by the instrument the roadmap
+// row v1-interpreter-p256-verify-cost-shape names; their executing route is the native gunbc test
+// row the frontier names.
 fn chain_link_verifies(subject: X509Certificate, issuer: X509Certificate) -> Bool? {
   let digest = if subject.signature_algorithm == oid_ecdsa_with_sha256 { Present { value: sha256(message: subject.tbs.tbs_octets) } }
     else if subject.signature_algorithm == oid_ecdsa_with_sha384 { Present { value: sha384(message: subject.tbs.tbs_octets) } }
@@ -452,38 +453,75 @@ fn validity_refusal(cert: X509Certificate, observed_at: Timestamp, which: String
   }
 }
 
-// Steps 9 and 10 read the authenticator data's extensions map.
-fn validation_category_refusal(extensions: CborValue?, admitted: List<Int>) -> AttestationRefusal? {
+// Steps 9 and 10 read the authenticator data's extensions map. EACH READER HAS ITS OWN RESULT
+// SUM, NAMING EXACTLY WHAT IT CAN CONCLUDE (review 69983 of gunbc#11989). Returning the whole
+// AttestationRefusal made the reader's real range -- three constructors -- invisible to its
+// consumers, so the assertion mappers had to carry a fallback arm for ten constructors the reader
+// cannot emit, and that arm needed a hand-written table of the sum's own constructor names to
+// print. A fallback that cannot fire is a decoration (DESIGN section 4b) and the name table was a
+// second naming authority for constructors the Node tree already names (section 3). With the range
+// declared, BOTH consumers below are total by construction and neither needs either.
+type ValidationCategoryReading
+  = ValidationCategoryAdmitted
+  | ValidationCategoryReadAbsent
+  | ValidationCategoryReadRefused { category: Int }
+  | ValidationCategoryReadUndecodable { cause: String }
+
+type BundleVersionReading
+  = BundleVersionMatched
+  | BundleVersionReadAbsent
+  | BundleVersionReadUnexpected { declared: String }
+  | BundleVersionReadUndecodable { cause: String }
+
+fn read_validation_category(extensions: CborValue?, admitted: List<Int>) -> ValidationCategoryReading {
   match extensions {
-    Absent => Present { value: AttestationValidationCategoryAbsent }
+    Absent => ValidationCategoryReadAbsent
     Present { value: ext } =>
       match app_attest_member(v: ext, key: app_attest_validation_category_extension_key) {
-        Absent => Present { value: AttestationValidationCategoryAbsent }
+        Absent => ValidationCategoryReadAbsent
         Present { value: v } =>
           match cbor_unsigned_value(v: v) {
-            Absent => Present { value: app_attest_undecodable(cause: "apple_validation_category_01 is not a CBOR unsigned integer") }
+            Absent => ValidationCategoryReadUndecodable { cause: "apple_validation_category_01 is not a CBOR unsigned integer" }
             Present { value: category } =>
-              if any(admitted, a => a == category) { none } else { Present { value: AttestationValidationCategoryRefused { category: category } } }
+              if any(admitted, a => a == category) { ValidationCategoryAdmitted } else { ValidationCategoryReadRefused { category: category } }
           }
       }
   }
 }
 
-fn bundle_version_refusal(extensions: CborValue?, expected: NonEmptyStr) -> AttestationRefusal? {
+fn read_bundle_version(extensions: CborValue?, expected: NonEmptyStr) -> BundleVersionReading {
   match extensions {
-    Absent => Present { value: AttestationBundleVersionAbsent }
+    Absent => BundleVersionReadAbsent
     Present { value: ext } =>
       match app_attest_member(v: ext, key: app_attest_bundle_version_extension_key) {
-        Absent => Present { value: AttestationBundleVersionAbsent }
+        Absent => BundleVersionReadAbsent
         Present { value: v } =>
           match cbor_text_string_value(v: v) {
-            Absent => Present { value: app_attest_undecodable(cause: "apple_bundle_version_01 is not a CBOR text string") }
-            Present { value: declared } => if declared == (expected as String) { none } else { Present { value: AttestationBundleVersionUnexpected { declared: declared } } }
+            Absent => BundleVersionReadUndecodable { cause: "apple_bundle_version_01 is not a CBOR text string" }
+            Present { value: declared } => if declared == (expected as String) { BundleVersionMatched } else { BundleVersionReadUnexpected { declared: declared } }
           }
       }
   }
 }
 
+fn validation_category_refusal(extensions: CborValue?, admitted: List<Int>) -> AttestationRefusal? {
+  match read_validation_category(extensions: extensions, admitted: admitted) {
+    ValidationCategoryAdmitted => none
+    ValidationCategoryReadAbsent => Present { value: AttestationValidationCategoryAbsent }
+    ValidationCategoryReadRefused { category: c } => Present { value: AttestationValidationCategoryRefused { category: c } }
+    ValidationCategoryReadUndecodable { cause: c } => Present { value: app_attest_undecodable(cause: c) }
+  }
+}
+
+fn bundle_version_refusal(extensions: CborValue?, expected: NonEmptyStr) -> AttestationRefusal? {
+  match read_bundle_version(extensions: extensions, expected: expected) {
+    BundleVersionMatched => none
+    BundleVersionReadAbsent => Present { value: AttestationBundleVersionAbsent }
+    BundleVersionReadUnexpected { declared: d } => Present { value: AttestationBundleVersionUnexpected { declared: d } }
+    BundleVersionReadUndecodable { cause: c } => Present { value: app_attest_undecodable(cause: c) }
+  }
+}
+
 fn first_attestation_refusal(rs: List<AttestationRefusal?>) -> AttestationRefusal? {
   fold(rs, init: none, f: (acc, r) => match acc {
     Present { value: a } => Present { value: a }
@@ -673,45 +711,25 @@ fn assertion_parts(object: List<UInt8>) -> AssertionPartsRead {
   }
 }
 
-// The assertion's steps 7 and 8 share the attestation's readers; every attestation refusal the
-// readers can produce maps to its assertion twin BY NAME, and an undecodable member stays
-// undecodable with its cause (review 69702 of gunbc#11989: a wildcard had reported a malformed
-// category as absent).
+// The assertion's steps 7 and 8 share the attestation's READERS -- not its refusal sum -- so each
+// reading maps to its assertion twin directly and every arm is reachable (review 69983 of
+// gunbc#11989). An undecodable member stays undecodable with its cause (review 69702: a wildcard
+// had reported a malformed category as absent); there is no wildcard left to regress to.
 fn assertion_category_refusal(extensions: CborValue?, admitted: List<Int>) -> AssertionRefusal? {
-  match validation_category_refusal(extensions: extensions, admitted: admitted) {
-    Absent => none
-    Present { value: AttestationValidationCategoryAbsent } => Present { value: AssertionValidationCategoryAbsent }
-    Present { value: AttestationValidationCategoryRefused { category: c } } => Present { value: AssertionValidationCategoryRefused { category: c } }
-    Present { value: AttestationUndecodable { cause: c } } => Present { value: AssertionUndecodable { cause: c } }
-    Present { value: other } => Present { value: AssertionUndecodable { cause: "validation category reader produced a refusal outside its contract: " + attestation_refusal_name(r: other) } }
+  match read_validation_category(extensions: extensions, admitted: admitted) {
+    ValidationCategoryAdmitted => none
+    ValidationCategoryReadAbsent => Present { value: AssertionValidationCategoryAbsent }
+    ValidationCategoryReadRefused { category: c } => Present { value: AssertionValidationCategoryRefused { category: c } }
+    ValidationCategoryReadUndecodable { cause: c } => Present { value: AssertionUndecodable { cause: c } }
   }
 }
 
 fn assertion_version_refusal(extensions: CborValue?, expected: NonEmptyStr) -> AssertionRefusal? {
-  match bundle_version_refusal(extensions: extensions, expected: expected) {
-    Absent => none
-    Present { value: AttestationBundleVersionAbsent } => Present { value: AssertionBundleVersionAbsent }
-    Present { value: AttestationBundleVersionUnexpected { declared: d } } => Present { value: AssertionBundleVersionUnexpected { declared: d } }
-    Present { value: AttestationUndecodable { cause: c } } => Present { value: AssertionUndecodable { cause: c } }
-    Present { value: other } => Present { value: AssertionUndecodable { cause: "bundle version reader produced a refusal outside its contract: " + attestation_refusal_name(r: other) } }
-  }
-}
-
-fn attestation_refusal_name(r: AttestationRefusal) -> String {
-  match r {
-    AttestationFormatUnexpected { declared: _ } => "AttestationFormatUnexpected"
-    AttestationChainUntrusted { detail: _ } => "AttestationChainUntrusted"
-    AttestationNonceMismatch => "AttestationNonceMismatch"
-    AttestationKeyIdMismatch { declared: _ } => "AttestationKeyIdMismatch"
-    AttestationAppIdMismatch { expected_app_id: _ } => "AttestationAppIdMismatch"
-    AttestationCounterNonZero { counter: _ } => "AttestationCounterNonZero"
-    AttestationEnvironmentUnexpected { expected: _ } => "AttestationEnvironmentUnexpected"
-    AttestationCredentialIdMismatch { declared: _ } => "AttestationCredentialIdMismatch"
-    AttestationValidationCategoryRefused { category: _ } => "AttestationValidationCategoryRefused"
-    AttestationValidationCategoryAbsent => "AttestationValidationCategoryAbsent"
-    AttestationBundleVersionAbsent => "AttestationBundleVersionAbsent"
-    AttestationBundleVersionUnexpected { declared: _ } => "AttestationBundleVersionUnexpected"
-    AttestationUndecodable { cause: _ } => "AttestationUndecodable"
+  match read_bundle_version(extensions: extensions, expected: expected) {
+    BundleVersionMatched => none
+    BundleVersionReadAbsent => Present { value: AssertionBundleVersionAbsent }
+    BundleVersionReadUnexpected { declared: d } => Present { value: AssertionBundleVersionUnexpected { declared: d } }
+    BundleVersionReadUndecodable { cause: c } => Present { value: AssertionUndecodable { cause: c } }
   }
 }
 

dag/extdeps/crypto/nist_p256.dag

@@ -62,10 +62,6 @@ data p256_gy: BigNat = bignat_from_octets(octets: p256_gy_octets)
 // 256-bit moduli in 24-bit limbs: the family fold derives 11 from the coordinate width.
 data p256_curve: PrimeCurve = prime_curve(p_octets: p256_p_octets, n_octets: p256_n_octets, b_octets: p256_b_octets, gx_octets: p256_gx_octets, gy_octets: p256_gy_octets, coordinate_octets: 32)
 
-fn p256_is_infinity(p: JacobianPoint) -> Bool {
-  jacobian_is_infinity(p: p)
-}
-
 fn p256_affine(x: BigNat, y: BigNat) -> JacobianPoint {
   curve_affine(c: p256_curve, x: x, y: y)
 }

dag/extdeps/crypto/nist_prime_curve.dag

@@ -3,6 +3,7 @@ module extdeps.crypto.nist_prime_curve
 import std.types { Int, List, Bool }
 import std.integer { UInt8 }
 import std.bignat {
+  bignat_below, bignat_nonzero_below,
   BigNat, MontgomeryModulus, bignat_from_octets, bignat_compare, bignat_is_zero, bignat_bits, bignat_zero_limbs, bignat_one,
   montgomery_modulus, montgomery_mul, montgomery_add, montgomery_sub, montgomery_to, montgomery_from,
   montgomery_inverse_prime, montgomery_reduce_once,
@@ -159,6 +160,28 @@ fn curve_double_scalar(c: PrimeCurve, u1: BigNat, g: JacobianPoint, u2: BigNat,
   })
 }
 
+// THE GROUP LAW'S OWN EVIDENCE (review 69917 of gunbc#11981): a Jacobian point (X:Y:Z) lies on
+// y^2 = x^3 - 3x + b exactly when Y^2 = X^3 - 3·X·Z^4 + b·Z^6, decided in a handful of field
+// operations and with no inversion, so a doubling or an addition can be checked for closure at a
+// cost near curve_on_curve's. Infinity is on every curve.
+fn curve_jacobian_on_curve(c: PrimeCurve, p: JacobianPoint) -> Bool {
+  if jacobian_is_infinity(p: p) { true } else {
+    let z2 = curve_fsqr(c: c, a: p.z)
+    let z4 = curve_fsqr(c: c, a: z2)
+    let z6 = curve_fmul(c: c, a: z4, b: z2)
+    let x3 = curve_fmul(c: c, a: curve_fsqr(c: c, a: p.x), b: p.x)
+    let xz4 = curve_fmul(c: c, a: p.x, b: z4)
+    let three_xz4 = curve_fadd(c: c, a: curve_fadd(c: c, a: xz4, b: xz4), b: xz4)
+    let bz6 = curve_fmul(c: c, a: montgomery_to(ctx: c.field, a: c.b), b: z6)
+    bignat_compare(a: curve_fsqr(c: c, a: p.y), b: curve_fadd(c: c, a: curve_fsub(c: c, a: x3, b: three_xz4), b: bz6)) == 0
+  }
+}
+
+// The additive inverse of an affine-embedded point: (X : −Y : Z).
+fn curve_negate(c: PrimeCurve, p: JacobianPoint) -> JacobianPoint {
+  JacobianPoint { x: p.x, y: curve_fsub(c: c, a: montgomery_to(ctx: c.field, a: bignat_zero_limbs()), b: p.y), z: p.z }
+}
+
 // ── Public key validation (SP 800-186 §D.1.1 partial validation: on the curve, in range) ─────
 fn curve_on_curve(c: PrimeCurve, x: BigNat, y: BigNat) -> Bool {
   let xm = montgomery_to(ctx: c.field, a: x)
@@ -169,14 +192,6 @@ fn curve_on_curve(c: PrimeCurve, x: BigNat, y: BigNat) -> Bool {
   bignat_compare(a: curve_fsqr(c: c, a: ym), b: curve_fadd(c: c, a: curve_fsub(c: c, a: x3, b: three_x), b: bm)) == 0
 }
 
-fn bignat_below(a: BigNat, m: BigNat) -> Bool {
-  bignat_compare(a: a, b: m) < 0
-}
-
-fn bignat_nonzero_below(a: BigNat, m: BigNat) -> Bool {
-  !bignat_is_zero(a: a) && bignat_below(a: a, m: m)
-}
-
 // Split a list after `n` elements.
 type OctetSplit {
   front: List<UInt8>

dag/extdeps/crypto/sha2.dag

@@ -411,6 +411,3 @@ fn sha384(message: List<UInt8>) -> List<UInt8> {
   fold([s.a, s.b, s.c, s.d, s.e, s.f], init: [], f: (acc, w) => list_append_octets(left: acc, right: word64_octets(w: w)))
 }
 
-fn sha384_hex(message: List<UInt8>) -> String {
-  base16_encode_lower(octets: sha384(message: message))
-}