Subject: [rohc] Finalizing the FN, proposal for annotations & "underscore" method s

From: "Lars-Erik Jonsson (LU/EAB)" <[email-masked]>
Date: Tue, 5 Oct 2004 10:43:37 +0200

FN folks,

We've had intensive discussions for a week now, and I think
these have been very healthy for getting us to a point where
we at least know what we all are talking about and how we
envision various pieces in the FN puzzle. 

It is obvious to me that even when understanding each others
arguments, we still do not fully agree. Some of us believe
the FN should not at all be influenced by potential/intended
use of verification tools in the profile development work,
while others think it would just be natural to adapt the FN.

Personally, I still have not seen any convincing argument
why it would actually be needed to adapt the FN for these
verification purposes, and all that we want to do with tools
seem to be possible to do also without FN adaptation. I do
not care if the tools get "ugly", it is just development
tools, while I do care about making the FN simple and clean.

Considering last days discussions, I therefore propose the
following way forward:

1) Ghyslain updates the FN to make it consistent and clean,
   incorporating what has been discussed since the last update

2) When it comes to "underscores" as escape character for
   profile-defined methods, or other ways to clearly refer
   to methods defined in FN versus in the profile, it is a
   choice left for profile developers to decide on. For
   the FN, we should take the text previously suggested by
   Ghyslain, while in the TCP profile we could e.g. use an
   approach similar to what Carsten suggested yesterday:

       "At some point, the TCP draft should have a section
        that summarizes/lists what methods are defined in
        English. This section might be phrased like this:

	    ipv4_inferred_dodo === "section 4.7";
	    udp_inferred_glorp === "section 4.9";

        An FN processor could take this as a hint that these
        methods are defined in English.
        Look, Ma, no (leading) underscores."

3) Regarding annotations, I strongly believe this is an 
   add-on for verification purposes only, and I am therefore
   convinced the right place for these is in comments. From
   yesterdays discussions, it seems like we agree that this
   approach would work also from a parsing point of view.
   It thus becomes a profile issue whether and how to use
   annotations, as Ghyslain wrote yesterday:

       "I suggested that the ROHC-FN draft removes anything
        about notation and that we had a note about such
        annotations being used inside comments into the TCP
        draft, in the section where we start specifying
        packet formats."

Can we let Ghyslain update the draft according to this, 
and move on? We will get annotations for the parser, which
we define in the TCP profile. We will also make sure in the
profile that all methods are clearly referenced, e.g. like
suggested by Carsten. Of course we should be able to verify
the packet formats, also when there are methods defined in
the profile.

Objections?
Otherwise I suggest that we change focus and start working
on the packet formats, a discussion Kristofer re-initiated 
yesterday.

/L-E

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

---

From: Carsten Bormann <[email-masked]>
Date: Tue, 5 Oct 2004 13:25:13 +0200

On Oct 05 2004, at 10:43 Uhr, Lars-Erik Jonsson (LU/EAB) wrote:

> and move on?

Yes, please.

I'm really looking forward to crunch the updated packet formats through 
our tool.
We should have a syntactically correct, reasonably up-to-date base set 
within a couple of hours.
I'll put those on the ROHC CVS server.

Gruesse, Carsten

(PS.: In case my yesterday evening's message was too vitriolic: I was 
attempting to say that, yes, we do have the in-comment style 
annotations now in our tool.  Unfortunately, I was out of kimchi, so I 
turned to wasabi covered broad beans.)

---

From: Carsten Bormann <[email-masked]>
Date: Tue, 5 Oct 2004 17:03:20 +0200

> I'll put those on the ROHC CVS server.

They are now at http://www.dmn.tzi.org/cgi-bin/cvsweb.cgi/fn/
I expect to update this location frequently with new versions; the CVS 
functionality also allows to see quickly what has changed.

Our semantic checker currently has to say the below about the formats.
This is certainly not everything a semantic checker can find, and it 
may not even all be useful observations, but it will certainly help in 
finding interesting spots for further examination.

