proofs/isabelle: add C functional correctness proof of forward NTT

Add MLKEM_FC_NTT.thy with contracts for ntt_butterfly_block, ntt_layer,
poly_ntt_c, and poly_ntt.

Author: DominicPM