Check in emitted CMS Rust module (fully verified)

Author: y1ca1

.github/workflows/ci.yml

@@ -83,16 +83,24 @@ jobs:
         include:
           - name: vest_lib-core
             cargo_args: -p vest_lib --no-default-features
+            verus_args: --expand-errors
           - name: vest_lib-alloc
             cargo_args: -p vest_lib --no-default-features --features alloc
+            verus_args: --expand-errors
           - name: vest_lib-std
             cargo_args: -p vest_lib
+            verus_args: --expand-errors
           - name: vest-tests
             cargo_args: -p vest_tests
+            verus_args: --expand-errors
+          # --rlimit matches vest_asn1_tests/Makefile: the width stress fixture
+          # needs more SMT budget than the Verus default.  Keep the two in step.
           - name: vest-asn1-tests
             cargo_args: -p vest_asn1_tests
+            verus_args: --expand-errors --rlimit 100
           - name: vest-dev
             cargo_args: -p vest_dev
+            verus_args: --expand-errors
     name: Verify ${{ matrix.name }}
     steps:
       - uses: actions/checkout@v4
@@ -114,7 +122,7 @@ jobs:
           restore-keys: |
             linux-verus-${{ matrix.name }}-
             linux-verus-
-      - run: cargo verus verify ${{ matrix.cargo_args }} -- --expand-errors
+      - run: cargo verus verify ${{ matrix.cargo_args }} -- ${{ matrix.verus_args }}
 
   verify-macos:
     if: github.event_name == 'schedule'
@@ -132,5 +140,5 @@ jobs:
         run: echo "${{ github.workspace }}/.verus" >> "$GITHUB_PATH"
       - run: cargo verus verify -p vest_lib -- --expand-errors
       - run: cargo verus verify -p vest_tests -- --expand-errors
-      - run: cargo verus verify -p vest_asn1_tests -- --expand-errors
+      - run: cargo verus verify -p vest_asn1_tests -- --expand-errors --rlimit 100
       - run: cargo verus verify -p vest_dev -- --expand-errors

README.md

@@ -23,7 +23,7 @@ proofs.
 - [`vest_lib/`](vest_lib/) — verified parser and serializer combinators;
 - [`vest_asn1/`](vest_asn1/) — an ASN.1 frontend targeting the same backend;
 - [`vest_tests/`](vest_tests/) — DSL fixtures, including TLS and Bitcoin;
-- [`vest_asn1_tests/`](vest_asn1_tests/) — generated DER, BER, and mixed-rule fixtures; and
+- [`vest_asn1_tests/`](vest_asn1_tests/) — generated DER, BER, and mixed-rule fixtures, including the curated RFC 5652 CMS module; and
 - [`vest_dev/`](vest_dev/) — handwritten formats and development examples.
 
 `vest_lib` includes primitive integer and byte formats, dependent and recursive
@@ -99,7 +99,7 @@ cargo check -p vest_lib --no-default-features --all-targets
 cargo check -p vest_lib --no-default-features --features alloc --all-targets
 cargo verus verify -p vest_lib -- --expand-errors
 cargo verus verify -p vest_tests -- --expand-errors
