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.



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.



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).



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'.


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] by various CLAMP calls.
  (todo: Get CLAMP to ensure it never returns NaN.)  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).
