Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Make the ref implementation accepted by the safety checker #4

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Make the ref implementation accepted by the safety checker #4

wants to merge 4 commits into from

Commits on Mar 13, 2023

  1. ref: tighter loop bounds

    @vbgl
    vbgl committed Mar 13, 2023
    Configuration menu
    Copy the full SHA
    dc0cd28 View commit details
    Browse the repository at this point in the history

  2. ref/gen-matrix: explicitly initialize the “poly” array

    @vbgl
    vbgl committed Mar 13, 2023
    Configuration menu
    Copy the full SHA
    c4ad140 View commit details
    Browse the repository at this point in the history

  3. ref/gen-matrix: rework loop condition in rej_uniform 

    When the destination array rp is full, the loop nonetheless continues to
completely consume the buf array. There is no longer an early exit, and
the loop will always iterate 56 times.
    @vbgl
    vbgl committed Mar 13, 2023
    Configuration menu
    Copy the full SHA
    5be30db View commit details
    Browse the repository at this point in the history

  4. ref: annotate loops to guide the safety checker 

    With these annotations, the key generation function can be proved safe
by the automatic safety checker.

The “no-termination-check” annotation in gen-matrix acknowledges that
proving (propabilistic) termination of this loop is beyond the scope of
the automated checker and must be justified by other means.
    @vbgl
    vbgl committed Mar 13, 2023
    Configuration menu
    Copy the full SHA
    511a108 View commit details
    Browse the repository at this point in the history