-cargo verus verify -p vest_asn1_tests -- --expand-errors
+cargo verus verify -p vest_asn1_tests -- --expand-errors --rlimit 100
 ```
 
 Regenerate checked-in fixtures with `make -C vest_tests vest` and

vest_asn1/README.md

@@ -127,12 +127,25 @@ silent approximation.
 
 ## Tests
 
-The checked-in DER, BER, and mixed-rule fixtures under `test/` cover nominal
-formats, inline helpers, slice serialization, tagging, OPTIONAL, DEFAULT,
-CHOICE, SEQUENCE/SET OF, heterogeneous DER SET, ENUMERATED, OID and REAL round
-trips, BER constructed values, SIZE refinements, and generated proof
-interfaces.
-
-Run `make test` or `make verify` in `test/` to test or verify the generated
-fixtures. Codegen freshness is checked by `cargo test`; set `UPDATE_GOLDEN=1`
-when intentionally regenerating the checked-in Rust files.
+The checked-in DER, BER, and mixed-rule fixtures in
+[`vest_asn1_tests/`](../vest_asn1_tests/) cover nominal formats, inline helpers,
+slice serialization, tagging, OPTIONAL, DEFAULT, CHOICE, SEQUENCE/SET OF,
+heterogeneous DER SET, ENUMERATED, OID and REAL round trips, BER constructed
+values, SIZE refinements, and generated proof interfaces.
+
+Two further fixtures are scalability probes rather than feature coverage:
+`schema_depth.asn1` chains 18 nested definitions, and `schema_width.asn1` is a
+16-field SEQUENCE cycling OPTIONAL, DEFAULT, and required components. The width
+fixture needs a raised SMT ceiling; see the `VERUS_ARGS` comment in
+[`vest_asn1_tests/Makefile`](../vest_asn1_tests/Makefile).
+
+`generated_cms.rs` compiles the curated RFC 5652 CMS module in
+[`rfcs/`](rfcs/) — a BER envelope with a DER island, and the largest schema in
+the corpus. [`rfcs/README.md`](rfcs/README.md) derives the encoding-rule split
+from RFC 5652, RFC 5280, and RFC 5755, and records the resulting strictness
+deviations.
+
+Run `make -C ../vest_asn1_tests test` or `make -C ../vest_asn1_tests verify` to
+test or verify the generated fixtures, and `make -C ../vest_asn1_tests generate`
+to regenerate them. Codegen freshness is checked by `cargo test`; set
+`UPDATE_GOLDEN=1` when intentionally regenerating the checked-in Rust files.

vest_asn1/rfcs/README.md

@@ -0,0 +1,132 @@
+# Curated RFC schemas
+
+This directory holds ASN.1 modules transcribed from published RFCs, curated so
+that `vest_asn1` can compile them. They are inputs to the verification corpus,
+not part of the `vest_asn1` library.
+
+| Schema | Source | Generated module |
+| --- | --- | --- |
+| [`CMS-RFC5652-Curated.asn1`](CMS-RFC5652-Curated.asn1) | RFC 5652 §12, with structured dependencies from RFC 5280 App. A and RFC 5755 §4 | [`vest_asn1_tests/src/generated_cms.rs`](../../vest_asn1_tests/src/generated_cms.rs) |
+
+The header comment of each schema records its curation rules — what was
+expanded, what was replaced by ordinary wire types, and what was deliberately
+left out.
+
+## Generating `generated_cms.rs`
+
+The rule is recorded once, in the `generate` target of
+[`vest_asn1_tests/Makefile`](../../vest_asn1_tests/Makefile). Regenerate with:
+
+```sh
+make -C vest_asn1_tests generate
+```
+
+which runs, for this schema:
+
+```sh
+cargo run -p vest_asn1 -- --rules ber \
+  --der-definition SignedAttributes \
+  --der-definition AuthAttributes \
+  --der-definition Certificate \
+  --der-definition CertificateList \
+  --der-definition AttributeCertificate \
+  --der-definition AttributeCertificateV1 \
+  vest_asn1/rfcs/CMS-RFC5652-Curated.asn1 -o vest_asn1_tests/src/generated_cms.rs
+```
+
+CI regenerates and requires `git diff --exit-code` to be empty, so the committed
+module and this command cannot drift apart.
+
+## Why BER is the default
+
+RFC 5652 §1 states the design intent for every CMS content type:
+
+> As a general design philosophy, each content type permits single pass
+> processing using indefinite-length Basic Encoding Rules (BER) encoding.
+
+and §5.2 confirms that the carried content itself is unconstrained:
+
+> The eContent need not be DER encoded.
+
+So the CMS envelope — `ContentInfo`, `SignedData`, `EnvelopedData`,
+`DigestedData`, `EncryptedData`, `AuthenticatedData`, the `RecipientInfo`
+family, `SignerInfo`, and the unsigned/unauthenticated/unprotected attribute
+sets — is generated under BER.
+
+## Why the overrides are DER
+
+Each override is a structure whose octets are an input to a signature or digest.
+A verifier that does not re-encode — and a Vest-generated parser must not
+re-encode, since re-encoding is precisely the step that reintroduces
+malleability — has to receive those octets already in DER.
+
+| Definition | Authority | Text |
+| --- | --- | --- |
+| `SignedAttributes` | RFC 5652 §5.3 | "SignedAttributes MUST be DER encoded, even if the rest of the structure is BER encoded." |
+| `AuthAttributes` | RFC 5652 §9.1 | "The AuthAttributes structure MUST be DER encoded, even if the rest of the structure is BER encoded." |
+| `Certificate` | RFC 5280 §4.1.1.3 | "The signatureValue field contains a digital signature computed upon the ASN.1 DER encoded tbsCertificate." |
+| | RFC 5755 §7.3 | "the digest MUST be calculated over the DER encoding of the entire PKC, including the signature value." |
+| `CertificateList` | RFC 5280 §5.1.1.3 | "The signatureValue field contains a digital signature computed upon the ASN.1 DER encoded tbsCertList." |
+| `AttributeCertificate` | RFC 5755 §7.3 | Same signed-object shape; RFC 5755 §4 profiles ACs on top of RFC 5280. |
+| `AttributeCertificateV1` | RFC 5652 §12.2 | Same signed-object shape. Declared obsolete by §10.2.2, but retained for backward compatibility. |
+
+RFC 5652 §1 also says that "signed attributes and authenticated attributes are
+the only data types used in the CMS that require DER encoding". That is a
+statement about the types CMS itself defines. `Certificate`, `CertificateList`,
+and `AttributeCertificate` are imported from RFC 5280 and RFC 5755, and are
+governed by those documents.
+
+`vest_asn1` propagates a rule to every transitive child of an overridden
+definition without changing its parents, so the six roots above put the whole
+X.509 subtree under DER — `TBSCertificate`, `AlgorithmIdentifier`, `Name`,
+`RDNSequence`, `Extensions`, `Validity`, `SubjectPublicKeyInfo`, `GeneralName`,
+the X.400 `ORAddress` subtree, and `Attribute`/`AttributeValue`. The result is a
+62/62 split between DER and BER nominal formats.
+
+`PersonalName` lands in that closure via
+`AttributeCertificate → GeneralNames → GeneralName → ORAddress →
+BuiltInStandardAttributes`. It has to: it is a heterogeneous `SET`, and BER
+permits a `SET` to carry its components in any order, so `vest_asn1` emits
+heterogeneous `SET`s only under DER, where X.690 clause 11 fixes them in
+ascending tag order and a single fixed-order combinator is sound.
+
+## What is deliberately *not* overridden
+
+`ExtendedCertificate` is a signed object too, but its closure reaches
+`UnauthAttributes`, which CMS leaves under BER. Forcing it to DER would make
+unauthenticated attributes stricter than RFC 5652 allows. RFC 5652 §10.2.2 also
+declares it obsolete:
+
+> The PKCS #6 extended certificate is obsolete. The PKCS #6 certificate is
+> included for backward compatibility, and PKCS #6 certificates SHOULD NOT be
+> used.
+
+so it stays BER.
+
+## Known strictness deviations
+
+`vest_asn1` gives each definition exactly one rule, so a definition shared
+between a DER and a BER context resolves to DER. Two shared definitions in this
+schema are therefore stricter than RFC 5652 alone requires:
+
+- **`Attribute` / `AttributeValue`** are DER because `SignedAttributes` and
+  `AuthAttributes` reach them. `UnsignedAttributes`, `UnauthAttributes`, and
+  `UnprotectedAttributes` remain BER `SET OF`s, but their *elements* must now be
+  DER-encoded. RFC 5652 permits BER there.
+- **`AlgorithmIdentifier`** is DER because `TBSCertificate` reaches it. The
+  aliases `DigestAlgorithmIdentifier`, `SignatureAlgorithmIdentifier`,
+  `KeyEncryptionAlgorithmIdentifier`, `ContentEncryptionAlgorithmIdentifier`,
+  `MessageAuthenticationCodeAlgorithm`, and `KeyDerivationAlgorithmIdentifier`
+  stay BER as parents, but the algorithm identifier they wrap — including the
+  one in a BER `SignerInfo` — must be DER-encoded. RFC 5652 permits BER there.
+
+Both narrow the set of accepted encodings; neither accepts anything the RFCs
+reject. Splitting the shared definitions in the curated schema would remove them
+at the cost of introducing type names that do not appear in the source RFCs.
+
+## Scope
+
+This is a wire schema. It does not express CMS version-selection rules,
+algorithm policy, attribute uniqueness, `ANY DEFINED BY` dispatch, or any
+cryptographic validation. See [`../scalability.md`](../scalability.md) for how
+this module drove the nominal-format and start-domain design.

vest_asn1_tests/Makefile

@@ -12,10 +12,46 @@ generate:
 		schema_depth.asn1 -o src/generated_stress_depth.rs
 	cargo run --manifest-path ../Cargo.toml -p vest_asn1 -- --rules ber \
 		schema_width.asn1 -o src/generated_stress_width.rs
+# CMS is a BER envelope around a DER island.  BER is the default because RFC 5652
+# section 1 designs every content type for "single pass processing using
+# indefinite-length Basic Encoding Rules".  Each DER override below is a
+# structure whose octets are a signature or digest input, so a parser that must
+# not re-encode has to receive it already in DER:
+#
+#   SignedAttributes       RFC 5652 5.3   "MUST be DER encoded, even if the rest
+#   AuthAttributes         RFC 5652 9.1    of the structure is BER encoded"
+#   Certificate            RFC 5280 4.1.1.3 signature is over the DER tbsCertificate;
+#                          RFC 5755 7.3   "the DER encoding of the entire PKC"
+#   CertificateList        RFC 5280 5.1.1.3 signature is over the DER tbsCertList
+#   AttributeCertificate   RFC 5755 7.3   same signed-object shape
+#   AttributeCertificateV1 RFC 5652 12.2  same signed-object shape
+#
+# The rule propagates to every transitive child, which is what puts the whole
+# X.509 subtree (AlgorithmIdentifier, Name, Extensions, GeneralName, ORAddress,
+# PersonalName, ...) and Attribute/AttributeValue under DER.  ExtendedCertificate
+# is deliberately NOT overridden: its closure reaches UnauthAttributes, which CMS
+# leaves BER, and RFC 5652 section 10.2.2 declares PKCS #6 extended certificates
+# obsolete.  See ../vest_asn1/rfcs/README.md for the full derivation.
+	cargo run --manifest-path ../Cargo.toml -p vest_asn1 -- --rules ber \
+		--der-definition SignedAttributes \
+		--der-definition AuthAttributes \
+		--der-definition Certificate \
+		--der-definition CertificateList \
+		--der-definition AttributeCertificate \
+		--der-definition AttributeCertificateV1 \
+		../vest_asn1/rfcs/CMS-RFC5652-Curated.asn1 -o src/generated_cms.rs
 
 test: generate
 	cargo test
 
+# schema_width.asn1 is a deliberate scalability probe: a 16-field BER SEQUENCE
+# cycling OPTIONAL, DEFAULT, and required components.  Its nominal exec proof
+# needs more SMT budget than the Verus default, so this crate raises the ceiling.
+# Everything else here verifies well inside the default limit.  --rlimit is a
+# resource ceiling, not a soundness setting.  Keep this value in step with the
+# `vest-asn1-tests` entry in .github/workflows/ci.yml.
+VERUS_ARGS := --expand-errors --rlimit 100
+
 verify: generate
 	touch src/lib.rs
-	cargo verus verify -- --expand-errors
+	cargo verus verify -- $(VERUS_ARGS)