proof: partition byte forgeries by returned component coverage

contracts/verification/easycrypt/c10-port/RAW-ADAPTIVE-EXPOSURES.md

@@ -75,3 +75,8 @@ component coordinates or values. #100 and #295 remain open. No new project
 axiom, admit, clone assumption, runtime, wire or parameter change is introduced.
 Rust extraction, concrete SHA-256, QROM and production assurance remain separate;
 the owner-triggered combined playbook pass #509 remains deferred.
+
+The later [returned-coordinate partition](RAW-FORGERY-PARTITION.md) retains
+response widths, proves exact ordinary/special returned-value agreement, and
+refines the actual game into explicit new-component/private/coverage cases.
+Their numerical charges and general information-exposure analysis remain open.

contracts/verification/easycrypt/c10-port/RAW-FORGERY-PARTITION.md

@@ -0,0 +1,73 @@
+# Returned-coordinate forgery partition
+
+This extends the [adaptive response ledger](RAW-ADAPTIVE-EXPOSURES.md) in the
+manual classical ideal-oracle model. The original signer, byte client, observer,
+oracle calls, counters, failure behavior and game are unchanged.
+
+`ExposureWidths.ec` proves that every successful response in the existing log
+has the actual signature widths, through subsequent adaptive calls and final
+verification. `ForsRootDeterminism.ec` proves uniqueness of complete FORS roots
+at fixed coordinates in the same public/private tables. It needs no collision
+exclusion: this is determinism of the retained reference construction.
+
+`ExposurePrivate.ec` combines each logged response's retained forest reference
+with the previous reverse-recovery theorem. Outside the explicit public-node
+collision event, an ordinary returned value equals the private-table value at
+its exact hypertree/tree/leaf coordinate. The thirteenth value is the complete
+tree-12 root, not an ordinary secret at index zero. Widths are used explicitly,
+including when changing the default value of an in-range list lookup.
+
+`ExposureCoverage.ec` defines coverage over **all** responses. Each of the
+twelve ordinary target coordinates must have been selected by some logged
+response at the same hypertree index. Different trees may use different prior
+responses. Repeats preserve the predicate; the empty log covers nothing. When
+the forged forest has private openings and all coordinates are covered, all
+twelve supplied values equal corresponding logged outputs, and its special
+root equals a logged special root. Otherwise, the proof identifies an ordinary
+coordinate absent from every returned response, together with the supplied
+value's exact private-table witness. This is absence from returned coordinates,
+not secrecy: public queries, intermediate values, other coordinates or guesses
+may still disclose the value.
+
+`ExposureComponents.ec` identifies the component messages of every logged
+response using its retained construction references and actual layer signature.
+A missing lower-root reference yields a top WOTS message unequal to every
+returned top message at that address. A missing forest-root reference similarly
+yields a new bottom WOTS message. These results do not exclude previously
+disclosed WOTS chain values or prove that either case is hard.
+
+`ExposurePartition.ec` and `ExposurePartitionGame.ec` refine the existing
+successful new-message extraction into four residual cases:
+
+1. A top WOTS opening on a new component message.
+2. Linked layer openings with a new bottom WOTS component message.
+3. Linked private FORS openings with an unreturned ordinary coordinate.
+4. Linked private FORS openings covered by accumulated responses, with exact
+   returned-value agreement including the special root.
+
+The theorem preserves the original message-freshness guard, public seed/root
+binding and signing cap. A separate lemma proves that the forged message's
+H_msg input differs from every logged response's H_msg input, using signature
+widths. It does **not** assert freshness against prior public queries.
+
+`ExposurePartitionHop.ec::byte_exposure_partition_hop` carries this partition
+into the existing real-to-independent probability hop via the exact passive
+observer projection. The residual still includes successful forgery `res` and
+the public collision/zero exclusions. The collision, zero-node and secret-prefix
+charges are unchanged. None of the four residual cases receives a numerical
+charge here; the result is not a nontrivial closed EUF bound.
+
+All new modules are replay targets under both proof drivers. Enrollment retains
+the old theorem statements and assumption census and introduces no project
+axiom, admit or clone assumption. Controls include exact consumers, empty/repeat
+and ordinary/special boundaries, a conditional mixed-coverage consumer, scope
+probes and deliberately mismatched theorem applications. The mixed consumer
+is not a constructed concrete counterexample. Rejected applications do not
+prove altered statements false or premises necessary. Scope probes remain
+name-level checks rather than full soundness or nonvacuity proofs.
+
+General information-exposure accounting, reverse-chain/private-guess and
+encoding/ITSR probability charges, and the final numerical bound remain open
+under #100/#295. Rust extraction, concrete SHA-256, QROM and production assurance
+remain separate. The combined owner-triggered playbook pass stays deferred
+under #509.