Gruesse, Carsten

ERROR: Annotation 32 for uncompressed field [item] does not match 
length 0 in optional32:format_not_present
ERROR: Annotation 32 for uncompressed field [item] does not match 
length 0 in opt_lsb_7_or_31:format_not_present
ERROR: Annotation 16 for compressed field [reserved1] does not match 
length 0 in optional16:format_cs_present
ERROR: Annotation 3 for compressed field [version] does not match 
length 0 in gre:format_gre_static
ERROR: Annotation 3 for compressed field [version] does not match 
length 0 in gre:format_gre_replicate_1
ERROR: Annotation 32 for compressed field [spi] does not match length 0 
in esp_null:format_esp_static
ERROR: Annotation 6 for uncompressed field [traffic_class] does not 
match length 8 in ipv6:format_ipv6_replicate
ERROR: Annotation 128 for compressed field [dst_addr] does not match 
length 0 in ipv6:format_ipv6_static
ERROR: Annotation 128 for compressed field [dst_addr] does not match 
length 0 in ipv6:format_ipv6_static_3095
ERROR: Annotation 6 for compressed field [traffic_class] does not match 
length 8 in ipv6:format_ipv6_replicate
ERROR: No uncompressed format for ip_id_behavior_enc!
ERROR: Annotation 32 for compressed field [dst_addr] does not match 
length 0 in ipv4:format_ipv4_static
ERROR: Annotation 32 for compressed field [dst_addr] does not match 
length 0 in ipv4:format_ipv4_static
ERROR: Annotation 1 for compressed field [df] does not match length 0 
in ipv4:format_ipv4_dynamic
ERROR: Annotation 1 for compressed field [ip_id_nbo_flag] does not 
match length 0 in ipv4:format_ipv4_dynamic
ERROR: Annotation 1 for compressed field [df] does not match length 0 
in ipv4:format_ipv4_replicate_1
ERROR: Annotation 1 for compressed field [ip_id_nbo_flag] does not 
match length 0 in ipv4:format_ipv4_replicate_1
ERROR: No uncompressed format for ecn_and_reserved_enc!
ERROR: Annotation 16 for compressed field [dst_port] does not match 
length 0 in tcp:format_tcp_static
ERROR: Annotation 1 for compressed field [reserved] does not match 
length 4 in tcp:format_tcp_dynamic
ERROR: No compressed format for tcp_opt_nop!
ERROR: No compressed format for tcp_opt_sack_permitted!
ERROR: No uncompressed format for list_index!

---

From: Kristofer Sandlund <[email-masked]>
Date: Wed, 06 Oct 2004 08:55:25 +0200

Hi Carsten and others,

As halfway promised, I'm going to _try_ (still no promise due to time 
constraints) to put together some packet formats before beginning of next week, 
but the latest version in the CVS is of course a subset of the full packet 
formats, so I'll have to merge in the packets from tcp-07.txt into this, update 
them and make some minor modifications to them.

So my questions for now are:
- Are you ok with the suggested change to remove the "next header iterating 
scheme" as I proposed earlier this week? I'm a bit relucatant to go into major 
edits and then find out that the consensus would be that we really would need 
these things.... Note that with these changes, there is no need to put packet 
formats for the IR, IR-DYN and IR-CR, since they are defined in the text instead.

