Hi,
continuing with the thread from #4, here the second discrepancy:
2. Ct1Ack is defined in the spec but it is not emitted; code adds undocumented behavior
2a. EkSentCt1Received.Send — spec sends None, code sends Ct1Ack
Spec (page 15, EkSentCt1Received.Send):
msg = {epoch: state.epoch, type: None}
Code (src/v1/chunked/states.rs:178–183):
Self::EkSentCt1Received(state) => {
let epoch = state.epoch();
Ok(Send {
state: Self::EkSentCt1Received(state),
msg: Message { epoch, payload: MessagePayload::Ct1Ack(true) },
key: None,
})
}
2b. EkReceivedCt1Sampled.Receive — spec accepts only EkCt1Ack, code also accepts Ct1Ack
Spec (page 20–21, EkReceivedCt1Sampled.Receive):
if msg.epoch == state.epoch and msg.type == EkCt1Ack:
# Transition (12) → Ct2Sampled
Code (src/v1/chunked/states.rs:464–467):
if matches!(msg.payload, MessagePayload::Ct1Ack(true) | MessagePayload::EkCt1Ack(_)) {
Self::Ct2Sampled(state.recv_ct1_ack(msg.epoch))
}
2c. §2.3 defines Ct1Ack but no Send function in §2.5 produces it
§2.3 lists Ct1Ack as a message type ("No payload, but the sender has completely received ct1"). But inspecting the Send functions in §2.5 we don't see any emitting Ct1Ack message.
Hi,
continuing with the thread from #4, here the second discrepancy:
2.
Ct1Ackis defined in the spec but it is not emitted; code adds undocumented behavior2a.
EkSentCt1Received.Send— spec sendsNone, code sendsCt1AckSpec (page 15,
EkSentCt1Received.Send):Code (
src/v1/chunked/states.rs:178–183):2b.
EkReceivedCt1Sampled.Receive— spec accepts onlyEkCt1Ack, code also acceptsCt1AckSpec (page 20–21,
EkReceivedCt1Sampled.Receive):Code (
src/v1/chunked/states.rs:464–467):2c. §2.3 defines
Ct1Ackbut noSendfunction in §2.5 produces it§2.3 lists
Ct1Ackas a message type ("No payload, but the sender has completely received ct1"). But inspecting theSendfunctions in §2.5 we don't see any emittingCt1Ackmessage.