…ponding read function readNLeastSignificantBits

- add read function readNBitsLSBFirst which is the counter part of appendBitsLSBFirst, and proved its post condition
- proved additional postcondition of appendBitsLSBFirst, to prepare the invertabilitsy proof

…of bits specification, in place of the array of UByte

…ion (i.e. functions that read the bitstream and returns

Then proves the equivalence between checkBits and the list specs

* verified appendNBits and appendNBitsLoops

* remove lemma call

* working on the verification of bitstream

* - proved invertability of appendNLeastSignificantBits with its corresponding read function readNLeastSignificantBits
- add read function readNBitsLSBFirst which is the counter part of appendBitsLSBFirst, and proved its post condition
- proved additional postcondition of appendBitsLSBFirst, to prepare the invertabilitsy proof

* verify invertibility appendBitsLSBFirst, with its corresponding lemma

* working on proving appendBitsMSBFirstLoop, before moving to the list of bits specification, in place of the array of UByte

* proved invertibility of appendBitsMSBFirst but with a List specification (i.e. functions that read the bitstream and returns
Then proves the equivalence between checkBits and the list specs

* verification script + stainless conf

* verified BitStream

* verify the by write functions

* finish bitstream verification

* make verification quicker for some VCs, in test

…onditions

Conflicts:
	BackendAst/DAstACN.fs
	FrontEndAst/AcnEncodingClasses.fs
	FrontEndAst/DAst.fs