C Part II · Module 24 · C Reference Models and Scoreboards
Encoder, Decoder and Packet Transformation Models
Only one of a transformation model's two obligations is cheap to check, and it is not the one that matters. Measured: a round trip over 65,536 frames came out exact for a correct encoder-decoder pair, and exact again for a pair that reads the length field's byte order the other way on both sides — so the exhaustive check separated them on nothing at all. A single frame derived by hand from the format clauses separated them immediately. The CRC is no help either: a swapped pair computes a perfectly correct check value over its own wrong bytes.
Expert23 min readCPart IIVerificationDPI-C
Part II · Module 24 · Chapter 24.7 · Encoder, Decoder and Packet Transformation Models
1. Two Halves, Two Obligations
A transformation model comes in a pair: something builds a frame, something takes one apart. The pair has two obligations, and they are routinely conflated.
- The halves must agree with each other — decode undoes encode.
- Both must agree with the wire — the bytes are what the format says.
The first is cheap to check and the second is not, which is why the first gets checked and the second gets assumed.
The format, added to the running example's specification:
P1 A frame is 6 bytes: a 12-bit addr, a 4-bit kind, a 16-bit len, a 16-bit crc.
P2 Byte 0 = addr[11:4]. Byte 1 = addr[3:0] in bits 7:4, kind in bits 3:0.
P3 len occupies bytes 2 and 3, BIG-endian (byte 2 is the high half).
P4 crc occupies bytes 4 and 5, BIG-endian, CRC-16/CCITT-FALSE over bytes 0..3.
P5 A frame whose crc does not match is invalid and must be rejected.Clause P3 exists because Chapter 14.3 established that byte order is a thing a specification must choose rather than something a reader can infer. This chapter is what happens when the clause is there and the implementation reads it the other way.
2. Deriving a Frame by Hand
Chapter 24.5 §1's order applies: validate the model before it judges anything, and for a format with no published vectors the independent answer is a hand derivation — Chapter 22.5 §4's technique.
For addr = 0x123, kind = 0x5, len = 0x00FF, read straight off P2 and P3:
P2: byte0 = addr[11:4] = 0x12 ; byte1 = addr[3:0]<<4 | kind = 0x35
P3: byte2 = len high = 0x00 ; byte3 = len low = 0xFFMeasured, the encoder against that derivation:
encoder gives : 12 35 00 FF 42 AA
bytes 0..3 match the hand derivation: yes
P4: CRC-16/CCITT-FALSE over those 4 bytes = 0x42AA, encoded as 42 AA: yesFour bytes derived by reading two clauses, and the CRC from Chapter 24.5's already-validated model. That took about two minutes and it is the only check in this chapter that looks at the wire.
3. The Round Trip, and What It Separates
Now the cheap check. Measured, every address and kind — 4096 × 16:
65536 frames, correct pair: round trip exactExhaustive over the address and kind space, and exact. That is a genuinely useful result: it means the two halves agree with each other on every frame they will ever see.
Now the same check on a pair that reads P3 the other way — little-endian in both the encoder and the decoder, which is what one person writing both in one sitting produces:
65536 frames, swapped pair : round trip exactAlso exact. Sixty-five thousand frames, every address, every kind, and the round trip cannot tell the two pairs apart.
And what the swapped pair puts on the wire:
but on the wire it emits: 12 35 FF 00 5F A5
against the hand-derived 12 35 00 FF : MISMATCH on bytes 2 and 3One frame. The hand derivation from §2 separates them on the first attempt, on bytes 2 and 3, exactly where P3 says the length lives.
4. What the Round Trip Is Actually For
This chapter's purpose asks for the round trip to be used as "an independent check on both halves", and the measurement above shows exactly what that phrase can and cannot mean. Both halves of the answer are true and worth stating together.
It is an independent check that the halves agree with each other — and that is genuinely valuable. Chapter 22.5 §3 measured it catching an asymmetric bug decisively: a decoder reading a field one bit too narrow failed 8 of 16 round trips. Any error in one half and not the other is caught, exhaustively, for free.
It is structurally unable to check either half against the wire. A symmetric error — both halves reading P3 the same wrong way — cancels by construction on every input, which is why 65,536 frames found nothing.
So the two checks are not alternatives and neither substitutes for the other:
- the round trip answers "do these two agree?" — exhaustively, cheaply, and catches every asymmetric bug
- a hand-derived frame answers "is this the right format?" — and one frame is enough
Chapter 22.5 §5 reached the identical conclusion on a 4-bit codec. This chapter is the same result on a realistic frame with a CRC, at 65,536 frames instead of 16, which is worth having because the scale is the thing that makes a round trip feel conclusive.
5. The Misconception: The CRC Will Catch It
"There is a check value over the frame. A byte-order error would change the bytes, so the CRC would not match."
Measured false, and the reason is worth understanding rather than memorising.
The swapped pair's CRC is correct. It is 0x5FA5 — a perfectly valid CRC-16/CCITT-FALSE over the bytes 12 35 FF 00, computed by the same validated CRC model used everywhere else in this module. The encoder computed the right check value over the wrong bytes, and the decoder verified it and accepted.
A check value verifies that bytes arrived as they were sent. It has no opinion about which bytes should have been sent.
And the rejection behaviour is intact too. Measured, flipping each of the 48 bits of a frame in turn:
48 single-bit corruptions: 48 rejected, 0 acceptedBoth pairs reject all 48. The swapped pair is a fully functional implementation of a frame format — just not the one in the specification. It would interoperate perfectly with another copy of itself and not at all with anything that read P3 correctly.
That is the general shape and it applies well beyond byte order:
An integrity check is downstream of the format decision. It protects the bytes you chose to send; it cannot tell you that you chose the wrong ones. Only a value derived from the format, outside both halves, can do that.
6. What You Should Be Able to Say Now
- Two obligations: the halves agree with each other, and both agree with the wire. Only the first is cheap.
- Derive one frame by hand from the layout clauses — measured,
12 35 00 FFfrom P2 and P3, matching the encoder. - And the check value with it — measured, 0x42AA over bytes 0..3, from Chapter 24.5's already-validated CRC.
- The round trip is exhaustive and exact — measured, 65,536 frames for the correct pair.
- And exact for a pair that swaps the length bytes on both sides — the same 65,536 frames separate nothing.
- One hand-derived frame separates them — measured,
12 35 FF 00, caught on bytes 2 and 3. - What the round trip is for: it catches every asymmetric bug (22.5: 8 of 16) and is structurally unable to catch a symmetric one.
- The CRC does not help — measured, 0x5FA5 is a correct check value over the wrong bytes.
- An integrity check is downstream of the format decision: it protects the bytes you chose, not the choice.
- Rejection is intact in both — measured, 48 of 48 single-bit corruptions rejected by each pair.
- Only the hand-derived frame requires reading the specification; everything else can pass against a model that read it wrong.
7. Exercises
- Derive the first four bytes of a frame by hand from a format you work with, showing which clause gives each byte. How long did it take?
- Build an encoder and decoder pair and round-trip the whole address space. What have you established, stated as precisely as §4 does?
- Swap a multi-byte field's order in both halves. Does the round trip still pass? Over how many frames?
- Now compare one frame against your hand derivation. How many bytes differ, and are they the ones you expected?
- Compute the check value of the swapped frame. Is it correct? Explain what "correct" means in that sentence.
- Flip each bit of a frame in turn and count rejections. Do this for both pairs — what does the result tell you about rejection as evidence?
- §5 says an integrity check is downstream of the format decision. Give a second example, not involving byte order, where the same reasoning applies.
- List every check your project runs on a transformation model. Which of them could pass against a model that read the format wrong?
8. Summary
- Two obligations: halves agree with each other · both agree with the wire.
- Measured: a hand-derived frame gives
12 35 00 FF, and the encoder matches; the check value is 0x42AA. - Round trip, 65,536 frames: exact for the correct pair and exact for the swapped pair — it separates nothing.
- One hand-derived frame separates them on bytes 2 and 3.
- The round trip catches every asymmetric bug (22.5: 8 of 16) and cannot catch a symmetric one.
- The CRC does not help — 0x5FA5 is a correct check value over the wrong bytes.
- An integrity check is downstream of the format decision.
- Measured, 48 of 48 corruptions rejected — by both pairs.
- Only the hand-derived frame requires reading the specification.
Every chapter since 24.4 has produced a mismatch and quoted a count. What has been left implicit is what the comparison actually does with the two values it is handed — whether it looks at all of them, whether it puts them in the same form first, and what it says when they differ.
Where this fits
Part of the C Programming curriculum.