- ECN. Currently, the ECN uses some form of this "previous" notation, and in 
line with my proposal to let the user construct the chains I say we add some 
text about ECN handling in the TCP draft ("when constructing the irregular 
chain, the user should choose the irregular format postfixed by _ecn if the ECN 
bits have been set in the context, otherwise the irregular format without _ecn 
should be chosen. blah blah, better text, but you get my meaning"). This way we 
get away from another thing that seems unsuitable for the FN to express.

- I've only briefly looked at your parser warnings, but some of them seem a bit 
strange. The first one says that optional32:format_not_present has a annotation 
of 32, which it does not in the CVS version. Have you updated it since then?

BR,
	Kristofer Sandlund, Effnet AB

Carsten Bormann wrote:
> This is certainly not everything a semantic checker can find, and it may 
> not even all be useful observations, but it will certainly help in 
> ERROR: Annotation 32 for uncompressed field [item] does not match length 
> 0 in optional32:format_not_present
> ERROR: Annotation 32 for uncompressed field [item] does not match length 
> 0 in opt_lsb_7_or_31:format_not_present
> ERROR: Annotation 3 for compressed field [version] does not match length 
> 0 in gre:format_gre_static
> ERROR: Annotation 3 for compressed field [version] does not match length 
> 0 in gre:format_gre_replicate_1
> ERROR: Annotation 1 for compressed field [df] does not match length 0 in 
> ipv4:format_ipv4_dynamic
> ERROR: Annotation 1 for compressed field [ip_id_nbo_flag] does not match 
> length 0 in ipv4:format_ipv4_dynamic
> ERROR: Annotation 1 for compressed field [df] does not match length 0 in 
> ipv4:format_ipv4_replicate_1
> ERROR: Annotation 1 for compressed field [ip_id_nbo_flag] does not match 
> length 0 in ipv4:format_ipv4_replicate_1

---

From: Eilert Brinkmann <[email-masked]>
Date: Wed, 06 Oct 2004 09:59:58 +0200

Kristofer Sandlund wrote:
> - I've only briefly looked at your parser warnings, but some of them
> seem a bit strange. The first one says that
> optional32:format_not_present has a annotation of 32, which it does
> not in the CVS version.

No, it says that a field in the *un*compressed format is annotated with

>> length 0 in optional32:format_not_present

This means that item in the field order list of uncompressed_format
("uncompressed field [item]") has an annotation of 32, while the
encoding for this field in format_not_present binds item:uncomp_length
with 0. (Maybe we need to find an easier to understand format for our
warnings?) And this is what's in the spec:

  optional32 (flag) === {
  
          uncompressed_format = item; %[ 32 ]
  
          [...]
  
          format_not_present = item, %[ 0 ]
          {
                  let (flag:uncomp_value == 0);
  
                  item ::= value (0, 0);
          };
  };

Here the length attribute for the encoding method should be 32 instead
of 0 (and value must be changed to uncompressed_value -- our parser
still accepts the old name, too).

Eilert

---

From: Carsten Bormann <[email-masked]>
Date: Wed, 6 Oct 2004 10:33:17 +0200

On Oct 06 2004, at 08:55 Uhr, Kristofer Sandlund wrote:

> constraints) to put together some packet formats before beginning of 
> next week, but the latest version in the CVS is of course a subset of 
> the full packet formats, so I'll have to merge in the packets from 
> tcp-07.txt into this, update them and make some minor modifications to 
> them.
>
> - Are you ok with the suggested change to remove the "next header 
> iterating scheme" as I proposed earlier this week? I'm a bit 
> relucatant to go into major edits and then find out that the consensus 
> would be that we really would need these things.... Note that with 
> these changes, there is no need to put packet formats for the IR, 
> IR-DYN and IR-CR, since they are defined in the text instead.

I think this is a reasonable fallback.
Of course, I'd prefer to have them in formal notation, as it makes 
testing the spec much easier, but I don't think we have the time to 
agree on them (and the FN magic needed) now.

