diff options
Diffstat (limited to 'src/proofs')
| -rw-r--r-- | src/proofs | 335 |
1 files changed, 335 insertions, 0 deletions
diff --git a/src/proofs b/src/proofs new file mode 100644 index 0000000..7134196 --- /dev/null +++ b/src/proofs @@ -0,0 +1,335 @@ + +# SPDX-License-Identifier: GPL-2.0-or-later + +This file contains some loose proofs of a few properties. It's somewhat +ad-hoc. At least it gives an indication of what assert/g_assert calls have +been checked by a developer. If an assertion does trigger, then this file may +help in debugging that assertion failure. + +It's currently ordered by caller. + +(Re-ordering to avoid forward references in proofs might be a good idea, +though this would in some cases require splitting up the proofs for a routine, +e.g. proving preconditions of g called from f, then proving g's postcondition, +then using that to prove something else in f again. Furthermore it may not +even be possible to avoid forward references for recursive/looping code.) + + + +src/pencil-context.cpp:fit_and_split + +Very loose proof of !sp_curve_empty (pc->red_curve) assertion: +fit_and_split is called successively with its input varying only by appending a point. +For the n_segs > 0 && unsigned(pc->npoints) < G_N_ELEMENTS(pc->p) condition to fail, +we must have at least 3 distinct points, which means that a previous call had 2 distinct points, +in which case we'd have filled in pc->red_curve to a non-empty curve. + +Expansion of the above claim of at least 3 distinct points: We know n_segs <= 0 || +unsigned(dc->npoints) >= G_N_ELEMENTS(pc->p) from the negation of the containing `if' condition. +G_N_ELEMENTS(pc->p) is greater than 3 (in int arithmetic), from PencilTool::p array definition +in pencil-context.h. npoints grows by no more than one per fit_and_split invocation; we should be +able to establish that dc->npoints == G_N_ELEMENTS(pc->p) if unsigned(dc->npoints) >= +G_N_ELEMENTS(pc->p), in which case 3 <= dc->npoints in int arithmetic. We know that dc->npoints >= +2 from assertion at head of fit_and_split; in which case if n_segs <= 0 then fit_and_split has +failed, which implies that dc->npoints > 2 (since the fitter can always exactly fit 2 points, +i.e. it never fails if npoints == 2; TODO: add sp_bezier_fit_cubic postcondition for this). + + +src/pencil-context.cpp:fit_and_split + +Proof of precondition: The only caller is spdc_add_freehand_point (by +textual search in that file, and staticness). See proof for that +function. + + +src/pencil-context.cpp:spdc_add_freehand_point + +Proof of fit_and_split `pc->npoints > 1' requirement: +It initially unconditionally asserts `pc->npoints > 0'. There are no function calls or modifications +of pc or pc->npoints other than incrementing pc->npoints after that assertion. +We assume that integer overflow doesn't occur during that increment, +so we get pc->npoints > 1. + + +src/pencil-context.cpp:spdc_set_endpoint + +Very loose proof of npoints > 0: Should be preceded by spdc_set_startpoint(pc) according to state +transitions. spdc_set_startpoint sets pc->npoints to 0 (handled at beginning of function) or 1. + + +src/display/bezier-utils.cpp:compute_max_error + +Proof of postcondition: *splitPoint is set only from i, which goes from 1 to less than last. +i isn't written to in the loop body: only uses are indexing built-in arrays d and u +(and RHS of assignment). + + +src/display/bezier-utils.cpp:sp_bezier_fit_cubic_full + +Proof of `nsegs1 != 0' assertion: nsegs1 is const. Have already +returned in the (nsegs1 < 0) case, so !(nsegs1 < 0), i.e. nsegs1 >= 0 +(given that nsegs1 is gint). nsegs1 is set to +sp_bezier_fit_cubic_full(_, _, _, splitPoint + 1, ...). We will show +that sp_bezier_fit_cubic_full ensures len < 2 || ret != 0. splitPoint +> 0 from compute_max_error postcondition combined with error >= +precondition and thus having handled the compute_max_error returning 0 +case: if returned 0 for maxError then maxError <= error * 9.0 would be +true, and we recalculate splitPoint; if the renewed maxError is 0 then +the maxError <= error test will succeed and we return. If we don't +return, then the most recent compute_max_error must have returned +non-zero, which implies (through compute_max_error postcondition) that +splitPoint would have been set s.t. 0 < splitPoint. splitPoint is not +subsequently written to. (It is subsequently passed only to +sp_darray_center_tangent 2nd arg, which is a plain unsigned rather +than reference.) 0 < splitPoint < last guarantees splitPoint + 1 >= +2. (We know splitPoint + 1 won't overflow because last = len - 1 and +len is of the same type as splitPoint.) Passing splitPoint + 1 for +len of the call that sets nsegs1 ensures that nsegs1 is non-zero (from +the len < 2 || ret != 0 property that we show below). QED. + +Proof that len < 2 || (failed no-dups precondition) || ret != 0: All +returns are either -1, 0, 1, or nsegs1 + nsegs2. There are two +literal 0 cases: one conditional on len < 2, and the other for failed +precondition (non-uniqued data). For the nsegs1 + nsegs2 case, we've +already ruled out nsegs1 < 0 (through conditional return) and nsegs2 < +0 (same). The nsegs1 + nsegs2 case occurs only when we recurse; we've +already shown the desired property for non-recursive case. In the +nsegs1 non-recursive case, we have that nsegs1 != 0, which combined +with !(nsegs1 < 0) and !(nsegs2 < 0) implies that nsegs1 + nsegs2 +either overflows or is greater than 0. We should be able to show that +nsegs1 + nsegs2 < len even with exact arithmetic. (Very loose proof: +given that len >= 2 (from earlier conditional return), we can fit len +points using len-1 segments even using straight line segments.) +nsegs1 and nsegs2 are the same type as len, and we've shown that +nsegs1 + nsegs2 in exact arithmetic is >= 0 from each operand being +non-negative, so nsegs1 + nsegs2 doesn't overflow. Thus nsegs1 + +nsegs2 > 0. Thus we have shown for each return point that either the +return value is -1 or > 0 or occurs when len < 2 or in failure of +no-dups precondition. (We should also show that no-dups outer +precondition being met implies it being met for inner instances of +sp_bezier_fit_cubic_full, because we pass a subsequence of the data +array, and don't write to that array.) QED. + +We should also show that the recursion is finite for the inductive +proof to hold. The finiteness comes from inner calls having len > 0 +and len less than that of outer calls (from splitPoint calculation and +0 < splitPoint < last for recursive case and last < len and transitive +property of < for gint). If len < 2 then we don't recurse +(conditional return). + +We should go over this proof to make it clear that there are no +"forward references" other than for recursive case. We could also be +more formal in use of inductive proof (e.g. clearly stating what the +base and inductive premises are; namely the non-recursing and +recursing cases of sp_bezier_fit_cubic_full). + +Better proof sketch that nseg1 + nsegs2 < len: ret < len for each +recursive case other than where len > 0 precondition fails. nsegs1 is +calculated for inner len=splitPoint + 1, nsegs2 for inner len=len - +splitPoint. Assuming exact arithmetic we'll transform that to ret <= +len - 1. Implies that in exact arithmetic, nsegs1 + nsegs2 <= +(splitPoint + 1 - 1) + (len - splitPoint - 1). Simplifying RHS (using +exact arithmetic): nsegs1 + nsegs2 <= len - 1, i.e. nsegs1 + nsegs2 < +len. Presumably we can show that machine arithmetic gets the same +results as exact arithmetic from similar arguments used so far for +showing that overflow doesn't occur. For the recursive case the +return values are either nsegs1 + nsegs2 or -1. + +We should also show that inner preconditions hold, especially the len +> 0 precondition. (For nsegs1 call, we use 0 < splitPoint and that +splitPoint + 1 doesn't overflow. For nsegs2 call, we pass len - +splitPoint; combine with splitPoint < last, last = len - 1, and no +overflow.) We've already sketched a proof for no-dups precondition. +The others are fairly simple. + +For error >= 0: error is const, and we pass it to all recursions. + +For inner max_beziers >= 1: recursions are conditional on outer +1 < max_beziers before setting rec_max_beziers1 to max_beziers - 1, +and passing rec_max_beziers1 as inner max_beziers value, +so we have outer max_beziers >= 2 so inner max_beziers >= 1. +max_beziers and rec_max_beziers1 are both const. + + +src/display/bezier-utils.cpp:sp_darray_right_tangent(Point const[], unsigned) + +Proof of unit_vector precondition that a != Point(0, 0): our unequal precondition. + +Loose (incorrect) proof of unit_vector precondition that neither +coordinate is NaN: our in_svg_plane precondition, and fact that +in_svg_plane returns false if either argument is infinite. HOWEVER, +the unchecked in_svg_plane precondition isn't currently guaranteed, so +we're just relying on the input points never being infinity (which +might occur with strange zoom settings). + + +src/display/bezier-utils.cpp:sp_darray_right_tangent(Point const[], unsigned, double) + +Loose proof of unit_vector precondition that a != Point(0, 0) for first call to unit_vector: + +We've asserted that 0 <= tolerance_sq; combine with tolerance_sq < +distsq and transitivity of <=/< show that 0 < distsq. Definition of +dot should give us that t != 0.0, given that 0.0 * 0.0 == +0.0, and 0 +< +0.0 is false. + +Loose proof for the second unit_vector invocation: distsq != 0 from ?: +condition, which should give us that t != Point(0, 0) in the same way +as in the above proof. + +Proof of sp_darray_right_tangent(Point[], unsigned) preconditions: We +have the same preconditions, and pass the same arguments. d, *d and +len are const. + + + +src/extension/internal/ps.cpp:PrintPS::print_fill_style: + +Proof of the + g_return_if_fail( style->fill.type == SP_PAINT_TYPE_COLOR + || ( style->fill.type == SP_PAINT_TYPE_PAINTSERVER + && SP_IS_GRADIENT(SP_STYLE_FILL_SERVER(style)) ) ) +at beginning of function: + +rgrep print_fill_style reveals no callers in any other files. There are two calls in ps.cpp, both +inside an `if' test of that same condition (with no relevant lines between the test and the call). +Each call uses `style' as its second argument, and `style' in print_fill_style refers to its second +parameter. In both caller & callee, `style' is a const pointer to const, and there is very little +code between the two tests, so the relevant values are very unlikely to change between the two +tests. + + +Proof of + g_assert( style->fill.type == SP_PAINT_TYPE_PAINTSERVER + && SP_IS_GRADIENT(SP_STYLE_FILL_SERVER(style)) ) : + +The g_return_if_fail(style->fill.type == SP_PAINT_TYPE_COLOR + || ( style->fill.type == SP_PAINT_TYPE_PAINTSERVER + && SP_IS_GRADIENT(SP_STYLE_FILL_SERVER(style)) ) ) +call at the beginning of the function, and we're in the `else' branch of a test for +style->fill.type == SP_PAINT_TYPE_COLOR, and style is a const pointer to const, so it's likely that +style->fill and the gradient object have the same values throughout. + + + +src/extensions/internal/ps.cpp:PrintPS::fill: + +Proof of the two assertions + g_assert( style->fill.type == SP_PAINT_TYPE_PAINTSERVER + && SP_IS_GRADIENT(SP_STYLE_FILL_SERVER(style)) ) : + +Each is in the `else' branch of a test for `style->fill.type == SP_PAINT_TYPE_COLOR', +within a test for + ( style->fill.type == SP_PAINT_TYPE_COLOR + || ( style->fill.type == SP_PAINT_TYPE_PAINTSERVER + && SP_IS_GRADIENT(SP_STYLE_FILL_SERVER(style)) ) ). + +`style' is a const pointer to const, so the values are unlikely to have changed between the tests. + + + +src/seltrans.cpp:sp_sel_trans_update_handles + +Proof of requirements of sp_show_handles: + +sp_show_handles requirements: !arg1.empty. + +Before any call to sp_show_handles is a test `if (... || seltrans.empty) { ...; return; }' +(with no `break' etc. call preventing that `return'). +Each subsequent sp_show_handles call uses seltrans as arg1. +seltrans is a reference. There are no calls between that failing seltrans.empty test +and the sp_show_handles calls that pass seltrans. The sole call is sp_remove_handles, +probably doesn't have access to seltrans. + + + +src/seltrans.cpp:sp_show_handles + +Proof of precondition: + +sp_show_handles is static. Searching reveals calls only in sp_sel_trans_update_handles (proof above). + + + +src/sp-spiral.cpp:sp_spiral_fit_and_draw + +Proof of postcondition is_unit_vector(*hat2): + +hat2 is set by sp_spiral_get_tangent unconditionally, which Ensures is_unit_vector(*hat2). +We then negate *hat2, which doesn't affect its length. +We pass it only to sp_bezier_fit_cubic_full, which claims constness of *hat2. + +Proof of unconditionalness: Not inside if/for/while. No previous `return'. + + +src/sp-spiral.cpp:sp_spiral_set_shape + +Loose proof of requirements for sp_spiral_fit_and_draw: + + Proof of dstep > 0: + + SAMPLE_STEP equals .25. + spiral->revo is bounded to [0.05, 20.0] (and non-NaN) by various CLAMP calls. + (TODO: Add precondition, given that those CLAMP calls are outside of this function.) + SAMPLE_SIZE equals 8. + dstep is const and equals SAMPLE_STEP / spiral->revo / (SAMPLE_SIZE - 1), + == 1 / (4 * [.05, 20.0] * 7) + == 1 / [1.4, 560] + dstep in [.0018, .714]. + + Proof of is_unit_vector(hat1): + + Initially guaranteed by sp_spiral_get_tangent Ensures. + For subsequent calls, hat1 is set from negated hat2 as set by sp_spiral_fit_and_draw, + which Ensures is_unit_vector(hat2). + + + +src/style.cpp:sp_css_attr_from_style: + +Proof of sp_style_write_string pre `style != NULL': + +Passes style as style argument. style is const, and has already been checked against NULL. + + +src/style.cpp:sp_css_attr_from_object + +Proof of `flags in {IFSET, ALWAYS} precondition: + + $ grep sp_css_attr_from_object `sed 's,#.*,,' make.files ` + file.cpp: SPCSSAttr *style = sp_css_attr_from_object (SP_DOCUMENT_ROOT (doc)); + selection-chemistry.cpp: SPCSSAttr *css = sp_css_attr_from_object (SP_OBJECT(item), SP_STYLE_FLAG_ALWAYS); + selection-chemistry.cpp: SPCSSAttr *temp = sp_css_attr_from_object (last_element, SP_STYLE_FLAG_IFSET); + style.cpp:sp_css_attr_from_object (SPObject *object, guint flags) + style.h:SPCSSAttr *sp_css_attr_from_object(SPObject *object, guint flags = SP_STYLE_FLAG_IFSET); + + +src/style.cpp:sp_css_attr_from_style + +Proof of precondition `style != NULL': + +Callers are selection-chemistry.cpp and style.cpp: + + $ grep sp_css_attr_from_style `sed 's,#.*,,' make.files ` +selection-chemistry.cpp: SPCSSAttr *css = sp_css_attr_from_style (query, SP_STYLE_FLAG_ALWAYS); + style.cpp:sp_css_attr_from_style (SPStyle const *const style, guint flags) + style.cpp: return sp_css_attr_from_style (style, flags); + style.h:SPCSSAttr *sp_css_attr_from_style (SPStyle const *const style, guint flags); + +selection-chemistry.cpp caller: query is initialized from sp_style_new() +(which guarantees non-NULL), and is const. + +style.cpp caller: preceded by explicit test for NULL: + + $ grep -B2 sp_css_attr_from_style style.cpp|tail -3 + if (style == NULL) + return NULL; + return sp_css_attr_from_style (style, flags); + + + + +# Local Variables: +# mode:indented-text +# fill-column:99 +# End: +# vim: filetype=text:tabstop=8:fileencoding=utf-8:textwidth=99 : |