cipher1024

-Q msl VST.msl -Q sepcomp VST.sepcomp -Q veric VST.veric -Q floyd VST.floyd -Q progs VST.progs -Q concurrency VST.concurrency -Q wand_demo wand_demo -Q sha sha -Q hmacfcf hmacfcf -Q tweetnacl20140427 tweetnacl20140427 -Q hmacdrbg hmacdrbg -Q aes aes -Q mailbox mailbox -Q atomics atomics -Q compcert/lib compcert.lib -Q compcert/common compcert.common -Q compcert/x86_32 compcert.x86_32 -Q compcert/cfrontend compcert.cfrontend -Q compcert/flocq compcert.flocq -Q compcert/exportclight compcert.exportclight

cipher1024

Set Implicit Arguments.

Inductive vtype : Set :=
| int32 : vtype
| array : vtype -> vtype.

Parameter vname : Set.
Parameter sig : vname -> vtype.

cipher1024

@[class]
def fact (p : Prop) := p

variables {n : ℕ}

namespace fin

def of_int [h : fact (0 < n)] (i : ℤ) : fin n :=
⟨(i % n).nat_abs, int.nat_abs_mod_lt⟩

cipher1024

import tactic

class linear_ordered_comm_group (α : Type)
    extends comm_group α, linear_order α :=
(mul_le_mul_left : ∀ {a b : α}, a ≤ b → ∀ c : α, c * a ≤ c * b)

class linear_ordered_comm_monoid (α : Type)
    extends comm_monoid α, linear_order α :=
(mul_le_mul_left : ∀ {a b : α}, a ≤ b → ∀ c : α, c * a ≤ c * b)

cipher1024

import tactic.norm_num

meta def expr.find_all (f : expr → list (expr × expr)) (e : expr) : list (expr × expr) :=
e.fold [] (λ x _ xs, f x ++ xs)

namespace tactic

meta def is_sub : expr → list (expr × expr)
 | `(%%x - %%y) := [(x,y)]
 | _ := []

cipher1024

-- These are pretty general lemmas about lists.
-- We could find them in the standard library
namespace list

universes u v w

variables {α : Type u} {β : Type v} {γ : Type w}
variables (f : α → β → γ)
variables {x : α} {y : β} {xs : list α} {ys : list β}

cipher1024

section unique

variables {α : Type*} [decidable_eq α]

def unique : list α → list α
 | [] := []
 | (x :: xs) :=
   if x ∈ xs
     then unique xs
     else x :: unique xs

cipher1024

import data.list.basic

section left_pad

variables {α : Type*}

open nat

lemma list.cons_repeat (c : α) :

cipher1024

namespace tactic
namespace interactive

open interactive interactive.types lean.parser
local postfix `?`:9001 := optional
local postfix *:9001 := many

meta def convert (sym : parse (with_desc "←" (tk "<-")?)) (r : parse texpr) (n : parse (tk "using" *> small_nat)?) : tactic unit :=
do v ← mk_mvar,
   if sym.is_some

cipher1024

import data.pfun

open nat

class bounded (p : ℕ → Prop) :=
  (ubound : ℕ)
  (only_below : ∀ i > ubound, ¬ p i)

export bounded (only_below)