Count

[cwagaman]

Files:

• make_count.tex -- the Latex document with the proof
• make_count.pdf -- the PDF generated from make_count.tex
• listings-rust.sty -- style document (only needed if you want to compile make_count.tex)-

This upload contains the proof for the function make_count, specifically the version of the function found at this GitHub permalink.

During the proof process, some questions arose. They are noted in the tex file using the format "\question{...}". The questions also appear in the pdf file generated from the tex file; they are displayed in red text and are prepended by "Question:".

The functions, traits, and other terms used in the pseudocode can be found in the "List of definitions used in the pseudocode" Overleaf document pseudocode-defns branch. Likewise, definitions used in the proof can be found in the "List of definitions used in the proofs" Overleaf document. Please let me know if you need access to either one.

Feel free to reach out here or on Slack with any questions. Thanks!

Update: September 6, 2021

This proof document now incorporates all suggestions made as of September 6, 2021.

Two questions (both noted in red text in the document):

• Is the proof of lemma 2.3 good? (Question is more specific in the document and appears immediately after the proof of lemma 2.3.)
• Should the examples in the "preconditions" be included, altered, or removed? They were added in response to this comment. (The question is more specific in the document and appears immediately after the preconditions in section 1.3.)

Update: September 23, 2021

This proof document now incorporates all suggestions made as of September 23, 2021. This includes the suggestions made by Marco Gaboardi. Currently, there is no remaining feedback to incorporate. Probably a final review is needed before we merge this into main and close the PR, but currently I have no more work to do on this.