Ongoing specification of RLAs in general, and RLAs for Colorado. #400
Conversation
In particular, I'll be focusing on their notion of rounds, or what are called stages in the literature.
| % with the most votes received 3,500 votes, the diluted margin of the | ||
| % contest is 5% [(4,000 – 3,500) / 10,000] | ||
| diluted_margin: TYPE FROM margin | ||
|
|
||
| % @trace struck from RDPR-6-Jul-2017 old Section 25.1.6 |
There was a problem hiding this comment.
Use this description instead of the one below. Just remove the trace.
There was a problem hiding this comment.
Recall that traces are going to turn into margin comments with hyperlinks to other artifacts. So I'm going to leave it in there for now.
specs/pvs/corla.pvs
Outdated
|
|
||
| %%% First, one must choose a ``simultaneous risk limit'' ($\alpha$) | ||
| %%% to be applied across all contents under audit. This notion is |
There was a problem hiding this comment.
=> "First, one must choose a ``risk limit'' (
I doubt we will ever be interested in simultaneous audits across contests, governed by a single risk limit, and Philip agrees. As discussed several times in slack, that would among other things mean that if there was a problem with one contest, all the contests being simultaneously audited would require a full hand count. A full hand count of multiple contests is far more of a nightmare than just hand counting a single one.
There was a problem hiding this comment.
As just mentioned in Slack, what I have been formalizing here is Stark10's definitions so that I can refine them for Colorado's specific style of "different risk-limits per contest". I'm refactoring now during my responding to @nealmcb's comments here.
specs/pvs/corla.pvs
Outdated
| %%% among the contests under audit (which we will call the | ||
| %%% \texttt{minimum\_margin}) divided by the total number of ballots | ||
| %%% cast across all the contests under audit.\todonealmcb{Is this | ||
| %%% true, or is it the smallest margin over all contests under audit?} |
There was a problem hiding this comment.
Use the definition above. No simultaneous audits. Calculated for each contest, each of which is audited independently.
There was a problem hiding this comment.
In my revisions that I'll be committing in a few minutes, I have refactored this definition in the colorado_rlas theory to the appropriate structures for Colorado's case.
| % in an audited contest, and the reported winning candidate with the | ||
| % fewest votes received 4,000 votes, and the reported losing candidate | ||
| % with the most votes received 3,500 votes, the diluted margin of the | ||
| % contest is 5% [(4,000 – 3,500) / 10,000] |
There was a problem hiding this comment.
It's not clear to me that you would want to duplicate the comments for % vs %%%, but I'll leave that to you.
There was a problem hiding this comment.
See above. Those that are currently in % with a @trace will be converted into margin comments.
specs/pvs/corla.pvs
Outdated
| %%% rules. First, the risk limit for comparison audits must be below | ||
| %%% $5\%$. | ||
| % @trace RDPR-6-Jul-2017 Section 25.2.2(A) | ||
| RDPR_risk_limit: TYPE = {n : nonneg_real | n <= 0.05} |
There was a problem hiding this comment.
We decided to leave out the restriction, given the escape clause. Also, the rule now says 10%, for county-wide contests, and doesn't actually say anything about contests smaller than a county. So I'd leave out this RDPR_escape_claus_risk_limit part - too deep in the weeds. They seem to want flexibility.
There was a problem hiding this comment.
I still need to model what is in the statutes and in the rules. That's doesn't mean that we will implement these dependent types as invariants in the system.
specs/pvs/corla.pvs
Outdated
| %%% is set any kind of risk limit they like. | ||
| RDPR_escape_clause_risk_limit: TYPE = {n : nonneg_real | n <= 1.0} | ||
|
|
||
| %%% As mentioned above, CDOS wants to be able to run a state-wide |
There was a problem hiding this comment.
"run an audit", since I expect they would do this if they ran just a local audit also.
specs/pvs/corla.pvs
Outdated
| %%% counties. | ||
| round_size: TYPE = [round_number -> nat] | ||
| %%% Eventually we run out of ballot cards to audit, as a full hand | ||
| %%% count will count all ballot cards. Thus, for all possible round |
There was a problem hiding this comment.
I don't understand this. Run out?
There was a problem hiding this comment.
I'm proposing a model of stages such that stages eventually terminate because the SOS will decide that the contest(s) in question must be hand-counted. I'll try to clarify.
specs/pvs/corla.pvs
Outdated
| %%% We propose that, under normal circumstances, the initial round | ||
| %%% size for any election in Colorado should be conservative enough | ||
| %%% that all counties will meet their risk limits for all contests | ||
| %%% under audit. |
There was a problem hiding this comment.
They can't mean that all counties audit the same number of ballots in a round. That would be crazy.
A typo in the docs for the ComparisonAudit class is also included.
In particular, I'll be focusing on their notion of rounds, or what are called stages in the literature.