Clean up {...}<:S strict cast syntax

[Scott-Guest]

This PR cleans up a few issues related to the {...}<:S syntax for strict casts. Specifically,

• Add a section to Lesson 1.11 explaining the need for the braced strict cast syntax
• Change the klabel from #InnerCast to #SyntacticCastBraced
  • #InnerCast was a holdover from prior to make the "inner cast" be a synonym for a strict cast #2352
• Opinionatedly, change the syntax from {...}<:S to {...}::S
  • Makes it more obvious this is just an alternative syntax for strict casts ::S
  • To me, the syntax <:S is misleading in that it reads as "subsort of S", but the actual meaning is "exactly the sort S and not a proper subsort".
  • Minimal fallout - there is only one rule in rv-match and two tests in pyk where this needs to be changed (https://github.com/search?q=org%3Aruntimeverification+%7D%3C%3A&type=code)

The commit history is clean and I can just drop the last commit if we don't want to change the syntax.

[Baltoli]

I'm in favour of the syntactic change; it's been a while since I looked at this and I'd totally forgotten we even had this inconsistency. The surface area seems small enough that we're unlikely to break anything by making the change.

[radumereuta]

Looks weird to me.
I would hardcode the type inferencer to go over braces when you have a strict cast.
If you have a strict cast on top of a parametric production, it should go as deep as possible as long as it is parametric.
That way the curly braces would simply disappear.

[Baltoli]

#2352 (comment)

By the way, one argument against making strictness pass through casts is that someone could theoretically write a grammar where the bracket itself needed to be strict casted in order to disambiguate it, which would no longer be possible without unintended side effects if we made such a change to the inferencer. Now such a grammar is highly unlikely in practice, but it is a limitation on the expressivity of k in terms of the set of grammars it is able to faithfully represent, so if you're concerned about theoretical completeness in the design of the parser, it's probably worth keeping the inferencer code the way it is in this PR instead. (@dwightguth)

Seems like we opted not to do that "push inwards through braces" solution previously.

[dwightguth]

The tutorial didn't have a lesson about this one because I was kinda of the opinion that it should be completely deleted. Where are we actually using this in practice and can we replace those usages?

[Baltoli]

In domains.md:

rule {SB:String +String S:String}<:StringBuffer => (SB +String S)::String

In C (seems like that could trivially be a strict cast, no braces):

rule HALT ~> cast(ut(S::Set, T::SimpleUType), {voidVal}<:RValue, _:Bool) => tv(trap, ut(S, T))
          requires T =/=K void andBool isErrorRecovery

[Baltoli]

Agreed in the K meeting that this is the right thing to do here; we want to keep this syntax for generality even if it's not actively being used other than that one case in domains.md.