mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
f6cbddcbf2
Python port rewritten to match spec: - Added Q0_16, PUSH_Q0, PUSH_BOOL as separate opcodes - Added V6 comparison (lt_q16_v6) - Added floor division (Lean Int.ediv) - Added stack depth limit (AVM_MAX_STACK = 1024) - Added type checking in exec_prim - All 10 tests passing Go AVM port: added test_avm_test.go with 8 test cases Milestone: Python → ✅, Go → 🔄
89 lines
3.1 KiB
Coq
89 lines
3.1 KiB
Coq
(* Coq Formalization of Q16_16 Fixed-Point Arithmetic *)
|
|
Require Import ZArith Lia.
|
|
|
|
Lemma le_neg2147483648_2147483647 : (-2147483648 <= 2147483647)%Z.
|
|
Proof. lia. Qed.
|
|
Lemma le_0_2147483647 : (0 <= 2147483647)%Z.
|
|
Proof. lia. Qed.
|
|
Lemma le_neg2147483648_0 : (-2147483648 <= 0)%Z.
|
|
Proof. lia. Qed.
|
|
|
|
Lemma le_2147483647_2147483647 : (2147483647 <= 2147483647)%Z.
|
|
Proof. lia. Qed.
|
|
|
|
Module Q16_16.
|
|
Open Scope Z_scope.
|
|
|
|
Definition q16_min_raw : Z := -2147483648.
|
|
Definition q16_max_raw : Z := 2147483647.
|
|
Definition q16_scale : Z := 65536.
|
|
|
|
Definition in_range (x : Z) : Prop :=
|
|
q16_min_raw <= x /\ x <= q16_max_raw.
|
|
|
|
Definition clamp_raw (i : Z) : Z :=
|
|
if Z_lt_dec q16_max_raw i then q16_max_raw
|
|
else if Z_lt_dec i q16_min_raw then q16_min_raw
|
|
else i.
|
|
|
|
Theorem clamp_bounded (x : Z) : in_range (clamp_raw x).
|
|
Proof.
|
|
unfold clamp_raw, in_range.
|
|
case (Z_lt_dec q16_max_raw x); intros H1.
|
|
- unfold q16_min_raw, q16_max_raw; split; [apply le_neg2147483648_2147483647 | apply Z.le_refl].
|
|
- case (Z_lt_dec x q16_min_raw); intros H2.
|
|
+ unfold q16_min_raw, q16_max_raw; split; [apply Z.le_refl | apply le_neg2147483648_2147483647].
|
|
+ split; apply Z.nlt_ge; assumption.
|
|
Qed.
|
|
|
|
Theorem clamp_idempotent (x : Z) (h : in_range x) : clamp_raw x = x.
|
|
Proof.
|
|
destruct h as [Hlo Hhi].
|
|
unfold clamp_raw.
|
|
case (Z_lt_dec q16_max_raw x); intros Hgt; [exfalso; exact (Zlt_not_le _ _ Hgt Hhi) |].
|
|
case (Z_lt_dec x q16_min_raw); intros Hlt; [exfalso; exact (Zlt_not_le _ _ Hlt Hlo) |].
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Definition zero : Z := 0.
|
|
Definition one : Z := 65536.
|
|
Definition epsilon : Z := 1.
|
|
Definition half : Z := 32768.
|
|
Definition pct1 : Z := 655.
|
|
Definition pct70 : Z := 45875.
|
|
Definition pct30 : Z := 19661.
|
|
Definition one50 : Z := 98304.
|
|
|
|
Definition add (a b : Z) : Z := clamp_raw (a + b).
|
|
Definition sub (a b : Z) : Z := clamp_raw (a - b).
|
|
Definition neg (a : Z) : Z := clamp_raw (-a).
|
|
Definition mul (a b : Z) : Z := clamp_raw (Z.div (a * b) q16_scale).
|
|
Definition div (a b : Z) : Z :=
|
|
if Z.eq_dec b 0 then zero else clamp_raw (Z.div (a * q16_scale) b).
|
|
|
|
Theorem add_comm (a b : Z) : add a b = add b a.
|
|
Proof. unfold add; rewrite Z.add_comm; reflexivity. Qed.
|
|
|
|
Theorem add_in_range (a b : Z) (ha : in_range a) (hb : in_range b)
|
|
(hsum : in_range (a + b)) : add a b = a + b.
|
|
Proof.
|
|
unfold add; rewrite clamp_idempotent; trivial.
|
|
Qed.
|
|
|
|
Theorem sub_self (a : Z) (ha : in_range a) : sub a a = zero.
|
|
Proof.
|
|
unfold sub, zero; rewrite Z.sub_diag.
|
|
apply clamp_idempotent; unfold in_range; unfold q16_min_raw, q16_max_raw.
|
|
split; [apply le_neg2147483648_0 | apply le_0_2147483647].
|
|
Qed.
|
|
|
|
Theorem mul_comm (a b : Z) : mul a b = mul b a.
|
|
Proof. unfold mul; rewrite Z.mul_comm; reflexivity. Qed.
|
|
|
|
Theorem in_range_zero : in_range 0.
|
|
Proof. unfold in_range, q16_min_raw, q16_max_raw. split; [apply le_neg2147483648_0 | apply le_0_2147483647]. Qed.
|
|
|
|
Theorem in_range_one : in_range 1.
|
|
Proof. unfold in_range, q16_min_raw, q16_max_raw. split; [apply le_neg2147483648_0 | apply le_0_2147483647]. Qed.
|
|
|
|
End Q16_16.
|