Standalone, portable specification of BIR syntax and semantics

[palmskog]

The BIR language and its semantics could be worth specifying and documenting standalone, most directly using Lem. Encoding BIR in Lem would also allow porting it to other proof assistants like Isabelle/HOL and Coq.