Skip to content
Merged
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
6 changes: 3 additions & 3 deletions pkg/tbtc/signer/docs/formal/models/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -33,12 +33,12 @@ Traceability matrix:

- `RoastAttemptStateMachine.tla`:
`MonotonicAttemptNumber`, `ReplaySafe` ->
`validate_attempt_context`, replay guards in start/finalize flow in
`tools/tbtc-signer/src/engine.rs`.
`validate_attempt_context` in `src/engine/roast.rs`; replay guards in
start/finalize flow in `src/engine/signing.rs`.
- `StateKeyProviderPolicy.tla`:
`LoadSuccessImpliesExactBinding`, `FailClosedDisallowedProvider` ->
`decode_encrypted_state_envelope`, `encode_encrypted_state_envelope` in
`tools/tbtc-signer/src/engine.rs`.
`src/engine/persistence.rs`.
- `TeeEnforcementModes.tla`:
`EnforceModeRequiresValidAttestationWithoutOverride`,
`NoDirectDisabledToEnforceTransition` -> policy design in
Expand Down
4 changes: 2 additions & 2 deletions pkg/tbtc/signer/docs/roast-coordinator-seed-derivation.md
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ Coordinator = GoMathRandShuffle(sort_ascending(IncludedSet), SourceSeed_i64)
**not** the engine's internal transcript digest
(`SHA256(message_bytes)`), which continues to feed the
`round_id`/`attempt_id` derivations only. Implemented by
`rfc21_message_digest` in `src/engine.rs`; feeding the transcript
`rfc21_message_digest` in `src/engine/roast.rs`; feeding the transcript
digest here instead was the cross-language coordinator divergence
caught in review of the unification PR.
- `AttemptNumber`: the RFC-21 **0-based** attempt number. The FFI
Expand All @@ -41,7 +41,7 @@ Coordinator = GoMathRandShuffle(sort_ascending(IncludedSet), SourceSeed_i64)
shuffle in `src/go_math_rand.rs`, pinned by keep-core PRs #4026 and
#4027.

Implemented by `roast_attempt_shuffle_seed` in `src/engine.rs`; the
Implemented by `roast_attempt_shuffle_seed` in `src/engine/roast.rs`; the
end-to-end acceptance of a Go-derived context through strict
`StartSignRound` is pinned by
`start_sign_round_accepts_go_derived_attempt_context_in_strict_mode`.
Expand Down
18,248 changes: 0 additions & 18,248 deletions pkg/tbtc/signer/src/engine.rs

This file was deleted.

Loading
Loading