From 587a4f053c3e90a80112064842afa4713dc09e48 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres@andres.systems>
Date: Wed, 26 Jun 2024 00:04:41 -0400
Subject: [PATCH] constant-time example with division

---
 bedrock2/src/bedrock2Examples/ct.v | 44 ++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)
 create mode 100644 bedrock2/src/bedrock2Examples/ct.v

diff --git a/bedrock2/src/bedrock2Examples/ct.v b/bedrock2/src/bedrock2Examples/ct.v
new file mode 100644
index 000000000..ea5889b8c
--- /dev/null
+++ b/bedrock2/src/bedrock2Examples/ct.v
@@ -0,0 +1,44 @@
+Require Import Coq.ZArith.ZArith coqutil.Z.div_mod_to_equations.
+Require Import bedrock2.NotationsCustomEntry.
+Import Syntax BinInt String List.ListNotations ZArith.
+Require Import coqutil.Z.Lia.
+Local Open Scope string_scope. Local Open Scope Z_scope. Local Open Scope list_scope.
+
+Definition div3329_vartime := func! (x) ~> ret {
+  ret = $(expr.op bopname.divu "x" 3329)
+}.
+
+Definition div3329 := func! (x) ~> ret {
+  ret = (x * $989558401) >> $32;
+  ret = (ret + (x - ret >> $1)) >> $11
+}.
+
+From coqutil Require Import Word.Properties Word.Interface Tactics.letexists.
+Import Interface.word Coq.Lists.List List.ListNotations.
+From bedrock2 Require Import Semantics BasicC32Semantics WeakestPrecondition ProgramLogic.
+Import ProgramLogic.Coercions.
+
+Instance ctspec_of_div3329 : spec_of "div3329" :=
+  fun functions => forall k, exists k_, forall t m x,
+      WeakestPrecondition.call functions "div3329" k t m [x]
+        (fun k' t' m' rets => exists ret, rets = [ret]
+        /\ t' = t /\ m' = m /\ k' = k_
+        (*x < 2^32 -> ret = x / 3329 :> Z*) ).
+
+Lemma div3329_ct : program_logic_goal_for_function! div3329.
+Proof.
+  repeat (straightline || eexists).
+  { (* no leakag -- 3 minutes *) cbv [k' k'0]. cbn. exact eq_refl. }
+Qed.
+
+Instance vtspec_of_div3329 : spec_of "div3329_vartime" :=
+  fun functions => forall k, forall t m x,
+      WeakestPrecondition.call functions "div3329_vartime" k t m [x]
+        (fun k' t' m' rets => exists ret, rets = [ret]
+        /\ t' = t /\ m' = m /\ k' = [leak_word (word.of_Z 3329); leak_word x]++k
+        (*x < 2^32 -> ret = x / 3329 :> Z*) ).
+
+Lemma div3329_vt : program_logic_goal_for_function! div3329_vartime.
+Proof.
+  repeat (straightline || eexists).
+Qed.