> - ECN. Currently, the ECN uses some form of this "previous" notation, 
> and in line with my proposal to let the user construct the chains I 
> say we add some text about ECN handling in the TCP draft ("when 
> constructing the irregular chain, the user should choose the irregular 
> format postfixed by _ecn if the ECN bits have been set in the context, 
> otherwise the irregular format without _ecn should be chosen. blah 
> blah, better text, but you get my meaning"). This way we get away from 
> another thing that seems unsuitable for the FN to express.

We could simply have a special (English-defined) encoding method that 
succeeds for different parameters depending on some context information 
about ECN.
Similar to (and possbly even formally definable based on) static.

> not in the CVS version. Have you updated it since then?

Well, as Eilert said, actually it does -- the *uncompressed* side is 32 
bits, and this does not mesh with the value(0, 0) method.
I was confused by the message, too -- we need to fix the text of the 
message, but the contents is fine.

Gruesse, Carsten

---

From: Kristofer Sandlund <[email-masked]>
Date: Wed, 06 Oct 2004 13:50:02 +0200

Ok, so now I know what is wrong, but I don't know how I'm supposed to fix this.
Mark wrote this structure to indicate that this field will be compressed either 
as 0 bits or as 32 bits (a variable-length encoding).
How should this be written according to the FN? Should I use static instead?

/Kristofer

---

From: Carsten Bormann <[email-masked]>
Date: Wed, 6 Oct 2004 14:02:28 +0200

On Oct 06 2004, at 13:50 Uhr, Kristofer Sandlund wrote:

> Mark wrote this structure to indicate that this field will be 
> compressed either as 0 bits or as 32 bits (a variable-length 
> encoding).

I think optional32 was meant to either include a value or not, based on 
a discriminator somewhere (which is given as a parameter).
If the flag is off, both the uncompressed and the compressed side are 
zero-length.
If the flag is on, we have an irregular 32-bit field.

So what is wrong here is the annotation of the uncompressed_format.
If you look at the places where this is used, there is no formal 
annotation, instead there is a comment saying

	                 	          orig_src,       %  0 or 32 bits

The same should be true for optional32, i.e.:

	uncompressed_format = item; %  0 or 32 bits, depending on "flag"

This, of course, is a rather boring inconsistency, but it at least 
identified incorrect documentation of the uncompressed_format of 
optional32.

Gruesse, Carsten

---

From: Eilert Brinkmann <[email-masked]>
Date: Wed, 06 Oct 2004 14:03:53 +0200

Kristofer Sandlund wrote:
> compressed either as 0 bits or as 32 bits (a variable-length encoding).

The only part that's wrong is the encoding for item in
format_not_present. The optional32 structure contains three formats:

- uncompressed_format (in this item has always 32 bits)

- format_present (which I left out with [...] in my previous message;
  in this format item is encoded as irregular and has always 32 bits)

- format_not_present (in which item has always 0 bits on the
  uncompressed side)

After correction the complete structure should look like this:

  optional32 (flag) === {

          format_present = item, %[ 32 ]
          {
                  let (flag:uncomp_value == 1);
  
                  item ::= irregular (32);
          };

                  item ::= uncompressed_value (32, 0);
          };
  };

I.e., the only change (aside from using uncompressed_value instead of
value) is the first argument of uncompressed_value which was 0 before.

Eilert

---

From: Eilert Brinkmann <[email-masked]>
Date: Wed, 06 Oct 2004 14:09:36 +0200

Carsten Bormann wrote:
> I think optional32 was meant to either include a value or not, based
> on a discriminator somewhere (which is given as a parameter).

Sorry, then I was wrong in my prevoius message. My thought was that if
the flag is off the uncompressed side should be 32 bits with value 0,
but probably that dosn't make sense.

Eilert

---

From: Kristofer Sandlund <[email-masked]>
Date: Wed, 06 Oct 2004 14:12:47 +0200

Carsten,

Thanks for your clarifications.
I'll rewrite the structure using "compressed_value" in the not_present part so 
that nothing is actually transmitted here. I also change the annotation to being 
"% 0 or 32" bits in the uncompressed_format

   optional32 (flag) === {

           uncompressed_format = item; % 0 or 32 bits

                 item ::= irregular (32);
           };

                   item ::= compressed_value (0, 0);
           };
   };

Will this satisfy the parser?

/Kristofer