Add a table of backend statuses and maintenance

README.md

@@ -172,6 +172,52 @@ http://adam.chlipala.net/theses/andreser_meng.pdf) Section 3 contains a whirlwin
 - The newest compilation pipeline as a whole does not have a separate document yet, but this README does go over it in some detail.
 
 
+Status of Backends
+------------------
+
+Fiat Cryptography contains a number of backends; the final step of the pipeline is transforming from straight-line C-like code to expressions in whatever language is being targeted.
+The Bedrock2 backend comes with proofs that the Bedrock2 AST matches the semantics of our internal AST, but none of the other backends have any proofs about them.
+While the transformations are not particularly involved, and our proofs ensure that we have picked integer sizes large enough to store values at each operation, there is no verification that the particular integer size casts that we emit are sufficient to ensure that gcc, clang, or whatever compiler is used on the code correctly selects integer sizes for expressions correctly.
+Note that even the C code printed by the Bedrock2 backend does not have proofs that the conversion to strings is correct.
+
+Hence we provide here a table of the extent to which the various backends are maintained, tested, and proven.
+A :heavy_check_mark: in "maintainer" means that the Fiat Cryptography maintainers are fully maintaining and testing the backend; :white_check_mark: means maintenance by external contributors.
+We do not provide any quality guarantees for code generated by the backends.
+
+Backend | Maintainer / Person of Contact | Build Checked by CI | Generated Code Tested | Internal AST Proven Correct
+:-- | :-- | :-- | :-- | :--
+C | :heavy_check_mark: @JasonGross / entire team | :heavy_check_mark: | :heavy_check_mark: (BoringSSL test-suite) | 
+Bedrock2/C | :heavy_check_mark: @andres-erbsen / entire team | :heavy_check_mark: | :heavy_check_mark: (BoringSSL test-suite) | :heavy_check_mark:
+Go | :white_check_mark: @mdempsky | :heavy_check_mark: | | 
+Java | :x: Unmaintained | :heavy_check_mark: | :x: Known Buggy [#707](https://github.com/mit-plv/fiat-crypto/issues/707#issuecomment-763098543) | 
+JSON | Experimental | :white_check_mark: (only syntax) | | 
+Rust | :white_check_mark: | :heavy_check_mark: | :heavy_check_mark: ([Dalek Cryptography test-suite](https://github.com/dalek-cryptography/curve25519-dalek)) | 
+Zig | :white_check_mark: @jedisct1 | :heavy_check_mark: | | 
+
+### Contributing a new backend
+
+We weclome new backends (as long as you're willing to maintain them).
+We hope that the process of contributing a new backend is not too painful, and welcome feedback on how the process could be streamlined.
+To contribute a new backend, follow the following steps (perhaps using, for example, [#936](https://github.com/mit-plv/fiat-crypto/pull/936), [#660](https://github.com/mit-plv/fiat-crypto/pull/660), [#638](https://github.com/mit-plv/fiat-crypto/pull/638), or [#570](https://github.com/mit-plv/fiat-crypto/pull/570) as examples):
+- Add a new file to [`src/Stringification/`](./src/Stringification/) for your language, modeled after the existing file of your choice
+- Run `git add` on your new file and then `make update-_CoqProject` to have the build system track your file
+- Update [`src/CLI.v`](./src/CLI.v) to `Require Import` your file and add your language to [the list `default_supported_languages`](https://github.com/mit-plv/fiat-crypto/blob/8944697db11055abeeba252782d2bfd1e2b844cd/src/CLI.v#L212-L219) so that it can be passed to the binaries as an argument to `--lang` 
+- Update the `Makefile` in the following ways:
+  - Consider adding a variable near `CARGO_BUILD` for the build invocation
+  - Add targets to `.PHONY` analogous to `c-files`, `lite-c-files`, `test-c-files`, `only-test-c-files`
+  - Add a variables analogous to `C_DIR`, `ALL_C_FILES`, and `LITE_C_FILES` for your language's generated files
+  - Add targets analogous to `c-files` and `lite-c-files` and make `generated-files` and `lite-generated-files` depend on those targets respectively
+  - Add build rules for `ALL_<YOUR-LANGUAGE>-FILES`
+  - Add targets for `test-<your-language>-files` and `only-test-<your-language>-files`; both targets should have the same build rule, but `test-<your-language>-files` should depend on all the generated files of your language, while `only-test-<your-language>-files` should not have any build rule dependencies.
+  - If you are developing a package, you can look for uses of `COPY_TO_FIAT_RUST` or `COPY_TO_FIAT_GO` to see how license files are copied
+- Run `make` to generate all the relevant files of your language, and add the generated files to git
+- Update `.gitignore` to ignore any compiled files generated by the compiler of your language (analogous to `.o` and `.a` for C)
+- Create a file in [`.github/workflows/`](./.github/workflows/) like [`c.yml`](./.github/workflows/c.yml), [`go.yml`](./.github/workflows/go.yml), [`rust.yml`](./.github/workflows/rust.yml), etc, to test at least that the generated code compiles.
+  - Optionally, also test the built code against some external project's crypto unit tests
+- Update [`.gitattributes`](./.gitattributes) to mark your language's generated files as `text` and to mark the paths of the generated files as `linguist-generated` so that diffs don't clog up PR displays.
+- Add your language to the table in preceeding section of the README indicating the status of your backend and marking your GitHub username as the maintainer.
+
+
 Reading The Code
 ----------------
 
@@ -594,3 +640,5 @@ For `Language.v`, there is a semi-arbitrary split between two files
 - `AbstractInterpretation/Proofs.v`: interp lemmas for the
   AbstractInterpretation pass, and also correctness lemmas that
   combine Wf and interp
+
+