(* AVM ISA v1 — Coq Test Harness (Rocq 9.0) *)
From Corelib Require Import BinNums PosDef NatDef IntDef Init.Datatypes.
Require Import SilverSight.coq.ZCompat.
Require Import SilverSight.coq.AVMIsa.avm.
Local Open Scope Z_scope.

Definition QS := 65536.

Example test_basic_add : True.
Proof.
  exact I.
Qed.

Example test_saturation : True.
Proof.
  exact I.
Qed.