Based on your specification, we prove in Isabelle/HOL that encoding followed by decoding produces the original data.
Here are a sample script and PDF produced in nine hours of work (this was a piece of hobby, for which nobody asked).
For this type of work, we take 60 EUR per hour (excluding VAT). Upon request, we produce an initial cost estimate.
If you are interested, send us an email.
ImpressumConvenience Logician Hirai UG (haftungsbeschränkt) firstname.lastname@example.org