Implementation of various cryptographic functions in Lean4
This is an experimental work in progress.