contracts/verification/easycrypt/c10-port/README.md

@@ -94,6 +94,12 @@ the original byte game's probability. All entries retain their construction
 references; the ledger matches the signed-message list and respects the cap.
 Full information-exposure and numerical private/encoding charges remain open.
 
+The [returned-coordinate partition](RAW-FORGERY-PARTITION.md) separates the
+actual game's residual into new WOTS component messages, an unreturned private
+FORS coordinate, or coverage assembled from earlier responses. Covered values
+agree with actual logged outputs; the special root remains separate. These
+cases still need probability charges.
+
 The [control evidence](CONTROL-EVIDENCE.md) distinguishes successful proofs,
 scope checks and expected proof-driver rejections. An exact theorem-statement
 mismatch does not establish that the altered statement is false or that every

contracts/verification/easycrypt/c10-port/cdrafts-split/ExposureComponents.ec

@@ -0,0 +1,57 @@
+(* Missing reference messages differ from every retained returned component message. *)
+require import AllCore List FMap IntDiv.
+require import C10RawOracle C10HashDomains RawKeygen RawForest RawSigner.
+require import ExposureLog ExposureSupport ExposureReferences.
+require import MerkleRootWitness ForestRootWitness LayerSignOpening VerifierWotsOpening.
+require import SubtreeOpeningCases ForestOpeningCases.
+
+op returned_top_message h s seed root (entries : signing_exposure list) tree value =
+  exists message signature d top, List.mem entries (message,signature) /\
+    h.[hmsg_input seed root (pad signature.`1) message]=Some d /\ hypertree_index d %/512=tree /\
+    merkle_root_witness h s seed 0 tree value /\
+    layer_opening h s seed 1 0 tree value (nth ([],0,[]) signature.`4 1) top.
+op returned_bottom_message h s seed root (entries : signing_exposure list) ht value =
+  exists message signature d lower, List.mem entries (message,signature) /\
+    h.[hmsg_input seed root (pad signature.`1) message]=Some d /\ hypertree_index d=ht /\
+    forest_root_witness h s seed ht value /\
+    layer_opening h s seed 0 (ht %/512) (ht %%512) value (nth ([],0,[]) signature.`4 0) lower.
+
+lemma logged_component_messages h s seed root entries message signature d :
+  exposures_supported h s seed root entries => List.mem entries (message,signature) =>
+  h.[hmsg_input seed root (pad signature.`1) message]=Some d =>
+  exists forest lower,
+    returned_bottom_message h s seed root entries (hypertree_index d) forest /\
+    returned_top_message h s seed root entries (hypertree_index d %/512) lower.
+proof.
+  move=> hs hm hd.
+  have [ha [forest lower upper top [hf [ho [hb [hr ht]]]]]] :=
+    logged_digest_references h s seed root entries message signature d hs hm hd.
+  exists forest upper; split.
+  + exists message signature d lower; smt().
+  exists message signature d top; smt().
+qed.
+
+op new_top_component h s seed root entries d (sig : raw_signature) =
+  exists lower leaf,
+    !returned_top_message h s seed root entries (hypertree_index d %/512) lower /\
+    wots_verifier_opening h s seed 1 0 (hypertree_index d %/512)
+      lower leaf ((nth ([],0,[]) sig.`4 1).`1,(nth ([],0,[]) sig.`4 1).`2).
+op new_bottom_component h s seed root entries d (sig : raw_signature) =
+  exists forest lower bottom_leaf top_leaf,
+    linked_forest_layers h s seed d sig forest lower bottom_leaf top_leaf /\
+    !returned_bottom_message h s seed root entries (hypertree_index d) forest.
+
+lemma missing_top_is_new_component h s seed root entries d sig :
+  unrecorded_top_message h s seed d sig => new_top_component h s seed root entries d sig.
+proof.
+  move=> [lower leaf [hn ho]]; exists lower leaf; split; last exact ho.
+  rewrite /returned_top_message; smt().
+qed.
+
+lemma missing_forest_is_new_component h s seed root entries d sig :
+  unrecorded_forest_message h s seed d sig => new_bottom_component h s seed root entries d sig.
+proof.
+  move=> [forest lower bottom_leaf top_leaf [hl hn]].
+  exists forest lower bottom_leaf top_leaf; split; first exact hl.
+  rewrite /returned_bottom_message; smt().
+qed.

contracts/verification/easycrypt/c10-port/cdrafts-split/ExposureCoverage.ec

@@ -0,0 +1,110 @@
+(* Coordinate coverage may combine different previous responses for different trees. *)
+require import AllCore List FMap.
+require import C10RawOracle C10HashDomains RawKeygen RawForest RawSigner RawSignature.
+require import ExposureLog ExposureSupport ExposureReferences ExposureWidths ExposurePrivate.
+require import ForestRootWitness ForsRootWitness ForsRootDeterminism ForsPrivateLeaves MemoNodeCollision.
+
+op logged_digest h seed root (entries : signing_exposure list) (d : digest) =
+  exists message signature, List.mem entries (message,signature) /\
+    h.[hmsg_input seed root (pad signature.`1) message]=Some d.
+op returned_coordinate h seed root entries ht tree index =
+  0<=tree<12 /\ exists d, logged_digest h seed root entries d /\
+    hypertree_index d=ht /\ forest_index d tree=index.
+op returned_coverage h seed root entries d =
+  forall tree, 0<=tree<12 =>
+    returned_coordinate h seed root entries (hypertree_index d) tree (forest_index d tree).
+
+lemma returned_coordinate_value h seed root entries ht tree index :
+  returned_coordinate h seed root entries ht tree index <=>
+  exists value, logged_fors_value h seed root entries ht tree index value.
+proof. rewrite /returned_coordinate /logged_digest /logged_fors_value; smt(). qed.
+
+lemma returned_coverage_empty h seed root d : !returned_coverage h seed root [] d.
+proof. rewrite /returned_coverage /returned_coordinate /logged_digest /=; smt(). qed.
+
+lemma returned_coverage_repeat h seed root entries d :
+  returned_coverage h seed root (entries++entries) d = returned_coverage h seed root entries d.
+proof. rewrite /returned_coverage /returned_coordinate /logged_digest; smt(mem_cat). qed.
+
+lemma returned_coordinate_cat h seed root entries1 entries2 ht tree index :
+  returned_coordinate h seed root (entries1++entries2) ht tree index =
+  (returned_coordinate h seed root entries1 ht tree index \/ returned_coordinate h seed root entries2 ht tree index).
+proof. rewrite /returned_coordinate /logged_digest; smt(mem_cat). qed.
+
+lemma logged_digest_covers_itself h seed root entries d :
+  logged_digest h seed root entries d => returned_coverage h seed root entries d.
+proof. rewrite /returned_coverage /returned_coordinate; smt(). qed.
+
+lemma private_covered_value h s seed root entries d secrets tree :
+  exposures_supported h s seed root entries => exposures_width entries =>
+  !public_node_collision h => forest_private_openings h s seed (hypertree_index d) d secrets =>
+  returned_coordinate h seed root entries (hypertree_index d) tree (forest_index d tree) =>
+  logged_fors_value h seed root entries (hypertree_index d) tree (forest_index d tree)
+    (nth (nseq 16 0) secrets tree).
+proof.
+  move=> hs hw hn [hp hl] hc.
+  have [value hv] : exists value, logged_fors_value h seed root entries (hypertree_index d) tree (forest_index d tree) value
+    by smt(returned_coordinate_value).
+  have [sd [hd he]] := logged_fors_private_value h s seed root entries (hypertree_index d)
+    tree (forest_index d tree) value hs hw hn hv.
+  have htr : 0<=tree<12 by move: hc; rewrite /returned_coordinate; smt().
+  have [sd' [hd' he']] := hp tree htr.
+  have heq : value=nth (nseq 16 0) secrets tree by smt().
+  by rewrite -heq.
+qed.
+
+lemma coverage_returns_special h s seed root entries d secrets :
+  exposures_supported h s seed root entries => exposures_width entries =>
+  !public_node_collision h => forest_private_openings h s seed (hypertree_index d) d secrets =>
+  returned_coverage h seed root entries d =>
+  logged_special_root h seed root entries (hypertree_index d) (nth (nseq 16 0) secrets 12).
+proof.
+  move=> hs hw hn [hp hl] hc.
+  have [htr [old [ho [hh hi]]]] := hc 0 _; first smt().
+  have [message signature [hm hd]] := ho.
+  have hv : logged_special_root h seed root entries (hypertree_index d) (nth [] signature.`2 12)
+    by exists message signature old; smt().
+  have hr := logged_special_private_root h s seed root entries (hypertree_index d)
+    (nth [] signature.`2 12) hs hw hn hv.
+  have he := fors_root_witness_unique h s seed (hypertree_index d) 12
+    (nth [] signature.`2 12) (nth (nseq 16 0) secrets 12) hr hl.
+  smt().
+qed.
+
+op unreturned_private_opening h s seed root entries d (secrets : raw_input list) =
+  exists tree sd, 0<=tree<12 /\
+    !returned_coordinate h seed root entries (hypertree_index d) tree (forest_index d tree) /\
+    s.[fors_private_key (hypertree_index d) tree (forest_index d tree)]=Some sd /\
+    nth (nseq 16 0) secrets tree=node sd.
+op returned_private_values h seed root entries d (secrets : raw_input list) =
+  (forall tree, 0<=tree<12 => logged_fors_value h seed root entries (hypertree_index d)
+    tree (forest_index d tree) (nth (nseq 16 0) secrets tree)) /\
+  logged_special_root h seed root entries (hypertree_index d) (nth (nseq 16 0) secrets 12).
+
+lemma unreturned_excludes_logged_values h s seed root entries d secrets :
+  unreturned_private_opening h s seed root entries d secrets =>
+  exists tree sd, 0<=tree<12 /\
+    (forall value, !logged_fors_value h seed root entries (hypertree_index d) tree (forest_index d tree) value) /\
+    s.[fors_private_key (hypertree_index d) tree (forest_index d tree)]=Some sd /\
+    nth (nseq 16 0) secrets tree=node sd.
+proof. rewrite /unreturned_private_opening; smt(returned_coordinate_value). qed.
+
+lemma private_opening_coverage_partition h s seed root entries d secrets :
+  exposures_supported h s seed root entries => exposures_width entries =>
+  !public_node_collision h => forest_private_openings h s seed (hypertree_index d) d secrets =>
+  (returned_coverage h seed root entries d /\ returned_private_values h seed root entries d secrets) \/
+    unreturned_private_opening h s seed root entries d secrets.
+proof.
+  move=> hs hw hn hp; case (returned_coverage h seed root entries d) => hc.
+  + left; split; first trivial.
+    rewrite /returned_private_values; split.
+    - move=> tree ht; apply (private_covered_value h s seed root entries d secrets tree) => //; exact (hc tree ht).
+    exact (coverage_returns_special h s seed root entries d secrets hs hw hn hp hc).
+  right; rewrite /unreturned_private_opening.
+  have [tree [ht hu]] : exists tree, 0<=tree<12 /\
+    !returned_coordinate h seed root entries (hypertree_index d) tree (forest_index d tree)
+    by move: hc; rewrite /returned_coverage; smt().
+  have [hp0 hp1] := hp.
+  have [sd [hd hv]] := hp0 tree ht.
+  exists tree sd; smt().
+qed.

contracts/verification/easycrypt/c10-port/cdrafts-split/ExposurePartition.ec

@@ -0,0 +1,61 @@
+(* Four explicit uncharged residual cases for the same new-message forgery. *)
+require import AllCore List FMap.
+require import C10RawOracle C10RawGrind C10HashDomains RawKeygen RawForest RawSigner RawSignature.
+require import ExposureLog ExposureSupport ExposureWidths ExposureCoverage ExposureComponents ExposureAccounting.
+require import MerkleRootWitness ForestRootWitness ForestOpeningCases SessionForestExtraction MemoNodeCollision.
+require import ByteReplay.
+
+op exposure_forgery_cases h s seed root entries d (sig : raw_signature) =
+  new_top_component h s seed root entries d sig \/
+  new_bottom_component h s seed root entries d sig \/
+  (linked_private_openings h s seed d sig /\
+    unreturned_private_opening h s seed root entries d sig.`2) \/
+  (linked_private_openings h s seed d sig /\
+    returned_coverage h seed root entries d /\ returned_private_values h seed root entries d sig.`2).
+
+lemma forest_cases_exposure_partition h s seed root entries d sig :
+  exposures_supported h s seed root entries => exposures_width entries => !public_node_collision h =>
+  forest_opening_cases h s seed d sig => exposure_forgery_cases h s seed root entries d sig.
+proof.
+  move=> hs hw hn [ht | [hf | hp]].
+  + left; exact (missing_top_is_new_component h s seed root entries d sig ht).
+  + right; left; exact (missing_forest_is_new_component h s seed root entries d sig hf).
+  have hprivate : forest_private_openings h s seed (hypertree_index d) d sig.`2
+    by move: hp; rewrite /linked_private_openings; smt().
+  have hc := private_opening_coverage_partition h s seed root entries d sig.`2 hs hw hn hprivate.
+  right; right; smt().
+qed.
+
+op new_message_exposure_partition h s seed root entries =
+  merkle_root_witness h s seed 1 0 root /\
+  exists message sig d, size message=32 /\ signature_width sig /\
+    !List.mem (exposure_messages entries) message /\ accept_digest d /\
+    h.[hmsg_input seed (pad root) (pad sig.`1) message]=Some d /\
+    exposure_forgery_cases h s seed (pad root) entries d sig.
+
+lemma new_message_forest_partition h s seed root entries :
+  exposures_supported h s seed (pad root) entries => exposures_width entries => !public_node_collision h =>
+  new_message_forest_opening h s seed root (exposure_messages entries) =>
+  new_message_exposure_partition h s seed root entries.
+proof.
+  move=> hs hw hn [hr [message sig [hm [hwidth [hf [d [ha [hd hc]]]]]]]].
+  split; first exact hr.
+  exists message sig d.
+  have hp := forest_cases_exposure_partition h s seed (pad root) entries d sig hs hw hn hc.
+  smt().
+qed.
+
+lemma partition_message_input_new seed root entries message (sig : raw_signature) :
+  exposures_width entries => signature_width sig =>
+  !List.mem (exposure_messages entries) message =>
+  forall oldmessage oldsig, List.mem entries (oldmessage,oldsig) =>
+    hmsg_input seed (pad root) (pad sig.`1) message <>
+      hmsg_input seed (pad root) (pad oldsig.`1) oldmessage.
+proof.
+  move=> hw hs hn oldmessage oldsig hm.
+  have he : message<>oldmessage by move: hn; rewrite /exposure_messages; smt(mapP).
+  have ho : signature_width oldsig by smt().
+  have hr : size (pad sig.`1)=size (pad oldsig.`1)
+    by move: hs ho; rewrite /signature_width /pad !size_cat; smt().
+  smt(hmsg_message_injective).
+qed.