Subject: RE: [rohc] Updated FN Draft - Appendix A

From: "Lars-Erik Jonsson \(LU/EAB\)" <[email-masked]>
Date: Wed, 30 Mar 2005 13:46:22 +0200

> I am going to be out for a week after today. It would be 
> great if you guys could thrash this out (and also let-statements)
> whilst I'm away, so that we can press on with this when I get
> back. 

Actually, I am much more concerned about the let-statement than
about appendix A. For me, appendix A is useless and just an add-on
appendix that I can ignore, it is just that it takes up a couple
of pages I had preferred to not keep in there. But I can live with
it if it makes other people happier. 

However, looking at the let statement:
This is the only mechanism in FN that is not intuitive to me,
considering that I am not reading the FN as mathematics. The
rest of it I can fully interpret, agree with the conceptual
structure of, and see the benefits of for ROHC profile work.
I had preferred a let statement that was only used for the
purpose of making definitions, while having a separate mechanism
for assertions. If people believe that is not doable, which I have
a hard time understanding, then the description of let must at
least be improved so that it can be read without a mathematical
mindset. The example appendix B must then also be expanded to cover
also the assertion usage of let, both when used separately and in
combination with a definition. Currently only the definition usage,
which I find fully intuitive, is exemplified.

So, just to make it clear, I am overall very happy with the current
FN, and I find all mechanisms clearly described and exemplified (in
appendix B), except for let. I'd prefer to be happy also with this
last piece.

Some more comments...
 
> > Of course, the mechanisms of ROHC-FN must be well-defined,
> > but can you give an example where something is not well-defined
> > enough to be unambiguous in section 4?
> 
> See below. However, the nature of these things is that you 
> don't notice the ambiguity until somebody uses it one way and
> somebody else interprets it another. 

You can never be sure. Often you assume people know English, but
in any case you have to make an assumption about what people know.
In normal IETF specifications, writing 7 is enough if you mean
decimal 7, you do not have to define it more formally than that,
as 7 means decimal 7 if nothing else is stated.

> > Looking at appendix A, section by section:
> > 
> > A.1 Reserved words
> > 
> >   I do not believe this adds anything, more than that it summarizes
> >   the mechanism defined by ROHC-FN. To me it is obvious that if you
> >   define packet formats with ROHC-FN, you can not use the same words
> >   with a different meaning without explicitly stating that you have
> >   overridden it.
> > 
> >   Summary: It could be useful with a summary of all keywords, in
> >            the beginning of the document, but it is not needed.
> 
> OK, I understand what you're saying. Part of the problem here 
> is the fact that we're using ABNF (more on this below), but the
> reserved words do have a formal meaning, which we can't state
> explicitly if we don't identify them formally. This is an example
> of an ambiguity actually - is it possible to have a field called
> "lsb" like this:
> 
> zero_low_word_16 ===
> {
>    uc_format = lsb, msb;
>    co_format = lsb, msb
>    {
>      lsb  ::= uncompressed_value(8, 0);
>      msb  ::= irregular(8);
>    };
> };
> 
> Your intuition may so "no", but somebody else's "yes". I agree
> with you that this particular problem could be solved by an
> explicit reserved words section elsewhere in the draft.

The FN is supposed to be used in future specifications, and since
lsb is an encoding method, I would as a profile reviewer argue that
using lsb to identify a field is a very bad idea, as it would be
confusing, and maybe even create an error. However, I do not need
what is in appendix A to back me up with that observation, common
sense is enough.

> > A.2 Characters
> > 
> >   This is not needed for humans!
> > 
> >   Summary: The world would be a better place if this is removed!
> > 
> I agree - this section is utterly ludicrous and only needs to 
> be present because we're currently using ABNF to represent the
> syntax. I'd far rather revert to EBNF which doesn't have this problem.

I believe the FN can be understood (and should be interpretable)
without any knowledge of ABNF or EBNF. The only place you have to
refer to those is in appendix A, not in the actual FN definitions,
which is the normative part of the FN.

> > And so on, I really have problems with seeing the point with
> > the content of this appendix.
> > 
> 
> This I disagree with. The bulk of the most useful stuff is in 
> the rest of the appendix which you haven't commented on - it
> builds on top of trivia like literals, that's why the first
> three sections are really needed; because they're used in the
> remainder of the appendix. It is these subsequent areas where
> you most need the formal clarification. I can understand you
> not wanting to read the whole of section A, but I think your
> comments stop a little too early at Literals!

I have of course read the whole appendix, but I did not want to
repeat the same comment for each section. What is in there might
be needed for a machine that is to verify an FN-defined profile,
but not for us humans. There is a common practice, also for RFCs,
you do not have to build every little detail from atoms. Further,
profiles making use of the FN will be reviewed by humans.

/L-E

_______________________________________________
Rohc mailing list
[email-masked]
https://www1.ietf.org/mailman/listinfo/rohc

---

From: Carsten Bormann <[email-masked]>
Date: Wed, 30 Mar 2005 14:24:02 +0200

On Mar 30 2005, at 13:46 Uhr, Lars-Erik Jonsson ((LU/EAB)) wrote:

> for assertions.

The problem here is that we don't seem to be communicating very well 
between the different mindsets.
Given that I'm looking at FN from a relational mindset, I'm still not 
sure what the distinction is.
We probably need half a dozen or so of examples to nail this down.
I've attached some candidates from the current TCP packet formats.

Gruesse, Carsten

Example 1:

variable_length_32_enc(flag) ===
{
         uc_format = field; %[ 32 ]

         co_format_not_present = field, %[ 0 ]
         {
            let(flag == 0);
            field ::= static;
         };
         co_format_8_bit = field, %[ 8 ]
         {
            let(flag == 1);
            field ::= lsb(8, 63);
         };
         co_format_16_bit = field, %[ 16 ]
         {
            let(flag == 2);
            field ::= lsb(16, 16383);
         };
         co_format_32_bit = field, %[ 32 ]
         {
            let(flag == 3);
            field ::= irregular(32);
         };
};

Example 2:

irreg_tos_tc ===
{
         uc_format = tos_tc; %[ 6 ]

         co_format_tos_tc_present = tos_tc, %[ 6 ]
         {
            let(ecn_used:uncomp_value == 1);
            tos_tc  ::= irregular (6);
         };

         co_format_tos_tc_not_present = tos_tc, %[ 0 ]
         {
            let(ecn_used:uncomp_value == 0);
            tos_tc  ::= static;
         };
};

Example 3:
[...]
         co_format_ipv6_innermost_irregular =
         {
                 let(ip_inner_ecn:uncomp_value ==
                     ip_ecn_flags:uncomp_value);
         };
[...]

Example 4:
[...]
         co_format_eol_irregular =
         {
                 let(nbits - 8 == pad_len:uncomp_value);
         };
[...]

Example 5:
[...]
         co_format_sack1_list_item = discriminator,
                                     block_1,
         {
                 let(length:uncomp_value == 10);
                 discriminator ::= '00000001';
                 block_1 ::= tcp_opt_sack_block (ack_value);
         };
[...]

Example 6:
[...]
       let (seq_number_scaled:uncomp_value ==
                seq_number:uncomp_value / payload_size);
       let (seq_number_residue:uncomp_value ==
                mod(seq_number:uncomp_value, payload_size));
       let (ack_number:uncomp_value ==
                (ack_stride:uncomp_value * 
ack_number_scaled:uncomp_value) +
                ack_number_residue:uncomp_value);
       let (ack_number_residue:uncomp_value ==
                mod(ack_number:uncomp_value, ack_stride:uncomp_value));
[...]