Add some description of `assert` and `assume` to body of PSA spec

[jfingerh]

Currently they are documented by fairly large comment blocks in the psa.p4 include file. Is it worth adding some description of them to the body of the PSA specification as well?

There is a risk that if we simply copy and paste the comments documenting them into the PSA specification, then it will be two redundant copies to keep up to date if they ever change in the future. Perhaps one straightforward solution is simply to make the comments in psa.p4 the authoritative verbose documentation, and simply mention these extern functions briefly in the PSA.mdk file, INCLUDE'ing the comments into the spec.

[apinski-cavium]

Currently they are documented by fairly large comment blocks in the psa.p4 include file.

I think the big question is what is the PSA specifications documentation and should it be self-contained or should it reference a reference psa.p4 too?
(Note I think PNA should follow what PSA does here and even to some extend the over all language specifications and core.p4).

I like the idea of having them automatically included really.
I read specifications first and then the header file but others are opposite.
Still having a verbose psa.p4 for folks who read the header file instead of the specifications.

[jfingerh]

@apinski-cavium See the PR #1187 for what I have done so far. I had forgotten that there is an INCLUDE directive in Madoko, one which I've used many times to include only a small selected subset of the psa.p4 include file directly in the document. Thus updating that section of lines in psa.p4 will automatically also update that part of the document the next time it is generated.